From d378f32594c371e7dca6dd7d9cc5f1747a07166a Mon Sep 17 00:00:00 2001
From: CC <78262508+Wenbobobo@users.noreply.github.com>
Date: Sat, 25 Jul 2026 23:59:46 +0800
Subject: [PATCH] Build image-owned Library substrate preflight

---
 Library/scripts/library_substrate_image.py    | 1357 +++++++++++++++++
 Prover/worker/Dockerfile.library-substrate    |   61 +
 .../AutoleanLibrarySubstrateInventory.lean    |  189 +++
 .../autolean-library-substrate-build          |  264 ++++
 .../autolean-library-substrate-build-receipt  |  123 ++
 ...tolean-library-substrate-independent-query |  290 ++++
 docs/README.md                                |    3 +
 docs/library-substrate-decision.md            |   10 +-
 docs/library-substrate-image-preflight.md     |  164 ++
 docs/phase-1-progress.md                      |    4 +-
 scripts/tests/test_library_substrate_image.py |  374 +++++
 11 files changed, 2835 insertions(+), 4 deletions(-)
 create mode 100644 Library/scripts/library_substrate_image.py
 create mode 100644 Prover/worker/Dockerfile.library-substrate
 create mode 100644 Prover/worker/library-substrate/AutoleanLibrarySubstrateInventory.lean
 create mode 100644 Prover/worker/library-substrate/autolean-library-substrate-build
 create mode 100644 Prover/worker/library-substrate/autolean-library-substrate-build-receipt
 create mode 100644 Prover/worker/library-substrate/autolean-library-substrate-independent-query
 create mode 100644 docs/library-substrate-image-preflight.md
 create mode 100644 scripts/tests/test_library_substrate_image.py

diff --git a/Library/scripts/library_substrate_image.py b/Library/scripts/library_substrate_image.py
new file mode 100644
index 0000000..c8268d5
--- /dev/null
+++ b/Library/scripts/library_substrate_image.py
@@ -0,0 +1,1357 @@
+"""Build and exercise the image-owned UniversalLK independent-reproof substrate.
+
+This is an operator-local preflight.  It deliberately stops before contracts,
+the signing gateway, provider execution, external dependency capsules, or
+admission of any Builder asset.
+"""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import json
+import os
+import re
+import stat
+import subprocess
+import sys
+import tempfile
+from collections.abc import Mapping, Sequence
+from pathlib import Path, PurePosixPath
+from typing import Final, NoReturn, cast
+
+if __package__ in {None, ""}:
+    repository_root = str(Path(__file__).resolve().parents[2])
+    if repository_root not in sys.path:
+        sys.path.insert(0, repository_root)
+
+from Library.scripts.verify_substrate_fixture import (
+    EXPECTED_MATHLIB_REVISION,
+    EXPECTED_PROFILE_IDS,
+    FIXTURE_ROOT,
+    MODULE_BY_NAME,
+    SOUND_DECLARATION,
+    SOURCE_V2_IMAGE,
+    TARGET_DECLARATION,
+    ValidatedProfileBoundary,
+    check,
+)
+
+WSL_DISTRIBUTION: Final = "Ubuntu-24.04"
+IMAGE_TAG: Final = "autolean/library-substrate:4.28.0-universal-lk-independent-preflight-v1"
+IMAGE_REPOSITORY: Final = "autolean/library-substrate"
+IMAGE_DIGEST_RE: Final = re.compile(r"^autolean/library-substrate@sha256:[0-9a-f]{64}$")
+SHA256_RE: Final = re.compile(r"^[0-9a-f]{64}$")
+TARGET_TYPE_SHA256: Final = "66d1fe3cbd2a62831bf57b9761248bf3fa5d84b95879be25c7e591c48ebeef8a"
+EXPECTED_TARGET_AXIOMS: Final = ("Classical.choice", "Quot.sound", "propext")
+ALLOWED_RUNTIME_AXIOMS: Final = frozenset(EXPECTED_TARGET_AXIOMS)
+PROFILE_PATH: Final = FIXTURE_ROOT / "profiles" / "independent_reproof.profile.v1.json"
+CANDIDATE_PATH: Final = FIXTURE_ROOT / "candidates" / "independent_reproof" / "Candidate.lean"
+WORKER_ROOT: Final = Path(__file__).resolve().parents[2] / "Prover" / "worker"
+DOCKERFILE: Final = WORKER_ROOT / "Dockerfile.library-substrate"
+HELPER_ROOT: Final = WORKER_ROOT / "library-substrate"
+ASSETS: Final = {
+    "AutoleanLibrarySubstrateInventory.lean": "INVENTORY_HELPER_SHA256",
+    "autolean-library-substrate-build": "BUILD_TOOL_SHA256",
+    "autolean-library-substrate-build-receipt": "RECEIPT_TOOL_SHA256",
+    "autolean-library-substrate-independent-query": "QUERY_WRAPPER_SHA256",
+}
+RUNTIME_MANIFEST_SCHEMA: Final = "autolean.library-substrate-runtime-manifest.v1"
+DECLARATION_INVENTORY_SCHEMA: Final = "autolean.library-substrate-declaration-inventory.v1"
+IMAGE_RECEIPT_SCHEMA: Final = "autolean.library-substrate-image-receipt.v1"
+QUERY_SCHEMA: Final = "autolean.library-substrate-independent-query.v1"
+CANARY_SCHEMA: Final = "autolean.library-substrate-independent-canary.v1"
+RUNTIME_SOURCE_CHECKSUM_FILENAME: Final = "runtime-sources.sha256"
+RUNTIME_FILE_CHECKSUM_FILENAME: Final = "runtime-files.sha256"
+
+
+class SubstrateImageError(RuntimeError):
+    """A fail-closed build input, image receipt, or canary error."""
+
+
+def fail(message: str) -> NoReturn:
+    raise SubstrateImageError(message)
+
+
+def _sha256_bytes(value: bytes) -> str:
+    return hashlib.sha256(value).hexdigest()
+
+
+def _sha256(path: Path) -> str:
+    return _sha256_bytes(path.read_bytes())
+
+
+def _canonical_json_bytes(value: object) -> bytes:
+    try:
+        rendered = json.dumps(
+            value,
+            allow_nan=False,
+            ensure_ascii=True,
+            separators=(",", ":"),
+            sort_keys=True,
+        )
+    except (TypeError, ValueError) as error:
+        raise SubstrateImageError("value is not canonical JSON") from error
+    return (rendered + "\n").encode("utf-8")
+
+
+def _canonical_json_compact_bytes(value: object) -> bytes:
+    return _canonical_json_bytes(value).removesuffix(b"\n")
+
+
+def _reject_duplicate_keys(pairs: list[tuple[str, object]]) -> dict[str, object]:
+    value: dict[str, object] = {}
+    for key, item in pairs:
+        if key in value:
+            fail(f"JSON contains duplicate key: {key}")
+        value[key] = item
+    return value
+
+
+def _json_record(raw: str, *, label: str) -> dict[str, object]:
+    lines = raw.splitlines()
+    if len(lines) != 1:
+        fail(f"{label} did not emit exactly one JSON record")
+    try:
+        value = json.loads(lines[0], object_pairs_hook=_reject_duplicate_keys)
+    except json.JSONDecodeError as error:
+        raise SubstrateImageError(f"{label} did not emit valid JSON") from error
+    if not isinstance(value, dict) or any(not isinstance(key, str) for key in value):
+        fail(f"{label} must be a JSON object")
+    return cast(dict[str, object], value)
+
+
+def _run(
+    command: list[str],
+    *,
+    timeout: int,
+    cwd: Path | None = None,
+    environment: Mapping[str, str] | None = None,
+) -> subprocess.CompletedProcess[str]:
+    try:
+        completed = subprocess.run(
+            command,
+            cwd=cwd,
+            env=None if environment is None else dict(environment),
+            check=False,
+            capture_output=True,
+            timeout=timeout,
+        )
+    except (OSError, subprocess.SubprocessError) as error:
+        raise SubstrateImageError("subprocess execution failed") from error
+    stdout = completed.stdout.decode("utf-8", errors="replace")
+    stderr = completed.stderr.decode("utf-8", errors="replace")
+    result = subprocess.CompletedProcess(command, completed.returncode, stdout, stderr)
+    if result.returncode != 0:
+        detail = (result.stdout + "\n" + result.stderr)[-12000:]
+        raise SubstrateImageError(f"subprocess failed ({command[0]}): {detail}")
+    return result
+
+
+def _safe_relative(value: str) -> Path:
+    pure = PurePosixPath(value)
+    if pure.is_absolute() or not pure.parts or ".." in pure.parts:
+        fail("path is not a safe POSIX relative path")
+    return Path(*pure.parts)
+
+
+def _regular_bytes(path: Path, *, label: str) -> bytes:
+    try:
+        before = path.lstat()
+    except OSError as error:
+        raise SubstrateImageError(f"{label} is unavailable") from error
+    if stat.S_ISLNK(before.st_mode) or not stat.S_ISREG(before.st_mode):
+        fail(f"{label} must be an unlinked regular file")
+    value = path.read_bytes()
+    after = path.lstat()
+    if (
+        before.st_dev,
+        before.st_ino,
+        before.st_size,
+        before.st_mtime_ns,
+    ) != (
+        after.st_dev,
+        after.st_ino,
+        after.st_size,
+        after.st_mtime_ns,
+    ):
+        fail(f"{label} changed while being read")
+    return value
+
+
+def _inspect(image: str) -> dict[str, object]:
+    raw = _run(["docker", "image", "inspect", image], timeout=60).stdout
+    try:
+        loaded = json.loads(raw)
+    except json.JSONDecodeError as error:
+        raise SubstrateImageError("Docker image inspection was not JSON") from error
+    if not isinstance(loaded, list) or len(loaded) != 1 or not isinstance(loaded[0], dict):
+        fail("Docker returned an unexpected image inspection record")
+    return cast(dict[str, object], loaded[0])
+
+
+def _child_image_reference(inspected: Mapping[str, object]) -> str:
+    repo_digests = inspected.get("RepoDigests")
+    if not isinstance(repo_digests, list):
+        fail("built child image has no repository digest list")
+    matching = sorted(
+        item
+        for item in repo_digests
+        if isinstance(item, str)
+        and item.startswith(f"{IMAGE_REPOSITORY}@sha256:")
+        and IMAGE_DIGEST_RE.fullmatch(item)
+    )
+    if not matching:
+        fail("built child image has no Docker-recorded autolean/library-substrate RepoDigest")
+    return matching[0]
+
+
+def _docker_run_base(*, read_only: bool = True) -> list[str]:
+    command = [
+        "docker",
+        "run",
+        "--rm",
+        "--pull=never",
+        "--network",
+        "none",
+        "--cap-drop",
+        "ALL",
+        "--security-opt",
+        "no-new-privileges",
+        "--pids-limit",
+        "128",
+        "--memory",
+        "2g",
+        "--tmpfs",
+        "/tmp:rw,exec,nosuid,nodev,size=256m,mode=1777",
+    ]
+    if read_only:
+        command.append("--read-only")
+    return command
+
+
+def _parent_receipt() -> tuple[dict[str, object], str, str, dict[str, object]]:
+    inspected = _inspect(SOURCE_V2_IMAGE)
+    repo_digests = inspected.get("RepoDigests")
+    if not isinstance(repo_digests, list) or SOURCE_V2_IMAGE not in repo_digests:
+        fail("source-v2 parent inspect record does not contain its required RepoDigest")
+    output = _run(
+        [
+            *_docker_run_base(),
+            SOURCE_V2_IMAGE,
+            "/opt/autolean/bin/autolean-mathlib-build-receipt",
+        ],
+        timeout=240,
+    ).stdout
+    receipt = _json_record(output, label="source-v2 parent receipt")
+    if (
+        receipt.get("schema_version") != "autolean.mathlib-source-build-receipt.v2"
+        or receipt.get("mathlib_revision") != EXPECTED_MATHLIB_REVISION
+    ):
+        fail("source-v2 parent receipt does not match the locked profile")
+    canonical = _canonical_json_bytes(receipt)
+    raw_hash_output = _run(
+        [
+            *_docker_run_base(),
+            "--entrypoint",
+            "/usr/bin/sha256sum",
+            SOURCE_V2_IMAGE,
+            "/opt/autolean/attestations/mathlib-source-build-receipt.v2.json",
+        ],
+        timeout=120,
+    ).stdout
+    raw_hash = raw_hash_output.strip().split(" ", maxsplit=1)[0]
+    if not SHA256_RE.fullmatch(raw_hash):
+        fail("source-v2 parent receipt file hash is unavailable")
+    return receipt, _sha256_bytes(canonical), raw_hash, inspected
+
+
+def _profile() -> tuple[ValidatedProfileBoundary, dict[str, object]]:
+    profiles = check()
+    profile = profiles.get("independent_reproof")
+    if profile is None or profile.task_mode != "independent_reproof":
+        fail("independent_reproof profile was not validated")
+    raw = _regular_bytes(PROFILE_PATH, label="independent profile")
+    try:
+        value = json.loads(raw, object_pairs_hook=_reject_duplicate_keys)
+    except json.JSONDecodeError as error:
+        raise SubstrateImageError("independent profile is not JSON") from error
+    if not isinstance(value, dict):
+        fail("independent profile must be an object")
+    return profile, cast(dict[str, object], value)
+
+
+def _runtime_source_records(
+    profile: ValidatedProfileBoundary,
+    *,
+    source_root: Path = FIXTURE_ROOT / "source",
+) -> tuple[list[dict[str, object]], str]:
+    records: list[dict[str, object]] = []
+    for module in profile.runtime_modules:
+        source = MODULE_BY_NAME[module]
+        relative = _safe_relative(source.path.removeprefix("source/"))
+        path = source_root / relative
+        content = _regular_bytes(path, label=f"runtime source {module}")
+        records.append(
+            {
+                "module": module,
+                "path": relative.as_posix(),
+                "role": source.role,
+                "sha256": _sha256_bytes(content),
+                "size": len(content),
+            }
+        )
+    return records, _sha256_bytes(_canonical_json_bytes(records))
+
+
+def _checksum_manifest_bytes(
+    records: Sequence[Mapping[str, object]], *, path_prefix: str = ""
+) -> bytes:
+    lines: list[str] = []
+    for record in records:
+        path = record.get("path")
+        digest = record.get("sha256")
+        if (
+            not isinstance(path, str)
+            or not isinstance(digest, str)
+            or not SHA256_RE.fullmatch(digest)
+        ):
+            fail("checksum manifest record is invalid")
+        relative = _safe_relative(path).as_posix()
+        lines.append(f"{digest}  {path_prefix}{relative}\n")
+    return "".join(lines).encode("ascii")
+
+
+def _validate_runtime_source_binding(
+    build_input: Mapping[str, object],
+    profile: ValidatedProfileBoundary,
+    *,
+    source_root: Path,
+    source_checksums: bytes,
+) -> tuple[list[dict[str, object]], str]:
+    records, tree_sha256 = _runtime_source_records(profile, source_root=source_root)
+    if build_input.get("runtime_sources") != records:
+        fail("runtime source records differ from the actual staged source bytes")
+    if build_input.get("runtime_source_tree_sha256") != tree_sha256:
+        fail("runtime source tree hash differs from the actual staged source bytes")
+    expected_checksums = _checksum_manifest_bytes(records, path_prefix="source/")
+    if source_checksums != expected_checksums:
+        fail("runtime source checksum manifest differs from the actual staged source bytes")
+    checksum_sha256 = _sha256_bytes(source_checksums)
+    if build_input.get("runtime_source_checksum_manifest_sha256") != checksum_sha256:
+        fail("runtime source checksum manifest is not bound by the build input")
+    return records, tree_sha256
+
+
+def _asset_hashes() -> dict[str, str]:
+    values = {"DOCKERFILE_SHA256": _sha256(DOCKERFILE)}
+    for filename, argument in ASSETS.items():
+        values[argument] = _sha256(HELPER_ROOT / filename)
+    return values
+
+
+def _build_input() -> tuple[
+    dict[str, object],
+    bytes,
+    ValidatedProfileBoundary,
+    dict[str, str],
+    str,
+]:
+    profile, profile_record = _profile()
+    (
+        parent_receipt,
+        parent_receipt_sha256,
+        parent_receipt_file_sha256,
+        parent_inspected,
+    ) = _parent_receipt()
+    sources, source_tree_sha256 = _runtime_source_records(profile)
+    source_checksums = _checksum_manifest_bytes(sources, path_prefix="source/")
+    assets = _asset_hashes()
+    parent_image_id = parent_inspected.get("Id")
+    if not isinstance(parent_image_id, str) or not re.fullmatch(
+        r"sha256:[0-9a-f]{64}", parent_image_id
+    ):
+        fail("source-v2 parent has no immutable image ID")
+    value: dict[str, object] = {
+        "assets": dict(sorted(assets.items())),
+        "build_context_policy": {
+            "flags": ["--no-cache", "--pull=false", "--network=none"],
+            "only_profile_runtime_sources": True,
+        },
+        "mathlib_revision": EXPECTED_MATHLIB_REVISION,
+        "parent_image": SOURCE_V2_IMAGE,
+        "parent_image_id": parent_image_id,
+        "parent_receipt": parent_receipt,
+        "parent_receipt_canonical_sha256": parent_receipt_sha256,
+        "parent_receipt_file_sha256": parent_receipt_file_sha256,
+        "profile_id": EXPECTED_PROFILE_IDS["independent_reproof"],
+        "profile_sha256": _sha256_bytes(_canonical_json_bytes(profile_record)),
+        "runtime_modules": list(profile.runtime_modules),
+        "runtime_source_checksum_manifest_sha256": _sha256_bytes(source_checksums),
+        "runtime_source_tree_sha256": source_tree_sha256,
+        "runtime_sources": sources,
+        "schema_version": "autolean.library-substrate-build-input.v1",
+        "task_mode": "independent_reproof",
+        "target": {
+            "canonical_type_sha256": TARGET_TYPE_SHA256,
+            "declaration": TARGET_DECLARATION,
+            "forbidden_ordinary_dependency": SOUND_DECLARATION,
+        },
+    }
+    return value, _canonical_json_bytes(value), profile, assets, source_tree_sha256
+
+
+def _copy_regular(source: Path, destination: Path, *, executable: bool = False) -> None:
+    content = _regular_bytes(source, label=str(source))
+    destination.parent.mkdir(parents=True, exist_ok=True)
+    destination.write_bytes(content)
+    destination.chmod(0o555 if executable else 0o444)
+
+
+def stage_build_context(root: Path) -> tuple[dict[str, object], dict[str, str]]:
+    (
+        build_input,
+        build_input_bytes,
+        profile,
+        assets,
+        source_tree_sha256,
+    ) = _build_input()
+    root.mkdir(parents=True, exist_ok=False)
+    _copy_regular(DOCKERFILE, root / "Dockerfile.library-substrate")
+    for filename in ASSETS:
+        _copy_regular(
+            HELPER_ROOT / filename,
+            root / "helpers" / filename,
+            executable=not filename.endswith(".lean"),
+        )
+    sources = cast(list[dict[str, object]], build_input["runtime_sources"])
+    for record in sources:
+        relative = cast(str, record["path"])
+        source = FIXTURE_ROOT / "source" / _safe_relative(relative)
+        _copy_regular(source, root / "source" / _safe_relative(relative))
+    (root / "build-input.v1.json").write_bytes(build_input_bytes)
+    (root / "build-input.v1.json").chmod(0o444)
+    source_checksums = _checksum_manifest_bytes(sources, path_prefix="source/")
+    (root / RUNTIME_SOURCE_CHECKSUM_FILENAME).write_bytes(source_checksums)
+    (root / RUNTIME_SOURCE_CHECKSUM_FILENAME).chmod(0o444)
+    _, staged_source_tree_sha256 = _validate_runtime_source_binding(
+        build_input,
+        profile,
+        source_root=root / "source",
+        source_checksums=source_checksums,
+    )
+    if staged_source_tree_sha256 != source_tree_sha256:
+        fail("staged runtime source tree differs from the frozen build input")
+
+    inventory: dict[str, str] = {}
+    for candidate in sorted(root.rglob("*")):
+        relative = candidate.relative_to(root).as_posix()
+        if candidate.is_symlink():
+            fail("fresh build context contains a symbolic link")
+        if candidate.is_file():
+            inventory[relative] = _sha256(candidate)
+        elif not candidate.is_dir():
+            fail("fresh build context contains a non-regular entry")
+    expected = {
+        "Dockerfile.library-substrate",
+        "build-input.v1.json",
+        RUNTIME_SOURCE_CHECKSUM_FILENAME,
+        *(f"helpers/{name}" for name in ASSETS),
+        *(f"source/{cast(str, item['path'])}" for item in sources),
+    }
+    if set(inventory) != expected:
+        fail("fresh build context inventory is not exact")
+    forbidden_fragments = ("/Targets/", "/Controls.", "Candidate.lean", "UniversalLK.lean")
+    if any(fragment in f"/{path}" for path in inventory for fragment in forbidden_fragments):
+        fail("fresh build context contains a target, control, aggregate, or Candidate source")
+    arguments = {
+        **assets,
+        "BUILD_INPUT_SHA256": _sha256_bytes(build_input_bytes),
+        "PARENT_RECEIPT_CANONICAL_SHA256": cast(
+            str, build_input["parent_receipt_canonical_sha256"]
+        ),
+        "PARENT_RECEIPT_FILE_SHA256": cast(str, build_input["parent_receipt_file_sha256"]),
+        "RUNTIME_SOURCE_CHECKSUM_MANIFEST_SHA256": cast(
+            str, build_input["runtime_source_checksum_manifest_sha256"]
+        ),
+        "RUNTIME_SOURCE_TREE_SHA256": source_tree_sha256,
+    }
+    return {
+        "build_input": build_input,
+        "build_input_sha256": arguments["BUILD_INPUT_SHA256"],
+        "context_inventory": inventory,
+        "context_inventory_sha256": _sha256_bytes(_canonical_json_bytes(inventory)),
+        "profile": {
+            "candidate_path": profile.candidate_path,
+            "forbidden_modules": list(profile.forbidden_modules),
+            "runtime_modules": list(profile.runtime_modules),
+            "task_mode": profile.task_mode,
+        },
+    }, arguments
+
+
+def _build_command(context: Path, arguments: Mapping[str, str]) -> list[str]:
+    command = [
+        "docker",
+        "build",
+        "--no-cache",
+        "--pull=false",
+        "--network=none",
+        "--file",
+        "Dockerfile.library-substrate",
+        "--tag",
+        IMAGE_TAG,
+    ]
+    for name, value in sorted(arguments.items()):
+        command.extend(("--build-arg", f"{name}={value}"))
+    command.append(str(context))
+    return command
+
+
+def build() -> dict[str, object]:
+    temporary_parent = Path("/tmp")
+    with tempfile.TemporaryDirectory(
+        prefix="autolean-library-substrate-image-", dir=temporary_parent
+    ) as raw:
+        context = Path(raw) / "context"
+        prepared, arguments = stage_build_context(context)
+        _run(
+            _build_command(context, arguments),
+            timeout=1800,
+            cwd=context,
+        )
+    inspected = _inspect(IMAGE_TAG)
+    image = _child_image_reference(inspected)
+    image_id = inspected.get("Id")
+    if not isinstance(image_id, str) or not re.fullmatch(r"sha256:[0-9a-f]{64}", image_id):
+        fail("built child image has no immutable image ID")
+    verified = verify(image)
+    return {
+        "build_input_sha256": prepared["build_input_sha256"],
+        "context_inventory": prepared["context_inventory"],
+        "context_inventory_sha256": prepared["context_inventory_sha256"],
+        "image": image,
+        "image_id": image_id,
+        "schema_version": "autolean.library-substrate-image-build.v1",
+        "verification": verified,
+    }
+
+
+def _receipt_output(image: str) -> tuple[dict[str, object], str]:
+    if not IMAGE_DIGEST_RE.fullmatch(image):
+        fail("child receipt verification requires a Docker-recorded repository digest")
+    output = _run(
+        [
+            *_docker_run_base(),
+            image,
+            "/opt/autolean/library-substrate/bin/autolean-library-substrate-build-receipt",
+        ],
+        timeout=240,
+    ).stdout
+    return (
+        _json_record(output, label="library substrate image receipt"),
+        _sha256_bytes(output.encode("utf-8")),
+    )
+
+
+def _read_image_json(image: str, path: str, *, label: str) -> tuple[dict[str, object], str]:
+    output = _read_image_text(image, path)
+    record = _json_record(output, label=label)
+    return record, _sha256_bytes(output.encode("utf-8"))
+
+
+def _read_image_text(image: str, path: str) -> str:
+    return _run(
+        [
+            *_docker_run_base(),
+            "--entrypoint",
+            "/bin/cat",
+            image,
+            path,
+        ],
+        timeout=120,
+    ).stdout
+
+
+def _image_file_sha256_and_size(image: str, path: str, *, label: str) -> tuple[str, int]:
+    digest_output = _run(
+        [
+            *_docker_run_base(),
+            "--entrypoint",
+            "/usr/bin/sha256sum",
+            image,
+            path,
+        ],
+        timeout=120,
+    ).stdout
+    digest_fields = digest_output.strip().split(maxsplit=1)
+    if len(digest_fields) != 2 or not SHA256_RE.fullmatch(digest_fields[0]):
+        fail(f"{label} hash is unavailable from the fixed child digest")
+    size_output = _run(
+        [
+            *_docker_run_base(),
+            "--entrypoint",
+            "/usr/bin/wc",
+            image,
+            "-c",
+            path,
+        ],
+        timeout=120,
+    ).stdout
+    size_fields = size_output.strip().split(maxsplit=1)
+    if len(size_fields) != 2 or not size_fields[0].isdigit() or int(size_fields[0]) <= 0:
+        fail(f"{label} size is unavailable from the fixed child digest")
+    return digest_fields[0], int(size_fields[0])
+
+
+def _sorted_unique_strings(value: object, *, label: str) -> tuple[str, ...]:
+    if not isinstance(value, list) or any(not isinstance(item, str) for item in value):
+        fail(f"{label} must be a string array")
+    strings = cast(list[str], value)
+    if strings != sorted(set(strings)):
+        fail(f"{label} must be sorted and unique")
+    return tuple(strings)
+
+
+def _runtime_files(manifest: Mapping[str, object]) -> dict[str, dict[str, object]]:
+    raw = manifest.get("runtime_files")
+    if not isinstance(raw, list) or len(raw) != 3:
+        fail("runtime manifest must contain exactly three OLean files")
+    result: dict[str, dict[str, object]] = {}
+    for item in raw:
+        if not isinstance(item, dict) or set(item) != {"module", "path", "sha256", "size"}:
+            fail("runtime file record schema drifted")
+        record = cast(dict[str, object], item)
+        module = record["module"]
+        path = record["path"]
+        digest = record["sha256"]
+        size = record["size"]
+        if (
+            not isinstance(module, str)
+            or not isinstance(path, str)
+            or not path.endswith(".olean")
+            or not SHA256_RE.fullmatch(cast(str, digest))
+            or not isinstance(size, int)
+            or isinstance(size, bool)
+            or size <= 0
+        ):
+            fail("runtime file record is invalid")
+        if module in result:
+            fail("runtime manifest repeats a module")
+        result[module] = record
+    return result
+
+
+def _validate_runtime_file_closure(
+    image: str,
+    runtime_files: Mapping[str, Mapping[str, object]],
+    *,
+    manifest: Mapping[str, object],
+    receipt: Mapping[str, object],
+) -> dict[str, dict[str, object]]:
+    actual_records: list[dict[str, object]] = []
+    actual_files: dict[str, dict[str, object]] = {}
+    for module, record in runtime_files.items():
+        path = cast(str, record["path"])
+        digest, size = _image_file_sha256_and_size(
+            image,
+            f"/opt/autolean/library-substrate/{path}",
+            label=f"runtime OLean {module}",
+        )
+        if digest != record["sha256"] or size != record["size"]:
+            fail(f"runtime OLean bytes differ from manifest for {module}")
+        actual = {"module": module, "path": path, "sha256": digest, "size": size}
+        actual_records.append(actual)
+        actual_files[module] = actual
+    actual_checksums = _checksum_manifest_bytes(actual_records)
+    checksum_path = f"/opt/autolean/library-substrate/attestations/{RUNTIME_FILE_CHECKSUM_FILENAME}"
+    stored_checksums = _read_image_text(image, checksum_path).encode("utf-8")
+    if stored_checksums != actual_checksums:
+        fail("runtime file checksum manifest differs from fixed-digest OLean bytes")
+    checksum_sha256 = _sha256_bytes(actual_checksums)
+    if (
+        manifest.get("compiled_tree_sha256") != checksum_sha256
+        or receipt.get("compiled_tree_sha256") != checksum_sha256
+    ):
+        fail("runtime file checksum manifest is not bound by manifest and receipt")
+    return actual_files
+
+
+def _validate_declaration_records(
+    value: object,
+    *,
+    runtime_files: Mapping[str, Mapping[str, object]],
+    include_origin_hash: bool,
+) -> list[dict[str, object]]:
+    if not isinstance(value, list) or not value:
+        fail("declaration inventory must be a nonempty array")
+    records: list[dict[str, object]] = []
+    names: list[str] = []
+    expected_fields = {
+        "canonical_type",
+        "declaration_kind",
+        "name",
+        "observed_axioms",
+        "origin_module",
+    }
+    if include_origin_hash:
+        expected_fields |= {"canonical_type_sha256", "origin_olean_sha256"}
+    for item in value:
+        if not isinstance(item, dict) or set(item) != expected_fields:
+            fail("declaration inventory record schema drifted")
+        record = cast(dict[str, object], item)
+        name = record["name"]
+        canonical = record["canonical_type"]
+        kind = record["declaration_kind"]
+        origin = record["origin_module"]
+        if (
+            not isinstance(name, str)
+            or not name.startswith("AutoLeanLibrary.")
+            or not isinstance(canonical, str)
+            or not canonical
+            or not isinstance(kind, str)
+            or kind
+            not in {
+                "axiom",
+                "constructor",
+                "definition",
+                "inductive",
+                "opaque",
+                "quotient",
+                "recursor",
+                "theorem",
+            }
+            or not isinstance(origin, str)
+            or origin not in runtime_files
+        ):
+            fail("declaration inventory record is invalid")
+        axioms = _sorted_unique_strings(
+            record["observed_axioms"], label=f"observed axioms for {name}"
+        )
+        if not set(axioms).issubset(ALLOWED_RUNTIME_AXIOMS):
+            fail(f"runtime declaration observes a forbidden axiom: {name}")
+        normalized = dict(record)
+        normalized["canonical_type_sha256"] = _sha256_bytes(canonical.encode("utf-8"))
+        normalized["origin_olean_sha256"] = runtime_files[origin]["sha256"]
+        if include_origin_hash and normalized != record:
+            fail(f"declaration hash or origin OLean binding is invalid: {name}")
+        records.append(normalized)
+        names.append(name)
+    if names != sorted(set(names)):
+        fail("declaration inventory names must be sorted and unique")
+    return records
+
+
+def _validate_ir_auxiliary_records(
+    value: object,
+    *,
+    runtime_files: Mapping[str, Mapping[str, object]],
+    include_origin_hash: bool,
+    kernel_names: frozenset[str],
+) -> list[dict[str, object]]:
+    if not isinstance(value, list) or not value:
+        fail("IR auxiliary inventory must be a nonempty array")
+    expected_fields = {"ir_decl_kind", "name", "origin_module"}
+    if include_origin_hash:
+        expected_fields |= {"origin_olean_sha256"}
+    reserved_identities = {
+        TARGET_DECLARATION,
+        SOUND_DECLARATION,
+        "Candidate",
+        "Init",
+        "Lean",
+        "Mathlib",
+        *runtime_files,
+        "AutoLeanLibrary.Fixtures.ModelTheory.Packet",
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK",
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Controls",
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Targets.ClosedSound",
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Targets.DerivSound",
+    }
+    records: list[dict[str, object]] = []
+    names: list[str] = []
+    for item in value:
+        if not isinstance(item, dict) or set(item) != expected_fields:
+            fail("IR auxiliary record schema drifted")
+        record = cast(dict[str, object], item)
+        declaration_kind = record["ir_decl_kind"]
+        name = record["name"]
+        origin = record["origin_module"]
+        if (
+            declaration_kind not in {"fdecl", "extern"}
+            or not isinstance(name, str)
+            or not name
+            or any(ord(character) < 33 or ord(character) > 126 for character in name)
+            or not isinstance(origin, str)
+            or origin not in runtime_files
+            or name in kernel_names
+            or name in reserved_identities
+        ):
+            fail("IR auxiliary record is invalid or collides with a reserved identity")
+        normalized = dict(record)
+        normalized["origin_olean_sha256"] = runtime_files[origin]["sha256"]
+        if include_origin_hash and normalized != record:
+            fail(f"IR auxiliary OLean origin binding is invalid: {name}")
+        records.append(normalized)
+        names.append(name)
+    if names != sorted(set(names)):
+        fail("IR auxiliary names must be sorted and unique")
+    return records
+
+
+def _validate_manifest(
+    manifest: dict[str, object],
+    *,
+    receipt: Mapping[str, object],
+) -> tuple[
+    dict[str, dict[str, object]],
+    list[dict[str, object]],
+    list[dict[str, object]],
+]:
+    required = {
+        "build_input_sha256",
+        "compiled_tree_sha256",
+        "declaration_inventory",
+        "declaration_inventory_sha256",
+        "ir_auxiliary_names_sha256",
+        "mathlib_revision",
+        "parent_image",
+        "parent_receipt_canonical_sha256",
+        "parent_receipt_file_sha256",
+        "profile_id",
+        "profile_sha256",
+        "runtime_files",
+        "runtime_modules",
+        "runtime_source_checksum_manifest_sha256",
+        "runtime_source_tree_sha256",
+        "schema_version",
+        "task_mode",
+    }
+    if set(manifest) != required:
+        fail("runtime manifest schema drifted")
+    if (
+        manifest["schema_version"] != RUNTIME_MANIFEST_SCHEMA
+        or manifest["task_mode"] != "independent_reproof"
+        or manifest["profile_id"] != EXPECTED_PROFILE_IDS["independent_reproof"]
+        or manifest["parent_image"] != SOURCE_V2_IMAGE
+        or manifest["mathlib_revision"] != EXPECTED_MATHLIB_REVISION
+    ):
+        fail("runtime manifest identity differs from the independent profile")
+    for field in (
+        "build_input_sha256",
+        "compiled_tree_sha256",
+        "declaration_inventory_sha256",
+        "ir_auxiliary_names_sha256",
+        "parent_receipt_canonical_sha256",
+        "parent_receipt_file_sha256",
+        "profile_sha256",
+        "runtime_source_checksum_manifest_sha256",
+        "runtime_source_tree_sha256",
+    ):
+        if not isinstance(manifest[field], str) or not SHA256_RE.fullmatch(
+            cast(str, manifest[field])
+        ):
+            fail(f"runtime manifest {field} is invalid")
+        if receipt.get(field) != manifest[field]:
+            fail(f"runtime manifest and receipt differ at {field}")
+    runtime_files = _runtime_files(manifest)
+    modules = manifest["runtime_modules"]
+    expected_modules = tuple(MODULE_BY_NAME)[:3]
+    runtime_file_records = cast(list[dict[str, object]], manifest["runtime_files"])
+    expected_paths = [f"lib/lean/{module.replace('.', '/')}.olean" for module in expected_modules]
+    if (
+        modules != list(expected_modules)
+        or list(runtime_files) != list(expected_modules)
+        or [record["path"] for record in runtime_file_records] != expected_paths
+    ):
+        fail("runtime module closure differs from the frozen independent profile")
+    inventory = manifest["declaration_inventory"]
+    if not isinstance(inventory, dict) or set(inventory) != {
+        "declarations",
+        "ir_auxiliary_names",
+        "ir_auxiliary_names_sha256",
+        "schema_version",
+    }:
+        fail("declaration inventory envelope drifted")
+    if inventory["schema_version"] != DECLARATION_INVENTORY_SCHEMA:
+        fail("declaration inventory protocol drifted")
+    records = _validate_declaration_records(
+        inventory["declarations"],
+        runtime_files=runtime_files,
+        include_origin_hash=True,
+    )
+    auxiliary = _validate_ir_auxiliary_records(
+        inventory["ir_auxiliary_names"],
+        runtime_files=runtime_files,
+        include_origin_hash=True,
+        kernel_names=frozenset(cast(str, record["name"]) for record in records),
+    )
+    auxiliary_sha256 = _sha256_bytes(_canonical_json_compact_bytes(auxiliary))
+    if (
+        inventory["ir_auxiliary_names_sha256"] != auxiliary_sha256
+        or manifest["ir_auxiliary_names_sha256"] != auxiliary_sha256
+        or receipt.get("ir_auxiliary_names_sha256") != auxiliary_sha256
+    ):
+        fail("IR auxiliary inventory hash differs across manifest and receipt")
+    for record in records:
+        if record["name"] in {TARGET_DECLARATION, SOUND_DECLARATION}:
+            fail("runtime inventory contains a forbidden pilot theorem")
+        if record["canonical_type_sha256"] == TARGET_TYPE_SHA256:
+            fail("runtime inventory contains an exact target-type collision")
+    return runtime_files, records, auxiliary
+
+
+def _validate_image_build_input(
+    build_input: Mapping[str, object],
+    *,
+    profile: ValidatedProfileBoundary,
+    source_checksums: bytes,
+    receipt: Mapping[str, object],
+) -> tuple[list[dict[str, object]], str]:
+    records, source_tree_sha256 = _validate_runtime_source_binding(
+        build_input,
+        profile,
+        source_root=FIXTURE_ROOT / "source",
+        source_checksums=source_checksums,
+    )
+    source_checksum_sha256 = _sha256_bytes(source_checksums)
+    if receipt.get("runtime_source_checksum_manifest_sha256") != source_checksum_sha256:
+        fail("image receipt is not bound to the runtime source checksum manifest")
+    return records, source_tree_sha256
+
+
+def verify(image: str) -> dict[str, object]:
+    inspected = _inspect(image)
+    actual_reference = _child_image_reference(inspected)
+    if actual_reference != image:
+        fail("requested child image differs from its Docker-recorded repository digest")
+    image_id = inspected.get("Id")
+    if not isinstance(image_id, str) or not re.fullmatch(r"sha256:[0-9a-f]{64}", image_id):
+        fail("child image has no immutable image ID")
+    receipt, image_receipt_sha256 = _receipt_output(image)
+    expected_receipt_fields = {
+        "build_input_sha256",
+        "build_tool_sha256",
+        "compiled_tree_sha256",
+        "declaration_inventory_sha256",
+        "dockerfile_sha256",
+        "inventory_helper_sha256",
+        "ir_auxiliary_names_sha256",
+        "parent_image",
+        "parent_receipt_canonical_sha256",
+        "parent_receipt_file_sha256",
+        "profile_id",
+        "profile_sha256",
+        "query_wrapper_sha256",
+        "receipt_tool_sha256",
+        "runtime_manifest_sha256",
+        "runtime_source_checksum_manifest_sha256",
+        "runtime_source_tree_sha256",
+        "schema_version",
+        "task_mode",
+    }
+    if set(receipt) != expected_receipt_fields:
+        fail("image receipt schema drifted")
+    if (
+        receipt["schema_version"] != IMAGE_RECEIPT_SCHEMA
+        or receipt["task_mode"] != "independent_reproof"
+        or receipt["profile_id"] != EXPECTED_PROFILE_IDS["independent_reproof"]
+        or receipt["parent_image"] != SOURCE_V2_IMAGE
+    ):
+        fail("image receipt identity differs from the independent profile")
+    for field in expected_receipt_fields - {
+        "parent_image",
+        "profile_id",
+        "schema_version",
+        "task_mode",
+    }:
+        if not isinstance(receipt[field], str) or not SHA256_RE.fullmatch(
+            cast(str, receipt[field])
+        ):
+            fail(f"image receipt {field} is invalid")
+    (
+        _,
+        current_parent_receipt_sha256,
+        current_parent_receipt_file_sha256,
+        _,
+    ) = _parent_receipt()
+    if receipt["parent_receipt_canonical_sha256"] != current_parent_receipt_sha256:
+        fail("child receipt is not bound to the verified source-v2 parent receipt")
+    if receipt["parent_receipt_file_sha256"] != current_parent_receipt_file_sha256:
+        fail("child receipt is not bound to the source-v2 receipt file")
+    _, current_profile_record = _profile()
+    current_profile_sha256 = _sha256_bytes(_canonical_json_bytes(current_profile_record))
+    if receipt["profile_sha256"] != current_profile_sha256:
+        fail("child receipt is not bound to the current independent profile")
+    labels = inspected.get("Config")
+    if not isinstance(labels, dict) or not isinstance(labels.get("Labels"), dict):
+        fail("child image labels are unavailable")
+    label_values = cast(dict[str, object], labels["Labels"])
+    if (
+        label_values.get("org.autolean.library-substrate.build-input-sha256")
+        != receipt["build_input_sha256"]
+        or label_values.get("org.autolean.library-substrate.parent-receipt-canonical-sha256")
+        != receipt["parent_receipt_canonical_sha256"]
+    ):
+        fail("child image labels differ from its image-owned receipt")
+    manifest, manifest_file_sha256 = _read_image_json(
+        image,
+        "/opt/autolean/library-substrate/attestations/runtime-manifest.v1.json",
+        label="runtime manifest",
+    )
+    if manifest_file_sha256 != receipt["runtime_manifest_sha256"]:
+        fail("runtime manifest file hash differs from the image receipt")
+    build_input, build_input_file_sha256 = _read_image_json(
+        image,
+        "/opt/autolean/library-substrate/attestations/build-input.v1.json",
+        label="substrate build input",
+    )
+    profile, _ = _profile()
+    source_checksums = _read_image_text(
+        image,
+        f"/opt/autolean/library-substrate/attestations/{RUNTIME_SOURCE_CHECKSUM_FILENAME}",
+    ).encode("utf-8")
+    source_records, source_tree_sha256 = _validate_image_build_input(
+        build_input,
+        profile=profile,
+        source_checksums=source_checksums,
+        receipt=receipt,
+    )
+    if (
+        build_input_file_sha256 != receipt["build_input_sha256"]
+        or build_input.get("schema_version") != "autolean.library-substrate-build-input.v1"
+        or build_input.get("profile_sha256") != current_profile_sha256
+        or build_input.get("parent_receipt_canonical_sha256") != current_parent_receipt_sha256
+        or build_input.get("parent_receipt_file_sha256") != current_parent_receipt_file_sha256
+        or manifest.get("runtime_source_checksum_manifest_sha256")
+        != _sha256_bytes(source_checksums)
+        or manifest.get("runtime_source_tree_sha256") != source_tree_sha256
+        or build_input.get("runtime_sources") != source_records
+    ):
+        fail("image-owned build input differs from the verified profile and parent")
+    runtime_files, records, auxiliary = _validate_manifest(manifest, receipt=receipt)
+    verified_runtime_files = _validate_runtime_file_closure(
+        image,
+        runtime_files,
+        manifest=manifest,
+        receipt=receipt,
+    )
+    return {
+        "declaration_count": len(records),
+        "image": image,
+        "image_id": image_id,
+        "image_receipt_sha256": image_receipt_sha256,
+        "parent_receipt_canonical_sha256": current_parent_receipt_sha256,
+        "receipt": receipt,
+        "runtime_file_count": len(runtime_files),
+        "verified_runtime_files": verified_runtime_files,
+        "ir_auxiliary_name_count": len(auxiliary),
+        "runtime_manifest": manifest,
+        "schema_version": "autolean.library-substrate-image-verification.v1",
+    }
+
+
+def _snapshot_candidate(destination: Path) -> tuple[Path, str]:
+    content = _regular_bytes(CANDIDATE_PATH, label="independent Candidate source")
+    destination.mkdir(parents=True, exist_ok=False)
+    candidate = destination / "Candidate.lean"
+    candidate.write_bytes(content)
+    candidate.chmod(0o444)
+    return candidate, _sha256_bytes(content)
+
+
+def _compile_candidate(image: str, candidate: Path, output: Path) -> Path:
+    output.mkdir()
+    output.chmod(0o777)
+    command = [
+        *_docker_run_base(),
+        "--mount",
+        f"type=bind,src={candidate.parent},dst=/input,readonly",
+        "--mount",
+        f"type=bind,src={output},dst=/output",
+        image,
+        "/opt/autolean/library-substrate/bin/autolean-library-substrate-independent-query",
+        "--phase",
+        "compile",
+        "--target",
+        TARGET_DECLARATION,
+    ]
+    _run(command, timeout=300)
+    compiler_output = output / "Candidate.olean"
+    if (
+        compiler_output.is_symlink()
+        or not compiler_output.is_file()
+        or compiler_output.stat().st_size <= 0
+        or compiler_output.stat().st_size > 64 * 1024 * 1024
+    ):
+        fail("candidate compiler did not emit a regular Candidate.olean")
+    sealed_root = output.parent / "sealed"
+    sealed_root.mkdir(mode=0o700)
+    sealed = sealed_root / "Candidate.olean"
+    sealed.write_bytes(compiler_output.read_bytes())
+    sealed.chmod(0o444)
+    return sealed
+
+
+def _query_candidate(image: str, compiled: Path) -> dict[str, object]:
+    command = [
+        *_docker_run_base(),
+        "--mount",
+        f"type=bind,src={compiled},dst=/compiled/Candidate.olean,readonly",
+        image,
+        "/opt/autolean/library-substrate/bin/autolean-library-substrate-independent-query",
+        "--phase",
+        "query",
+        "--target",
+        TARGET_DECLARATION,
+    ]
+    output = _run(command, timeout=300).stdout
+    return _json_record(output, label="independent Candidate query")
+
+
+def _validate_query(
+    query: dict[str, object],
+    *,
+    runtime_files: Mapping[str, Mapping[str, object]],
+    verified_runtime_files: Mapping[str, Mapping[str, object]],
+    manifest_records: list[dict[str, object]],
+    manifest_auxiliary: list[dict[str, object]],
+    expected_identity: Mapping[str, object],
+) -> dict[str, object]:
+    if dict(runtime_files) != dict(verified_runtime_files):
+        fail("fresh query origin hashes cannot be supplemented before OLean facts close")
+    expected = {
+        "candidate_direct_imports",
+        "candidate_ir_auxiliary_names",
+        "candidate_kernel_names",
+        "candidate_namespace_disjoint",
+        "candidate_owns_target",
+        "canonical_type",
+        "declaration",
+        "direct_proof_dependencies",
+        "loaded_module_closure",
+        "observed_axioms",
+        "runtime_declarations",
+        "runtime_ir_auxiliary_names",
+        "schema_version",
+        "substrate_identity",
+    }
+    if set(query) != expected:
+        fail("Candidate query schema drifted")
+    if (
+        query["schema_version"] != QUERY_SCHEMA
+        or query["candidate_owns_target"] is not True
+        or query["candidate_namespace_disjoint"] is not True
+        or query["declaration"] != TARGET_DECLARATION
+    ):
+        fail("Candidate query did not establish sealed-module ownership")
+    candidate_kernel_names = _sorted_unique_strings(
+        query["candidate_kernel_names"], label="Candidate kernel names"
+    )
+    candidate_auxiliary_names = _sorted_unique_strings(
+        query["candidate_ir_auxiliary_names"], label="Candidate IR auxiliary names"
+    )
+    if TARGET_DECLARATION not in candidate_kernel_names:
+        fail("Candidate kernel ownership omits the target")
+    if set(candidate_kernel_names).intersection(candidate_auxiliary_names):
+        fail("Candidate kernel and IR ownership overlap")
+    runtime_owned_names = {
+        *(cast(str, record["name"]) for record in manifest_records),
+        *(cast(str, record["name"]) for record in manifest_auxiliary),
+    }
+    if runtime_owned_names.intersection((*candidate_kernel_names, *candidate_auxiliary_names)):
+        fail("Candidate owned names collide with runtime ownership")
+    identity = query["substrate_identity"]
+    if not isinstance(identity, dict) or set(identity) != {
+        "image_receipt_sha256",
+        "profile_sha256",
+        "query_wrapper_sha256",
+        "runtime_manifest_sha256",
+    }:
+        fail("Candidate query substrate identity drifted")
+    if identity != expected_identity:
+        fail("Candidate query is not bound to the verified image-owned substrate")
+    direct_imports = _sorted_unique_strings(
+        query["candidate_direct_imports"], label="Candidate direct imports"
+    )
+    if direct_imports != (
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude",
+        "Init",
+    ):
+        fail(f"Candidate direct imports differ from the independent profile: {direct_imports}")
+    loaded = _sorted_unique_strings(query["loaded_module_closure"], label="loaded module closure")
+    for module in (*runtime_files, "Candidate"):
+        if module not in loaded:
+            fail(f"loaded module closure omits {module}")
+    forbidden_modules = {
+        "AutoLeanLibrary.Fixtures.ModelTheory.Packet",
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK",
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Controls",
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Targets.ClosedSound",
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Targets.DerivSound",
+    }
+    if forbidden_modules.intersection(loaded):
+        fail("loaded module closure contains a forbidden module")
+    canonical_type = query["canonical_type"]
+    if (
+        not isinstance(canonical_type, str)
+        or _sha256_bytes(canonical_type.encode("utf-8")) != TARGET_TYPE_SHA256
+    ):
+        fail("Candidate target type differs from the historical frozen diagnostic")
+    axioms = _sorted_unique_strings(query["observed_axioms"], label="target axioms")
+    if axioms != EXPECTED_TARGET_AXIOMS:
+        fail("Candidate target axiom observation differs from the historical diagnostic")
+    dependencies = _sorted_unique_strings(
+        query["direct_proof_dependencies"], label="direct proof dependencies"
+    )
+    if SOUND_DECLARATION in dependencies:
+        fail("independent Candidate directly uses Deriv.sound")
+    fresh_records = _validate_declaration_records(
+        query["runtime_declarations"],
+        runtime_files=runtime_files,
+        include_origin_hash=False,
+    )
+    if fresh_records != manifest_records:
+        fail("fresh runtime declaration inventory differs from the image manifest")
+    fresh_auxiliary = _validate_ir_auxiliary_records(
+        query["runtime_ir_auxiliary_names"],
+        runtime_files=runtime_files,
+        include_origin_hash=False,
+        kernel_names=frozenset(cast(str, record["name"]) for record in fresh_records),
+    )
+    if fresh_auxiliary != manifest_auxiliary:
+        fail("fresh IR auxiliary inventory differs from the image manifest")
+    return {
+        "candidate_direct_imports": list(direct_imports),
+        "candidate_ir_auxiliary_names": list(candidate_auxiliary_names),
+        "candidate_kernel_names": list(candidate_kernel_names),
+        "candidate_namespace_disjoint": True,
+        "direct_proof_dependencies": list(dependencies),
+        "loaded_module_closure": list(loaded),
+        "observed_axioms": list(axioms),
+        "runtime_inventory_replayed": True,
+        "ir_auxiliary_inventory_replayed": True,
+        "target_canonical_type_sha256": TARGET_TYPE_SHA256,
+    }
+
+
+def canary(image: str) -> dict[str, object]:
+    verified = verify(image)
+    manifest = cast(dict[str, object], verified["runtime_manifest"])
+    receipt = cast(dict[str, object], verified["receipt"])
+    runtime_files, records, auxiliary = _validate_manifest(manifest, receipt=receipt)
+    with tempfile.TemporaryDirectory(
+        prefix="autolean-library-substrate-candidate-", dir="/tmp"
+    ) as raw:
+        root = Path(raw)
+        candidate, candidate_sha256 = _snapshot_candidate(root / "source")
+        compiled = _compile_candidate(image, candidate, root / "compiled")
+        compiled_sha256 = _sha256(compiled)
+        query = _query_candidate(image, compiled)
+    observation = _validate_query(
+        query,
+        runtime_files=runtime_files,
+        verified_runtime_files=cast(
+            dict[str, dict[str, object]], verified["verified_runtime_files"]
+        ),
+        manifest_records=records,
+        manifest_auxiliary=auxiliary,
+        expected_identity={
+            "image_receipt_sha256": verified["image_receipt_sha256"],
+            "profile_sha256": receipt["profile_sha256"],
+            "query_wrapper_sha256": receipt["query_wrapper_sha256"],
+            "runtime_manifest_sha256": receipt["runtime_manifest_sha256"],
+        },
+    )
+    return {
+        "authority": "operator-local-image-owned-preflight-only",
+        "candidate_olean_sha256": compiled_sha256,
+        "candidate_source_sha256": candidate_sha256,
+        "image": image,
+        "image_id": verified["image_id"],
+        "non_claims": [
+            "no_contract_or_gateway_integration",
+            "no_external_dependency_capsule",
+            "no_formal_asset_admission",
+            "no_oci_lean_runner_v2_adapter",
+            "no_provider_execution",
+            "no_v2_evidence_or_gateway_receipt",
+        ],
+        "observation": observation,
+        "parent_receipt_canonical_sha256": verified["parent_receipt_canonical_sha256"],
+        "receipt_canonical_sha256": _sha256_bytes(_canonical_json_bytes(receipt)),
+        "schema_version": CANARY_SCHEMA,
+        "task_mode": "independent_reproof",
+    }
+
+
+def _wsl_path(path: Path) -> str:
+    completed = _run(
+        ["wsl.exe", "-d", WSL_DISTRIBUTION, "-e", "wslpath", "-a", str(path)],
+        timeout=30,
+    )
+    translated = completed.stdout.strip()
+    if not translated:
+        fail("WSL path translation returned an empty path")
+    return translated
+
+
+def _delegate_to_wsl(arguments: argparse.Namespace) -> int:
+    script = Path(__file__).resolve()
+    forwarded = [
+        "wsl.exe",
+        "-d",
+        WSL_DISTRIBUTION,
+        "--cd",
+        _wsl_path(script.parents[2]),
+        "--",
+        "python3",
+        _wsl_path(script),
+        arguments.action,
+        "--native",
+    ]
+    if arguments.image is not None:
+        forwarded.extend(("--image", arguments.image))
+    return subprocess.run(forwarded, check=False).returncode
+
+
+def parse_arguments(arguments: Sequence[str] | None = None) -> argparse.Namespace:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("action", choices=("build", "verify", "canary", "all"))
+    parser.add_argument("--image")
+    parser.add_argument("--native", action="store_true", help=argparse.SUPPRESS)
+    parsed = parser.parse_args(arguments)
+    if parsed.action in {"verify", "canary"} and parsed.image is None:
+        parser.error(f"{parsed.action} requires --image")
+    if parsed.action in {"build", "all"} and parsed.image is not None:
+        parser.error(f"{parsed.action} does not accept --image")
+    return parsed
+
+
+def main(arguments: Sequence[str] | None = None) -> int:
+    parsed = parse_arguments(arguments)
+    if os.name == "nt" and not parsed.native:
+        return _delegate_to_wsl(parsed)
+    try:
+        if parsed.action == "build":
+            result = build()
+        elif parsed.action == "verify":
+            result = verify(cast(str, parsed.image))
+        elif parsed.action == "canary":
+            result = canary(cast(str, parsed.image))
+        else:
+            build_result = build()
+            result = {
+                "build": build_result,
+                "canary": canary(cast(str, build_result["image"])),
+                "schema_version": "autolean.library-substrate-image-all.v1",
+            }
+        print(json.dumps(result, ensure_ascii=True, sort_keys=True))
+        return 0
+    except (SubstrateImageError, SystemExit) as error:
+        print(f"library-substrate-image: {error}", file=sys.stderr)
+        return 2
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())
diff --git a/Prover/worker/Dockerfile.library-substrate b/Prover/worker/Dockerfile.library-substrate
new file mode 100644
index 0000000..abd8461
--- /dev/null
+++ b/Prover/worker/Dockerfile.library-substrate
@@ -0,0 +1,61 @@
+FROM autolean/mathlib-worker@sha256:3237192cf627a05367c75d46e61ec9034fefe43a4fd0c06139e38c80358648d6 AS library-substrate-builder
+
+USER 0:0
+
+ARG BUILD_INPUT_SHA256
+ARG BUILD_TOOL_SHA256
+ARG DOCKERFILE_SHA256
+ARG INVENTORY_HELPER_SHA256
+ARG PARENT_RECEIPT_CANONICAL_SHA256
+ARG PARENT_RECEIPT_FILE_SHA256
+ARG QUERY_WRAPPER_SHA256
+ARG RECEIPT_TOOL_SHA256
+ARG RUNTIME_SOURCE_CHECKSUM_MANIFEST_SHA256
+ARG RUNTIME_SOURCE_TREE_SHA256
+
+COPY build-input.v1.json /build/input/build-input.v1.json
+COPY runtime-sources.sha256 /build/input/runtime-sources.sha256
+COPY source/ /build/source/
+COPY helpers/AutoleanLibrarySubstrateInventory.lean /build/tools/AutoleanLibrarySubstrateInventory.lean
+COPY helpers/autolean-library-substrate-build /build/tools/autolean-library-substrate-build
+COPY helpers/autolean-library-substrate-independent-query /build/tools/autolean-library-substrate-independent-query
+COPY helpers/autolean-library-substrate-build-receipt /build/tools/autolean-library-substrate-build-receipt
+COPY Dockerfile.library-substrate /build/tools/Dockerfile.library-substrate
+
+RUN /build/tools/autolean-library-substrate-build \
+      "${BUILD_INPUT_SHA256}" \
+      "${BUILD_TOOL_SHA256}" \
+      "${DOCKERFILE_SHA256}" \
+      "${INVENTORY_HELPER_SHA256}" \
+      "${PARENT_RECEIPT_CANONICAL_SHA256}" \
+      "${PARENT_RECEIPT_FILE_SHA256}" \
+      "${QUERY_WRAPPER_SHA256}" \
+      "${RECEIPT_TOOL_SHA256}" \
+      "${RUNTIME_SOURCE_CHECKSUM_MANIFEST_SHA256}" \
+      "${RUNTIME_SOURCE_TREE_SHA256}"
+
+FROM autolean/mathlib-worker@sha256:3237192cf627a05367c75d46e61ec9034fefe43a4fd0c06139e38c80358648d6
+
+USER 0:0
+
+ARG BUILD_INPUT_SHA256
+ARG PARENT_RECEIPT_CANONICAL_SHA256
+
+LABEL org.opencontainers.image.title="AutoLean library-substrate-v1 preflight" \
+      org.opencontainers.image.description="Image-owned independent-reproof UniversalLK substrate preflight" \
+      org.opencontainers.image.version="library-substrate-v1-independent-preflight" \
+      org.autolean.library-substrate.profile="library-substrate-v1-model-theory-universal-lk-independent-reproof" \
+      org.autolean.library-substrate.task-mode="independent_reproof" \
+      org.autolean.library-substrate.build-input-sha256="${BUILD_INPUT_SHA256}" \
+      org.autolean.library-substrate.parent-receipt-canonical-sha256="${PARENT_RECEIPT_CANONICAL_SHA256}"
+
+COPY --from=library-substrate-builder --chown=0:0 \
+  /build/final/ /opt/autolean/library-substrate/
+
+RUN test -x /opt/autolean/library-substrate/bin/autolean-library-substrate-build-receipt \
+    && test -x /opt/autolean/library-substrate/bin/autolean-library-substrate-independent-query \
+    && test -z "$(find /opt/autolean/library-substrate -name '*.lean' -o -name '*.ilean')" \
+    && /opt/autolean/library-substrate/bin/autolean-library-substrate-build-receipt >/dev/null
+
+USER 65532:65532
+WORKDIR /workspace
diff --git a/Prover/worker/library-substrate/AutoleanLibrarySubstrateInventory.lean b/Prover/worker/library-substrate/AutoleanLibrarySubstrateInventory.lean
new file mode 100644
index 0000000..1fa1c5a
--- /dev/null
+++ b/Prover/worker/library-substrate/AutoleanLibrarySubstrateInventory.lean
@@ -0,0 +1,189 @@
+import AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude
+import Lean.Compiler.IR.CompilerM
+import Lean.PrettyPrinter
+import Lean.Util.CollectAxioms
+
+open Lean
+
+private def coreModule :=
+  `AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Core
+
+private def semanticModule :=
+  `AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.SemanticPrelude
+
+private def ruleModule :=
+  `AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude
+
+private def moduleRecords : Array (Name × System.FilePath) := #[
+  (coreModule,
+    "/build/compiled/AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/Core.olean"),
+  (semanticModule,
+    "/build/compiled/AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/SemanticPrelude.olean"),
+  (ruleModule,
+    "/build/compiled/AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/RulePrelude.olean")
+]
+
+private def canonicalOptions : Options :=
+  ((((({} : Options).setBool `pp.all true).setBool `pp.explicit true).setBool
+        `pp.universes true).setBool `pp.notation false).set `pp.width (1000000 : Nat)
+
+private def sortedNames (names : Array Name) : Array Name :=
+  names.qsort fun left right => left.toString < right.toString
+
+private def namesJson (names : Array Name) : Json :=
+  Json.arr <| sortedNames names |>.map fun name => Json.str name.toString
+
+private def canonicalType (environment : Environment) (info : ConstantInfo) : IO String := do
+  if info.type.hasMVar then
+    throw <| IO.userError s!"declaration type contains a metavariable: {info.name}"
+  let rendered :=
+    (← PrettyPrinter.ppExprLegacy environment {} {} canonicalOptions info.type).pretty 1000000
+  if rendered.isEmpty || rendered.length > 1000000 then
+    throw <| IO.userError s!"canonical type has invalid size: {info.name}"
+  if rendered.any fun char => char == '\x00' || char == '\n' || char == '\r' then
+    throw <| IO.userError s!"canonical type is not one line: {info.name}"
+  return rendered
+
+private def sha256Text (value : String) : IO String := do
+  let path : System.FilePath := "/tmp/autolean-library-substrate-type.txt"
+  IO.FS.writeFile path value
+  let output ← IO.Process.output { cmd := "sha256sum", args := #[path.toString] }
+  if output.exitCode != 0 then
+    throw <| IO.userError "sha256sum failed while hashing a canonical type"
+  let digest := (output.stdout.trimAscii.take 64).toString
+  if digest.length != 64 || !digest.all fun char => char.isDigit || ('a' ≤ char && char ≤ 'f') then
+    throw <| IO.userError "sha256sum emitted an invalid digest"
+  return digest
+
+private def observedAxioms (environment : Environment) (name : Name) : IO (Array Name) := do
+  let context : Core.Context := {
+    fileName := "<AutoLeanLibrarySubstrateInventory>"
+    fileMap := default
+    options := canonicalOptions
+  }
+  let state : Core.State := { env := environment }
+  let axioms ← Core.CoreM.toIO' (collectAxioms name) context state
+  return sortedNames axioms
+
+private def constantKind : ConstantInfo → String
+  | .axiomInfo _ => "axiom"
+  | .defnInfo _ => "definition"
+  | .thmInfo _ => "theorem"
+  | .opaqueInfo _ => "opaque"
+  | .quotInfo _ => "quotient"
+  | .inductInfo _ => "inductive"
+  | .ctorInfo _ => "constructor"
+  | .recInfo _ => "recursor"
+
+private def originModule (environment : Environment) (name : Name) : IO Name := do
+  let some index := environment.getModuleIdxFor? name
+    | throw <| IO.userError s!"imported declaration has no module mapping: {name}"
+  let some moduleName := environment.header.moduleNames[index.toNat]?
+    | throw <| IO.userError s!"module index is outside the loaded header: {name}"
+  return moduleName
+
+private def originOleanSha256
+    (origin : Name) (coreSha semanticSha ruleSha : String) : IO String := do
+  if origin == coreModule then
+    return coreSha
+  if origin == semanticModule then
+    return semanticSha
+  if origin == ruleModule then
+    return ruleSha
+  throw <| IO.userError s!"AutoLean declaration resolved outside the runtime closure: {origin}"
+
+private def declarationRecord
+    (environment : Environment)
+    (expectedOrigin name : Name)
+    (coreSha semanticSha ruleSha : String) : IO Json := do
+  let some info := environment.checked.get.find? name
+    | throw <| IO.userError s!"runtime declaration has no ConstantInfo: {name}"
+  let origin ← originModule environment name
+  if origin != expectedOrigin then
+    throw <| IO.userError s!"runtime declaration origin mismatch: {name}"
+  let renderedType ← canonicalType environment info
+  let typeSha ← sha256Text renderedType
+  let axioms ← observedAxioms environment name
+  return Json.mkObj [
+    ("canonical_type", Json.str renderedType),
+    ("canonical_type_sha256", Json.str typeSha),
+    ("declaration_kind", Json.str (constantKind info)),
+    ("name", Json.str name.toString),
+    ("observed_axioms", namesJson axioms),
+    ("origin_module", Json.str origin.toString),
+    ("origin_olean_sha256",
+      Json.str (← originOleanSha256 origin coreSha semanticSha ruleSha))
+  ]
+
+private def auxiliaryRecord
+    (environment : Environment)
+    (expectedOrigin name : Name)
+    (coreSha semanticSha ruleSha : String) : IO Json := do
+  if (environment.checked.get.find? name).isSome then
+    throw <| IO.userError s!"IR auxiliary name overlaps a kernel declaration: {name}"
+  let some declaration := Lean.IR.findEnvDecl environment name
+    | throw <| IO.userError s!"IR auxiliary has no IR declaration: {name}"
+  if declaration.name != name then
+    throw <| IO.userError s!"IR auxiliary declaration name mismatch: {name}"
+  let declarationKind :=
+    match declaration with
+    | .fdecl .. => "fdecl"
+    | .extern .. => "extern"
+  let origin ← originModule environment name
+  if origin != expectedOrigin then
+    throw <| IO.userError s!"IR auxiliary origin mismatch: {name}"
+  return Json.mkObj [
+    ("ir_decl_kind", Json.str declarationKind),
+    ("name", Json.str name.toString),
+    ("origin_module", Json.str origin.toString),
+    ("origin_olean_sha256",
+      Json.str (← originOleanSha256 origin coreSha semanticSha ruleSha))
+  ]
+
+private def inventory (coreSha semanticSha ruleSha : String) : IO Json := do
+  let environment ← importModules #[{ module := ruleModule }] canonicalOptions
+  let mut records : Array (String × Json) := #[]
+  let mut auxiliary : Array (String × Json) := #[]
+  let mut seen : NameSet := {}
+  let mut seenAuxiliary : NameSet := {}
+  for (moduleName, path) in moduleRecords do
+    let (moduleData, _) ← readModuleData path
+    for name in moduleData.extraConstNames do
+      if seenAuxiliary.contains name then
+        throw <| IO.userError s!"duplicate IR auxiliary name: {name}"
+      seenAuxiliary := seenAuxiliary.insert name
+      auxiliary := auxiliary.push (
+        name.toString,
+        ← auxiliaryRecord environment moduleName name coreSha semanticSha ruleSha
+      )
+    for name in moduleData.constNames do
+      if name.toString.startsWith "AutoLeanLibrary." then
+        if seen.contains name then
+          throw <| IO.userError s!"duplicate runtime declaration: {name}"
+        seen := seen.insert name
+        records := records.push (
+          name.toString,
+          ← declarationRecord environment moduleName name coreSha semanticSha ruleSha
+        )
+  records := records.qsort fun left right => left.1 < right.1
+  auxiliary := auxiliary.qsort fun left right => left.1 < right.1
+  let auxiliaryJson := Json.arr <| auxiliary.map (·.2)
+  return Json.mkObj [
+    ("declarations", Json.arr <| records.map (·.2)),
+    ("ir_auxiliary_names", auxiliaryJson),
+    ("ir_auxiliary_names_sha256", Json.str (← sha256Text auxiliaryJson.compress)),
+    ("schema_version", Json.str "autolean.library-substrate-declaration-inventory.v1")
+  ]
+
+def main (arguments : List String) : IO UInt32 := do
+  try
+    let [coreSha, semanticSha, ruleSha] := arguments
+      | throw <| IO.userError "expected the three runtime OLean SHA-256 values"
+    for digest in #[coreSha, semanticSha, ruleSha] do
+      if digest.length != 64 then
+        throw <| IO.userError "runtime OLean SHA-256 has invalid length"
+    IO.println (← inventory coreSha semanticSha ruleSha).compress
+    return (0 : UInt32)
+  catch error =>
+    IO.eprintln s!"autolean-library-substrate-inventory: {error}"
+    return (2 : UInt32)
diff --git a/Prover/worker/library-substrate/autolean-library-substrate-build b/Prover/worker/library-substrate/autolean-library-substrate-build
new file mode 100644
index 0000000..76abc7d
--- /dev/null
+++ b/Prover/worker/library-substrate/autolean-library-substrate-build
@@ -0,0 +1,264 @@
+#!/bin/sh
+set -eu
+
+fail() {
+  printf '%s\n' "autolean-library-substrate-build: $1" >&2
+  exit 2
+}
+
+[ "$#" -eq 10 ] || fail "expected the frozen build argument profile"
+build_input_sha256=$1
+build_tool_sha256=$2
+dockerfile_sha256=$3
+inventory_helper_sha256=$4
+parent_receipt_sha256=$5
+parent_receipt_file_sha256=$6
+query_wrapper_sha256=$7
+receipt_tool_sha256=$8
+runtime_source_checksum_manifest_sha256=$9
+runtime_source_tree_sha256=${10}
+
+for digest in "$@"; do
+  case "$digest" in
+    *[!0-9a-f]*|"") fail "build argument is not a lowercase SHA-256" ;;
+  esac
+  [ "${#digest}" -eq 64 ] || fail "build argument has invalid SHA-256 length"
+done
+
+input=/build/input/build-input.v1.json
+source_checksums=/build/input/runtime-sources.sha256
+source=/build/source
+tools=/build/tools
+compiled=/build/compiled
+final=/build/final
+parent_receipt=/opt/autolean/attestations/mathlib-source-build-receipt.v2.json
+
+core_rel=AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/Core
+semantic_rel=AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/SemanticPrelude
+rule_rel=AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/RulePrelude
+
+test "$(sha256sum "$input" | awk '{print $1}')" = "$build_input_sha256"
+test "$(sha256sum "$source_checksums" | awk '{print $1}')" = \
+  "$runtime_source_checksum_manifest_sha256"
+test "$(sha256sum "$tools/autolean-library-substrate-build" | awk '{print $1}')" = \
+  "$build_tool_sha256"
+test "$(sha256sum "$tools/Dockerfile.library-substrate" | awk '{print $1}')" = \
+  "$dockerfile_sha256"
+test "$(sha256sum "$tools/AutoleanLibrarySubstrateInventory.lean" | awk '{print $1}')" = \
+  "$inventory_helper_sha256"
+test "$(sha256sum "$tools/autolean-library-substrate-independent-query" | awk '{print $1}')" = \
+  "$query_wrapper_sha256"
+test "$(sha256sum "$tools/autolean-library-substrate-build-receipt" | awk '{print $1}')" = \
+  "$receipt_tool_sha256"
+test "$(sha256sum "$parent_receipt" | awk '{print $1}')" = \
+  "$parent_receipt_file_sha256"
+test "$(
+  LC_ALL=C sed -n \
+    's/^.*"parent_receipt_canonical_sha256":"\([0-9a-f]\{64\}\)".*$/\1/p' \
+    "$input"
+)" = "$parent_receipt_sha256"
+profile_sha256=$(
+  LC_ALL=C sed -n \
+    's/^.*"profile_sha256":"\([0-9a-f]\{64\}\)".*$/\1/p' \
+    "$input"
+)
+test "${#profile_sha256}" -eq 64
+
+test -z "$(find "$source" ! -type f ! -type d -print -quit)"
+test "$(find "$source" -type f | wc -l | tr -d ' ')" -eq 3
+for relative in "$core_rel" "$semantic_rel" "$rule_rel"; do
+  test -f "$source/$relative.lean"
+  test ! -L "$source/$relative.lean"
+done
+(cd /build && sha256sum --check --strict --status input/runtime-sources.sha256) ||
+  fail "runtime source checksum mismatch"
+input_hash() {
+  field=$1
+  LC_ALL=C sed -n "s/^.*\"$field\":\"\\([0-9a-f]\\{64\\}\)\".*$/\\1/p" "$input"
+}
+source_record() {
+  module=$1
+  relative=$2
+  LC_ALL=C sed -n \
+    "s|^.*\"module\":\"$module\",\"path\":\"$relative\",\"role\":\"[^\"]*\",\"sha256\":\"\\([0-9a-f]\\{64\\}\)\",\"size\":\\([0-9]\\+\\)}.*$|\\1 \\2|p" \
+    "$input"
+}
+source_records=$(
+  LC_ALL=C sed -n 's/^.*"runtime_sources":\(\[.*\]\),"schema_version".*$/\1/p' "$input"
+)
+test -n "$source_records" || fail "runtime source records are unavailable"
+test "$(printf '%s\n' "$source_records" | sha256sum | awk '{print $1}')" = \
+  "$runtime_source_tree_sha256" || fail "runtime source tree argument drifted"
+test "$(input_hash runtime_source_tree_sha256)" = "$runtime_source_tree_sha256" ||
+  fail "runtime source tree is not bound by the build input"
+test "$(input_hash runtime_source_checksum_manifest_sha256)" = \
+  "$runtime_source_checksum_manifest_sha256" ||
+  fail "runtime source checksum manifest is not bound by the build input"
+
+core_source_record=$(source_record \
+  AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Core "$core_rel.lean")
+semantic_source_record=$(source_record \
+  AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.SemanticPrelude "$semantic_rel.lean")
+rule_source_record=$(source_record \
+  AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude "$rule_rel.lean")
+for record in "$core_source_record" "$semantic_source_record" "$rule_source_record"; do
+  set -- $record
+  test "$#" -eq 2 || fail "runtime source record schema drifted"
+  case "$1" in *[!0-9a-f]*|"") fail "runtime source hash is invalid" ;; esac
+  case "$2" in *[!0-9]*|"") fail "runtime source size is invalid" ;; esac
+done
+set -- $core_source_record
+core_source_sha=$1
+core_source_size=$2
+set -- $semantic_source_record
+semantic_source_sha=$1
+semantic_source_size=$2
+set -- $rule_source_record
+rule_source_sha=$1
+rule_source_size=$2
+for relative_and_expected in \
+  "$core_rel.lean:$core_source_sha:$core_source_size" \
+  "$semantic_rel.lean:$semantic_source_sha:$semantic_source_size" \
+  "$rule_rel.lean:$rule_source_sha:$rule_source_size"
+do
+  relative=${relative_and_expected%%:*}
+  remaining=${relative_and_expected#*:}
+  expected_sha=${remaining%%:*}
+  expected_size=${remaining#*:}
+  actual_sha=$(sha256sum "$source/$relative" | awk '{print $1}')
+  actual_size=$(wc -c <"$source/$relative" | tr -d ' ')
+  test "$actual_sha" = "$expected_sha" || fail "runtime source bytes differ from build input"
+  test "$actual_size" = "$expected_size" || fail "runtime source bytes differ from build input"
+done
+expected_source_checksum_sha=$(
+  {
+    printf '%s  source/%s\n' "$core_source_sha" "$core_rel.lean"
+    printf '%s  source/%s\n' "$semantic_source_sha" "$semantic_rel.lean"
+    printf '%s  source/%s\n' "$rule_source_sha" "$rule_rel.lean"
+  } | sha256sum | awk '{print $1}'
+)
+test "$expected_source_checksum_sha" = "$runtime_source_checksum_manifest_sha256" ||
+  fail "runtime source checksum manifest differs from build input"
+
+mkdir -p \
+  "$compiled/$(dirname "$core_rel")" \
+  "$final/bin" \
+  "$final/lib/lean/$(dirname "$core_rel")" \
+  "$final/attestations"
+
+parent_lean_path=$(cat /opt/autolean/environment/lean-path)
+test -n "$parent_lean_path"
+export LEAN_PATH="$compiled:$parent_lean_path"
+
+lean -R "$source" -o "$compiled/$core_rel.olean" "$source/$core_rel.lean"
+lean -R "$source" -o "$compiled/$semantic_rel.olean" "$source/$semantic_rel.lean"
+lean -R "$source" -o "$compiled/$rule_rel.olean" "$source/$rule_rel.lean"
+
+test -z "$(find "$compiled" ! -type f ! -type d -print -quit)"
+test "$(find "$compiled" -type f | wc -l | tr -d ' ')" -eq 3
+
+core_sha=$(sha256sum "$compiled/$core_rel.olean" | awk '{print $1}')
+semantic_sha=$(sha256sum "$compiled/$semantic_rel.olean" | awk '{print $1}')
+rule_sha=$(sha256sum "$compiled/$rule_rel.olean" | awk '{print $1}')
+
+lean --run "$tools/AutoleanLibrarySubstrateInventory.lean" \
+  "$core_sha" "$semantic_sha" "$rule_sha" \
+  >"$final/attestations/declaration-inventory.v1.json" \
+  2>"$final/attestations/declaration-inventory.stderr"
+test ! -s "$final/attestations/declaration-inventory.stderr"
+rm "$final/attestations/declaration-inventory.stderr"
+test "$(wc -l <"$final/attestations/declaration-inventory.v1.json" | tr -d ' ')" -eq 1
+inventory_sha256=$(
+  sha256sum "$final/attestations/declaration-inventory.v1.json" | awk '{print $1}'
+)
+ir_auxiliary_names_sha256=$(
+  LC_ALL=C sed -n \
+    's/^.*"ir_auxiliary_names_sha256":"\([0-9a-f]\{64\}\)".*$/\1/p' \
+    "$final/attestations/declaration-inventory.v1.json"
+)
+test "${#ir_auxiliary_names_sha256}" -eq 64
+
+cp "$compiled/$core_rel.olean" "$final/lib/lean/$core_rel.olean"
+cp "$compiled/$semantic_rel.olean" "$final/lib/lean/$semantic_rel.olean"
+cp "$compiled/$rule_rel.olean" "$final/lib/lean/$rule_rel.olean"
+cp "$input" "$final/attestations/build-input.v1.json"
+cp "$source_checksums" "$final/attestations/runtime-sources.sha256"
+cp "$tools/autolean-library-substrate-independent-query" \
+  "$final/bin/autolean-library-substrate-independent-query"
+cp "$tools/autolean-library-substrate-build-receipt" \
+  "$final/bin/autolean-library-substrate-build-receipt"
+chmod 0555 "$final/bin/"*
+find "$final/lib" -type f -exec chmod 0444 {} \;
+find "$final/attestations" -type f -exec chmod 0444 {} \;
+
+(
+  cd "$final"
+  printf '%s  %s\n' "$core_sha" "lib/lean/$core_rel.olean"
+  printf '%s  %s\n' "$semantic_sha" "lib/lean/$semantic_rel.olean"
+  printf '%s  %s\n' "$rule_sha" "lib/lean/$rule_rel.olean"
+) >"$final/attestations/runtime-files.sha256"
+compiled_tree_sha256=$(
+  sha256sum "$final/attestations/runtime-files.sha256" | awk '{print $1}'
+)
+
+core_size=$(wc -c <"$compiled/$core_rel.olean" | tr -d ' ')
+semantic_size=$(wc -c <"$compiled/$semantic_rel.olean" | tr -d ' ')
+rule_size=$(wc -c <"$compiled/$rule_rel.olean" | tr -d ' ')
+
+{
+  printf '{'
+  printf '"build_input_sha256":"%s",' "$build_input_sha256"
+  printf '"compiled_tree_sha256":"%s",' "$compiled_tree_sha256"
+  printf '"declaration_inventory":'
+  tr -d '\n' <"$final/attestations/declaration-inventory.v1.json"
+  printf ',"declaration_inventory_sha256":"%s",' "$inventory_sha256"
+  printf '"ir_auxiliary_names_sha256":"%s",' "$ir_auxiliary_names_sha256"
+  printf '"mathlib_revision":"8f9d9cff6bd728b17a24e163c9402775d9e6a365",'
+  printf '"parent_image":"autolean/mathlib-worker@sha256:3237192cf627a05367c75d46e61ec9034fefe43a4fd0c06139e38c80358648d6",'
+  printf '"parent_receipt_canonical_sha256":"%s",' "$parent_receipt_sha256"
+  printf '"parent_receipt_file_sha256":"%s",' "$parent_receipt_file_sha256"
+  printf '"profile_id":"library-substrate-v1-model-theory-universal-lk-independent-reproof",'
+  printf '"profile_sha256":"%s",' "$profile_sha256"
+  printf '"runtime_files":['
+  printf '{"module":"AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Core","path":"lib/lean/%s.olean","sha256":"%s","size":%s},' "$core_rel" "$core_sha" "$core_size"
+  printf '{"module":"AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.SemanticPrelude","path":"lib/lean/%s.olean","sha256":"%s","size":%s},' "$semantic_rel" "$semantic_sha" "$semantic_size"
+  printf '{"module":"AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude","path":"lib/lean/%s.olean","sha256":"%s","size":%s}' "$rule_rel" "$rule_sha" "$rule_size"
+  printf '],'
+  printf '"runtime_modules":["AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Core","AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.SemanticPrelude","AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude"],'
+  printf '"runtime_source_checksum_manifest_sha256":"%s",' "$runtime_source_checksum_manifest_sha256"
+  printf '"runtime_source_tree_sha256":"%s",' "$runtime_source_tree_sha256"
+  printf '"schema_version":"autolean.library-substrate-runtime-manifest.v1",'
+  printf '"task_mode":"independent_reproof"'
+  printf '}\n'
+} >"$final/attestations/runtime-manifest.v1.json"
+
+runtime_manifest_sha256=$(
+  sha256sum "$final/attestations/runtime-manifest.v1.json" | awk '{print $1}'
+)
+{
+  printf '{'
+  printf '"build_input_sha256":"%s",' "$build_input_sha256"
+  printf '"build_tool_sha256":"%s",' "$build_tool_sha256"
+  printf '"compiled_tree_sha256":"%s",' "$compiled_tree_sha256"
+  printf '"declaration_inventory_sha256":"%s",' "$inventory_sha256"
+  printf '"dockerfile_sha256":"%s",' "$dockerfile_sha256"
+  printf '"inventory_helper_sha256":"%s",' "$inventory_helper_sha256"
+  printf '"ir_auxiliary_names_sha256":"%s",' "$ir_auxiliary_names_sha256"
+  printf '"parent_image":"autolean/mathlib-worker@sha256:3237192cf627a05367c75d46e61ec9034fefe43a4fd0c06139e38c80358648d6",'
+  printf '"parent_receipt_canonical_sha256":"%s",' "$parent_receipt_sha256"
+  printf '"parent_receipt_file_sha256":"%s",' "$parent_receipt_file_sha256"
+  printf '"profile_id":"library-substrate-v1-model-theory-universal-lk-independent-reproof",'
+  printf '"profile_sha256":"%s",' "$profile_sha256"
+  printf '"query_wrapper_sha256":"%s",' "$query_wrapper_sha256"
+  printf '"receipt_tool_sha256":"%s",' "$receipt_tool_sha256"
+  printf '"runtime_manifest_sha256":"%s",' "$runtime_manifest_sha256"
+  printf '"runtime_source_checksum_manifest_sha256":"%s",' "$runtime_source_checksum_manifest_sha256"
+  printf '"runtime_source_tree_sha256":"%s",' "$runtime_source_tree_sha256"
+  printf '"schema_version":"autolean.library-substrate-image-receipt.v1",'
+  printf '"task_mode":"independent_reproof"'
+  printf '}\n'
+} >"$final/attestations/library-substrate-image-receipt.v1.json"
+chmod 0444 "$final/attestations/"*
+
+test -z "$(find "$final" -name '*.lean' -o -name '*.ilean')"
+(cd "$final" && sha256sum --check --strict --status attestations/runtime-files.sha256)
diff --git a/Prover/worker/library-substrate/autolean-library-substrate-build-receipt b/Prover/worker/library-substrate/autolean-library-substrate-build-receipt
new file mode 100644
index 0000000..04b51dc
--- /dev/null
+++ b/Prover/worker/library-substrate/autolean-library-substrate-build-receipt
@@ -0,0 +1,123 @@
+#!/bin/sh
+set -eu
+
+fail() {
+  printf '%s\n' "autolean-library-substrate-build-receipt: $1" >&2
+  exit 2
+}
+
+[ "$#" -eq 0 ] || fail "no arguments are accepted"
+root=/opt/autolean/library-substrate
+receipt=$root/attestations/library-substrate-image-receipt.v1.json
+manifest=$root/attestations/runtime-manifest.v1.json
+inventory=$root/attestations/declaration-inventory.v1.json
+runtime_files=$root/attestations/runtime-files.sha256
+runtime_sources=$root/attestations/runtime-sources.sha256
+build_input=$root/attestations/build-input.v1.json
+
+for path in "$receipt" "$manifest" "$inventory" "$runtime_files" "$runtime_sources" "$build_input"; do
+  test -f "$path" && test ! -L "$path" || fail "required attestation is unavailable"
+done
+test -z "$(find "$root" ! -type f ! -type d -print -quit)" ||
+  fail "substrate tree contains a non-regular entry"
+test -z "$(find "$root" -name '*.lean' -o -name '*.ilean')" ||
+  fail "substrate tree contains Lean source"
+(cd "$root" && sha256sum --check --strict --status attestations/runtime-files.sha256) ||
+  fail "runtime file checksum mismatch"
+
+json_hash() {
+  field=$1
+  LC_ALL=C sed -n \
+    "s/^.*\"$field\":\"\\([0-9a-f]\\{64\\}\\)\".*$/\\1/p" \
+    "$receipt"
+}
+
+check_hash() {
+  field=$1
+  path=$2
+  expected=$(json_hash "$field")
+  test "${#expected}" -eq 64 || fail "receipt hash field is invalid"
+  actual=$(sha256sum "$path" | awk '{print $1}')
+  test "$actual" = "$expected" || fail "receipt hash does not match runtime content"
+}
+
+check_hash build_input_sha256 "$build_input"
+check_hash declaration_inventory_sha256 "$inventory"
+check_hash runtime_manifest_sha256 "$manifest"
+check_hash compiled_tree_sha256 "$runtime_files"
+check_hash runtime_source_checksum_manifest_sha256 "$runtime_sources"
+check_hash query_wrapper_sha256 \
+  "$root/bin/autolean-library-substrate-independent-query"
+check_hash receipt_tool_sha256 "$root/bin/autolean-library-substrate-build-receipt"
+check_hash parent_receipt_file_sha256 \
+  /opt/autolean/attestations/mathlib-source-build-receipt.v2.json
+
+manifest_hash() {
+  field=$1
+  LC_ALL=C sed -n "s/^.*\"$field\":\"\\([0-9a-f]\\{64\\}\)\".*$/\\1/p" "$manifest"
+}
+runtime_file_record() {
+  module=$1
+  path=$2
+  LC_ALL=C sed -n \
+    "s|^.*\"module\":\"$module\",\"path\":\"$path\",\"sha256\":\"\\([0-9a-f]\\{64\\}\)\",\"size\":\\([0-9]\\+\\)}.*$|\\1 \\2|p" \
+    "$manifest"
+}
+runtime_records=$(
+  LC_ALL=C sed -n 's/^.*"runtime_files":\(\[.*\]\),"runtime_modules".*$/\1/p' "$manifest"
+)
+test -n "$runtime_records" || fail "runtime manifest does not contain OLean records"
+test "$(printf '%s' "$runtime_records" | grep -o '"module":' | wc -l | tr -d ' ')" -eq 3 ||
+  fail "runtime manifest does not contain exactly three OLean records"
+
+core_rel=AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/Core
+semantic_rel=AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/SemanticPrelude
+rule_rel=AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/RulePrelude
+core_record=$(runtime_file_record \
+  AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Core "lib/lean/$core_rel.olean")
+semantic_record=$(runtime_file_record \
+  AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.SemanticPrelude "lib/lean/$semantic_rel.olean")
+rule_record=$(runtime_file_record \
+  AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude "lib/lean/$rule_rel.olean")
+for record in "$core_record" "$semantic_record" "$rule_record"; do
+  set -- $record
+  test "$#" -eq 2 || fail "runtime OLean record schema drifted"
+  case "$1" in *[!0-9a-f]*|"") fail "runtime OLean hash is invalid" ;; esac
+  case "$2" in *[!0-9]*|"") fail "runtime OLean size is invalid" ;; esac
+done
+set -- $core_record
+core_sha=$1
+core_size=$2
+set -- $semantic_record
+semantic_sha=$1
+semantic_size=$2
+set -- $rule_record
+rule_sha=$1
+rule_size=$2
+for relative_and_expected in \
+  "$core_rel.olean:$core_sha:$core_size" \
+  "$semantic_rel.olean:$semantic_sha:$semantic_size" \
+  "$rule_rel.olean:$rule_sha:$rule_size"
+do
+  relative=${relative_and_expected%%:*}
+  remaining=${relative_and_expected#*:}
+  expected_sha=${remaining%%:*}
+  expected_size=${remaining#*:}
+  actual_sha=$(sha256sum "$root/lib/lean/$relative" | awk '{print $1}')
+  actual_size=$(wc -c <"$root/lib/lean/$relative" | tr -d ' ')
+  test "$actual_sha" = "$expected_sha" || fail "runtime OLean bytes differ from manifest"
+  test "$actual_size" = "$expected_size" || fail "runtime OLean bytes differ from manifest"
+done
+expected_runtime_file_sha=$(
+  {
+    printf '%s  lib/lean/%s.olean\n' "$core_sha" "$core_rel"
+    printf '%s  lib/lean/%s.olean\n' "$semantic_sha" "$semantic_rel"
+    printf '%s  lib/lean/%s.olean\n' "$rule_sha" "$rule_rel"
+  } | sha256sum | awk '{print $1}'
+)
+test "$expected_runtime_file_sha" = "$(json_hash compiled_tree_sha256)" ||
+  fail "runtime-files checksum manifest differs from runtime OLean records"
+
+test "$(wc -l <"$receipt" | tr -d ' ')" -eq 1 ||
+  fail "receipt is not a single canonical record"
+cat "$receipt"
diff --git a/Prover/worker/library-substrate/autolean-library-substrate-independent-query b/Prover/worker/library-substrate/autolean-library-substrate-independent-query
new file mode 100644
index 0000000..a3edb6e
--- /dev/null
+++ b/Prover/worker/library-substrate/autolean-library-substrate-independent-query
@@ -0,0 +1,290 @@
+#!/bin/sh
+set -eu
+
+fail() {
+  printf '%s\n' "autolean-library-substrate-independent-query: $1" >&2
+  exit 2
+}
+
+[ "$#" -eq 4 ] || fail "expected the frozen wrapper argument profile"
+[ "$1" = "--phase" ] || fail "missing phase argument"
+phase=$2
+[ "$3" = "--target" ] || fail "missing target argument"
+target=$4
+[ "$target" = "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Deriv.closed_sound" ] ||
+  fail "unsupported target declaration"
+
+parent_lean_path=$(cat /opt/autolean/environment/lean-path)
+runtime=/opt/autolean/library-substrate/lib/lean
+lean_path="$runtime:$parent_lean_path"
+scratch=$(mktemp -d /tmp/autolean-library-substrate-query.XXXXXX)
+trap 'rm -rf "$scratch"' EXIT HUP INT TERM
+
+case "$phase" in
+  compile)
+    test -f /input/Candidate.lean && test ! -L /input/Candidate.lean ||
+      fail "candidate source is unavailable"
+    test -d /output && test ! -L /output ||
+      fail "compiler output is unavailable"
+    LEAN_PATH="$lean_path" lean -R /input \
+      -o /output/Candidate.olean /input/Candidate.lean
+    ;;
+  query)
+    test -f /compiled/Candidate.olean && test ! -L /compiled/Candidate.olean ||
+      fail "sealed Candidate.olean is unavailable"
+    cat >"$scratch/Query.lean" <<'LEAN'
+import Candidate
+import Lean.Compiler.IR.CompilerM
+import Lean.PrettyPrinter
+import Lean.Util.CollectAxioms
+import Lean.Util.FoldConsts
+
+open Lean
+
+private def runtimeModules : Array (Name × System.FilePath) := #[
+  (`AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Core,
+    "/opt/autolean/library-substrate/lib/lean/AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/Core.olean"),
+  (`AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.SemanticPrelude,
+    "/opt/autolean/library-substrate/lib/lean/AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/SemanticPrelude.olean"),
+  (`AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.RulePrelude,
+    "/opt/autolean/library-substrate/lib/lean/AutoLeanLibrary/Fixtures/ModelTheory/UniversalLK/RulePrelude.olean")
+]
+
+private def canonicalOptions : Options :=
+  ((((({} : Options).setBool `pp.all true).setBool `pp.explicit true).setBool
+        `pp.universes true).setBool `pp.notation false).set `pp.width (1000000 : Nat)
+
+private def sortedNames (names : Array Name) : Array Name :=
+  names.qsort fun left right => left.toString < right.toString
+
+private def uniqueSortedNames (names : Array Name) : Array Name := Id.run do
+  let mut seen : NameSet := {}
+  let mut result := #[]
+  for name in sortedNames names do
+    unless seen.contains name do
+      seen := seen.insert name
+      result := result.push name
+  return result
+
+private def namesJson (names : Array Name) : Json :=
+  Json.arr <| names.map fun name => Json.str name.toString
+
+private def canonicalType (environment : Environment) (info : ConstantInfo) : IO String := do
+  if info.type.hasMVar then
+    throw <| IO.userError s!"declaration type contains a metavariable: {info.name}"
+  let rendered :=
+    (← PrettyPrinter.ppExprLegacy environment {} {} canonicalOptions info.type).pretty 1000000
+  if rendered.isEmpty || rendered.length > 1000000 then
+    throw <| IO.userError s!"canonical type has invalid size: {info.name}"
+  if rendered.any fun char => char == '\x00' || char == '\n' || char == '\r' then
+    throw <| IO.userError s!"canonical type is not one line: {info.name}"
+  return rendered
+
+private def observedAxioms (environment : Environment) (name : Name) : IO (Array Name) := do
+  let context : Core.Context := {
+    fileName := "<AutoLeanLibrarySubstrateIndependentQuery>"
+    fileMap := default
+    options := canonicalOptions
+  }
+  let state : Core.State := { env := environment }
+  let axioms ← Core.CoreM.toIO' (collectAxioms name) context state
+  return sortedNames axioms
+
+private def constantKind : ConstantInfo → String
+  | .axiomInfo _ => "axiom"
+  | .defnInfo _ => "definition"
+  | .thmInfo _ => "theorem"
+  | .opaqueInfo _ => "opaque"
+  | .quotInfo _ => "quotient"
+  | .inductInfo _ => "inductive"
+  | .ctorInfo _ => "constructor"
+  | .recInfo _ => "recursor"
+
+private def originModule (environment : Environment) (name : Name) : IO Name := do
+  let some index := environment.getModuleIdxFor? name
+    | throw <| IO.userError s!"imported declaration has no module mapping: {name}"
+  let some moduleName := environment.header.moduleNames[index.toNat]?
+    | throw <| IO.userError s!"module index is outside the loaded header: {name}"
+  return moduleName
+
+private def runtimeInventory (environment : Environment) : IO (Array Json) := do
+  let mut records : Array (String × Json) := #[]
+  let mut seen : NameSet := {}
+  for (expectedOrigin, path) in runtimeModules do
+    let (moduleData, _) ← readModuleData path
+    for name in moduleData.constNames do
+      if name.toString.startsWith "AutoLeanLibrary." then
+        if seen.contains name then
+          throw <| IO.userError s!"duplicate runtime declaration: {name}"
+        seen := seen.insert name
+        let some info := environment.checked.get.find? name
+          | throw <| IO.userError s!"runtime declaration has no ConstantInfo: {name}"
+        let origin ← originModule environment name
+        if origin != expectedOrigin then
+          throw <| IO.userError s!"runtime declaration origin mismatch: {name}"
+        records := records.push (name.toString, Json.mkObj [
+          ("canonical_type", Json.str (← canonicalType environment info)),
+          ("declaration_kind", Json.str (constantKind info)),
+          ("name", Json.str name.toString),
+          ("observed_axioms", namesJson (← observedAxioms environment name)),
+          ("origin_module", Json.str origin.toString)
+        ])
+  records := records.qsort fun left right => left.1 < right.1
+  return records.map (·.2)
+
+private def runtimeIrAuxiliaryNames (environment : Environment) : IO (Array Json) := do
+  let mut records : Array (String × Json) := #[]
+  let mut seen : NameSet := {}
+  for (expectedOrigin, path) in runtimeModules do
+    let (moduleData, _) ← readModuleData path
+    for name in moduleData.extraConstNames do
+      if seen.contains name then
+        throw <| IO.userError s!"duplicate IR auxiliary name: {name}"
+      seen := seen.insert name
+      if (environment.checked.get.find? name).isSome then
+        throw <| IO.userError s!"IR auxiliary overlaps a kernel declaration: {name}"
+      let some declaration := Lean.IR.findEnvDecl environment name
+        | throw <| IO.userError s!"IR auxiliary has no IR declaration: {name}"
+      if declaration.name != name then
+        throw <| IO.userError s!"IR auxiliary declaration name mismatch: {name}"
+      let declarationKind :=
+        match declaration with
+        | .fdecl .. => "fdecl"
+        | .extern .. => "extern"
+      let origin ← originModule environment name
+      if origin != expectedOrigin then
+        throw <| IO.userError s!"IR auxiliary origin mismatch: {name}"
+      records := records.push (name.toString, Json.mkObj [
+        ("ir_decl_kind", Json.str declarationKind),
+        ("name", Json.str name.toString),
+        ("origin_module", Json.str origin.toString)
+      ])
+  records := records.qsort fun left right => left.1 < right.1
+  return records.map (·.2)
+
+private def targetProof (environment : Environment) (name : Name) : IO Expr := do
+  let some info := environment.checked.get.find? name
+    | throw <| IO.userError s!"target declaration not found: {name}"
+  match info with
+  | .thmInfo value => return value.value
+  | _ => throw <| IO.userError s!"target declaration is not a theorem: {name}"
+
+private def query
+    (runtimeManifestSha imageReceiptSha queryWrapperSha profileSha : String) : IO Json := do
+  let environment ← importModules #[{ module := `Candidate }] canonicalOptions
+  let target := `AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.Deriv.closed_sound
+  let (candidate, _) ← readModuleData "/compiled/Candidate.olean"
+  let candidateKernelNames := uniqueSortedNames candidate.constNames
+  let candidateAuxiliaryNames := uniqueSortedNames candidate.extraConstNames
+  if candidateKernelNames.size != candidate.constNames.size ||
+      candidateAuxiliaryNames.size != candidate.extraConstNames.size then
+    throw <| IO.userError "Candidate repeats an owned declaration name"
+  if !candidateKernelNames.any (· == target) then
+    throw <| IO.userError s!"target declaration is not owned by Candidate: {target}"
+  let mut runtimeKernelNames : NameSet := {}
+  let mut runtimeAuxiliaryNames : NameSet := {}
+  for (_, path) in runtimeModules do
+    let (moduleData, _) ← readModuleData path
+    for name in moduleData.constNames do
+      if runtimeKernelNames.contains name || runtimeAuxiliaryNames.contains name then
+        throw <| IO.userError s!"runtime modules repeat an owned name: {name}"
+      runtimeKernelNames := runtimeKernelNames.insert name
+    for name in moduleData.extraConstNames do
+      if runtimeKernelNames.contains name || runtimeAuxiliaryNames.contains name then
+        throw <| IO.userError s!"runtime modules repeat an owned name: {name}"
+      runtimeAuxiliaryNames := runtimeAuxiliaryNames.insert name
+  let mut candidateNames : NameSet := {}
+  for name in candidateKernelNames do
+    if runtimeKernelNames.contains name || runtimeAuxiliaryNames.contains name then
+      throw <| IO.userError s!"Candidate kernel name collides with runtime ownership: {name}"
+    candidateNames := candidateNames.insert name
+    let origin ← originModule environment name
+    if origin != `Candidate then
+      throw <| IO.userError s!"Candidate kernel name has the wrong module origin: {name}"
+  for name in candidateAuxiliaryNames do
+    if candidateNames.contains name ||
+        runtimeKernelNames.contains name || runtimeAuxiliaryNames.contains name then
+      throw <| IO.userError s!"Candidate IR name collides with sealed ownership: {name}"
+    candidateNames := candidateNames.insert name
+    if (environment.checked.get.find? name).isSome then
+      throw <| IO.userError s!"Candidate IR name overlaps a kernel declaration: {name}"
+    let some declaration := Lean.IR.findEnvDecl environment name
+      | throw <| IO.userError s!"Candidate IR name has no IR declaration: {name}"
+    if declaration.name != name then
+      throw <| IO.userError s!"Candidate IR declaration name mismatch: {name}"
+    let origin ← originModule environment name
+    if origin != `Candidate then
+      throw <| IO.userError s!"Candidate IR name has the wrong module origin: {name}"
+  let some targetInfo := environment.checked.get.find? target
+    | throw <| IO.userError "owned target has no ConstantInfo"
+  let direct := uniqueSortedNames (← targetProof environment target).getUsedConstants
+  let candidateImports := candidate.imports.map (·.module)
+  return Json.mkObj [
+    ("candidate_direct_imports", namesJson (sortedNames candidateImports)),
+    ("candidate_ir_auxiliary_names", namesJson candidateAuxiliaryNames),
+    ("candidate_kernel_names", namesJson candidateKernelNames),
+    ("candidate_namespace_disjoint", Json.bool true),
+    ("candidate_owns_target", Json.bool true),
+    ("canonical_type", Json.str (← canonicalType environment targetInfo)),
+    ("declaration", Json.str target.toString),
+    ("direct_proof_dependencies", namesJson direct),
+    ("loaded_module_closure", namesJson (sortedNames environment.header.moduleNames)),
+    ("observed_axioms", namesJson (← observedAxioms environment target)),
+    ("runtime_declarations", Json.arr (← runtimeInventory environment)),
+    ("runtime_ir_auxiliary_names", Json.arr (← runtimeIrAuxiliaryNames environment)),
+    ("schema_version", Json.str "autolean.library-substrate-independent-query.v1"),
+    ("substrate_identity", Json.mkObj [
+      ("image_receipt_sha256", Json.str imageReceiptSha),
+      ("profile_sha256", Json.str profileSha),
+      ("query_wrapper_sha256", Json.str queryWrapperSha),
+      ("runtime_manifest_sha256", Json.str runtimeManifestSha)
+    ])
+  ]
+
+def main (arguments : List String) : IO UInt32 := do
+  try
+    let [runtimeManifestSha, imageReceiptSha, queryWrapperSha, profileSha] := arguments
+      | throw <| IO.userError "expected the image-owned substrate identity arguments"
+    IO.println
+      (← query runtimeManifestSha imageReceiptSha queryWrapperSha profileSha).compress
+    return (0 : UInt32)
+  catch error =>
+    IO.eprintln s!"autolean-library-substrate-independent-query: {error}"
+    return (2 : UInt32)
+LEAN
+    runtime_manifest_sha256=$(
+      sha256sum \
+        /opt/autolean/library-substrate/attestations/runtime-manifest.v1.json |
+        awk '{print $1}'
+    )
+    image_receipt_sha256=$(
+      sha256sum \
+        /opt/autolean/library-substrate/attestations/library-substrate-image-receipt.v1.json |
+        awk '{print $1}'
+    )
+    query_wrapper_sha256=$(
+      sha256sum \
+        /opt/autolean/library-substrate/bin/autolean-library-substrate-independent-query |
+        awk '{print $1}'
+    )
+    profile_sha256=$(
+      LC_ALL=C sed -n \
+        's/^.*"profile_sha256":"\([0-9a-f]\{64\}\)".*$/\1/p' \
+        /opt/autolean/library-substrate/attestations/build-input.v1.json
+    )
+    for digest in \
+      "$runtime_manifest_sha256" "$image_receipt_sha256" \
+      "$query_wrapper_sha256" "$profile_sha256"
+    do
+      test "${#digest}" -eq 64 || fail "image-owned identity hash is malformed"
+    done
+    LEAN_PATH="/compiled:$lean_path" lean --run "$scratch/Query.lean" \
+      "$runtime_manifest_sha256" \
+      "$image_receipt_sha256" \
+      "$query_wrapper_sha256" \
+      "$profile_sha256"
+    ;;
+  *)
+    fail "unsupported phase"
+    ;;
+esac
diff --git a/docs/README.md b/docs/README.md
index 82b0d7c..ab66f9d 100644
--- a/docs/README.md
+++ b/docs/README.md
@@ -52,6 +52,9 @@ runner reports success.
 17. [Target-free Library substrate](library-substrate-decision.md) separates the focused
     `library-substrate-v1` pilot profile from any future general Mathlib substrate, and defines
     independent versus compositional proof-dependency gates. The
+    [image-owned substrate preflight](library-substrate-image-preflight.md) records the exact
+    child build, typed/IR inventory, sealed-Candidate query, and deliberately missing V2 adapter.
+    The
     [executable proof-dependency spike](proof-dependency-gate-spike.md) records a host-mounted
     source-v2 replay and the remaining image, type, origin, contract, and gateway blockers.
     The [Lean 4.28 module-origin API note](lean-module-origin-spike.md) records the imported
diff --git a/docs/library-substrate-decision.md b/docs/library-substrate-decision.md
index a140dc7..f7f36b6 100644
--- a/docs/library-substrate-decision.md
+++ b/docs/library-substrate-decision.md
@@ -1,6 +1,7 @@
 # Target-Free Library Substrate Decision
 
-Status: accepted Phase 1 architecture; implementation and pilot admission remain open
+Status: accepted Phase 1 architecture; operator-local image preflight verified; pilot admission
+and V2 integration remain open
 
 Decision date: 2026-07-25
 
@@ -41,7 +42,7 @@ presented as the implementation or evidence for the focused Library profile.
 
 | Profile | Immediate purpose | Mathlib scope | Decision state |
 | --- | --- | --- | --- |
-| `library-substrate-v1` | Target-free AutoLean definitions for the first T5/T6 pilot | Reuse the locked `Mathlib.ModelTheory.Semantics` closure | Accepted architecture; not implemented |
+| `library-substrate-v1` | Target-free AutoLean definitions for the first T5/T6 pilot | Reuse the locked `Mathlib.ModelTheory.Semantics` closure | Operator-local image preflight verified; not admitted or V2-integrated |
 | `mathlib-substrate-v1` | Possible general upstream Mathlib basis for later domains | Full default target or reviewed closures, as preflight determines | Deferred; no build choice accepted |
 | external `/deps` V3 | Dynamic accepted AutoLean theorem dependencies across project frontiers | Image-owned Mathlib plus a sealed external capsule | Deferred until the multi-file trigger below |
 
@@ -149,6 +150,11 @@ write only the proof slot, and the final image contains no target module to disc
 Registration must allowlist the new image only after its manifest and build receipt pass the
 release checks.
 
+The implemented preflight query intentionally uses a distinct command and schema. It neither
+occupies the V2 wrapper path nor emits V2 OCI evidence or a gateway receipt. See the
+[image-owned substrate preflight](library-substrate-image-preflight.md) for the exact observed
+digest, receipt boundary, and remaining adapter gate.
+
 ## Required rejection tests
 
 The profile is not usable for a real T5/T6 contract until all of the following fail closed:
diff --git a/docs/library-substrate-image-preflight.md b/docs/library-substrate-image-preflight.md
new file mode 100644
index 0000000..2a93911
--- /dev/null
+++ b/docs/library-substrate-image-preflight.md
@@ -0,0 +1,164 @@
+# Library Substrate Image Preflight
+
+Status: operator-local image-owned preflight verified; not admitted and not V2-integrated
+
+Observed date: 2026-07-25
+
+## Result and authority boundary
+
+The focused `library-substrate-v1` implementation now has one real, offline build and
+independent-reproof canary:
+
+| Evidence | Observed value |
+| --- | --- |
+| Exact parent | `autolean/mathlib-worker@sha256:3237192cf627a05367c75d46e61ec9034fefe43a4fd0c06139e38c80358648d6` |
+| Docker-recorded child RepoDigest | `autolean/library-substrate@sha256:5a71d357ce26e07a44bcce43dc26de06dd8470d2dda5f7341ffdfa2fe9e3dd2e` |
+| Child image ID | `sha256:5a71d357ce26e07a44bcce43dc26de06dd8470d2dda5f7341ffdfa2fe9e3dd2e` |
+| Build-input SHA-256 | `858b1dafb9150e117eb0886fd53cf5d4707b5c42880e5374ebab7c9a94066883` |
+| Raw child receipt SHA-256 | `02f7fd99edbc29f817e2f87477fb6f4b69364b160a5659e5b2ccb8eab8e59fa9` |
+| Runtime-manifest SHA-256 | `923914c53d499eb21d405035ecc0df7ee145eda570bd476b799c7011ba287817` |
+| Runtime-source checksum-manifest SHA-256 | `e6638ec0117dcb0b700e695b760bb32c87bb7290b38ed98329d158e92e2ed2f3` |
+| Query-wrapper SHA-256 | `f1c09f0002af1b0729305534433286659e4af343c78a01b2d9873b368348d8d3` |
+| Runtime closure | 3 Library `.olean` files, 77 typed AutoLean declarations, 22 IR auxiliaries |
+
+The RepoDigest above came from Docker's `RepoDigests` inspection field. The runner refuses to
+invent a `repo@sha256:...` reference from an image ID. This is local technical evidence only:
+the image has not been pushed to a registry, signed by the production verifier authority,
+admitted into a frozen contract, or exercised through the OCI V2 evidence and signing gateway.
+
+## Exact build boundary
+
+[`library_substrate_image.py`](../Library/scripts/library_substrate_image.py) creates a fresh,
+exact build context. It contains:
+
+- the child Dockerfile and one canonical build-input record;
+- four image-owned helper assets; and
+- exactly the `Core`, `SemanticPrelude`, and `RulePrelude` Library sources selected by the
+  `independent_reproof` profile.
+
+The build command fixes `--no-cache --pull=false --network=none`; Dockerfile syntax uses only
+the standard builder instructions and does not require a floating Dockerfile frontend. Both stages
+use the exact source-v2 digest. The builder compiles only those three profile modules. The child layer adds
+only their `.olean` files, the build input, inventory/manifest/receipt records, and the two
+image-owned helper programs under `/opt/autolean/library-substrate`.
+
+The three Library runtime module source files and their `.ilean` files are absent from that
+dedicated final tree. This is deliberately not a claim that every parent-image source or every
+piece of Lean text is absent from the whole child image. In particular, the independent query's
+Lean program is embedded in a here-document inside the hashed query wrapper and materialized
+only in a temporary, read-only-container run.
+
+The source-v2 Dockerfile, receipt, and historical `UniversalLK.lean` inputs remain unchanged.
+The fresh context never includes the aggregate module, target modules, controls, Candidate
+source, or any host `/deps` tree.
+
+## Receipt and inventory semantics
+
+The build input lists each of the three source paths, sizes, and SHA-256 values, plus the
+canonical source-record tree hash. Staging writes an exact `runtime-sources.sha256` checksum
+manifest. The image build verifies that manifest with `sha256sum --check`, rechecks every staged
+source hash and size against the build input, and recomputes the tree hash before compiling. The
+source-manifest hash is carried by a build argument, build input, runtime manifest, and image
+receipt. The host verifier retrieves the image-owned build input and source manifest from the
+fixed Docker RepoDigest, then independently rereads the current three profile sources and
+recomputes all per-file hashes, sizes, manifest bytes, and the tree hash. A source change between
+input capture and context staging is therefore rejected instead of silently changing compilation.
+
+`runtime-files.sha256` has a separate role: it is the exact three-line checksum manifest for the
+final `.olean` files. The image-owned receipt command validates it, parses the runtime manifest,
+and recomputes the hash and size of each fixed runtime path before emitting the receipt. The host
+verifier repeats those hash and size calculations from the fixed Docker RepoDigest, reconstructs
+the checksum-manifest bytes, and requires the reconstructed hash to agree with both runtime
+manifest and receipt. Typed and IR inventory origins are accepted only after this actual-file
+closure; a fresh query that omits the origin `.olean` hash is supplemented only from that closed
+fact.
+
+The child binds two distinct observations of the parent receipt:
+
+- `parent_receipt_file_sha256` is the hash of the exact in-image receipt file bytes:
+  `ce2a2a6f0dbaf7eb8e873ec952ee5ee04bbd8d5cafe214bac08fa8c114c3e356`;
+- `parent_receipt_canonical_sha256` is the host-derived hash of the parsed record rendered as
+  canonical JSON:
+  `40e15776cec80a03b9d5b0affd59a3f613b7f1855c48aa0c1e91f24ec0e1eed7`.
+
+The image-owned receipt command emits the raw child receipt file, and its reported receipt hash
+binds those bytes. Canonical record hashes reported by the host are derived comparisons; they
+are not represented as a second hash implicitly bound by the same raw byte stream.
+
+For each typed AutoLean declaration, the inventory records its name, declaration kind,
+canonical type and type hash, observed axioms, imported module name, and origin `.olean` hash.
+`ModuleIdx` is used only to resolve the module name and is never treated as stable identity.
+
+Lean's module data also lists code-generation/IR auxiliaries in `extraConstNames`. These names
+are intentionally absent from kernel `ConstantInfo`; suffix-based filtering would be incorrect.
+The preflight records every one in a separate, sorted `ir_auxiliary_names` inventory and requires:
+
+- no overlap with any kernel declaration or reserved target/module identity;
+- a matching `Lean.IR.findEnvDecl` entry whose declaration name is exact;
+- an `fdecl` or `extern` IR declaration kind;
+- exact imported-module origin and origin `.olean` hash; and
+- global uniqueness plus a receipt-bound aggregate hash.
+
+The image canary regenerates both inventories from the runtime `.olean` files and requires exact
+replay against the manifest.
+
+The content receipts above are replayable for the observed image. Two measured no-cache builds
+produced different image identities (`bb271a4362f4b3a7fc7e858f9d8349790cbdf8191a53085c95e3d9b1fa860903`
+and the recorded final digest above), while their build input, both checksum manifests, runtime
+manifest, raw receipt, and all three `.olean` hashes matched. This is not a claim that two Docker
+builds are byte-identical or will always have the same content: Docker image/config metadata can
+vary between builds. Every verify or canary invocation therefore requires the specific
+Docker-recorded RepoDigest it is evaluating.
+
+## Independent Candidate query
+
+The image-owned query compiles the fixed independent Candidate in one container, copies only the
+resulting regular `Candidate.olean` into a separately sealed read-only mount, and queries it in a
+fresh container. The query proves that:
+
+- the target is owned by sealed `Candidate.olean`, not imported from the runtime;
+- Candidate kernel and IR-owned names are mutually unique and disjoint from the complete runtime
+  kernel-plus-IR ownership sets;
+- Candidate IR auxiliaries have real IR declarations and `Candidate` module origin;
+- direct imports and the loaded closure match the independent profile;
+- the target canonical type and observed axioms match the historical diagnostic;
+- the proof expression does not directly use `Deriv.sound`; and
+- the query is bound to the runtime manifest, raw image receipt, query wrapper, and profile hash.
+
+The helper lives at
+`/opt/autolean/library-substrate/bin/autolean-library-substrate-independent-query`. It does not
+occupy `/opt/autolean/bin/autolean-lean-wrapper`, does not implement
+`autolean.oci-lean-wrapper.v2`, and is not a drop-in `OciLeanRunner` adapter. It emits neither V2
+OCI evidence nor a gateway receipt. A separate integration change must adapt this verified
+runtime/query boundary to the existing V2 compile/query and evidence protocol.
+
+## Operator commands
+
+From the repository root:
+
+```text
+uv run --frozen python -m Library.scripts.library_substrate_image build
+uv run --frozen python -m Library.scripts.library_substrate_image verify --image <recorded-repodigest>
+uv run --frozen python -m Library.scripts.library_substrate_image canary --image <recorded-repodigest>
+uv run --frozen python -m Library.scripts.library_substrate_image all
+```
+
+Windows delegates the Docker work to WSL `Ubuntu-24.04`; Linux runs it natively. `verify` and
+`canary` require the exact Docker-recorded child RepoDigest.
+
+Focused negative tests cover context leakage, missing offline flags, fabricated child references,
+source-to-context TOCTOU, source checksum-manifest drift, synchronized runtime
+manifest/inventory/checksum forgery against unchanged actual `.olean` bytes, typed/IR inventory
+drift, invalid IR kind and origin, kernel/IR/target collisions, forbidden pilot theorems, exact
+target-type collision, and accidental V2-wrapper claims.
+
+## Non-claims and next gate
+
+This preflight does not implement a contract, the signing gateway, a provider run, an external
+dependency capsule, formal-asset admission, or T6. It is limited to `independent_reproof`;
+`compositional_bridge` and external `/deps` remain deferred.
+
+The next Prover step is a narrow V2 adapter and adversarial integration suite that carries the
+verified child digest, runtime-manifest identity, task mode, type/origin inventory, Candidate
+ownership, and ordinary-dependency observation through OCI evidence and gateway replay. Builder
+admission and semantic review remain separate prerequisites.
diff --git a/docs/phase-1-progress.md b/docs/phase-1-progress.md
index 72b3c7c..c28a65a 100644
--- a/docs/phase-1-progress.md
+++ b/docs/phase-1-progress.md
@@ -67,7 +67,7 @@ These labels are deliberately non-interchangeable:
 | Imported-declaration module-origin API note | Design note, not replayable evidence | PR #19 documents Lean 4.28's imported-only lookup: an imported `ConstantInfo` may resolve through `getModuleIdxFor?`; a declaration in the current `Candidate` normally yields `none`, so Candidate ownership remains a separate sealed-`ModuleData` check | The early ad hoc probe was not retained and is not evidence. The note supplies no image-owned helper, module-origin observation, collision check, or admission result |
 | Dashboard | Verified, loopback | Projection/API tests, 15 UI tests, production build, controlled-browser desktop/mobile rendering, XSS/display sanitization, stable three-lane graph layout, and task/gap/verification drill-down | Remote mode remains unapproved; current JS bundle has a non-blocking 500 kB chunk warning |
 | Independent Library workspace | Verified, local diagnostic | Pinned Lean 4.28.0 and mathlib `8f9d9cff6bd728b17a24e163c9402775d9e6a365`; WSL/ext4 build of public root plus the three-node DAG fixture passed in 11.3 s | A local Lake build is not a Builder freeze, semantic review, OCI verification, or promotion |
-| Target-free Library substrate | Architecture accepted; split preflight verified only in its stated local scope | The ADR fixes `library-substrate-v1` as a new side-by-side image design. PR #20 adds a target-free staged split and profile-bound diagnostic preflight without changing source-v2/T4 history | No substrate image, content-addressed build receipt, complete closure/module-origin/collision checks, environment revision, frozen bundle, proof-dependency admission gate, or gateway run exists; neither the ADR nor preflight can close T3 or T6 |
+| Target-free Library substrate | Operator-local image preflight verified | The exact source-v2 child build completed offline with Docker-recorded RepoDigest `autolean/library-substrate@sha256:5a71d357ce26e07a44bcce43dc26de06dd8470d2dda5f7341ffdfa2fe9e3dd2e`. Its dedicated runtime tree contains three target-free Library `.olean` files, a receipt-bound inventory of 77 typed declarations and 22 separately validated IR auxiliaries, and an image-owned sealed-Candidate query. The independent canary preserved the historical target type/axioms, rejected `Deriv.sound` as an ordinary dependency, replayed both inventories, and established Candidate/runtime kernel-plus-IR name disjointness. The fixed-digest verifier also recomputed each staged source and final `.olean` hash/size against the receipt-bound checksum manifests | Local preflight only: no registry publication, production signer, frozen contract/environment revision, formal-asset admission, provider run, V2 `OciLeanRunner` adapter/evidence, gateway receipt, or T6 result exists. The query's Lean source is embedded in its hashed wrapper; only the three Library runtime source files are absent from the dedicated final substrate tree. Receipt replay is not a claim that separate Docker builds have identical image metadata or RepoDigest |
 | Builder self-calibration and pilot selection | T3 gap, `not_selected`; review tooling merged | The pinned Library packet includes the kernel-checked `UniversalLK` micro-slice for the classical two-sided `⊥`, `→`, and `∀` fragment: level-indexed formulas, capture-avoiding instantiation, eigenvariable-safe universal rules, local/global soundness, the level-zero sentence bridge, and retained Bool rejection controls. The immutable public-safe V2 decision records the gap; a digest-only attachment covers all nine fine-anchor requirements with ten machine-located spans, and a separate exact-image attachment binds the source-v2 query artifact, all 46 declaration types/axiom sets, and the 2,744-module closure without changing that decision. PR #13 adds a byte-bound, versioned human-review packet and reproducible page-rendering workflow for the two ambiguous page pairs | No independent reviewer response has been accepted. Every fine span remains `machine_located_pending_review`; generating or visually opening the packet is not semantic review. The source-v2 observation still conflicts with the old decision's image/import/strict empty-axiom profile and requires an explicit successor profile plus authenticated admission authority. The fragment has no existential constructors or sequent-level structural rules; it is not frozen or handed to Prover |
 | Model-theory source egress | Enforced, source-specific `local_only` | The current reference manifest, source-rule matrix, and human-review packet all bind `model_egress_policy=local_only` | Exact textbook bytes or rendered pages may not be sent to an external provider or model-backed subagent. This is the current source record's rights/egress decision, not a missing Provider or Harness capability; changing it requires a reviewed manifest/rights revision |
 | Builder reference cache | Verified offline | Five locked source/derived records. The manifest-v2 fifth record is the 437-page `pypdf 6.14.2` extraction of Open Logic Project *Sets, Logic, Computation*, text SHA `6184495568a4487848e747f25385cb4081be1cd87f77488c9de0046d600cfa6d`; manifest SHA `b947a08ef2455beb77d9481c4cbddc481ec6590f03746fd22affb03dd8b06f91` | Retained only as local reference/provenance material; no human-calibrated pilot statement is recorded and model egress remains forbidden |
@@ -112,7 +112,7 @@ permits an RC.
 | Pilot self-calibration | T3 gap, blocked | V2 records `gap/not_selected` and remains unchanged. Complete local review of the ten machine-located spans, resolve the Section 7.5 and universal-right (`∀R`) locator ambiguity, decide a successor formal profile consistent with the exact image/import/axiom observation, and close semantic-review and admission-authority checks. The two audited backups are not selected, so a different backup requires its own audit |
 | Pinned Library selection spike | Partial passed with gap | The universal fragment is kernel-checked, but local replay does not select it or establish source fidelity |
 | First calibrated contract slice (T5) | Blocked by T3 | A different backup may be audited, but no statement may freeze until one boundary is admitted with rights and review readiness |
-| Target-free substrate and dependency gate (T6) | Preflight only, blocked by T5 | The split/profile diagnostic is useful implementation input, but T6 still needs a new image and content-addressed receipt, full closure, imported-origin and collision checks, immutable contract, OCI evidence, and gateway replay |
+| Target-free substrate and dependency gate (T6) | Image-owned preflight verified; blocked by T5 and integration | The focused child image now binds its parent/build/runtime receipts, complete typed and IR-owned declaration inventories, imported origins, collision checks, sealed Candidate ownership, and independent ordinary-dependency observation. T6 still needs an admitted immutable contract/environment revision, the V2 `OciLeanRunner` adapter and evidence, signing-gateway replay, adversarial integration rejections, and an accepted frozen-to-verified result |
 | Real project-scale loop (T7) | Input preflight only | The synthetic scheduling fixture and real Lean content fixture are both retained, but acceptance still needs changed-source rebuild, lease/bundle flow, clean integration, and per-node verification evidence |
 | Authoritative Prover path | Partially verified | One unchanged source-backed synthetic bundle passed the full local pure-Lean path through real OCI, an independent gateway rerun, and terminal acceptance. Preserve that contract while extending the same path to the exact mathlib profile and closing production-authority and full adversarial-suite gaps |
 | Controlled model/benchmark evaluation | Blocked before egress | External execution authorization and production evaluators must exist before requesting an API secret. Once ready, fixed suites and ablations remain secondary diagnostics; no FATE result closes a Builder or Library gate |
diff --git a/scripts/tests/test_library_substrate_image.py b/scripts/tests/test_library_substrate_image.py
new file mode 100644
index 0000000..0fc1701
--- /dev/null
+++ b/scripts/tests/test_library_substrate_image.py
@@ -0,0 +1,374 @@
+from __future__ import annotations
+
+import copy
+from pathlib import Path
+from typing import cast
+
+import pytest
+
+from Library.scripts import library_substrate_image as substrate
+from Library.scripts.verify_substrate_fixture import (
+    EXPECTED_MATHLIB_REVISION,
+    EXPECTED_PROFILE_IDS,
+    FIXTURE_ROOT,
+    MODULE_BY_NAME,
+    SOUND_DECLARATION,
+    SOURCE_V2_IMAGE,
+    TARGET_DECLARATION,
+    ValidatedProfileBoundary,
+)
+
+
+def _runtime_files() -> dict[str, dict[str, object]]:
+    return {
+        module: {
+            "module": module,
+            "path": f"lib/lean/{module.replace('.', '/')}.olean",
+            "sha256": character * 64,
+            "size": 100 + index,
+        }
+        for index, (module, character) in enumerate(
+            zip(tuple(MODULE_BY_NAME)[:3], ("a", "b", "c"), strict=True)
+        )
+    }
+
+
+def _kernel_record() -> dict[str, object]:
+    canonical_type = "Nat"
+    return {
+        "canonical_type": canonical_type,
+        "canonical_type_sha256": substrate._sha256_bytes(canonical_type.encode()),
+        "declaration_kind": "definition",
+        "name": "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.fixtureHelper",
+        "observed_axioms": [],
+        "origin_module": next(iter(MODULE_BY_NAME)),
+        "origin_olean_sha256": "a" * 64,
+    }
+
+
+def _auxiliary_record() -> dict[str, object]:
+    return {
+        "ir_decl_kind": "fdecl",
+        "name": "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.fixtureHelper._boxed",
+        "origin_module": next(iter(MODULE_BY_NAME)),
+        "origin_olean_sha256": "a" * 64,
+    }
+
+
+def _manifest_fixture() -> tuple[dict[str, object], dict[str, str]]:
+    files = _runtime_files()
+    declarations = [_kernel_record()]
+    auxiliary = [_auxiliary_record()]
+    auxiliary_sha256 = substrate._sha256_bytes(substrate._canonical_json_compact_bytes(auxiliary))
+    hashes = {
+        "build_input_sha256": "d" * 64,
+        "compiled_tree_sha256": "e" * 64,
+        "declaration_inventory_sha256": "f" * 64,
+        "ir_auxiliary_names_sha256": auxiliary_sha256,
+        "parent_receipt_canonical_sha256": "1" * 64,
+        "parent_receipt_file_sha256": "2" * 64,
+        "profile_sha256": "3" * 64,
+        "runtime_source_checksum_manifest_sha256": "4" * 64,
+        "runtime_source_tree_sha256": "4" * 64,
+    }
+    manifest: dict[str, object] = {
+        **hashes,
+        "declaration_inventory": {
+            "declarations": declarations,
+            "ir_auxiliary_names": auxiliary,
+            "ir_auxiliary_names_sha256": auxiliary_sha256,
+            "schema_version": substrate.DECLARATION_INVENTORY_SCHEMA,
+        },
+        "mathlib_revision": EXPECTED_MATHLIB_REVISION,
+        "parent_image": SOURCE_V2_IMAGE,
+        "profile_id": EXPECTED_PROFILE_IDS["independent_reproof"],
+        "runtime_files": list(files.values()),
+        "runtime_modules": list(tuple(MODULE_BY_NAME)[:3]),
+        "schema_version": substrate.RUNTIME_MANIFEST_SCHEMA,
+        "task_mode": "independent_reproof",
+    }
+    return manifest, hashes
+
+
+def test_stage_build_context_contains_only_runtime_sources(
+    tmp_path: Path, monkeypatch: pytest.MonkeyPatch
+) -> None:
+    modules = tuple(MODULE_BY_NAME)[:3]
+    sources = [
+        {
+            "module": module,
+            "path": MODULE_BY_NAME[module].path.removeprefix("source/"),
+            "role": MODULE_BY_NAME[module].role,
+            "sha256": substrate._sha256(FIXTURE_ROOT / MODULE_BY_NAME[module].path),
+            "size": (FIXTURE_ROOT / MODULE_BY_NAME[module].path).stat().st_size,
+        }
+        for module in modules
+    ]
+    profile = ValidatedProfileBoundary(
+        task_mode="independent_reproof",
+        runtime_modules=modules,
+        forbidden_modules=(),
+        candidate_path="candidates/independent_reproof/Candidate.lean",
+    )
+    assets = substrate._asset_hashes()
+    source_tree_sha256 = substrate._sha256_bytes(substrate._canonical_json_bytes(sources))
+    source_checksums = substrate._checksum_manifest_bytes(sources, path_prefix="source/")
+    build_input: dict[str, object] = {
+        "parent_receipt_canonical_sha256": "1" * 64,
+        "parent_receipt_file_sha256": "2" * 64,
+        "runtime_source_checksum_manifest_sha256": substrate._sha256_bytes(source_checksums),
+        "runtime_source_tree_sha256": source_tree_sha256,
+        "runtime_sources": sources,
+    }
+    monkeypatch.setattr(
+        substrate,
+        "_build_input",
+        lambda: (
+            build_input,
+            substrate._canonical_json_bytes(build_input),
+            profile,
+            assets,
+            source_tree_sha256,
+        ),
+    )
+
+    prepared, arguments = substrate.stage_build_context(tmp_path / "context")
+
+    inventory = cast(dict[str, str], prepared["context_inventory"])
+    assert len(inventory) == 10
+    assert set(path for path in inventory if path.endswith(".lean")) == {
+        "helpers/AutoleanLibrarySubstrateInventory.lean",
+        *(f"source/{cast(str, source['path'])}" for source in sources),
+    }
+    assert not any(
+        token in path
+        for path in inventory
+        for token in ("Candidate.lean", "/Targets/", "Controls.lean", "UniversalLK.lean")
+    )
+    assert arguments["PARENT_RECEIPT_CANONICAL_SHA256"] == "1" * 64
+    assert arguments["PARENT_RECEIPT_FILE_SHA256"] == "2" * 64
+    assert arguments["RUNTIME_SOURCE_CHECKSUM_MANIFEST_SHA256"] == substrate._sha256_bytes(
+        source_checksums
+    )
+
+
+def test_stage_build_context_rejects_source_to_context_toctou(
+    tmp_path: Path, monkeypatch: pytest.MonkeyPatch
+) -> None:
+    modules = tuple(MODULE_BY_NAME)[:3]
+    sources, source_tree_sha256 = substrate._runtime_source_records(
+        ValidatedProfileBoundary(
+            task_mode="independent_reproof",
+            runtime_modules=modules,
+            forbidden_modules=(),
+            candidate_path="candidates/independent_reproof/Candidate.lean",
+        )
+    )
+    source_checksums = substrate._checksum_manifest_bytes(sources, path_prefix="source/")
+    profile = ValidatedProfileBoundary(
+        task_mode="independent_reproof",
+        runtime_modules=modules,
+        forbidden_modules=(),
+        candidate_path="candidates/independent_reproof/Candidate.lean",
+    )
+    build_input: dict[str, object] = {
+        "parent_receipt_canonical_sha256": "1" * 64,
+        "parent_receipt_file_sha256": "2" * 64,
+        "runtime_source_checksum_manifest_sha256": substrate._sha256_bytes(source_checksums),
+        "runtime_source_tree_sha256": source_tree_sha256,
+        "runtime_sources": sources,
+    }
+    monkeypatch.setattr(
+        substrate,
+        "_build_input",
+        lambda: (
+            build_input,
+            substrate._canonical_json_bytes(build_input),
+            profile,
+            substrate._asset_hashes(),
+            source_tree_sha256,
+        ),
+    )
+    copy_regular = substrate._copy_regular
+
+    def drift_after_copy(source: Path, destination: Path, *, executable: bool = False) -> None:
+        copy_regular(source, destination, executable=executable)
+        if destination.name == "Core.lean" and "source" in destination.parts:
+            destination.chmod(0o644)
+            destination.write_bytes(b"TOCTOU source replacement\n")
+
+    monkeypatch.setattr(substrate, "_copy_regular", drift_after_copy)
+    with pytest.raises(substrate.SubstrateImageError, match="actual staged source bytes"):
+        substrate.stage_build_context(tmp_path / "context")
+
+
+def test_build_command_has_frozen_offline_flags(tmp_path: Path) -> None:
+    command = substrate._build_command(
+        tmp_path,
+        {
+            "BUILD_INPUT_SHA256": "a" * 64,
+            "PARENT_RECEIPT_CANONICAL_SHA256": "b" * 64,
+        },
+    )
+
+    assert command[:7] == [
+        "docker",
+        "build",
+        "--no-cache",
+        "--pull=false",
+        "--network=none",
+        "--file",
+        "Dockerfile.library-substrate",
+    ]
+    assert command[-1] == str(tmp_path)
+
+
+def test_child_image_reference_requires_docker_recorded_repo_digest() -> None:
+    digest = "autolean/library-substrate@sha256:" + "a" * 64
+    assert substrate._child_image_reference({"RepoDigests": [digest]}) == digest
+    with pytest.raises(substrate.SubstrateImageError, match="Docker-recorded"):
+        substrate._child_image_reference({"RepoDigests": []})
+    with pytest.raises(substrate.SubstrateImageError, match="Docker-recorded"):
+        substrate._child_image_reference({"RepoDigests": ["autolean/other@sha256:" + "a" * 64]})
+
+
+@pytest.mark.parametrize(
+    "mutation",
+    (
+        "auxiliary-omitted",
+        "auxiliary-origin-drift",
+        "auxiliary-hash-drift",
+        "auxiliary-kernel-collision",
+        "auxiliary-target-collision",
+        "auxiliary-invalid-kind",
+    ),
+)
+def test_ir_auxiliary_inventory_rejects_drift_and_collisions(mutation: str) -> None:
+    files = _runtime_files()
+    record = _auxiliary_record()
+    value: object = [record]
+    include_origin_hash = True
+    kernel_names = frozenset({cast(str, _kernel_record()["name"])})
+    if mutation == "auxiliary-omitted":
+        value = []
+    elif mutation == "auxiliary-origin-drift":
+        record["origin_module"] = "AutoLeanLibrary.NotInRuntime"
+    elif mutation == "auxiliary-hash-drift":
+        record["origin_olean_sha256"] = "9" * 64
+    elif mutation == "auxiliary-kernel-collision":
+        record["name"] = next(iter(kernel_names))
+    elif mutation == "auxiliary-target-collision":
+        record["name"] = TARGET_DECLARATION
+    elif mutation == "auxiliary-invalid-kind":
+        record["ir_decl_kind"] = "boxed"
+    else:
+        raise AssertionError(mutation)
+
+    with pytest.raises(substrate.SubstrateImageError):
+        substrate._validate_ir_auxiliary_records(
+            value,
+            runtime_files=files,
+            include_origin_hash=include_origin_hash,
+            kernel_names=kernel_names,
+        )
+
+
+def test_manifest_accepts_split_inventory_and_rejects_forbidden_theorems() -> None:
+    manifest, receipt = _manifest_fixture()
+    files, declarations, auxiliary = substrate._validate_manifest(manifest, receipt=receipt)
+    assert len(files) == 3
+    assert [record["name"] for record in declarations] == [
+        "AutoLeanLibrary.Fixtures.ModelTheory.UniversalLK.fixtureHelper"
+    ]
+    assert len(auxiliary) == 1
+
+    for forbidden in (TARGET_DECLARATION, SOUND_DECLARATION):
+        mutated = copy.deepcopy(manifest)
+        inventory = cast(dict[str, object], mutated["declaration_inventory"])
+        records = cast(list[dict[str, object]], inventory["declarations"])
+        records[0]["name"] = forbidden
+        with pytest.raises(substrate.SubstrateImageError, match="forbidden pilot theorem"):
+            substrate._validate_manifest(mutated, receipt=receipt)
+
+
+def test_manifest_rejects_exact_target_type_collision(
+    monkeypatch: pytest.MonkeyPatch,
+) -> None:
+    manifest, receipt = _manifest_fixture()
+    record = cast(
+        list[dict[str, object]],
+        cast(dict[str, object], manifest["declaration_inventory"])["declarations"],
+    )[0]
+    monkeypatch.setattr(
+        substrate,
+        "TARGET_TYPE_SHA256",
+        cast(str, record["canonical_type_sha256"]),
+    )
+
+    with pytest.raises(substrate.SubstrateImageError, match="exact target-type collision"):
+        substrate._validate_manifest(manifest, receipt=receipt)
+
+
+def test_runtime_olean_actual_bytes_reject_synchronized_manifest_and_inventory_forgery(
+    monkeypatch: pytest.MonkeyPatch,
+) -> None:
+    manifest, receipt = _manifest_fixture()
+    original_files = _runtime_files()
+    forged = copy.deepcopy(manifest)
+    forged_receipt = dict(receipt)
+    files = cast(list[dict[str, object]], forged["runtime_files"])
+    files[1]["sha256"] = "9" * 64
+    inventory = cast(dict[str, object], forged["declaration_inventory"])
+    declaration = cast(list[dict[str, object]], inventory["declarations"])[0]
+    second_module = tuple(MODULE_BY_NAME)[1]
+    declaration["origin_module"] = second_module
+    declaration["origin_olean_sha256"] = "9" * 64
+    auxiliary = cast(list[dict[str, object]], inventory["ir_auxiliary_names"])[0]
+    auxiliary["origin_module"] = second_module
+    auxiliary["origin_olean_sha256"] = "9" * 64
+    auxiliary_sha256 = substrate._sha256_bytes(
+        substrate._canonical_json_compact_bytes(
+            cast(list[dict[str, object]], inventory["ir_auxiliary_names"])
+        )
+    )
+    inventory["ir_auxiliary_names_sha256"] = auxiliary_sha256
+    forged["ir_auxiliary_names_sha256"] = auxiliary_sha256
+    forged_receipt["ir_auxiliary_names_sha256"] = auxiliary_sha256
+    forged_checksums = substrate._checksum_manifest_bytes(files)
+    forged_tree_sha256 = substrate._sha256_bytes(forged_checksums)
+    forged["compiled_tree_sha256"] = forged_tree_sha256
+    forged_receipt["compiled_tree_sha256"] = forged_tree_sha256
+    runtime_files, _, _ = substrate._validate_manifest(forged, receipt=forged_receipt)
+
+    monkeypatch.setattr(
+        substrate,
+        "_read_image_text",
+        lambda _image, _path: forged_checksums.decode("ascii"),
+    )
+
+    def actual_metadata(_image: str, path: str, *, label: str) -> tuple[str, int]:
+        relative_path = path.removeprefix("/opt/autolean/library-substrate/")
+        for record in original_files.values():
+            if record["path"] == relative_path:
+                return cast(str, record["sha256"]), cast(int, record["size"])
+        raise AssertionError(label)
+
+    monkeypatch.setattr(substrate, "_image_file_sha256_and_size", actual_metadata)
+    with pytest.raises(substrate.SubstrateImageError, match=r"actual-file closure|bytes differ"):
+        substrate._validate_runtime_file_closure(
+            "autolean/library-substrate@sha256:" + "a" * 64,
+            runtime_files,
+            manifest=forged,
+            receipt=forged_receipt,
+        )
+
+
+def test_query_wrapper_does_not_claim_v2_gateway_compatibility() -> None:
+    wrapper = (substrate.HELPER_ROOT / "autolean-library-substrate-independent-query").read_text(
+        encoding="utf-8"
+    )
+
+    assert "/opt/autolean/bin/autolean-lean-wrapper" not in wrapper
+    assert "autolean.oci-lean-wrapper.v2" not in wrapper
+    assert "runtime_manifest_sha256" in wrapper
+    assert "image_receipt_sha256" in wrapper