diff --git a/.github/workflows/adapter-conformance.yml b/.github/workflows/adapter-conformance.yml
index 78149a3b..1c78163d 100644
--- a/.github/workflows/adapter-conformance.yml
+++ b/.github/workflows/adapter-conformance.yml
@@ -10,9 +10,14 @@ on:
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   sympy-conformance:
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
diff --git a/.github/workflows/adversarial.yml b/.github/workflows/adversarial.yml
index 9846c6ad..6fc78f21 100644
--- a/.github/workflows/adversarial.yml
+++ b/.github/workflows/adversarial.yml
@@ -9,9 +9,14 @@ on:
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   adversarial-seed:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
diff --git a/.github/workflows/assurance-exact-replay.yml b/.github/workflows/assurance-exact-replay.yml
index 5fb36730..15b9f6ce 100644
--- a/.github/workflows/assurance-exact-replay.yml
+++ b/.github/workflows/assurance-exact-replay.yml
@@ -1,4 +1,4 @@
-# Exact-candidate binding / regenerability (no Lake theorem minting).
+# Exact-candidate binding / regenerability. Pinned Lean execution is required by lean.yml.
 name: assurance-exact-replay
 
 on:
@@ -10,9 +10,14 @@ on:
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   assurance-exact-replay:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
@@ -43,11 +48,15 @@ jobs:
           python -m pytest \
             tests/forensic/test_exact_replay_framework.py \
             tests/forensic/test_exact_phase2_plugins.py \
+            tests/forensic/test_rational_exact_kernel_decision.py \
             tests/forensic/test_assurance_policy.py \
             tests/forensic/test_certification_record_v04.py \
             tests/forensic/test_assurance_adversarial_corpus.py \
             -q
 
-      - name: Note Lake E2E status
+      - name: Production exact matrix loader regression
+        run: python -m pytest tests/forensic/test_cr_exact_lean_e2e_loader.py -q
+
+      - name: Cross-gate contract
         run: |
-          echo "::notice title=assurance-exact-replay::Python exact-binding gate green. Lean theorem E2E remains gated by lean.yml; crEligible stays false until offline+tamper+E2E prove a capability."
+          echo "::notice title=assurance-exact-replay::Candidate binding, deterministic generation, policy, CR, and adversarial tests are green here. Every CR-eligible capability must also pass production-generated candidate execution in the required lean workflow (scripts/ci/run_cr_exact_lean_e2e_production.py)."
diff --git a/.github/workflows/benchmarks.yml b/.github/workflows/benchmarks.yml
index f421ad09..3259dbcf 100644
--- a/.github/workflows/benchmarks.yml
+++ b/.github/workflows/benchmarks.yml
@@ -22,6 +22,12 @@ on:
       - "scripts/run_ideal_membership_benchmark.py"
       - "scripts/smoke_ideal_membership.py"
       - "scripts/generate_exact_ideal_replay_module.py"
+      - "scripts/ci/run_cr_exact_lean_e2e.py"
+      - "scripts/ci/run_cr_exact_lean_e2e_production.py"
+      - "tests/forensic/test_ideal_benchmark_scoring.py"
+      - "registry/maturity-inventory.json"
+      - "registry/capabilities/**"
+      - "adapters/common/exact_replay/**"
       - "MathEvidence/Checkers/IdealMembership/**"
       - "MathEvidence/Core/ExprSerialize.lean"
       - "MathEvidence/Exe/DeclarationIdentity.lean"
@@ -30,14 +36,21 @@ on:
       - "adapters/common/environment_lock.py"
       - "agent/api/receipt.py"
       - ".github/workflows/benchmarks.yml"
+      - ".github/workflows/lean.yml"
+      - ".github/workflows/release.yml"
 
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   # Mathematical/task benchmark behavior (not assurance policy).
   benchmark-task-suite:
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
@@ -69,6 +82,42 @@ jobs:
           uv sync --frozen --extra dev --extra sympy
           echo "$PWD/.venv/bin" >> "$GITHUB_PATH"
 
+      - name: Ideal-membership scoring trust regression
+        run: python -m pytest tests/forensic/test_ideal_benchmark_scoring.py -q
+
+      - name: Ideal-membership frozen 55-task corpus (candidate/checker tier)
+        env:
+          MATHEVIDENCE_IDEAL_BACKEND: sympy
+        run: |
+          set -euo pipefail
+          python scripts/run_ideal_membership_benchmark.py --tier candidate | tee /tmp/ideal-candidate.json
+          python - <<'PY'
+          import json
+          from pathlib import Path
+
+          p = json.loads(Path("/tmp/ideal-candidate.json").read_text(encoding="utf-8"))
+          manifest = json.loads(
+              Path("benchmarks/ideal_membership/manifest.json").read_text(encoding="utf-8")
+          )
+          expected_scored = int(manifest["passTasks"]) + int(manifest["xfailTasks"])
+          assert p.get("tier") == "candidate", p.get("tier")
+          assert p.get("taskCount") == manifest.get("taskCount"), (p.get("taskCount"), manifest.get("taskCount"))
+          assert p.get("scoredTasks") == expected_scored, (p.get("scoredTasks"), expected_scored)
+          assert p.get("skipped") == manifest.get("skipTasks"), (p.get("skipped"), manifest.get("skipTasks"))
+          assert p.get("passed") == p.get("scoredTasks"), (p.get("passed"), p.get("scoredTasks"))
+          assert p.get("criticalFalseAcceptCount") == 0, p.get("criticalFalseAcceptTasks")
+          assert not p.get("criticalFalseAcceptTasks"), p.get("criticalFalseAcceptTasks")
+          assert p.get("adapterCheckerDisagreementCount") == 0, p.get("adapterCheckerDisagreementTasks")
+          for task in p.get("tasks") or []:
+              assert (task.get("lean") or {}).get("resultStatus") is None, task.get("id")
+          print(
+              "ideal frozen corpus OK:",
+              p.get("taskCount"),
+              "tasks; scored=", p.get("scoredTasks"),
+              "false_accepts=", p.get("criticalFalseAcceptCount"),
+          )
+          PY
+
       - name: Agent held-out suite
         run: python scripts/run_agent_held_out.py
 
@@ -96,18 +145,24 @@ jobs:
       - name: Tool-selection benchmark
         run: python scripts/run_tool_selection_benchmark.py
 
-  # ME-RV-035 / P0-F: backend-proposed multipliers -> exact Lean theorem ->
-  # Lean.Environment identity -> strict Certification Record.
-  # Failure taxonomy: Lake/setup failures are not benchmark-logic failures.
-  # Benchmark score must never write crEligible (registry remains authority).
+  # Bounded exact theorem subset: backend-proposed multipliers -> exact Lean
+  # theorem -> Lean.Environment identity -> strict Certification Record.
+  # The full 55-task corpus runs separately above. Benchmark score never grants
+  # CR eligibility.
   ideal-release-grade:
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
       - name: Install elan (checksum-pinned release asset)
         run: bash scripts/ci/install-elan-pinned.sh
 
+      - name: Restore pinned Mathlib build cache
+        run: |
+          set -euo pipefail
+          lake exe cache get
+
       - name: Setup Python
         uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5
         with:
@@ -131,26 +186,30 @@ jobs:
           echo "::notice title=ideal-release-grade setup::Lake build of exact-replay deps. Failure here is setup/replay, not benchmark scoring."
           lake build MathEvidenceCheckers mathevidence-declaration-identity
 
-      - name: Ideal membership release-grade (exact Certification Record)
+      - name: Ideal membership bounded exact theorem subset
         env:
           MATHEVIDENCE_IDEAL_BENCH_TIER: release
           MATHEVIDENCE_IDEAL_BACKEND: sympy
         run: |
           set -euo pipefail
-          echo "::notice title=ideal-release-grade bench::Benchmark logic + exact CR asserts. Distinct from Lake setup step above."
+          echo "::notice title=ideal-release-grade bench::Bounded exact-CR subset. The full 55-task candidate/checker corpus is a separate job."
           python scripts/run_ideal_membership_benchmark.py --tier release | tee /tmp/ideal-release.json
           python - <<'PY'
           import json
           p = json.load(open("/tmp/ideal-release.json", encoding="utf-8"))
+          tasks = p.get("tasks") or []
+          release_tasks = p.get("releaseCertificationTasks") or []
           assert p.get("tier") == "release", p.get("tier")
+          assert p.get("taskCount") == len(release_tasks) == len(tasks) and len(tasks) > 0
+          assert {t.get("id") for t in tasks} == set(release_tasks)
           assert p.get("passed") == p.get("scoredTasks") and p.get("scoredTasks", 0) > 0
+          assert p.get("criticalFalseAcceptCount") == 0, p.get("criticalFalseAcceptTasks")
           assert "OfflineFixtures" not in (p.get("scoringRule") or "")
-          for t in p.get("tasks") or []:
+          for t in tasks:
               lean = t.get("lean") or {}
               assert lean.get("resultStatus") == "soundness_verified", (t.get("id"), lean)
               assert lean.get("certificationRecordDigest"), t.get("id")
               assert lean.get("identityAuthority") == "Lean.Environment ConstantInfo", lean
-          # Benchmark must not claim registry crEligible flips.
           assert "crEligible" not in p
-          print("ideal exact release-grade OK:", p.get("passed"), "Certification Records")
-          PY
\ No newline at end of file
+          print("ideal bounded exact subset OK:", p.get("passed"), "Certification Records")
+          PY
diff --git a/.github/workflows/lean-assurance-audit.yml b/.github/workflows/lean-assurance-audit.yml
index 3704d12a..d1124d1e 100644
--- a/.github/workflows/lean-assurance-audit.yml
+++ b/.github/workflows/lean-assurance-audit.yml
@@ -12,9 +12,14 @@ on:
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   lean-assurance-audit:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
@@ -56,7 +61,7 @@ jobs:
             --ignore=tests/forensic/test_wave2_kernel_replay.py \
             --ignore=tests/forensic/test_verify_bundle_no_theorem_status.py \
             --ignore=tests/forensic/test_theorem_producing_replay.py
-        # Lake-dependent E2E files stay in lean.yml. This gate distinguishes
+        # Lake-dependent E2E files stay in lean.yml.
         # Keep Python assurance independent of Lean setup failures.
 
       - name: Note
diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml
index c0b5c6bc..f9da127c 100644
--- a/.github/workflows/lean.yml
+++ b/.github/workflows/lean.yml
@@ -1,4 +1,4 @@
-# Lake build, import boundaries, sorry/axiom audit.
+# Lake build, exact-candidate execution, import boundaries, and sorry/axiom audit.
 name: lean
 
 on:
@@ -9,14 +9,43 @@ on:
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   lean:
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
-      - name: Install elan (checksum-pinned release asset)
-        run: bash scripts/ci/install-elan-pinned.sh
+      - name: Install checksum-pinned Lean 4.14.0 release asset
+        run: bash scripts/ci/install-lean-pinned.sh
+
+      - name: Restore pinned Mathlib build cache
+        run: |
+          set -euo pipefail
+
+          retry_network() {
+            local attempt
+            for attempt in 1 2 3; do
+              if "$@"; then
+                return 0
+              fi
+              if [ "$attempt" -eq 3 ]; then
+                echo "network cache command failed after ${attempt} attempts: $*" >&2
+                return 1
+              fi
+              sleep_seconds=$((5 * (2 ** (attempt - 1))))
+              echo "network cache attempt ${attempt} failed; retrying in ${sleep_seconds}s: $*" >&2
+              sleep "$sleep_seconds"
+            done
+          }
+
+          lean --version
+          lake --version
+          retry_network lake exe cache get
 
       - name: Setup Python
         uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5
@@ -44,15 +73,25 @@ jobs:
       - name: Sorry / axiom audit
         run: python scripts/audit_sorry_axioms.py
 
-      - name: Lake build (verification + declaration identity + audit drivers)
+      - name: Lake build (checker closure + verification + declaration identity + audit drivers)
         run: |
+          set -euo pipefail
+          # Generated exact-candidate modules import capability ReplaySound declarations
+          # directly. Build the complete checker barrel first so every CR-eligible
+          # production E2E import has a materialized .olean before replay.
           lake build \
+            MathEvidenceCheckers \
             mathevidence-verify-bundle \
             mathevidence-kernel-replay \
             mathevidence-declaration-identity \
             mathevidence-import-graph \
             mathevidence-axiom-report
 
+      - name: CR-eligible exact candidate production Lean E2E
+        run: |
+          set -euo pipefail
+          python scripts/ci/run_cr_exact_lean_e2e_production.py | tee /tmp/cr-exact-lean-e2e.jsonl
+
       - name: Environment import/axiom audits (Lean.Environment)
         run: |
           set -euo pipefail
diff --git a/.github/workflows/offline-replay.yml b/.github/workflows/offline-replay.yml
index c07dba3d..d6734bfc 100644
--- a/.github/workflows/offline-replay.yml
+++ b/.github/workflows/offline-replay.yml
@@ -9,9 +9,14 @@ on:
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   offline-replay:
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
@@ -63,6 +68,11 @@ jobs:
       - name: Install elan (checksum-pinned release asset)
         run: bash scripts/ci/install-elan-pinned.sh
 
+      - name: Restore pinned Mathlib build cache
+        run: |
+          set -euo pipefail
+          lake exe cache get
+
       - name: Lean offline replay (checker fixtures + tactic examples)
         env:
           MATHEVIDENCE_ADAPTER_MODE: fixture
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 639d4cfd..3384ee6f 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -1,6 +1,4 @@
-# Release provenance toward signed 0.x experimental prerelease (ME-RV-074).
-# Honest gaps: long-term release key + human prerelease publish approval.
-# See docs/validation/ci/signed_0x_prerelease.md
+# Experimental 0.x release provenance. Stable promotion and production signing remain separate gates.
 name: release
 
 on:
@@ -11,17 +9,26 @@ on:
 
 permissions:
   contents: read
-  id-token: write
+
+concurrency:
+  group: release-${{ github.ref }}
+  cancel-in-progress: false
 
 jobs:
   release-provenance:
     runs-on: ubuntu-latest
+    timeout-minutes: 45
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
       - name: Install elan (checksum-pinned release asset)
         run: bash scripts/ci/install-elan-pinned.sh
 
+      - name: Restore pinned Mathlib build cache
+        run: |
+          set -euo pipefail
+          lake exe cache get
+
       - name: Install uv (SHA-pinned)
         uses: astral-sh/setup-uv@d4b2f3b6ecc6e67c4457f6d3e41ec42d3d0fcb86 # v5.4.2
         with:
@@ -39,30 +46,71 @@ jobs:
           uv sync --frozen --extra dev --extra sympy
           echo "$PWD/.venv/bin" >> "$GITHUB_PATH"
 
-      - name: Validate schemas, registry, audits
+      - name: Validate schemas, registry, maturity, and audits
+        env:
+          MATHEVIDENCE_ENV_AUDIT_OUT_DIR: ${{ runner.temp }}/mathevidence-env-audits
         run: |
+          set -euo pipefail
           python scripts/validate_schemas.py
           python scripts/validate_registry.py
+          python scripts/validate_maturity_inventory.py
           python scripts/check_import_boundaries.py
           python scripts/audit_sorry_axioms.py
           python scripts/scaffold_env_audits.py
+          test -f "$RUNNER_TEMP/mathevidence-env-audits/environment_audit_scaffold.json"
+          test -f "$RUNNER_TEMP/mathevidence-env-audits/import_graph_env.json"
+          test -f "$RUNNER_TEMP/mathevidence-env-audits/axiom_report_env.json"
 
-      - name: Lake build (verify-bundle + kernel-replay + audit drivers)
+      - name: Lake build with lock immutability
         run: |
-          lake build mathevidence-verify-bundle mathevidence-kernel-replay mathevidence-import-graph mathevidence-axiom-report
+          set -euo pipefail
+          cp lake-manifest.json /tmp/lake-manifest.before.json
+          # Exact candidate execution imports capability ReplaySound declarations
+          # directly, so release materializes the complete checker closure first.
+          lake build \
+            MathEvidenceCheckers \
+            mathevidence-verify-bundle \
+            mathevidence-kernel-replay \
+            mathevidence-declaration-identity \
+            mathevidence-import-graph \
+            mathevidence-axiom-report
+          cmp /tmp/lake-manifest.before.json lake-manifest.json
+          git diff --exit-code -- lake-manifest.json lean-toolchain
 
-      - name: Offline replay + exe smoke
+      - name: Production-generated CR exact Lean E2E + declaration identity
+        run: |
+          set -euo pipefail
+          python scripts/ci/run_cr_exact_lean_e2e_production.py | tee /tmp/cr-exact-lean-e2e.jsonl
+
+      - name: Offline bundle replay + tamper + exe smoke
         env:
           MATHEVIDENCE_ADAPTER_MODE: fixture
           MATHEVIDENCE_REQUIRE_EXE_SMOKE: "1"
+          MATHEVIDENCE_OFFLINE: "1"
         run: |
+          set -euo pipefail
           python scripts/offline_replay_python.py
+          python -m pytest tests/forensic/test_offline_exact_replay.py -q
           python scripts/smoke_exe.py
           python scripts/smoke_ideal_membership.py
 
-      - name: Generate provenance + SBOM + digests
+      - name: Assert exact checked-out source tree remained clean
+        run: |
+          set -euo pipefail
+          status="$(git status --porcelain --untracked-files=normal)"
+          if [ -n "$status" ]; then
+            echo "Release checks mutated the non-ignored source tree:" >&2
+            printf '%s\n' "$status" >&2
+            exit 1
+          fi
+
+      - name: Generate exact-tree provenance + SBOM + digests
         run: |
-          mkdir -p dist/provenance dist/sbom dist/signed
+          set -euo pipefail
+          mkdir -p dist/provenance/environment-audits dist/sbom dist/signed
+          cp "$RUNNER_TEMP/mathevidence-env-audits/environment_audit_scaffold.json" dist/provenance/environment-audits/
+          cp "$RUNNER_TEMP/mathevidence-env-audits/import_graph_env.json" dist/provenance/environment-audits/
+          cp "$RUNNER_TEMP/mathevidence-env-audits/axiom_report_env.json" dist/provenance/environment-audits/
           python scripts/generate_release_provenance.py dist/provenance
           test -f dist/provenance/provenance-manifest.json
           python scripts/generate_sbom.py dist/sbom
@@ -73,50 +121,77 @@ jobs:
           )
           python - <<'PY'
           import json
+          import os
           from pathlib import Path
-          m = json.loads(Path("dist/provenance/provenance-manifest.json").read_text(encoding="utf-8"))
+
+          path = Path("dist/provenance/provenance-manifest.json")
+          m = json.loads(path.read_text(encoding="utf-8"))
+          assert m.get("schemaVersion") == "0.2.0"
           assert m.get("leanToolchain"), "missing leanToolchain pin"
-          assert m.get("gitCommit"), "missing gitCommit"
-          assert m.get("gitCommit") != "workspace", "gitCommit must not be workspace"
+          assert m.get("gitCommit") == os.environ.get("GITHUB_SHA"), "release SHA mismatch"
+          assert m.get("gitTree") and m["gitTree"] != "unknown", "missing git tree"
+          assert m.get("gitWorkingTreeCleanAtGeneration") is True, "release provenance generated from dirty source tree"
+          maturity = m.get("maturityInventory") or {}
+          assert str(maturity.get("digest") or "").startswith("sha256:")
+          assert maturity.get("auditedBaselineCommit"), "missing maturity baseline"
+          assert m.get("registryFiles"), "missing registry trust-surface hashes"
+          assert m.get("schemaFiles"), "missing schema trust-surface hashes"
+          assert m.get("workflowFiles"), "missing workflow trust-surface hashes"
+          assert m.get("lockFiles"), "missing lock/toolchain hashes"
           lake = m.get("lake") or {}
           assert lake.get("packages"), "missing lake package pins"
-          print("provenance ok:", m["leanToolchain"], "files=", len(m.get("evidenceAndBenchmarkFiles") or []))
+
+          evidence_rows = m.get("evidenceAndBenchmarkFiles") or []
+          bound_evidence = {row.get("path") for row in evidence_rows}
+          expected_evidence = {
+              file.relative_to(Path.cwd()).as_posix()
+              for root in ("evidence", "benchmarks")
+              for file in (Path.cwd() / root).rglob("*")
+              if file.is_file()
+          }
+          assert bound_evidence == expected_evidence, (
+              "release evidence provenance coverage mismatch",
+              sorted(expected_evidence - bound_evidence)[:20],
+              sorted(bound_evidence - expected_evidence)[:20],
+          )
+
+          audit_dir = Path("dist/provenance/environment-audits")
+          assert (audit_dir / "environment_audit_scaffold.json").is_file()
+          assert (audit_dir / "import_graph_env.json").is_file()
+          assert (audit_dir / "axiom_report_env.json").is_file()
+          print(
+              "provenance ok:",
+              m["gitCommit"],
+              m["gitTree"],
+              "clean=", m["gitWorkingTreeCleanAtGeneration"],
+              "evidence=", len(bound_evidence),
+              "registry=", len(m["registryFiles"]),
+              "schemas=", len(m["schemaFiles"]),
+          )
           PY
 
-      - name: Sign artifacts with cosign (keyless when identity available)
-        env:
-          COSIGN_YES: "true"
+      - name: Record signing status explicitly
         run: |
           set -euo pipefail
-          # Install cosign from a pinned GitHub release when missing.
-          if ! command -v cosign >/dev/null 2>&1; then
-            COSIGN_VERSION=v2.4.3
-            COSIGN_URL="https://github.com/sigstore/cosign/releases/download/${COSIGN_VERSION}/cosign-linux-amd64"
-            curl -fsSL "$COSIGN_URL" -o /tmp/cosign
-            chmod +x /tmp/cosign
-            sudo mv /tmp/cosign /usr/local/bin/cosign
-          fi
-          cosign version
-          # Keyless OIDC signing via GitHub Actions identity token.
-          # This signs digests + SBOM; human publish approval is still required.
-          if [ "${{ github.event_name }}" = "workflow_dispatch" ] || [ "${{ github.event_name }}" = "push" ]; then
-            cosign sign-blob --yes \
-              --bundle dist/signed/artifact-digests.cosign.bundle \
-              dist/provenance/artifact-digests.sha256 \
-              || {
-                echo "::warning title=ME-RV-074::cosign sign-blob soft-failed; digests remain unsigned until identity/key is configured"
-                echo "cosign_soft_fail" > dist/signed/STATUS.txt
-              }
-            if [ -f dist/sbom/sbom.json ]; then
-              cosign sign-blob --yes \
-                --bundle dist/signed/sbom.cosign.bundle \
-                dist/sbom/sbom.json \
-                || echo "::warning title=ME-RV-074::SBOM cosign soft-failed"
-            fi
-          fi
-          if [ ! -f dist/signed/STATUS.txt ]; then
-            echo "cosign_attempted" > dist/signed/STATUS.txt
-          fi
+          cat > dist/signed/STATUS.json <<'JSON'
+          {
+            "schemaVersion": "0.1.0",
+            "signed": false,
+            "status": "production_release_signing_deferred",
+            "note": "This experimental release workflow does not claim a production signature. Configure and independently verify an approved release identity before advertising signed release provenance."
+          }
+          JSON
+
+      - name: Recompute release artifact digests including signing status
+        run: |
+          set -euo pipefail
+          (
+            cd dist
+            find . -type f ! -path './provenance/artifact-digests.sha256' -print0 \
+              | sort -z \
+              | xargs -0 sha256sum \
+              > provenance/artifact-digests.sha256
+          )
 
       - name: Upload release artifacts
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
@@ -129,25 +204,17 @@ jobs:
 
       - name: Experimental prerelease publish gate (manual)
         if: github.event_name == 'workflow_dispatch'
-        env:
-          PUBLISH_PRERELEASE: ${{ vars.PUBLISH_EXPERIMENTAL_PRERELEASE || 'false' }}
         run: |
           set -euo pipefail
-          echo "=== ME-RV-074 experimental 0.x prerelease gate ==="
-          echo "Branch protection on main: ENABLED (required PR + checks)."
-          echo "This job does NOT auto-publish a GitHub Release."
-          echo "Manual steps for a maintainer:"
-          echo "  1. Tag an experimental commit: git tag v0.1.0-experimental.<sha7>"
-          echo "  2. Push the tag OR run workflow_dispatch after checks are green."
-          echo "  3. Download the release-provenance artifact."
-          echo "  4. Verify cosign bundles (keyless) or sign with the org Ed25519 release key:"
-          echo "       cosign verify-blob --bundle dist/signed/artifact-digests.cosign.bundle \\"
-          echo "         dist/provenance/artifact-digests.sha256"
-          echo "  5. Create a GitHub *prerelease* only after human review:"
-          echo "       gh release create <tag> --prerelease --title '0.x experimental' \\"
-          echo "         dist/provenance/* dist/sbom/* dist/signed/*"
-          echo "  6. Set repo variable PUBLISH_EXPERIMENTAL_PRERELEASE=true only when automating step 5."
-          if [ "${PUBLISH_PRERELEASE}" = "true" ]; then
-            echo "::warning::PUBLISH_EXPERIMENTAL_PRERELEASE=true but auto-publish is intentionally not wired; use gh release create."
-          fi
-          echo "release.yml: provenance+SBOM+digests+cosign hooks ready; publish remains human-gated."
+          echo "=== MathEvidence experimental 0.x release gate ==="
+          echo "This workflow does NOT infer or configure GitHub branch protection."
+          echo "Verify live repository rules/settings independently before release."
+          echo "This workflow does NOT auto-publish a GitHub Release."
+          echo "This workflow does NOT claim production release signing."
+          echo "Manual maintainer sequence after all exact-SHA checks are green:"
+          echo "  1. Verify the intended commit SHA and branch/ruleset state."
+          echo "  2. Create an immutable experimental tag on that exact SHA."
+          echo "  3. Run/download this release-provenance artifact for the tag."
+          echo "  4. Verify artifact-digests.sha256 and inspect STATUS.json."
+          echo "  5. Publish a GitHub prerelease only with experimental scope/limitations."
+          echo "Stable promotion and production signing remain separate explicit gates."
diff --git a/.github/workflows/replay-tamper.yml b/.github/workflows/replay-tamper.yml
index 32f0e19f..9d7db7c1 100644
--- a/.github/workflows/replay-tamper.yml
+++ b/.github/workflows/replay-tamper.yml
@@ -10,9 +10,14 @@ on:
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   replay-tamper:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
diff --git a/.github/workflows/security.yml b/.github/workflows/security.yml
index 40e78c4f..9600fc03 100644
--- a/.github/workflows/security.yml
+++ b/.github/workflows/security.yml
@@ -11,9 +11,14 @@ permissions:
   contents: read
   pull-requests: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   security-bounded-execution:
     runs-on: ubuntu-latest
+    timeout-minutes: 20
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
 
diff --git a/.github/workflows/supply-chain.yml b/.github/workflows/supply-chain.yml
index 7749b0ca..0907bc4c 100644
--- a/.github/workflows/supply-chain.yml
+++ b/.github/workflows/supply-chain.yml
@@ -9,9 +9,14 @@ on:
 permissions:
   contents: read
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 jobs:
   gitleaks:
     runs-on: ubuntu-latest
+    timeout-minutes: 10
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
         with:
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 00000000..91253d34
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,40 @@
+# Changelog
+
+All notable changes to the MathEvidence experimental 0.x line are documented here.
+The project remains experimental: this file does not promote any capability to
+`stable` and does not supersede `registry/maturity-inventory.json`.
+
+## [Unreleased]
+
+### Assurance and exact replay
+
+- Rebased theorem-level Certification Record eligibility on exact submitted-candidate binding.
+- Added registry-driven exact replay policy with fail-closed unsupported modes and no exact-to-fixture fallback.
+- Added deterministic typed exact-replay generators for the currently CR-eligible owned capabilities.
+- Added candidate-specific Lean E2E execution as a release gate and coupled its coverage to the maturity inventory and production operation whitelists.
+- Preserved explicit result polarity: finite counterexamples certify `refuted`, not `proved`.
+- Separated deterministic offline bundle replay from offline kernel theorem replay in maturity reporting.
+- Strengthened Certification Record binding to candidate, request, generated source, generator/grammar, verifier identity, toolchain/dependency contracts, and replay provenance.
+
+### Trust and security
+
+- Kept adapters, generators, model outputs, and submitted evidence outside the trusted theorem boundary.
+- Hardened generated replay around typed IR, bounded execution, argv-only process spawning, output/time limits, path controls, and tamper tests.
+- Preserved sorry/axiom/import/declaration-identity audits and prevented fixture substitution from serving as Certification Record authority.
+- Kept benchmark outcomes independent from theorem-level assurance eligibility.
+
+### Reproducibility and release engineering
+
+- Added machine-readable maturity inventory validation and status-document drift checks.
+- Strengthened release provenance to bind the exact repository revision, toolchain/dependency pins, registry/schema trust surface, and release evidence.
+- Added release-oriented citation and reproducibility documentation.
+- Removed temporary audit scratch material from the release tree.
+
+### Scope
+
+The experimental exact-certification surface is intentionally narrow. Consult
+`docs/STATUS.md` and `docs/security/KNOWN_TRUST_GAPS.md` for the proposition
+established by each capability and for unsupported claims. Human stable-promotion,
+external reproduction, independent semantic review, production signing/PKI, and
+other governance gates remain separate unless a later release records completed
+artifacts for them.
diff --git a/CITATION.cff b/CITATION.cff
new file mode 100644
index 00000000..fc909b11
--- /dev/null
+++ b/CITATION.cff
@@ -0,0 +1,24 @@
+cff-version: 1.2.0
+message: "If you use MathEvidence in research, please cite this software and the exact release tag or commit used."
+title: "MathEvidence"
+type: software
+authors:
+  - name: "MathEvidence contributors"
+version: 0.1.0
+repository-code: "https://github.com/fraware/MathEvidence"
+url: "https://github.com/fraware/MathEvidence"
+license: Apache-2.0
+keywords:
+  - formal methods
+  - Lean 4
+  - computational evidence
+  - proof certificates
+  - reproducibility
+  - assurance
+abstract: >-
+  MathEvidence is an experimental computational-evidence platform for Lean 4.
+  Untrusted external adapters may propose candidates or evidence; theorem-level
+  Certification Records are restricted to explicitly supported exact
+  candidate-bound replay paths whose advertised proposition is checked by the
+  declared Lean trust path. Fixture replay, benchmark success, and numerical
+  agreement are not theorem certification.
diff --git a/MathEvidence/Checkers/Calculus/Tests.lean b/MathEvidence/Checkers/Calculus/Tests.lean
index 3cfbc9db..6a55fc90 100644
--- a/MathEvidence/Checkers/Calculus/Tests.lean
+++ b/MathEvidence/Checkers/Calculus/Tests.lean
@@ -53,6 +53,34 @@ def cert_antideriv : Certificate where
   operation := .antiderivativeCandidate
   domainConditions := []
 
+/-- Production-shape antiderivative: `F = (1/2)x^2`, `f = x`.
+
+The exact replay generator receives an already-validated request digest and emits
+that digest literally into both `Request` and `Certificate`.  This fixture uses
+the same representation instead of `Request.ofClaim`, whose digest computation
+is intentionally outside the generated theorem's reduction path.  The canonical
+rational literal `1/2` is structurally well-formed and creates no runtime domain
+condition. -/
+def claim_antideriv_half : Claim where
+  operation := .antiderivativeCandidate
+  varNames := ["x"]
+  independentVar := 0
+  expr := .var 0
+  candidate := .mul (.rat 1 2) (.pow (.var 0) 2)
+  domainConditions := []
+  claimClass := .soundResult
+
+def req_antideriv_half : Request where
+  claim := claim_antideriv_half
+  requestDigest :=
+    ⟨"sha256:1111111111111111111111111111111111111111111111111111111111111111"⟩
+
+def cert_antideriv_half : Certificate where
+  requestDigest :=
+    ⟨"sha256:1111111111111111111111111111111111111111111111111111111111111111"⟩
+  operation := .antiderivativeCandidate
+  domainConditions := []
+
 /-- Closed form `u(n) = n`; recurrence `u(n+1) = u + 1`. -/
 def claim_recurrence : Claim where
   operation := .recurrenceIdentity
@@ -159,6 +187,22 @@ theorem replay_deriv_x2 :
 theorem replay_antideriv :
     checkBool req_antideriv cert_antideriv = true := by native_decide
 
+theorem replay_antideriv_half_kernel :
+    checkBool req_antideriv_half cert_antideriv_half = true := by
+  have hDigest : digestOk req_antideriv_half cert_antideriv_half = true := by
+    native_decide
+  have hWellFormed : wellFormedOk req_antideriv_half = true := by
+    native_decide
+  have hDomain : domainCoverOk req_antideriv_half cert_antideriv_half = true := by
+    native_decide
+  have hOp : opOk req_antideriv_half = true := by
+    simp [opOk, req_antideriv_half, claim_antideriv_half, Claim.opHolds,
+      antiderivativeOk, exprEqual, formalDeriv, polyEqual, differenceNumerator,
+      toFrac, Poly.combineLike, Poly.sub, Poly.add, Poly.neg, Poly.mul, Poly.pow,
+      Poly.one, Poly.C, Poly.X, Poly.mulTerm, Poly.Term.sortVars, Poly.sortNats,
+      Poly.insertSorted]
+  simp [checkBool, hDigest, hWellFormed, hDomain, hOp]
+
 theorem replay_recurrence :
     checkBool req_recurrence cert_recurrence = true := by native_decide
 
@@ -185,6 +229,10 @@ theorem sound_deriv_x2 :
     Claim.proposition claim_deriv_x2 :=
   checkBool_sound req_deriv_x2 cert_deriv_x2 replay_deriv_x2
 
+theorem sound_antideriv_half :
+    Claim.proposition claim_antideriv_half :=
+  checkBool_sound req_antideriv_half cert_antideriv_half replay_antideriv_half_kernel
+
 theorem sound_ode :
     Claim.proposition claim_ode :=
   checkBool_sound req_ode cert_ode replay_ode
diff --git a/MathEvidence/Checkers/RationalEquality/Soundness.lean b/MathEvidence/Checkers/RationalEquality/Soundness.lean
index 5c9e6e7c..88e93296 100644
--- a/MathEvidence/Checkers/RationalEquality/Soundness.lean
+++ b/MathEvidence/Checkers/RationalEquality/Soundness.lean
@@ -11,16 +11,20 @@ namespace MathEvidence.Checkers.RationalEquality
 
 open MathEvidence.IR.RationalExpr
 
+theorem checkBool_wellFormedOk (req : Request) (cert : Certificate)
+    (h : checkBool req cert = true) : wellFormedOk req cert = true := by
+  simp [checkBool, Bool.and_eq_true] at h
+  -- (((((resource ∧ digest) ∧ wellFormed) ∧ factors) ∧ poly) ∧ cover)
+  exact h.1.1.1.2
+
 theorem checkBool_polyOk (req : Request) (cert : Certificate)
     (h : checkBool req cert = true) : polyOk req = true := by
   simp [checkBool, Bool.and_eq_true] at h
-  -- ((digestOk ∧ wellFormedOk) ∧ polyOk) ∧ coverOk
   exact h.1.2
 
 theorem checkBool_coverOk (req : Request) (cert : Certificate)
     (h : checkBool req cert = true) : coverOk req cert = true := by
   simp [checkBool, Bool.and_eq_true] at h
-  -- ((digestOk ∧ wellFormedOk) ∧ polyOk) ∧ coverOk
   exact h.2
 
 private theorem contains_true_iff_mem [DecidableEq α] (xs : List α) (x : α) :
@@ -42,64 +46,82 @@ private theorem factor_defined_nonzero
     Defined env e ∧ ∃ v, eval env e = some v ∧ v ≠ 0 :=
   hconds e (List.mem_append_left known he)
 
+/--
+A well-formed rational expression is defined once every runtime denominator
+introduced by an explicit `div` node is defined and nonzero.  Literal
+rational denominators are discharged by `wellFormed`, not exported as domain
+assumptions.
+-/
 private theorem defined_of_denominators_nonzero
-    (env : Env ℚ) :
+    (env : Env ℚ) (varCount : Nat) :
     (e : Expr) →
+      e.wellFormed varCount = true →
       (∀ d ∈ e.denominators, Defined env d ∧
         ∃ v, eval env d = some v ∧ v ≠ 0) →
       Defined env e := by
-  intro e hdenoms
+  intro e
   induction e with
-  | var _ => trivial
-  | int _ => trivial
+  | var _ =>
+    intro _ _
+    trivial
+  | int _ =>
+    intro _ _
+    trivial
   | rat _ d =>
-    have hz := hdenoms (.int (Int.ofNat d)) (by simp [Expr.denominators])
-    obtain ⟨v, hev, hv⟩ := hz.2
-    have hcast : (d : ℚ) ≠ 0 := by
-      intro hd
-      apply hv
-      simpa [eval, hd] using hev.symm
+    intro hwell _
     have hd : d ≠ 0 := by
-      intro hd0
-      exact hcast (by simp [hd0])
+      simpa [Expr.wellFormed] using hwell
+    have hcast : (d : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr hd
     exact ⟨hd, hcast⟩
   | neg e ih =>
-    exact ih (by
-      intro d hd
-      exact hdenoms d (by simpa [Expr.denominators] using hd))
+    intro hwell hdenoms
+    apply ih
+    · simpa [Expr.wellFormed] using hwell
+    · intro d hd
+      exact hdenoms d (by simpa [Expr.denominators] using hd)
   | add a b iha ihb =>
+    intro hwell hdenoms
+    simp [Expr.wellFormed, Bool.and_eq_true] at hwell
     constructor
-    · exact iha (by
+    · exact iha hwell.1 (by
         intro d hd
         exact hdenoms d (by simp [Expr.denominators, hd]))
-    · exact ihb (by
+    · exact ihb hwell.2 (by
         intro d hd
         exact hdenoms d (by simp [Expr.denominators, hd]))
   | sub a b iha ihb =>
+    intro hwell hdenoms
+    simp [Expr.wellFormed, Bool.and_eq_true] at hwell
     constructor
-    · exact iha (by
+    · exact iha hwell.1 (by
         intro d hd
         exact hdenoms d (by simp [Expr.denominators, hd]))
-    · exact ihb (by
+    · exact ihb hwell.2 (by
         intro d hd
         exact hdenoms d (by simp [Expr.denominators, hd]))
   | mul a b iha ihb =>
+    intro hwell hdenoms
+    simp [Expr.wellFormed, Bool.and_eq_true] at hwell
     constructor
-    · exact iha (by
+    · exact iha hwell.1 (by
         intro d hd
         exact hdenoms d (by simp [Expr.denominators, hd]))
-    · exact ihb (by
+    · exact ihb hwell.2 (by
         intro d hd
         exact hdenoms d (by simp [Expr.denominators, hd]))
   | pow b _ ih =>
-    exact ih (by
-      intro d hd
-      exact hdenoms d (by simpa [Expr.denominators] using hd))
+    intro hwell hdenoms
+    apply ih
+    · simpa [Expr.wellFormed] using hwell
+    · intro d hd
+      exact hdenoms d (by simpa [Expr.denominators] using hd)
   | div n d ihn ihd =>
-    have hn : Defined env n := ihn (by
+    intro hwell hdenoms
+    simp [Expr.wellFormed, Bool.and_eq_true] at hwell
+    have hn : Defined env n := ihn hwell.1 (by
       intro x hx
       exact hdenoms x (by simp [Expr.denominators, hx]))
-    have hd : Defined env d := ihd (by
+    have hd : Defined env d := ihd hwell.2 (by
       intro x hx
       exact hdenoms x (by simp [Expr.denominators, hx]))
     have hd_nonzero := hdenoms d (by simp [Expr.denominators])
@@ -111,12 +133,13 @@ private theorem defined_of_denominators_nonzero
     exact hv hv0
 
 theorem defined_of_denomsCovered
-    (env : Env ℚ) (e : Expr) (factors known : List Expr)
+    (env : Env ℚ) (varCount : Nat) (e : Expr) (factors known : List Expr)
+    (hwell : e.wellFormed varCount = true)
     (hcover : denomsCovered e factors = true)
     (hconds : ∀ f ∈ factors ++ known, Defined env f ∧
       ∃ v, eval env f = some v ∧ v ≠ 0) :
     Defined env e := by
-  apply defined_of_denominators_nonzero env e
+  apply defined_of_denominators_nonzero env varCount e hwell
   intro d hd
   have hcontains : factors.contains d = true := by
     exact List.all_eq_true.mp hcover d hd
@@ -124,31 +147,36 @@ theorem defined_of_denomsCovered
     ((contains_true_iff_mem factors d).1 hcontains)
 
 theorem coverOk_defined_lhs (req : Request) (cert : Certificate) (env : Env ℚ)
+    (hwell : wellFormedOk req cert = true)
     (hcover : coverOk req cert = true)
     (hconds : ∀ f ∈ cert.denomFactors ++ req.claim.knownAssumptions,
       Defined env f ∧ ∃ v, eval env f = some v ∧ v ≠ 0) :
     Defined env req.claim.lhs := by
+  simp [wellFormedOk, Bool.and_eq_true] at hwell
   simp [coverOk, Bool.and_eq_true] at hcover
-  exact defined_of_denomsCovered env req.claim.lhs cert.denomFactors
-    req.claim.knownAssumptions hcover.1 hconds
+  exact defined_of_denomsCovered env req.claim.varNames.length req.claim.lhs
+    cert.denomFactors req.claim.knownAssumptions hwell.1.1 hcover.1 hconds
 
 theorem coverOk_defined_rhs (req : Request) (cert : Certificate) (env : Env ℚ)
+    (hwell : wellFormedOk req cert = true)
     (hcover : coverOk req cert = true)
     (hconds : ∀ f ∈ cert.denomFactors ++ req.claim.knownAssumptions,
       Defined env f ∧ ∃ v, eval env f = some v ∧ v ≠ 0) :
     Defined env req.claim.rhs := by
+  simp [wellFormedOk, Bool.and_eq_true] at hwell
   simp [coverOk, Bool.and_eq_true] at hcover
-  exact defined_of_denomsCovered env req.claim.rhs cert.denomFactors
-    req.claim.knownAssumptions hcover.2 hconds
+  exact defined_of_denomsCovered env req.claim.varNames.length req.claim.rhs
+    cert.denomFactors req.claim.knownAssumptions hwell.1.2 hcover.2 hconds
 
 theorem checkBool_sound (req : Request) (cert : Certificate)
     (h : checkBool req cert = true) :
     Claim.proposition req.claim cert.denomFactors := by
   intro env hconds
+  have hwell : wellFormedOk req cert = true := checkBool_wellFormedOk req cert h
   have hp : polyEqual req.claim.lhs req.claim.rhs = true := checkBool_polyOk req cert h
   have hcover : coverOk req cert = true := checkBool_coverOk req cert h
-  have hl : Defined env req.claim.lhs := coverOk_defined_lhs req cert env hcover hconds
-  have hr : Defined env req.claim.rhs := coverOk_defined_rhs req cert env hcover hconds
+  have hl : Defined env req.claim.lhs := coverOk_defined_lhs req cert env hwell hcover hconds
+  have hr : Defined env req.claim.rhs := coverOk_defined_rhs req cert env hwell hcover hconds
   exact eval_eq_of_polyEqual_defined req.claim.lhs req.claim.rhs env hp hl hr
 
 theorem check_sound (req : Request) (cand : Candidate) (cert : Certificate)
diff --git a/MathEvidence/Checkers/RationalEquality/Tests.lean b/MathEvidence/Checkers/RationalEquality/Tests.lean
index b2477868..f1aad5cb 100644
--- a/MathEvidence/Checkers/RationalEquality/Tests.lean
+++ b/MathEvidence/Checkers/RationalEquality/Tests.lean
@@ -54,6 +54,30 @@ def cert_sub_self : Certificate where
   requestDigest := req_sub_self.requestDigest
   denomFactors := [.var 0]
 
+/-- Canonical rational literals are structural values, not domain assumptions. -/
+def claim_half : Claim where
+  varNames := []
+  lhs := .add (.rat 1 2) (.int 0)
+  rhs := .rat 1 2
+
+def req_half : Request := Request.ofClaim! claim_half
+
+def cert_half : Certificate where
+  requestDigest := req_half.requestDigest
+  denomFactors := []
+
+/-- A zero literal denominator remains malformed through `wellFormed`. -/
+def claim_zero_literal_denom : Claim where
+  varNames := []
+  lhs := .rat 1 0
+  rhs := .int 0
+
+def req_zero_literal_denom : Request := Request.ofClaim! claim_zero_literal_denom
+
+def cert_zero_literal_denom : Certificate where
+  requestDigest := req_zero_literal_denom.requestDigest
+  denomFactors := []
+
 /-- False identity `x = x + 1` must be rejected. -/
 def claim_false : Claim where
   varNames := ["x"]
@@ -85,6 +109,12 @@ theorem replay_cancel :
 theorem replay_sub_self :
     checkBool req_sub_self cert_sub_self = true := by native_decide
 
+theorem replay_half_without_domain_factor :
+    checkBool req_half cert_half = true := by native_decide
+
+theorem reject_zero_literal_denom :
+    checkBool req_zero_literal_denom cert_zero_literal_denom = false := by native_decide
+
 theorem reject_false :
     checkBool req_false cert_false = false := by native_decide
 
@@ -103,4 +133,9 @@ theorem sound_add0 :
     Claim.proposition req_add0.claim cert_add0.denomFactors :=
   checkBool_sound req_add0 cert_add0 replay_add0
 
+/-- Literal definedness is discharged by well-formedness in the soundness proof. -/
+theorem sound_half_without_domain_factor :
+    Claim.proposition req_half.claim cert_half.denomFactors :=
+  checkBool_sound req_half cert_half replay_half_without_domain_factor
+
 end MathEvidence.Checkers.RationalEquality.Tests
diff --git a/MathEvidence/IR/RationalExpr/Syntax.lean b/MathEvidence/IR/RationalExpr/Syntax.lean
index 5a662728..d66569eb 100644
--- a/MathEvidence/IR/RationalExpr/Syntax.lean
+++ b/MathEvidence/IR/RationalExpr/Syntax.lean
@@ -48,10 +48,15 @@ def Expr.wellFormed (varCount : Nat) : Expr → Bool
     a.wellFormed varCount && b.wellFormed varCount
   | .pow b _ => b.wellFormed varCount
 
-/-- Collect denominator subexpressions appearing under `div` (and `rat` dens as ints). -/
+/--
+Collect runtime denominator subexpressions introduced by explicit `div` nodes.
+
+A canonical rational literal `.rat n d` is not a domain condition: `wellFormed`
+already rejects `d = 0`.  RFC 0001 exposes nonzero assumptions for divisions in
+the represented expression, while literal validity is a structural obligation.
+-/
 def Expr.denominators : Expr → List Expr
-  | .var _ | .int _ => []
-  | .rat _ d => [.int (Int.ofNat d)]
+  | .var _ | .int _ | .rat _ _ => []
   | .neg e => e.denominators
   | .add a b | .sub a b | .mul a b => a.denominators ++ b.denominators
   | .pow b _ => b.denominators
diff --git a/README.md b/README.md
index b5667a19..c65233c9 100644
--- a/README.md
+++ b/README.md
@@ -10,7 +10,7 @@
 
 </pre>
   
-<strong>External computation in. Lean theorems out.</strong>
+<strong>External computation in. Explicit evidence. Lean decides.</strong>
 </div>
 
 <p align="center">
@@ -25,8 +25,8 @@ and Studio surfaces share one idea — use powerful external tools without
 trusting them inside the theorem prover.
 
 **Experimental** research preview: no capability is stable. Theorem-level
-Certification Records require exact candidate binding
-([ADR 0005](docs/adr/0005-exact-candidate-binding.md)); see
+Certification Records require exact candidate binding **and current registry CR
+eligibility** ([ADR 0005](docs/adr/0005-exact-candidate-binding.md)); see
 [status](docs/STATUS.md) and
 [known limitations](docs/security/KNOWN_TRUST_GAPS.md) before relying on results.
 
@@ -36,10 +36,38 @@ Formal work often needs exact algebra, search, or symbolic computation that
 mature external systems already do well. One-off bridges reinvent translation
 and trust boundaries — and can smuggle unchecked solver answers into proofs.
 
-MathEvidence offers a shared path: an explicit semantic contract, checkable
-evidence, and a reusable Lean theorem.
+MathEvidence offers a shared path: explicit semantic contracts, candidate-bound
+evidence, capability-specific checkers, and reproducible verification.
 
-**Do not trust the solver. Lean checks the evidence.**
+**Do not trust the solver. Trust only the proposition the declared checker
+actually establishes.**
+
+## Current exact scope
+
+The registry currently marks five owned capability fragments CR-eligible under
+exact candidate binding. These are narrow contracts, not generic automation
+claims. Rational equality remains an experimental checker/soundness/bridge
+capability but is deliberately fail-closed for theorem Certification Records in
+the pinned Lean 4.14 public-preview path.
+
+| Capability | Exact claim scope |
+| --- | --- |
+| `algebra.ideal_membership_witness` | Supplied witness establishes the supported polynomial ideal-membership identity; no Gröbner/non-membership/completeness claim |
+| `algebra.linear_algebra` | Exact rational `inverse_witness`, `system_solution`, `kernel_vector`, and `det_identity` operations |
+| `logic.finite_counterexample` | Explicit finite witness establishes `refuted`; no-witness search does not prove universality |
+| `algebra.formal_rational_calculus` | Registered formal/algebraic grammar and exact `soundResult` operations only |
+| `analysis.analytic_calculus` | Strict registered theorem-form whitelist with explicit hypotheses; not arbitrary analysis |
+
+`algebra.rational_equality` still exposes its exact rational-expression checker,
+soundness theorem, bridge, and generator surface. Theorem-CR promotion is
+disabled for this release because the candidate-specific checker proposition
+cannot be admitted on the production Lean 4.14 native-reduction path without an
+unacceptable `sorryAx` dependency. Fixture closure is not substituted for that
+missing candidate theorem.
+
+Federated SAT/PB/SMT metadata is not theorem-CR eligible in this repository.
+The authoritative machine-readable state is
+[`registry/maturity-inventory.json`](registry/maturity-inventory.json).
 
 ## Quick start
 
@@ -63,8 +91,11 @@ authoritative — see
 [`docs/audits/2026-07-26-real-vision/KERNEL_REPLAY_PLATFORM.md`](docs/audits/2026-07-26-real-vision/KERNEL_REPLAY_PLATFORM.md).
 
 Optional: SymPy for open backends; `wolframscript` (set
-`MATHEVIDENCE_WOLFRAMSCRIPT`) for live Mathematica. Bundles under `evidence/`
-replay offline without a live CAS.
+`MATHEVIDENCE_WOLFRAMSCRIPT`) for live Mathematica. Sealed exact replay bundles
+can be regenerated and integrity-checked without a live CAS after dependencies
+are materialized. This **offline bundle replay** is distinct from a required
+offline Lean/kernel theorem-execution guarantee; see
+[`docs/STATUS.md`](docs/STATUS.md).
 
 ## Try one example
 
@@ -75,10 +106,13 @@ Open the committed rational-equality example
 evidence/examples/rational_equality_basic/
 ```
 
-Inspect `request.cjson`, `certificate.cjson`, and `theorem.lean`. Lean owns
-acceptance; the adapter is untrusted. Then follow
-[`docs/getting-started/`](docs/getting-started/) for offline replay, or start
-the local Agent API:
+Inspect `request.cjson`, `certificate.cjson`, and `theorem.lean`. The adapter is
+untrusted. Checker/theorem authority is determined by the declared assurance
+path, not by the presence of those files alone. In the pinned Lean 4.14 public
+preview this capability is **not** theorem-CR eligible; the committed theorem is
+therefore not release authority for an arbitrary submitted candidate. Then
+follow [`docs/getting-started/`](docs/getting-started/) for replay, or start the
+local Agent API:
 
 ```text
 python -m agent.api.server --host 127.0.0.1 --port 8787
@@ -88,29 +122,54 @@ Health check: `GET http://127.0.0.1:8787/v1/health`. Public open / inspect /
 replay take opaque `bundleId` values — not filesystem paths. See
 [`agent/README.md`](agent/README.md).
 
+## Assurance chain
+
+For an exact CR-eligible path, the intended chain is:
+
+```text
+submitted request + candidate/evidence
+  -> schema/canonical validation
+  -> capability-specific exact replay IR
+  -> deterministic generated Lean source
+  -> pinned Lean/checker execution
+  -> declaration/result identity
+  -> registry policy evaluation
+  -> Certification Record
+```
+
+Generation is not verification. Fixture replay is not candidate verification.
+Benchmark success is not theorem promotion. Unsupported exact modes fail closed.
+The required `lean` CI workflow executes production-generated exact candidates
+for every CR-eligible capability; structural generator tests alone do not
+satisfy that release gate.
+
 ## Repository map
 
 | Path | Role |
 | --- | --- |
 | `MathEvidence/` | Lean protocol types, encodings, checkers, tactics |
-| `adapters/` | Untrusted backends (SymPy, Mathematica, and related) |
+| `adapters/` | Untrusted backends and exact replay generation framework |
 | `agent/` | AI-facing Agent API and SDKs |
 | `studio/` | Notebook and editor surfaces |
-| `registry/` | Capability declarations (all experimental today) |
-| `evidence/` | Committed Evidence Bundles (schema v0.2 `.cjson`) |
-| `foundry/` | Schemas and pipelines for certified tool-use episodes |
-| `benchmarks/` | Conformance, adversarial, and real-world suites |
-| `docs/` | Specs, status, trust model, getting started |
+| `registry/` | Capability declarations and machine-readable assurance maturity |
+| `evidence/` | Committed Evidence Bundles and conformance artifacts |
+| `foundry/` | Schemas and pipelines for verified tool-use episodes |
+| `benchmarks/` | Frozen conformance/regression and evaluation suites |
+| `docs/` | Specs, status, trust model, getting started, release docs |
 
 ## Contribute
 
-Contributions are welcome. Keep backends untrusted and Lean authoritative.
+Contributions are welcome. Keep backends untrusted and checker authority
+explicit.
 
 1. Read [`CONTRIBUTING.md`](CONTRIBUTING.md) and [`docs/STATUS.md`](docs/STATUS.md).
-2. Prefer a focused change with tests (positive, negative, and replay when relevant).
+2. Prefer a focused change with positive, negative, mutation, and replay tests
+   where relevant.
 3. Run `just check` before opening a PR.
-4. Do not flip capabilities to `"stable"` from a single PR — promotion follows a
-   documented checklist with real human review.
+4. Exact-capability changes must preserve candidate binding and fail-closed
+   policy; never substitute a fixture for the submitted candidate.
+5. Do not flip capabilities to `"stable"` from a single PR — promotion follows
+   the documented checklist with real human/domain/trust review.
 
 Protocol-wide changes belong in an RFC under `docs/rfcs/`.
 
@@ -122,7 +181,7 @@ Protocol-wide changes belong in an RFC under `docs/rfcs/`.
 | [`docs/getting-started/`](docs/getting-started/) | Install, check, Agent API, first replay |
 | [`docs/STATUS.md`](docs/STATUS.md) | Public-preview status and CR eligibility |
 | [`docs/HANDOFF.md`](docs/HANDOFF.md) | Exact-certification operator runbook |
-| [`docs/security/KNOWN_TRUST_GAPS.md`](docs/security/KNOWN_TRUST_GAPS.md) | Known limitations |
+| [`docs/security/KNOWN_TRUST_GAPS.md`](docs/security/KNOWN_TRUST_GAPS.md) | Known limitations and trust gaps |
 
 Also: [`docs/SPEC_INDEX.md`](docs/SPEC_INDEX.md),
 [`docs/ROADMAP.md`](docs/ROADMAP.md),
@@ -131,15 +190,22 @@ Also: [`docs/SPEC_INDEX.md`](docs/SPEC_INDEX.md),
 ## What to expect
 
 - Everything in the registry is still **experimental**.
-- Six owned capabilities are CR-eligible under exact binding (see STATUS); federated
-  logic is not. Offline exact inspect defaults to `theorem_pending`.
+- Five owned capability fragments are CR-eligible under exact candidate binding;
+  rational equality and federated logic are not theorem-CR eligible in this
+  release.
+- Offline **bundle** replay and offline **kernel** theorem replay are tracked as
+  distinct maturity properties; the stronger kernel property is not currently
+  claimed release-wide.
 - A green local `just check` is useful feedback — not attested release CI or
   completed human review.
+- The final release SHA must have the required remote assurance/security/replay
+  gates green. Repository branch/ruleset configuration is operational governance,
+  not mathematical assurance evidence for this experimental preview.
 - Receipt crypto under `dev/receipt-keys/` is **dev-only**, not production PKI.
-  Signing / third-party attestation remains deferred.
+  Production signing / third-party attestation remains a separate explicit gate.
 
-When unsure, trust Lean’s checkers and the written limitations — not a backend
-status code.
+When unsure, follow the exact proposition, checker, registry policy, and current
+limitations — not a backend status code or historical completion label.
 
 ---
 
diff --git a/REPRODUCIBILITY.md b/REPRODUCIBILITY.md
new file mode 100644
index 00000000..38ebea60
--- /dev/null
+++ b/REPRODUCIBILITY.md
@@ -0,0 +1,140 @@
+# Reproducibility protocol
+
+This document defines how to reproduce an experimental MathEvidence release
+without confusing repository reproducibility, evidence replay, and theorem
+certification.
+
+## 1. Identify the exact revision
+
+Record the release tag and resolved Git commit before running anything. A release
+artifact must be traceable to one immutable commit. `scripts/generate_release_provenance.py`
+records the commit/tree and hashes the assurance-relevant repository surface.
+
+Do not reproduce from an unspecified moving branch and call the result release
+reproduction.
+
+## 2. Materialize pinned dependencies
+
+Use the committed `lean-toolchain`, `lake-manifest.json`, `uv.lock`, and project
+metadata. Dependency installation may require network access during initial
+materialization. After materialization, offline-replay claims apply only to the
+scope explicitly described in the maturity inventory.
+
+Typical setup:
+
+```text
+bash scripts/ci/install-elan-pinned.sh
+uv sync --frozen --extra dev --extra sympy
+```
+
+## 3. Validate the trust surface
+
+Before evaluating benchmark or theorem claims, validate schemas, capability
+registries, maturity policy, import boundaries, and proof-audit constraints:
+
+```text
+python scripts/validate_schemas.py
+python scripts/validate_registry.py
+python scripts/validate_maturity_inventory.py
+python scripts/check_import_boundaries.py
+python scripts/audit_sorry_axioms.py
+```
+
+A validation failure is a setup/integrity failure, not a mathematical rejection.
+
+## 4. Build the pinned Lean trust path
+
+Build the complete checker closure, verification executables, and audit drivers
+with the pinned toolchain:
+
+```text
+lake build \
+  MathEvidenceCheckers \
+  mathevidence-verify-bundle \
+  mathevidence-kernel-replay \
+  mathevidence-declaration-identity \
+  mathevidence-import-graph \
+  mathevidence-axiom-report
+```
+
+Then run the environment-level import/axiom audits used by CI.
+
+## 5. Reproduce candidate-specific exact assurance
+
+For theorem-level Certification Record eligibility, structural source generation
+is insufficient. The authoritative release gate must generate each exact
+candidate-specific Lean module through the production exact-replay plugin,
+compile it through the same staged project path used by production kernel replay,
+and inspect the resulting declaration in the pinned Lean environment:
+
+```text
+python scripts/ci/run_cr_exact_lean_e2e_production.py
+```
+
+The production runner imports its case/coverage matrix from
+`scripts/ci/run_cr_exact_lean_e2e.py`. That matrix module also contains a
+standalone diagnostic executor, but the standalone temporary-file invocation is
+**not** release authority for Lean 4.14 modules that depend on the production
+staging/compiled-module path.
+
+The matrix derives the CR-eligible capability set from
+`registry/maturity-inventory.json`. For operation-discriminated capabilities it
+also requires coverage of the complete production exact-operation/whitelist set.
+Adding a promoted exact form without an E2E case therefore fails release CI.
+
+## 6. Reproduce offline bundle integrity separately
+
+Offline bundle replay checks canonical inputs, generated source, manifests,
+artifacts, toolchain contracts, and tamper resistance without relying on a live
+CAS backend:
+
+```text
+MATHEVIDENCE_OFFLINE=1 python -m pytest tests/forensic/test_offline_exact_replay.py -q
+```
+
+`offline_bundle_replay_exists` does not imply
+`offline_kernel_replay_exists`. A result such as `theorem_pending` is not a
+kernel theorem proof and must not be relabeled.
+
+## 7. Reproduce benchmarks without assurance escalation
+
+Run the benchmark workflows/commands only as empirical task-performance evidence.
+Benchmark pass/fail never changes Certification Record eligibility and cannot
+replace exact candidate replay.
+
+The ideal-membership suite is a frozen conformance/regression corpus. Its results
+must not be generalized into a claim that arbitrary external solver output is
+sound.
+
+## 8. Generate and inspect release provenance
+
+Generate the release manifest:
+
+```text
+python scripts/generate_release_provenance.py dist/provenance
+```
+
+Verify that the manifest records the exact Git revision, Lean toolchain, Lake
+package pins, and hashes of the assurance-relevant registry/schema/workflow/lock
+and evidence surfaces. Compare artifact digests before relying on copied release
+files.
+
+## 9. Interpret outcomes correctly
+
+Use these categories consistently:
+
+- **proved** — the declared exact proposition for the submitted candidate passed the trusted theorem path;
+- **refuted** — a certified counterexample establishes falsity of the scoped claim;
+- **evidence-only / checker accepted** — useful evidence without theorem-level promotion;
+- **tamper/setup/integrity error** — replay environment or artifact integrity failed;
+- **unavailable** — the requested assurance mode is not supported and no stronger label may be retained.
+
+A compiler/dependency/setup failure is not a theorem rejection. Absence of a
+counterexample is not a proof. Numerical agreement is not exact proof.
+
+## 10. Release acceptance
+
+An experimental release should be created only from a frozen commit after its
+required CI matrix is green. Stable capability promotion is governed separately
+and requires the additional human/external artifacts documented in the stable
+promotion checklist; experimental release readiness does not satisfy those gates.
diff --git a/adapters/common/exact_replay/plugins/formal_rational_calculus.py b/adapters/common/exact_replay/plugins/formal_rational_calculus.py
index 44f6a2ff..94600bea 100644
--- a/adapters/common/exact_replay/plugins/formal_rational_calculus.py
+++ b/adapters/common/exact_replay/plugins/formal_rational_calculus.py
@@ -266,6 +266,40 @@ def render(self, ir: ReplayIR) -> str:
         req_name = f"{decl}_req"
         cert_name = f"{decl}_cert"
         binding_decl = f"{decl}_request_binding"
+        if op == "antiderivative_candidate":
+            # The checker combines opaque imported definitions with a small closed
+            # symbolic calculation. Keep native evaluation for binding/shape/domain
+            # bookkeeping, but expose the formal derivative and sparse-polynomial
+            # computation explicitly for the mathematical obligation. This avoids
+            # Lean 4.14's native_decide bridge failure without changing checkBool.
+            checker_proof = f"""show checkBool {req_name} {cert_name} = true from by
+      have hDigest : digestOk {req_name} {cert_name} = true := by native_decide
+      have hWellFormed : wellFormedOk {req_name} = true := by native_decide
+      have hDomain : domainCoverOk {req_name} {cert_name} = true := by native_decide
+      have hOp : opOk {req_name} = true := by
+        simp [opOk, {req_name}, {claim_name}, Claim.opHolds,
+          antiderivativeOk, exprEqual, formalDeriv,
+          MathEvidence.IR.RationalExpr.polyEqual,
+          MathEvidence.IR.RationalExpr.differenceNumerator,
+          MathEvidence.IR.RationalExpr.toFrac,
+          MathEvidence.IR.RationalExpr.Poly.combineLike,
+          MathEvidence.IR.RationalExpr.Poly.sub,
+          MathEvidence.IR.RationalExpr.Poly.add,
+          MathEvidence.IR.RationalExpr.Poly.neg,
+          MathEvidence.IR.RationalExpr.Poly.mul,
+          MathEvidence.IR.RationalExpr.Poly.pow,
+          MathEvidence.IR.RationalExpr.Poly.one,
+          MathEvidence.IR.RationalExpr.Poly.C,
+          MathEvidence.IR.RationalExpr.Poly.X,
+          MathEvidence.IR.RationalExpr.Poly.mulTerm,
+          MathEvidence.IR.RationalExpr.Poly.Term.sortVars,
+          MathEvidence.IR.RationalExpr.Poly.sortNats,
+          MathEvidence.IR.RationalExpr.Poly.insertSorted]
+      simp [checkBool, hDigest, hWellFormed, hDomain, hOp]"""
+        else:
+            checker_proof = (
+                f"by native_decide : checkBool {req_name} {cert_name} = true"
+            )
         claim_fields = (
             f"  operation := {_OP_LEAN[op]}\n"
             f"  varNames := {names}\n"
@@ -313,13 +347,13 @@ def {cert_name} : Certificate where
 
 theorem {binding_decl} :
     {req_name}.requestDigest = ⟨{lean_string(request_digest)}⟩ := by
-  native_decide
+  rfl
 
 theorem {decl} : Claim.proposition {req_name}.claim :=
   replaySound
     {req_name}
     {cert_name}
-    (by native_decide : checkBool {req_name} {cert_name} = true)
+    ({checker_proof})
 
 #print axioms {binding_decl}
 #print axioms {decl}
diff --git a/adapters/common/exact_replay/plugins/rational_equality.py b/adapters/common/exact_replay/plugins/rational_equality.py
index 4adb1b77..cab10004 100644
--- a/adapters/common/exact_replay/plugins/rational_equality.py
+++ b/adapters/common/exact_replay/plugins/rational_equality.py
@@ -23,10 +23,42 @@
 from adapters.common.limits import ResourceLimits
 
 CAPABILITY = "algebra.rational_equality"
+CAPABILITY_VERSION = "0.1.0"
 GENERATOR_ID = "mathevidence.exact_rational_equality"
 GENERATOR_VERSION = "0.1.0"
 GRAMMAR_VERSION = "0.1.0"
 VERIFIER = "mathevidence-declaration-identity"
+# ``MathEvidence.Checkers.RationalEquality.Wire.claimToRequestJson`` currently
+# reconstructs exactly this v0.1 policy. Exact theorem replay must reject any
+# broader wire policy until the Lean binding projection carries those fields.
+EXACT_RESOURCE_POLICY = {
+    "maxWallTimeMs": 10000,
+    "maxOutputBytes": 1048576,
+}
+
+
+def _validate_exact_expr(
+    value: Any,
+    *,
+    var_names: list[str],
+    what: str,
+) -> dict[str, Any]:
+    """Validate an expression without silently changing request wire semantics.
+
+    ``validate_rational_expr`` canonicalizes rational literals (for example
+    ``2/4`` to ``1/2``). That normalization is useful for non-theorem adapter
+    handling, but exact candidate replay must reconstruct the same wire object
+    whose digest the submitter bound. The Lean v0.1 wire projection emits
+    canonical integer/rational syntax, so non-canonical inputs are unsupported
+    here and fail closed rather than being normalized behind the digest.
+    """
+    canonical = validate_rational_expr(value, var_names=var_names, what=what)
+    if canonical != value:
+        raise ValueError(
+            f"{what} must use canonical exact RationalExpr wire syntax; "
+            "silent normalization is not permitted for exact candidate binding"
+        )
+    return canonical
 
 
 @dataclass(frozen=True)
@@ -60,9 +92,22 @@ def parse_and_validate(
         capability_version = validate_semver(
             request.get("capabilityVersion"), what="request capabilityVersion"
         )
+        if capability_version != CAPABILITY_VERSION:
+            raise ValueError(
+                f"exact rational replay supports capabilityVersion {CAPABILITY_VERSION} only; "
+                "the Lean v0.1 wire binding must be extended before another version is eligible"
+            )
         if certificate.get("capabilityVersion") != capability_version:
             raise ValueError("certificate capabilityVersion does not match request")
 
+        resource_policy = request.get("resourcePolicy")
+        if resource_policy != EXACT_RESOURCE_POLICY:
+            raise ValueError(
+                "exact rational replay requires resourcePolicy "
+                f"{EXACT_RESOURCE_POLICY!r}; broader policy fields are not yet represented "
+                "by the Lean v0.1 request-binding projection"
+            )
+
         request_digest = validate_digest(request.get("requestDigest"), what="requestDigest")
         validate_digest(candidate_bundle_digest, what="candidateBundleDigest")
         if certificate.get("requestDigest") != request_digest:
@@ -83,12 +128,16 @@ def parse_and_validate(
                 raise ValueError(f"variable {index} name invalid")
             if var.get("type") != "Rat":
                 raise ValueError(f"variable {index} type must be Rat")
+            if set(var) != {"name", "type"}:
+                raise ValueError(
+                    f"variable {index} contains fields outside the Lean v0.1 wire projection"
+                )
             if name in var_names:
                 raise ValueError(f"duplicate variable name {name!r}")
             var_names.append(name)
 
-        lhs = validate_rational_expr(request.get("lhs"), var_names=var_names, what="lhs")
-        rhs = validate_rational_expr(request.get("rhs"), var_names=var_names, what="rhs")
+        lhs = _validate_exact_expr(request.get("lhs"), var_names=var_names, what="lhs")
+        rhs = _validate_exact_expr(request.get("rhs"), var_names=var_names, what="rhs")
 
         assumptions_raw = request.get("knownAssumptions")
         if not isinstance(assumptions_raw, list):
@@ -97,9 +146,15 @@ def parse_and_validate(
         for index, item in enumerate(assumptions_raw):
             if not isinstance(item, dict) or item.get("kind") != "nonzero":
                 raise ValueError(f"knownAssumptions[{index}] must be kind=nonzero")
+            if set(item) != {"kind", "expr"}:
+                raise ValueError(
+                    f"knownAssumptions[{index}] contains fields outside the Lean v0.1 wire projection"
+                )
             assumptions.append(
-                validate_rational_expr(
-                    item.get("expr"), var_names=var_names, what=f"knownAssumptions[{index}].expr"
+                _validate_exact_expr(
+                    item.get("expr"),
+                    var_names=var_names,
+                    what=f"knownAssumptions[{index}].expr",
                 )
             )
 
@@ -113,17 +168,17 @@ def parse_and_validate(
             role = item.get("role")
             if role not in {"original_division", "common_denominator", "factorization"}:
                 raise ValueError(f"denominatorFactors[{index}] role unsupported")
-            denom_factors.append(
-                validate_rational_expr(
-                    item.get("expr"),
-                    var_names=var_names,
-                    what=f"denominatorFactors[{index}].expr",
-                )
+            canonical_expr = _validate_exact_expr(
+                item.get("expr"),
+                var_names=var_names,
+                what=f"denominatorFactors[{index}].expr",
             )
+            denom_factors.append(canonical_expr)
 
-        # differenceNumerator is diagnostic; reject malformed when present.
+        # differenceNumerator is diagnostic; reject malformed/non-canonical when present so
+        # the generated source never silently rewrites an exact Candidate Bundle field.
         if "differenceNumerator" in certificate:
-            validate_rational_expr(
+            _validate_exact_expr(
                 certificate["differenceNumerator"],
                 var_names=var_names,
                 what="differenceNumerator",
@@ -198,7 +253,6 @@ def render(self, ir: ReplayIR) -> str:
         request_digest = meta["request_digest"]
         candidate_bundle_digest = meta["candidate_bundle_digest"]
         decl = ir.declaration_name
-        binding_decl = f"{decl}_request_binding"
 
         claim_fields = (
             f"  varNames := {names}\n"
@@ -207,7 +261,6 @@ def render(self, ir: ReplayIR) -> str:
             f"  knownAssumptions := {assumptions}\n"
             f"  claimClass := .soundResult"
         )
-        decl = ir.declaration_name
         claim_name = f"{decl}_claim"
         req_name = f"{decl}_req"
         cert_name = f"{decl}_cert"
@@ -232,20 +285,23 @@ def render(self, ir: ReplayIR) -> str:
 def {claim_name} : Claim where
 {claim_fields}
 
-def {req_name} : Request where
-  claim := {claim_name}
-  requestDigest := ⟨{lean_string(request_digest)}⟩
+/-- Reconstruct the request digest from Lean wire semantics; callers do not supply it. -/
+def {req_name} : Request :=
+  Request.ofClaim! {claim_name}
 
 def {cert_name} : Certificate where
   requestDigest := ⟨{lean_string(request_digest)}⟩
   denomFactors := {denoms}
 
-/-- Lean-side request binding for the reconstructed exact wire semantics. -/
+/-- Lean-side equality between reconstructed wire binding and submitted digest.
+The submitted digest is not copied into the request: `native_decide` evaluates
+Lean's canonical-JSON/SHA-256 reconstruction of `Request.ofClaim!`. -/
 theorem {binding_decl} :
     {req_name}.requestDigest = ⟨{lean_string(request_digest)}⟩ := by
   native_decide
 
-/-- Exact Candidate Bundle semantic claim. -/
+/-- Exact Candidate Bundle semantic claim. The checker includes digest equality,
+so this native decision independently re-evaluates the same request binding. -/
 theorem {decl} : Claim.proposition {req_name}.claim {cert_name}.denomFactors :=
   replaySound
     {req_name}
diff --git a/adapters/common/test_wave4_la_cex.py b/adapters/common/test_wave4_la_cex.py
index 08a12728..ccd1b8af 100644
--- a/adapters/common/test_wave4_la_cex.py
+++ b/adapters/common/test_wave4_la_cex.py
@@ -13,6 +13,7 @@
     run_kernel_replay,
 )
 from adapters.common.lean_mirrors import check_finite_counterexample, check_linear_algebra
+from agent.api.assurance_policy import ASSURANCE_MODE_UNAVAILABLE, decide_exact_kernel_replay
 
 ROOT = Path(__file__).resolve().parents[2]
 
@@ -21,8 +22,8 @@ def _rat(n: int, d: int = 1) -> dict:
     return {"tag": "rat", "num": str(n), "den": str(d)}
 
 
-def test_la_profile_and_generic_kernel_replay_fails_closed(tmp_path: Path) -> None:
-    """LA keeps its checker profile but cannot mint a generic record from a fixture."""
+def test_la_profile_rejects_historical_fixture_as_exact_candidate(tmp_path: Path) -> None:
+    """LA exact support must reject a historical fixture that is not valid exact evidence."""
     bundle = ROOT / "evidence" / "conformance" / "linear_algebra" / "inverse_witness_2x2" / "bundle"
     if not bundle.is_dir():
         pytest.skip("LA conformance bundle missing")
@@ -46,6 +47,7 @@ def test_la_profile_and_generic_kernel_replay_fails_closed(tmp_path: Path) -> No
     assert profile["capability_id"] == "algebra.linear_algebra"
     assert profile["soundness_theorem"] == "replaySound"
     assert profile["fixture"] == "inv"  # historical self-test hint only
+    assert decide_exact_kernel_replay("algebra.linear_algebra").ok is True
 
     with pytest.raises(KernelReplayError) as exc:
         run_kernel_replay(
@@ -53,13 +55,14 @@ def test_la_profile_and_generic_kernel_replay_fails_closed(tmp_path: Path) -> No
             require_lean=False,
             out_record_dir=tmp_path / "la_cert",
         )
-    assert exc.value.code == "assurance_mode_unavailable"
-    assert "exact-candidate generator" in str(exc.value)
+    # Exact mode is available now. The old fixture is rejected because it is not
+    # valid candidate-bound evidence for the exact generator; it must never mint a CR.
+    assert exc.value.code == "malformed_evidence"
     assert not (tmp_path / "la_cert").exists()
 
 
-def test_cex_profile_and_generic_kernel_replay_fails_closed(tmp_path: Path) -> None:
-    """CEX fixture replay is a protocol test, not arbitrary Certification authority."""
+def test_cex_profile_rejects_historical_fixture_as_exact_candidate(tmp_path: Path) -> None:
+    """CEX exact support must reject fixture evidence as arbitrary Certification authority."""
     bundle = (
         ROOT
         / "evidence"
@@ -91,6 +94,7 @@ def test_cex_profile_and_generic_kernel_replay_fails_closed(tmp_path: Path) -> N
     profile = _capability_replay_profile(req)
     assert profile["capability_id"] == "logic.finite_counterexample"
     assert profile["fixture"] == "nat_eq0"  # historical self-test hint only
+    assert decide_exact_kernel_replay("logic.finite_counterexample").ok is True
 
     with pytest.raises(KernelReplayError) as exc:
         run_kernel_replay(
@@ -98,11 +102,20 @@ def test_cex_profile_and_generic_kernel_replay_fails_closed(tmp_path: Path) -> N
             require_lean=False,
             out_record_dir=tmp_path / "cex_cert",
         )
-    assert exc.value.code == "assurance_mode_unavailable"
-    assert "exact-candidate generator" in str(exc.value)
+    assert exc.value.code == "malformed_evidence"
     assert not (tmp_path / "cex_cert").exists()
 
 
+def test_unsupported_federated_exact_replay_fails_closed() -> None:
+    """A genuinely unsupported capability must still fail closed with no exact fallback."""
+    decision = decide_exact_kernel_replay("logic.sat_unsat")
+    assert decision.ok is False
+    assert decision.code == ASSURANCE_MODE_UNAVAILABLE
+    assert decision.policy is not None
+    assert decision.policy["exactBinding"]["supported"] is False
+    assert decision.policy["certification"]["crEligible"] is False
+
+
 def test_la_adversarial_mirrors() -> None:
     # Dimension mismatch
     req = bind_request_digest(
diff --git a/agent/api/assurance_policy.py b/agent/api/assurance_policy.py
index aff2554e..f520ee10 100644
--- a/agent/api/assurance_policy.py
+++ b/agent/api/assurance_policy.py
@@ -111,8 +111,9 @@ def supported_assurance_modes(capability_id: str) -> frozenset[str]:
 def decide_exact_kernel_replay(capability_id: str) -> AssuranceDecision:
     """Gate for theorem-producing exact kernel replay.
 
-    Unknown capability, missing policy, unsupported mode, or unsupported exact
-    binding => ``assurance_mode_unavailable``. Never falls back to fixtures.
+    Unknown capability, missing policy, non-CR-eligible policy, unsupported mode,
+    or unsupported exact binding => ``assurance_mode_unavailable``. Never falls
+    back to fixtures.
     """
     cap = find_capability(capability_id)
     if cap is None:
@@ -130,6 +131,17 @@ def decide_exact_kernel_replay(capability_id: str) -> AssuranceDecision:
             message=f"capability {capability_id} has no assurancePolicy",
             capability_id=capability_id,
         )
+    if not cr_eligible(capability_id):
+        return AssuranceDecision(
+            ok=False,
+            code=ASSURANCE_MODE_UNAVAILABLE,
+            message=(
+                f"theorem Certification Record replay is not enabled for {capability_id}; "
+                "registry certification.crEligible must be true"
+            ),
+            capability_id=capability_id,
+            policy=policy,
+        )
     modes = supported_assurance_modes(capability_id)
     if "kernel_replay" not in modes:
         return AssuranceDecision(
diff --git a/benchmarks/ideal_membership/manifest.json b/benchmarks/ideal_membership/manifest.json
index 12107cc0..eb26af9e 100644
--- a/benchmarks/ideal_membership/manifest.json
+++ b/benchmarks/ideal_membership/manifest.json
@@ -69,6 +69,7 @@
   "passTasks": 53,
   "skipTasks": 1,
   "xfailTasks": 1,
-  "valueGate": "Wave3: score backend-proposed witnesses (not expectedMultipliers). Stratified unit/adversarial/scale/held_out via task.stratum; byStratum reported in runner output.",
-  "honestyNote": "ME-RV-035/P0-F: candidate tier = propose ∧ decode ∧ checkMembership(proposed) and MUST NOT claim soundness_verified. release tier = candidate gates + OfflineFixtures kernel_replay Certification Record (fixture-backed subset). expectedMultipliers is oracle-only. In-repo held_out stratum is synthetic; ME-RV-081 external library-derived held-out remains BLOCKED(human)."
+  "evaluationRole": "frozen_release_conformance_and_assurance_regression",
+  "valueGate": "Score backend-proposed witnesses, never expectedMultipliers. Report answer correctness and evidence verification independently, including the critical incorrect-answer + verified-evidence false-accept cell. Stratified unit/adversarial/scale/held_out results are descriptive for this frozen corpus.",
+  "honestyNote": "Candidate tier = propose + decode + candidate-specific witness checking and MUST NOT claim theorem certification from backend success. The exact release tier uses candidate-bound generated replay and the declared Lean verification path when CR policy permits; OfflineFixtures are protocol self-tests only and can never certify a submitted candidate. expectedMultipliers is oracle-only. The in-repo held_out stratum is synthetic; external library-derived held-out validation remains a separate human/external gate. This 55-task corpus is release conformance/regression evidence, not a population estimate of solver soundness or broad mathematical generalization."
 }
diff --git a/benchmarks/ideal_membership/tasks/IM51_false_membership_xfail.json b/benchmarks/ideal_membership/tasks/IM51_false_membership_xfail.json
index d5da571f..7e264879 100644
--- a/benchmarks/ideal_membership/tasks/IM51_false_membership_xfail.json
+++ b/benchmarks/ideal_membership/tasks/IM51_false_membership_xfail.json
@@ -49,7 +49,7 @@
   "expectedStatus": "xfail",
   "xfailReason": "false membership; no witness expected",
   "baselineNotes": [
-    "Target overridden to x^5; with gens ⟨x^2,y^2⟩ this is false membership."
+    "Target is x; every monomial in the monomial ideal ⟨x^2,y^2⟩ is divisible by x^2 or y^2, so x is not a member."
   ],
   "stratum": "adversarial"
 }
diff --git a/docs/STATUS.md b/docs/STATUS.md
index dbbca11f..f7e32c6b 100644
--- a/docs/STATUS.md
+++ b/docs/STATUS.md
@@ -17,37 +17,51 @@ cannot certify a different claim.
 Historical dated audits under
 [`audits/2026-07-26-real-vision/`](audits/2026-07-26-real-vision/) and older
 `MET` labels are engineering-archive records — not current Certification Record
-authority. Current `main` may still use fixture-substitution semantics; this
-branch’s live status is exact candidate binding.
+authority. Current code uses exact candidate binding for the registry-enabled
+exact paths; protocol fixtures remain self-tests and cannot certify a different
+submitted candidate.
 
 ## Current assurance maturity
 
-Independent booleans. Checker or fixture existence does not imply exact binding
-or Certification Record eligibility. Six owned exact-bound capabilities are
-`cr_eligible=true` after Lean exact-replay E2E; federated logic remains false.
+These are independent dimensions. Checker or fixture existence does not imply
+exact binding or Certification Record eligibility. The registry currently marks
+five owned exact-bound capabilities `cr_eligible=true`; rational equality keeps
+its checker/soundness/bridge surface but is deliberately fail-closed for theorem
+Certification Records under the pinned Lean 4.14 public-preview path. Federated
+logic remains non-eligible. The required `lean` release gate executes
+production-generated candidates for every CR-eligible capability and every
+exact-enabled linear-algebra operation.
+
+Offline maturity is intentionally split. `offline_bundle_replay_exists` means a
+sealed bundle can be deterministically regenerated/validated without consulting
+the solver or network after materialization. `offline_kernel_replay_exists`
+means release CI requires successful offline Lean theorem execution; no capability
+claims that stronger maturity today. The legacy `offline_replay_exists` JSON
+field is only a compatibility alias for bundle replay and is not an independent
+column below.
 
 <!-- maturity-inventory-table:begin -->
-| Capability | adapter_exists | checker_exists | lean_soundness_exists | bridge_replay_exists | exact_candidate_binding_exists | offline_replay_exists | cr_eligible |
-| --- | --- | --- | --- | --- | --- | --- | --- |
-| `algebra.ideal_membership_witness` | true | true | true | true | true | true | true |
-| `algebra.rational_equality` | true | true | true | true | true | true | true |
-| `algebra.linear_algebra` | true | true | true | true | true | true | true |
-| `logic.finite_counterexample` | true | true | true | true | true | true | true |
-| `algebra.formal_rational_calculus` | true | true | true | true | true | true | true |
-| `analysis.analytic_calculus` | true | true | true | true | true | true | true |
-| `logic.sat_unsat` | true | false | false | false | false | false | false |
-| `logic.pseudo_boolean` | true | false | false | false | false | false | false |
-| `logic.smt` | true | false | false | false | false | false | false |
+| Capability | adapter_exists | checker_exists | lean_soundness_exists | bridge_replay_exists | exact_candidate_binding_exists | offline_bundle_replay_exists | offline_kernel_replay_exists | cr_eligible |
+| --- | --- | --- | --- | --- | --- | --- | --- | --- |
+| `algebra.ideal_membership_witness` | true | true | true | true | true | true | false | true |
+| `algebra.rational_equality` | true | true | true | true | false | true | false | false |
+| `algebra.linear_algebra` | true | true | true | true | true | true | false | true |
+| `logic.finite_counterexample` | true | true | true | true | true | true | false | true |
+| `algebra.formal_rational_calculus` | true | true | true | true | true | true | false | true |
+| `analysis.analytic_calculus` | true | true | true | true | true | true | false | true |
+| `logic.sat_unsat` | true | false | false | false | false | false | false | false |
+| `logic.pseudo_boolean` | true | false | false | false | false | false | false | false |
+| `logic.smt` | true | false | false | false | false | false | false | false |
 <!-- maturity-inventory-table:end -->
 
-**Outcomes:** owned CR-eligible capabilities mint `proved` except
-`logic.finite_counterexample` (`refuted`). Federated SAT / PB / SMT stay
-fail-closed for theorem CR.
+**Outcomes:** CR-eligible owned capabilities mint `proved` except
+`logic.finite_counterexample` (`refuted`). Rational equality and federated SAT /
+PB / SMT stay fail-closed for theorem CR.
 
 ## What this preview is
 
 Protocol, semantic IR, verified checkers, untrusted adapters, Agent API, Studio
-surfaces, registry, Foundry schemas/corpus samples, and offline evidence
+surfaces, registry, Foundry schemas/corpus samples, and replayable evidence
 bundles.
 
 It is **not**:
@@ -55,27 +69,33 @@ It is **not**:
 - a stable computational-evidence layer;
 - completed human gates (external confirmations, dual-area review, live
   federation, usability studies);
-- attested immutable CI green on a tagged release with required checks
-  (branch protection is on; release attestation still open — see
-  [`validation/ci/`](validation/ci/));
+- attested immutable CI green on a tagged release;
 - a production signing / PKI story (dev keys under `dev/receipt-keys/` only);
 - a Foundry Q2 formally-verified corpus at scale (v0.1 samples remain
   `Q1_checker_preview` pending Certification Records).
 
+Repository branch/ruleset configuration is an operational governance choice for
+this experimental preview; it is not mathematical assurance evidence and is not
+a prerequisite for the public-preview release.
+
 ## Honest limits (summary)
 
 | Topic | Status |
 | --- | --- |
 | Exact binding | Required for theorem CR; see ADR 0005 |
-| CR-eligible set | Six owned capabilities above; federated logic never eligible under exact binding |
-| Offline exact inspect | Defaults to `theorem_pending`; `MATHEVIDENCE_OFFLINE_LEAN=1` / `require_lean=True` may yield `theorem_proved` when Lake is available — still not a CR mint |
+| CR-eligible set | Five owned capabilities above; rational equality and federated logic are not theorem-CR eligible in this release |
+| Rational equality | Checker, soundness theorem, bridge, and exact-source generator remain; theorem CR is disabled fail-closed under pinned Lean 4.14 because the candidate-specific checker proposition cannot be admitted on the production native-reduction path without an unacceptable `sorryAx` dependency |
+| Exact Lean release gate | `scripts/ci/run_cr_exact_lean_e2e_production.py` executes production-generated candidates through the production kernel-replay staging and declaration-inspection path under pinned Lean; structural generation or standalone temporary-file execution is insufficient |
+| Offline bundle replay | Available for owned capability bundles where declared; deterministic integrity/re-generation may end at `theorem_pending` |
+| Offline kernel replay | Not claimed as release maturity today; optional `require_lean=True` may prove when the materialized closure is available, but setup failure does not count as proof |
+| Analytic calculus | Strict theorem-form whitelist; unsupported forms fail closed |
 | Analytic ODE | Empty domain obligations + at most one initial condition; multi-IC / obligation-bearing ODE fail closed |
-| Formal vs analytic calculus | Separate IDs; formal is not Mathlib `HasDerivAt` / analytic ODE |
+| Formal vs analytic calculus | Separate IDs; formal rational calculus is not general Mathlib analysis |
 | Bundle / CR schemas | Candidate Bundle v0.3; Certification Record **v0.4** for exact promotion. Legacy v0.3 records must not be silently upgraded |
 | Bundle verifier | `mathevidence-verify-bundle` emits `native_checked` / `checker_accepted` only — not theorem Certified |
 | OfflineFixtures | Protocol self-tests — not Certification Record authority for a submitted candidate |
 | Windows kernel-replay | Required path: `scripts/link_exe_via_rsp.py`; degrade honestly — never fake Certified |
-| Stable promotion | Frozen; mechanical promotion-record gate only |
+| Stable promotion | Blocked until the repository-defined stable-promotion and human/trust gates are genuinely closed |
 
 ## Engineering surface (preview)
 
@@ -83,8 +103,12 @@ It is **not**:
 | --- | --- |
 | Agent API | v0.1.0; open / inspect / replay by opaque `bundleId` only |
 | Ideal membership | Witness identity; no Groebner / non-membership completeness |
-| Linear algebra | Exact int/rational ops; practical matrix size bounded by IR policy |
-| Rational tactic | Fixtures + live `eq_of_replaySound` Bridge close; not independent `field_simp; ring` |
+| Rational equality | Exact rational checker/soundness/bridge surface remains experimental; theorem Certification Record promotion is disabled for the pinned Lean 4.14 release path |
+| Linear algebra | Exact rational `inverse_witness`, `system_solution`, `kernel_vector`, `det_identity`; no broad linear-algebra completeness claim |
+| Finite counterexample | Exact witness establishes `refuted`; no-witness search does not prove the universal claim |
+| Formal rational calculus | Formal/algebraic grammar only; candidate-only requests remain evidence-only |
+| Analytic calculus | Exact whitelist only; capability name must not be read as arbitrary analytic proof support |
+| Rational tactic | Fixtures + live `eq_of_replaySound` Bridge close; not independent `field_simp; ring`; fixture closure is not candidate CR authority |
 | CODEOWNERS | Single-owner incubation stub — see `GOVERNANCE.md` |
 | Python lock | `uv.lock` committed; see `docs/architecture/python-deps.md` |
 
@@ -97,8 +121,19 @@ See [`getting-started/`](getting-started/) and the root
 pytest tests/forensic -q
 ```
 
+Production-generated exact Lean E2E:
+
+```text
+python scripts/ci/run_cr_exact_lean_e2e_production.py
+```
+
+The companion `scripts/ci/run_cr_exact_lean_e2e.py` module owns the checked-in
+case/coverage matrix and a standalone diagnostic runner. Its temporary-file Lean
+execution is not the authoritative release path.
+
 Workflow definitions: `.github/workflows/`. Local green alone is not promotion
-evidence.
+or release evidence; the exact release SHA must have the required remote gates
+green.
 
 ## Related docs
 
@@ -111,7 +146,7 @@ evidence.
 | [`audits/2026-07-26-real-vision/`](audits/2026-07-26-real-vision/) | Historical re-audit (not current CR authority) |
 | [`security/KNOWN_TRUST_GAPS.md`](security/KNOWN_TRUST_GAPS.md) | Known limitations |
 | [`validation/stable-capability-checklist.md`](validation/stable-capability-checklist.md) | Only path to `stable` |
-| [`validation/ci/`](validation/ci/) | Machine-readable CI truth records |
+| [`validation/ci/`](validation/ci/) | Machine-readable CI configuration and truth records |
 | [`architecture/python-deps.md`](architecture/python-deps.md) | Frozen `uv.lock` policy |
 | [`validation/remaining-spec-matrix.md`](validation/remaining-spec-matrix.md) | Spec / milestone honesty matrix |
 | [`release/RELEASE_NOTES_DRAFT.md`](release/RELEASE_NOTES_DRAFT.md) | Public-preview release notes draft |
diff --git a/docs/release/RELEASE_NOTES_DRAFT.md b/docs/release/RELEASE_NOTES_DRAFT.md
index 5fd4168b..c09823bd 100644
--- a/docs/release/RELEASE_NOTES_DRAFT.md
+++ b/docs/release/RELEASE_NOTES_DRAFT.md
@@ -1,54 +1,104 @@
-# Release notes draft — engineering-closure public preview
+# Release notes draft — experimental public preview
 
-**Status:** draft for a public preview of branch `engineering-closure`  
+**Status:** draft for the final experimental 0.x public preview.  
 **Not a stable release.** No capability is promoted to `"stable"`.
 
 ## Summary
 
 MathEvidence is published as an **experimental** open computational-evidence
 platform for Lean. This preview packages protocol, checkers, adapters, Agent
-API v0.1.0, Studio surfaces, registry, Foundry samples, and offline evidence
-under honest limitation docs
+API v0.1.0, Studio surfaces, registry, Foundry samples, benchmark/conformance
+corpora, and replayable evidence under explicit limitation documentation
 ([`KNOWN_TRUST_GAPS.md`](../security/KNOWN_TRUST_GAPS.md),
 [`STATUS.md`](../STATUS.md)).
 
+The theorem-promotion rule is candidate-bound and fail-closed: a theorem-level
+Certification Record requires the exact submitted candidate to pass the
+registered production verification path. Fixtures, nearby theorems, adapter
+booleans, and benchmark scores cannot grant theorem status.
+
+## Assurance scope in this preview
+
+Five owned capability fragments are theorem-CR eligible under exact candidate
+binding:
+
+- `algebra.ideal_membership_witness` — witness identity only;
+- `algebra.linear_algebra` — exact rational `inverse_witness`,
+  `system_solution`, `kernel_vector`, and `det_identity`;
+- `logic.finite_counterexample` — exact witness establishes `refuted`;
+- `algebra.formal_rational_calculus` — registered formal/algebraic operations;
+- `analysis.analytic_calculus` — strict theorem-form whitelist with explicit
+  hypotheses.
+
+`algebra.rational_equality` remains an experimental checker/soundness/bridge
+capability, but theorem Certification Record promotion is disabled for the
+pinned Lean 4.14 public-preview path. The candidate-specific checker proposition
+does not currently elaborate through the production native-reduction path
+without an unacceptable `sorryAx` dependency, so the release fails closed
+instead of substituting fixture evidence.
+
+Federated SAT/PB/SMT metadata remains non-CR-eligible in this repository.
+
+## Protocol and evidence versions
+
+- Candidate Bundle: **v0.3**.
+- Certification Record for exact theorem promotion: **v0.4**.
+- Legacy records retain their original semantics and must not be silently
+  upgraded.
+- Offline bundle replay and offline kernel theorem replay are separate maturity
+  properties; the stronger release-wide offline-kernel property is not claimed.
+
 ## Highlights
 
-- **Trust posture documented:** known limitations and open human gates are
-  explicit; do not invent confirmations or dual-area approvals.
-- **Agent API v0.1.0:** operation-level HTTP API; bundle open/inspect/replay
-  accept opaque **`bundleId` only** (raw paths rejected).
-- **Evidence Bundle v0.2:** full Evidence Bundle trees use `.cjson` layout;
-  dual-read retained for older consumers during migration.
-- **Capability ID:** formal rational calculus is
-  `algebra.formal_rational_calculus` (not analytic `HasDerivAt`).
-- **Forensic suite:** `tests/forensic/` guards core trust properties.
+- **Trust posture explicit:** untrusted adapters propose; checker/Lean authority
+  is capability-specific and proposition-scoped.
+- **Production exact gate:** CR-eligible paths are exercised through
+  `scripts/ci/run_cr_exact_lean_e2e_production.py` and declaration identity is
+  read from `Lean.Environment` rather than inferred from source presence.
+- **Agent API v0.1.0:** public bundle open/inspect/replay accepts opaque
+  **`bundleId` only**; raw filesystem paths are rejected.
+- **Capability separation:** formal rational calculus is
+  `algebra.formal_rational_calculus`; analytic calculus is a separate strict
+  whitelist capability.
+- **Forensic suite:** `tests/forensic/` guards exact-binding, tamper, policy,
+  adapter/checker, and assurance-boundary regressions.
+- **Benchmark discipline:** conformance/regression scores never grant theorem
+  Certification Record eligibility.
 
 ## Explicit non-claims
 
 - No stable capability promotion.
+- No universal solver soundness or broad mathematical completeness claim.
+- No claim that the frozen benchmark corpus estimates population false-accept
+  probability or generalization.
 - No live external federation agreements.
 - No completed external user-confirmation / workflow-win / usability study
   counts invented for this draft.
-- No attested immutable CI green on a release tag claimed in-tree.
-- Dev receipt HMAC/Ed25519 material is **not** production PKI.
+- No attested immutable CI green on a release tag claimed in-tree before that
+  tag is actually created and checked.
+- Dev receipt HMAC/Ed25519 material is **not** production PKI; production release
+  signing remains deferred unless separately established by release evidence.
+- Repository branch/ruleset configuration is operational governance, not
+  mathematical assurance evidence for this experimental preview.
 
 ## Upgrade / migration notes for users
 
 1. Prefer Agent `bundleId` flows; do not pass filesystem paths to public open /
    inspect / replay endpoints.
-2. Prefer Evidence Bundle **v0.2** trees under `evidence/`.
+2. Treat Candidate Bundle v0.3 and Certification Record v0.4 as the current
+   exact-promotion protocol surface.
 3. Use registry ID `algebra.formal_rational_calculus`; treat legacy
    `symbolic_calculus` path names under `evidence/conformance/` as fixture
    directory names only.
-4. Read [`docs/security/KNOWN_TRUST_GAPS.md`](../security/KNOWN_TRUST_GAPS.md)
+4. Do not treat rational-equality fixtures or bridge theorems as authority for
+   an arbitrary submitted candidate; theorem CR is disabled for that capability
+   in this pinned Lean 4.14 preview.
+5. Read [`docs/security/KNOWN_TRUST_GAPS.md`](../security/KNOWN_TRUST_GAPS.md)
    before relying on any experimental capability.
 
-## Next (human / org)
+## Separate stable-promotion work
 
-- External confirmations and review packets
-  (`docs/validation/user-confirmation.md`, `docs/validation/review-packets/`).
-- Live federation agreements (`docs/architecture/federation-agreements.md`).
-- Multi-area CODEOWNERS and enforceable dual review.
-- Immutable CI green evidence on a candidate release commit, then governance PR
-  for any `stable` flip per `docs/validation/stable-capability-checklist.md`.
+External confirmations, independent domain/trust review, federation agreements,
+usability evidence, multi-area review, and other checklist items remain future
+requirements for a `stable` lifecycle promotion. They are not fabricated or
+relabelled as completed by this experimental release.
diff --git a/docs/security/KNOWN_TRUST_GAPS.md b/docs/security/KNOWN_TRUST_GAPS.md
index b585a55e..2f1e44df 100644
--- a/docs/security/KNOWN_TRUST_GAPS.md
+++ b/docs/security/KNOWN_TRUST_GAPS.md
@@ -1,117 +1,169 @@
 # Known limitations and trust gaps
 
-This document lists **honest limitations** of the MathEvidence public preview.
-It is part of the trust surface: do not treat experimental capabilities as
-stable, and do not invent human confirmations to close the gates below.
+This document lists **current, honest limitations** of the MathEvidence public
+preview. It is part of the trust surface. Experimental capabilities must not be
+presented as stable, and human/external gates must not be invented.
 
 All registry capabilities remain `"status": "experimental"` until the
-[stable promotion checklist](../validation/stable-capability-checklist.md)
-and [governance](../../GOVERNANCE.md) requirements are met with real artifacts.
+[stable promotion checklist](../validation/stable-capability-checklist.md) and
+[GOVERNANCE.md](../../GOVERNANCE.md) requirements are met with real artifacts.
 
-For a short project status summary, see [`docs/STATUS.md`](../STATUS.md).
-For the 2026-07-26 triple-check, see
-[`audits/2026-07-26-real-vision/TRIPLE_CHECK_GAP_MATRIX.md`](../audits/2026-07-26-real-vision/TRIPLE_CHECK_GAP_MATRIX.md).
+For machine-readable CR maturity, use
+[`registry/maturity-inventory.json`](../../registry/maturity-inventory.json).
+For the short public status, use [`docs/STATUS.md`](../STATUS.md). Historical
+dated audits are evidence of their date, not current promotion authority.
 
 ---
 
-## Trust invariants (always)
+## Trust invariants
 
-- External backends are untrusted.
-- Lean is the sole authority for theorem acceptance.
-- A backend Boolean answer is never sufficient evidence.
-- Accepted results must be bound to the exact request by cryptographic digest.
-- Offline replay must recheck committed evidence without trusting the solver.
+These do not change with backend, benchmark, or release status.
 
-Forensic regressions under `tests/forensic/` guard several of these properties.
+- External backends, models, search procedures, and adapters are untrusted.
+- Lean/checker authority is capability-specific and must match the advertised
+  proposition.
+- A backend Boolean answer is never sufficient theorem evidence.
+- A fixture or nearby theorem cannot certify a different submitted candidate.
+- Theorem-level Certification Records require exact candidate binding and live
+  registry CR eligibility.
+- Assurance may not be escalated by an adapter, serializer, receipt field, user
+  flag, benchmark result, or fallback path.
+- Unsupported exact modes fail closed.
+- Counterexample certification has polarity `refuted`, not `proved`.
+- Numerical agreement is not exact proof by relabeling.
+- Failure to find a counterexample is not a proof of universality.
+- Historical records retain the semantics under which they were created; they
+  are not silently upgraded when a later version gains stronger assurance.
+
+Forensic regressions under `tests/forensic/` guard these properties.
 
 ---
 
 ## Current engineering posture
 
-Exact candidate binding is required for theorem-level Certification Records
-([ADR 0005](../adr/0005-exact-candidate-binding.md)). Live CR eligibility is
-registry-backed ([`docs/STATUS.md`](../STATUS.md),
-[`registry/maturity-inventory.json`](../../registry/maturity-inventory.json)).
-OfflineFixtures and checker-only green are **not** CR authority for a submitted
-candidate. Mathlib-heavy Checkers/IR compile remains the main local/CI cost center.
+Exact candidate binding is the theorem-CR rule
+([ADR 0005](../adr/0005-exact-candidate-binding.md)). CR eligibility is
+registry-backed, and the required `lean` workflow executes production-generated
+candidate modules for every CR-eligible capability. Structural source
+generation alone is not sufficient release evidence.
 
 | Area | Honest status |
 | --- | --- |
-| Exact binding / CR | Six owned capabilities are `cr_eligible=true` after Lean exact-replay E2E (`proved`, except CEX `refuted`). Federated SAT/PB/SMT never CR-eligible under exact binding. |
-| Rational equality | Protocol / semantic-boundary **reference**; interactive tactic closes fixtures and supported live certs via `eq_of_proposition` / `eq_of_replaySound`. Exact generator + CR path when registry allows. Linux CI authoritative for linked exe; Windows **required** rsp path. |
-| Linear algebra / finite CEX | Bridge + exact generators for registered ops; practical det scale bounded by intentional `defaultSizeLimit` (64 entries). CEX CR outcome is `refuted` only. |
-| Formal / analytic calculus | `algebra.formal_rational_calculus` is formal/algebraic only. `analysis.analytic_calculus` is a separate whitelist; exact ODE requires empty domain obligations and at most one initial condition. |
-| Ideal membership | Witness identity only (`algebra.ideal_membership_witness`); no Groebner / non-membership completeness. Exact generator + CR path when registry allows. OfflineFixtures remain protocol self-tests. External held-out (ME-RV-081) **BLOCKED(human)**. |
-| Agent API | Experimental. Public ops use opaque IDs. Certified only via verified Certification Record (`open_certification`). |
-| Evidence bundles | Candidate Bundle **v0.3**; Certification Record **v0.4** for exact promotion. Legacy v0.3 must not be silently upgraded. Placeholders rejected. |
-| Offline exact inspect | Defaults to `theorem_pending`; `MATHEVIDENCE_OFFLINE_LEAN=1` / `require_lean=True` may yield `theorem_proved` when Lake is available — still not a CR mint. |
-| CI / `just check` | Workflows under `.github/workflows/`. Branch protection enabled on `main` (see [`validation/ci/`](../validation/ci/)). Local green `just check` is not promotion evidence or attested release CI. |
-| CODEOWNERS | Single-owner incubation stub (`@fraware`). Multi-area dual review is **not** enforceable yet (ME-RV-084 / `admin:org`). |
-| Stable promotion | **Blocked** until acceptance matrix + human gates below close. Mechanical gate: `schemas/promotion-record.schema.json` + `registry/promotions/`. Historical scoreboard: [`TRIPLE_CHECK_GAP_MATRIX.md`](../audits/2026-07-26-real-vision/TRIPLE_CHECK_GAP_MATRIX.md). |
-| Bundle verifier vs kernel replay | `mathevidence-verify-bundle` → `native_checked` / `checker_accepted` only. Exact theorem path uses declaration-identity + registry policy. Windows: `scripts/link_exe_via_rsp.py` required; degrade with `replay_dependency_missing` — never fake Certified. |
-| Signing / PKI | Production receipt PKI and signed 0.x prerelease attestation remain **deferred** (dev keys under `dev/receipt-keys/` only). |
-| Foundry Q2 | Redefined to require Certification Record fields; v0.1 corpus is `Q1_checker_preview` (0 Q2). |
-| Env import/axiom audits | `mathevidence-import-graph` / `mathevidence-axiom-report` use `Lean.importModules` + `CollectAxioms`; regex source scans remain defense-in-depth. |
+| Exact binding / CR | Five owned capabilities are registry-eligible for exact CR (`proved`, except finite CEX `refuted`). Rational equality is deliberately non-eligible for theorem CR in the pinned Lean 4.14 public preview. Federated SAT/PB/SMT remain non-eligible. |
+| Ideal membership | Witness identity only (`algebra.ideal_membership_witness`); no Gröbner-basis, non-membership, radical, minimality, or completeness claim. |
+| Rational equality | Checker, soundness theorem, bridge, and exact-source generation remain. Candidate-specific theorem CR is disabled fail-closed because the pinned Lean 4.14 production native-reduction path does not admit the generated checker proposition without an unacceptable `sorryAx` dependency. Binary floating point is not silently promoted to exact arithmetic. |
+| Linear algebra | Exact rational `inverse_witness`, `system_solution`, `kernel_vector`, and `det_identity`; no broad linear-algebra completeness/rank/basis claim. |
+| Finite counterexample | Exact finite witness can establish `refuted`. No-witness or sampled search cannot establish the universal claim. |
+| Formal calculus | `algebra.formal_rational_calculus` is a formal/algebraic grammar, not general analytic calculus. |
+| Analytic calculus | `analysis.analytic_calculus` is a strict theorem-form whitelist, not arbitrary analysis. Exact ODE support retains its documented obligation/initial-condition restrictions. |
+| Evidence bundles | Candidate Bundle v0.3; Certification Record v0.4 for exact promotion. Legacy records must not be silently upgraded. |
+| Offline bundle replay | Available where declared: sealed candidate artifacts can be regenerated/validated without consulting the solver after materialization. This may end at `theorem_pending`. |
+| Offline kernel replay | Tracked separately as `offline_kernel_replay_exists`. It is currently **false** as a release maturity property; optional Lean execution succeeding on a machine is not the same as a required, network-isolated release gate. |
+| Bundle verifier | `mathevidence-verify-bundle` emits operational checker status only. It is not theorem Certification authority. |
+| CI / local checks | Local `just check` is useful feedback, not release attestation. Exact release claims require green remote gates on the exact release SHA. |
+| Repository rules | Branch protection/rulesets are operational governance choices for this experimental preview. They are not mathematical assurance evidence and are not a public-preview release prerequisite. |
+| Stable promotion | **Blocked** until the repository-defined human/domain/trust/external gates close. Experimental CR eligibility and stable lifecycle promotion are separate. |
+| CODEOWNERS | Single-owner incubation stub (`@fraware`). Multi-area dual review is not enforceable yet. |
+| Signing / PKI | Production receipt PKI and production release signing remain deferred. Dev keys are not production authority. The experimental release workflow records unsigned status explicitly rather than claiming a signature. |
 
 ---
 
-## Open limitations (do not invent closures)
-
-### Human and governance (blocking stable)
+## Open human and governance gates — blocking `stable`
 
 | ID | Limitation | Where to record progress |
 | --- | --- | --- |
-| H-1 | ≥3 external Milestone 0 user confirmations | `docs/validation/user-confirmation.md` (0 completed); index: `docs/validation/human-gates-runbook.md` |
-| H-2 | ≥1 external workflow-win confirmation (§21.10) | `docs/validation/workflow-win-log.md`; index: `human-gates-runbook.md` |
-| H-3 | Independent domain + trust-model reviews for stable promotion | `docs/validation/review-packets/`, `docs/validation/stable-capability-checklist.md`; index: `human-gates-runbook.md` |
-| H-4 | Live federation agreements (≥2 external peers) | `docs/validation/federation-live-checklist.md`, `docs/architecture/federation-agreements.md` (fixture peers only today) |
-| H-5 | Studio usability session results (≥3 completed) | `docs/validation/studio/usability/` (0 completed results); index: `human-gates-runbook.md` |
-| H-6 | Expert judgments (hypothesis interfaces, conjecture precision, TTP lemma graph) | Unsigned review packets under `docs/validation/review-packets/`; index: `human-gates-runbook.md` |
-| H-7 | Real multi-area CODEOWNERS / dual approval | `.github/CODEOWNERS`, `GOVERNANCE.md`, `docs/validation/ci/github_teams_me_rv084.md` |
-
-Wave 8 human scaffolding (still **BLOCKED**; do not invent completions):
-ME-RV-081 [`held-out-external-benchmark.md`](../validation/held-out-external-benchmark.md),
-ME-RV-082/083 [`federation-live-checklist.md`](../validation/federation-live-checklist.md),
-ME-RV-085 [`external-validation-interview.md`](../validation/external-validation-interview.md),
-ME-RV-086 [`external-adoption-checklist.md`](../validation/external-adoption-checklist.md).
-Full index: [`human-gates-runbook.md`](../validation/human-gates-runbook.md).
-
-### Engineering and product (honest gaps)
+| H-1 | ≥3 external Milestone 0 user confirmations | `docs/validation/user-confirmation.md` (0 completed) |
+| H-2 | ≥1 external workflow-win confirmation (§21.10) | `docs/validation/workflow-win-log.md` |
+| H-3 | Independent domain + trust-model reviews for stable promotion | `docs/validation/review-packets/`, `stable-capability-checklist.md` |
+| H-4 | Live federation agreements with ≥2 external peers | `docs/validation/federation-live-checklist.md`, `docs/architecture/federation-agreements.md` |
+| H-5 | Studio usability results with ≥3 completed sessions | `docs/validation/studio/usability/` |
+| H-6 | Expert judgments for hypothesis interfaces / conjecture precision / TTP graph | `docs/validation/review-packets/` |
+| H-7 | Real multi-area CODEOWNERS / dual approval | `.github/CODEOWNERS`, `GOVERNANCE.md` |
+
+The `semanticReview` and `trustReview` registry fields refer to this
+**stable-promotion human review layer**. Their `absent` state is intentional and
+must not be presented as completed review. They are distinct from the mechanical
+exact-candidate CR gate used by this experimental preview.
+
+Wave-8 human scaffolding remains blocked until real external artifacts exist;
+templates are not confirmations.
+
+---
+
+## Open engineering and product gaps
 
 | ID | Limitation | Notes |
 | --- | --- | --- |
-| E-1 | Immutable CI green on a release commit | Workflows exist; attested immutable green is still required before calling engineering gates “complete”. |
-| E-2 | Lean toolchain pin | Project remains on the committed `lean-toolchain`; a bump is a deliberate, separately validated change. |
-| E-3 | LeanLink native Mathematica bridge | Deferred; live Mathematica transport is `wolframscript` when `MATHEVIDENCE_WOLFRAMSCRIPT` is set. |
-| E-4 | Sage rational equality | Declared / placeholder; not advertised as live Agent routing. |
-| E-5 | Analytic calculus completeness | `Interpret` + `AnalyticCalculus/Soundness` + `ReplaySound` oleans green; `cert_product` generator + CI `--self-test-analytic`; completeness/uniqueness out of scope; Windows exe link via **required** `scripts/link_exe_via_rsp.py` when Lake 4.14 hits CreateProcess 206. |
-| E-6 | Production receipt PKI | Dev keys under `dev/receipt-keys/` are for local experiments only. |
-| E-7 | Foundry frontier / funding exits | Trivial tool-selection lift may be measured on a tiny suite; frontier acceleration and maintenance funding remain open. |
-| E-8 | Frozen `uv.lock` | **Closed for lock-in-history:** committed @ `1eb1e15`. Remote attested CI freeze remains under P0-G / E-1. |
-| E-9 | Signed 0.x prerelease | Provenance/SBOM scaffolding present; signing + human publish approval open (ME-RV-074). |
-| E-10 | Environment-level Lean audits | **Closed for ME-RV-071/072** via `importModules` / `CollectAxioms` drivers + CI; keep source-scan as defense-in-depth. |
-| E-11 | Ideal flagship adoption | Exact CR path exists for witness identity when registry `crEligible`. OfflineFixtures are not CR authority for a submitted candidate. No live external adoption; ME-RV-081 external held-out **BLOCKED(human)**. |
-| E-12 | Rational tactic authority | **Closed for supported live fragment:** fixtures + elaborated live `eq_of_replaySound` (`RationalClose.tryCloseViaReplaySoundLive`); non-fixture examples + adversarial rejects in `Tactic/Examples.olean`. Authority remains checker soundness (no independent final `field_simp; ring`). |
-| E-13 | LA Bridge det (closed) | General-n `det_of_isDetIdentity` via non-partial `detRatsFuel`; Fin-5/6 examples green. **Intentional resource policy:** factorial Laplace cost + `IR/MatrixExpr.defaultSizeLimit` (64 entries) bound practical `n` — not a missing proof (A5). |
-| E-14 | Theorem identity `Expr.hash` | Type + proof-term digests via structural `ExprSerialize` MET; Lean-internal `Expr.hash` across compiler revisions still not claimed (must not be used). |
-| E-15 | Windows kernel-replay native Lake link | PARTIAL(toolchain). Required local path: `scripts/link_exe_via_rsp.py`; `smoke_exe` / `just exe-smoke` degrade with `replay_dependency_missing`. Linux CI authoritative. |
+| E-1 | Immutable all-green release commit | The final tagged SHA must have the required assurance/security/replay/conformance gates green. |
+| E-2 | Repository governance hardening | Optional operational hardening for this experimental preview; not a mathematical-assurance or release prerequisite. |
+| E-3 | Lean toolchain changes | `lean-toolchain` is pinned; a bump requires a separately validated change. |
+| E-4 | LeanLink native Mathematica bridge | Deferred; live Mathematica transport is `wolframscript` when configured. |
+| E-5 | Sage rational equality | Declared/placeholder; not advertised as live Agent routing. |
+| E-6 | Analytic-calculus completeness | Out of scope. Only the registered whitelist and explicit hypotheses are supported. |
+| E-7 | Production receipt PKI / release signing identity | Deferred; no dev key or soft signing attempt may be marketed as production signing. |
+| E-8 | Foundry frontier / funding exits | Tiny-suite tool-selection results do not establish frontier acceleration or maintenance funding. |
+| E-9 | Independent external reproduction | Release artifacts are designed for it; third-party reproduction remains external work and must not be fabricated. |
+| E-10 | Ideal flagship adoption | Exact candidate path exists, but live external adoption/held-out validation remains open. |
+| E-11 | Windows native Lake link | Required workaround remains `scripts/link_exe_via_rsp.py`; degrade with dependency/setup status, never fake Certified. |
+| E-12 | Practical LA scale | Exact determinant/checker cost and the IR size policy intentionally bound practical dimensions; this is not a completeness claim. |
+| E-13 | Lean internal expression identity | Compiler-internal `Expr.hash` stability across revisions is not claimed as a protocol guarantee. |
+| E-14 | Rational theorem CR on pinned Lean 4.14 | Disabled fail-closed for this public preview. Re-enabling requires a candidate-specific production theorem path that passes without `sorryAx` and is then requalified on an exact release SHA. |
+
+Environment-level Lean import/axiom audits are **implemented** through the
+`mathevidence-import-graph` / `mathevidence-axiom-report` drivers and CI; source
+scans remain defense in depth.
+
+---
+
+## Capability naming and claim-scope notes
+
+- Public formal-calculus ID: `algebra.formal_rational_calculus`.
+- Public analytic-calculus ID: `analysis.analytic_calculus`; strict whitelist
+  only.
+- Ideal-membership ID: `algebra.ideal_membership_witness`; witness identity
+  only.
+- Rational equality must not be described as theorem-CR eligible in this pinned
+  Lean 4.14 release, even though its checker/soundness/bridge code exists.
+- Linear algebra must be described operation-by-operation, not as generic
+  verified linear algebra.
+- Legacy fixture/conformance directories may use historical names such as
+  `calculus` or `symbolic_calculus`; directory names do not broaden the public
+  mathematical claim.
+- Do not advertise a live registry capability that does not exist.
 
 ---
 
-## Capability naming notes
+## Benchmark interpretation
+
+The frozen ideal-membership release corpus is a **release conformance and
+assurance-regression corpus**. It is useful for deterministic implementation
+checks, mutation testing, answer/evidence separation, and observed false-accept
+behavior on that corpus.
+
+It does **not** by itself establish a population false-accept probability,
+universal solver soundness, broad mathematical generalization, or formal
+checker soundness. Formal assurance comes from the declared checker/soundness
+argument within its exact scope; empirical suites test the implementation and
+integration of that argument.
+
+The critical failure cell remains:
 
-- Public calculus capability ID: **`algebra.formal_rational_calculus`**.
-- Analytic calculus capability ID: **`analysis.analytic_calculus`** (separate;
-  whitelist only; exact ODE empty-obligation single-IC).
-- Ideal membership capability ID: **`algebra.ideal_membership_witness`**.
-- Legacy schema and conformance paths may still use `symbolic_calculus` /
-  `calculus` directory names; those are wire/fixture names, not analytic claims.
-- Do not advertise a live `analysis.symbolic_calculus` registry ID.
+> answer incorrect + evidence verified
+
+Any such deterministic release-corpus event is a release blocker.
 
 ---
 
-## Forensic suite
+## Release truth rule
+
+For a release claim, prefer evidence in this order:
+
+1. the mathematical proposition actually established;
+2. executable checker/verifier implementation;
+3. adversarial and contract tests;
+4. exact-SHA CI / replay evidence;
+5. machine-readable capability and maturity registry;
+6. current status documentation;
+7. historical audits and roadmap labels.
 
-Trust regressions live under `tests/forensic/`. They assert correct trust
-behavior (binding, path rejection, registry/API honesty, and related cases).
-A green forensic suite does **not** by itself authorize `"status": "stable"`.
+Documentation cannot strengthen a weaker checker.
diff --git a/docs/validation/remaining-spec-matrix.md b/docs/validation/remaining-spec-matrix.md
index 602d420c..2d608156 100644
--- a/docs/validation/remaining-spec-matrix.md
+++ b/docs/validation/remaining-spec-matrix.md
@@ -4,21 +4,22 @@ Maps every [PROJECT_SPEC §21](../PROJECT_SPEC.md) DoD row and every
 [DELIVERY_ROADMAP](../DELIVERY_ROADMAP.md) milestone exit criterion to an
 in-repo artifact path or `OPEN`.
 
-**Authority:** [`docs/security/KNOWN_TRUST_GAPS.md`](../security/KNOWN_TRUST_GAPS.md) and
-[`STATUS.md`](../STATUS.md) supersede optimistic labels when they conflict.
-Do not invent human confirmations. Capabilities remain
-`"status": "experimental"` until
+**Authority:** [`docs/security/KNOWN_TRUST_GAPS.md`](../security/KNOWN_TRUST_GAPS.md),
+[`STATUS.md`](../STATUS.md), the capability registry, and exact-head CI supersede
+optimistic historical labels when they conflict. Do not invent human
+confirmations. Capabilities remain `"status": "experimental"` until
 [stable-capability-checklist.md](stable-capability-checklist.md) is fully
 checked with real artifacts.
 
 **Status labels (historical engineering-artifact records)**
 
 These `MET` / `PARTIAL` / `OPEN` cells describe whether a qualifying
-implementation artifact existed for the §21 / roadmap row as written. They are
+implementation artifact exists for the §21 / roadmap row as written. They are
 **not** theorem-level Certification Record eligibility. Current CR authority is
-[`registry/maturity-inventory.json`](../../registry/maturity-inventory.json)
-and PR #53 / post-repair semantics in [`STATUS.md`](../STATUS.md). Dated audit
-files under `docs/audits/` are left unchanged.
+[`registry/maturity-inventory.json`](../../registry/maturity-inventory.json),
+capability-specific assurance policy, and the release gates described in
+[`STATUS.md`](../STATUS.md). Dated audit files under `docs/audits/` are retained
+as history, not silently upgraded to current authority.
 
 - `MET` — qualifying engineering artifact exists and matches the row as written.
 - `PARTIAL` — some required artifact exists; gaps listed.
@@ -32,14 +33,14 @@ Local `just check` ≠ attested immutable CI green on a release commit.
 
 | Row | Criterion | Status | Artifact path or OPEN |
 | --- | --- | --- | --- |
-| §21.1 | Rational-function equality works end to end through Mathematica and one open backend | PARTIAL — protocol reference | Dual adapters (`adapters/sympy/`, `adapters/mathematica/`). Not proof of indispensable external search (`externalSearchEssential: false`). Capability **experimental**. |
+| §21.1 | Rational-function equality works end to end through Mathematica and one open backend | PARTIAL — protocol reference | Dual adapters (`adapters/sympy/`, `adapters/mathematica/`). Not proof of indispensable external search. Capability **experimental**. |
 | §21.2 | Same Lean checker accepts both evidence formats after adapter normalization | MET (eng) | `MathEvidence/Checkers/RationalEquality/` + conformance fixtures. |
 | §21.3 | All side conditions are explicit | MET (eng) | RFC/schemas; coverage⇒Defined bridge for ℚ present in checker soundness path. |
-| §21.4 | Every example rechecks offline with backends unavailable | MET (eng) | Offline packaging + Lean request digest recompute from claim payload. |
+| §21.4 | Every example rechecks offline with backends unavailable | PARTIAL | Offline bundle integrity/regeneration is implemented and tamper-tested. Offline **kernel theorem execution** is now tracked separately and is not claimed as a release-wide maturity property; see `STATUS.md`. |
 | §21.5 | Request/certificate mismatch and malformed evidence are rejected | MET (eng) | Conformance + forensic binding/forgery suites under `tests/forensic/`. |
-| §21.6 | Lean package contains no forbidden axioms or incomplete proofs | PARTIAL | Regex audits (`scripts/audit_sorry_axioms.py`); compiled axiom/import audits still desired. |
+| §21.6 | Lean package contains no forbidden axioms or incomplete proofs | MET (eng) | Source audits plus `mathevidence-import-graph` / `mathevidence-axiom-report` environment-level drivers and `lean-assurance-audit` CI. |
 | §21.7 | Capability discoverable through registry and Agent API | MET (eng) | Registry + Agent; public API is `bundleId`-only; registry-driven dispatch. |
-| §21.8 | Benchmark includes real and adversarial tasks | MET (eng) | Suites under `benchmarks/` + `tests/forensic/`. |
+| §21.8 | Benchmark includes real and adversarial tasks | MET (eng) | Frozen release conformance/regression suites under `benchmarks/` + adversarial/forensic suites. External held-out validation remains separate. |
 | §21.9 | User can invoke one stable tactic and receive precise status reporting | PARTIAL | Tactic remains **experimental**; theorem-producing rational replay exists — not a `stable` claim. |
 | §21.10 | At least one external Lean contributor or project confirms a real workflow problem | OPEN | Template: `docs/validation/workflow-win-log.md` (0 entries). Do not invent. |
 
@@ -61,10 +62,12 @@ Local `just check` ≠ attested immutable CI green on a release commit.
 | Exit criterion | Status | Artifact |
 | --- | --- | --- |
 | Two backends share one checker | MET (eng) | SymPy + Mathematica → `MathEvidence.Checkers.RationalEquality` |
-| Offline replay | MET (eng) | `just replay`, `evidence/examples/`, `evidence/conformance/rfc0001/` |
-| Side conditions / mismatch reject / no forbidden axioms | See §21.3–§21.6 | |
+| Offline replay | PARTIAL | Offline bundle replay is implemented; offline kernel replay is a distinct stronger maturity field and is currently false in the authoritative inventory. |
+| Side conditions / mismatch reject / no forbidden axioms | MET (eng) | See §21.3, §21.5, and §21.6. |
 
-Evidence Bundle trees for full bundles use schema **v0.2** (`.cjson`).
+Candidate Bundle trees use `bundleVersion: 0.3.0` with canonical `.cjson`
+encoding. Schema v0.2 remains accepted only for historical canonical bundles;
+it is not the current Candidate Bundle protocol version.
 
 ---
 
@@ -73,7 +76,7 @@ Evidence Bundle trees for full bundles use schema **v0.2** (`.cjson`).
 | Exit criterion | Status | Artifact |
 | --- | --- | --- |
 | Common core remains small | MET (eng) | Core + LA/CEX checkers and conformance |
-| No unsafe generic escape hatch | MET | Domain-specific IR/checkers |
+| No unsafe generic escape hatch | MET | Domain-specific IR/checkers; exact generators use typed replay IR |
 | Agent held-out improvement | MET (eng) | `benchmarks/agent/held_out/`, `just agent-held-out` |
 | External Lean project adoption | OPEN | `docs/validation/adoption-log.md` (0 entries) |
 | First Agent API release | MET (eng) | Agent API **v0.1.0** (`agent/api/openapi.yaml`, `agent/CHANGELOG.md`) |
@@ -85,7 +88,7 @@ Evidence Bundle trees for full bundles use schema **v0.2** (`.cjson`).
 | Exit criterion | Status | Artifact |
 | --- | --- | --- |
 | Repaired statements pass semantic expert review | OPEN | Unsigned packets under `docs/validation/review-packets/` |
-| Weaker variants receive certified counterexamples where claimed | MET (eng) | Lean + Agent lattice/CEX paths; product spec `docs/products/03_HYPOTHESIS_SYNTHESIS.md` |
+| Weaker variants receive certified counterexamples where claimed | MET (eng) | Exact CEX path uses outcome `refuted`; product spec `docs/products/03_HYPOTHESIS_SYNTHESIS.md` |
 | Minimality never asserted without proof | MET (eng) | Agent tests assert `claimsMinimal is False` |
 
 ---
@@ -97,17 +100,21 @@ Evidence Bundle trees for full bundles use schema **v0.2** (`.cjson`).
 | Interoperability without replacing specialized checkers | PARTIAL | Federated registry entries + `docs/architecture/collaboration-cslib-lean-auto-smt.md` |
 | ≥2 projects consume or emit shared metadata | OPEN (live) / PARTIAL (fixture) | Ledger: `docs/architecture/federation-agreements.md`; fixtures under `evidence/federation/` |
 
+Federated SAT/PB/SMT metadata is not exact-CR eligible in this repository.
+
 ---
 
 ## Milestone 5 — Symbolic / formal calculus
 
 | Exit criterion | Status | Artifact |
 | --- | --- | --- |
-| Repeated evidence patterns | PARTIAL | `evidence/conformance/symbolic_calculus/` (fixture path name); capability id `algebra.formal_rational_calculus` |
-| Branch/singularity conditions explicit | MET (eng) | Capability admissibility + schemas |
-| Candidate ≠ completeness | MET (eng) | Claim classes + checker package |
+| Repeated evidence patterns | PARTIAL | `evidence/conformance/symbolic_calculus/` is a historical fixture path name; capability id is `algebra.formal_rational_calculus`. |
+| Branch/singularity conditions explicit | MET (eng) | Capability admissibility + schemas for supported forms. |
+| Candidate ≠ completeness | MET (eng) | Claim classes + checker package; candidate-only requests remain evidence-only. |
 
-Analytic Mathlib calculus is a separate experimental id: `analysis.analytic_calculus`.
+Analytic Mathlib calculus is a separate experimental id:
+`analysis.analytic_calculus`. It is a strict theorem-form whitelist, not a claim
+of arbitrary analytic-calculus automation.
 
 ---
 
@@ -130,15 +137,19 @@ Analytic Mathlib calculus is a separate experimental id: `analysis.analytic_calc
 | `logic.finite_counterexample` | `conformance_verified` | `live_generator_complete` (gated) | `live_generator_complete` (gated) |
 | `algebra.formal_rational_calculus` | `conformance_verified` | `live_generator_complete` (derivative/antiderivative gated) | n/a |
 
-Supported Mathematica live transport: `MATHEVIDENCE_WOLFRAMSCRIPT` → wolframscript.
-LeanLink native bridge remains deferred.
+Supported Mathematica live transport: `MATHEVIDENCE_WOLFRAMSCRIPT` →
+`wolframscript`. LeanLink native bridge remains deferred.
 
 ---
 
 ## Governance packaging (humans OPEN)
 
 Engineering may be packaging-ready; humans are not. See
-[`stable-capability-checklist.md`](stable-capability-checklist.md).
+[`stable-capability-checklist.md`](stable-capability-checklist.md). The
+`semanticReview` / `trustReview` registry fields belong to **stable-promotion
+human review**, not to the mechanical exact-candidate CR gate for this
+experimental preview; absent values must never be presented as completed
+review.
 
 | Gate | Status | Artifact when closed |
 | --- | --- | --- |
diff --git a/registry/capabilities/algebra.rational_equality.json b/registry/capabilities/algebra.rational_equality.json
index a41b31dd..1e0c220f 100644
--- a/registry/capabilities/algebra.rational_equality.json
+++ b/registry/capabilities/algebra.rational_equality.json
@@ -17,7 +17,7 @@
     "leanPackage": "MathEvidence.IR.RationalExpr"
   },
   "admissibility": {
-    "summary": "Rational expressions over \u211a with explicit division; transcendentals and approximate numerals rejected.",
+    "summary": "Rational expressions over ℚ with explicit division; transcendentals and approximate numerals rejected.",
     "rejectedConstructs": [
       "transcendentals",
       "conditionals",
@@ -63,10 +63,10 @@
   },
   "knownLimitations": [
     "PROTOCOL REFERENCE ONLY: external search is not essential; Lean can close equalities via field_simp/ring independently of backend output (docs/security/KNOWN_TRUST_GAPS.md).",
-    "P0 trust gaps open at audit baseline: live digest substitution, offline digest trust, coverage\u2260Defined (docs/security/KNOWN_TRUST_GAPS.md).",
+    "The checker, soundness theorem, bridge, and exact-source generator remain available, but theorem-level Certification Record promotion is disabled for the pinned Lean 4.14 public preview because the candidate-specific checker proposition does not elaborate on the production native-reduction path without an unacceptable sorryAx dependency.",
     "Equality is established only under explicit nonzero denominator conditions.",
     "Does not claim identity at poles or under totalized field conventions.",
-    "Status remains experimental; stable promotion blocked until P0 trust path + human gates ME-401\u2013408 close.",
+    "Status remains experimental; lifecycle promotion is separate from mechanical checker availability.",
     "Transcendentals, conditionals, and approximate numerals are rejected.",
     "Dual-backend evidence: SymPy live (conformance_verified) + Mathematica live_generator_complete via wolframscript when MATHEVIDENCE_WOLFRAMSCRIPT is set (public CI without Wolfram remains offline fixtures / differential skip-fixture). Sage is deliberately NOT advertised for rational equality (spec 05: implement+conformance or remove)."
   ],
@@ -120,37 +120,28 @@
   "semanticReview": "absent",
   "trustReview": "absent",
   "assurancePolicy": {
-    "supportedAssuranceModes": [
-      "kernel_replay"
-    ],
+    "supportedAssuranceModes": [],
     "exactBinding": {
-      "supported": true,
-      "generatorId": "mathevidence.exact_rational_equality",
-      "generatorVersion": "0.1.0",
-      "grammarVersion": "0.1.0",
-      "generatorPath": "scripts/generate_exact_rational_equality_replay_module.py",
-      "verifier": "mathevidence-declaration-identity"
+      "supported": false
     },
     "replay": {
       "backend": "exact_generator",
       "offlineSupported": true
     },
     "certification": {
-      "allowedOutcomes": [
-        "proved"
-      ],
-      "crEligible": true
+      "allowedOutcomes": [],
+      "crEligible": false
     },
     "maturity": {
       "adapterExists": true,
       "checkerExists": true,
       "leanSoundnessExists": true,
       "bridgeReplayExists": true,
-      "exactCandidateBindingExists": true,
+      "exactCandidateBindingExists": false,
       "offlineReplayExists": true
     },
     "limitations": [
-      "CR eligibility enabled after local Lean exact-replay E2E (named-def renderer + Lake path fixes).",
+      "The pinned Lean 4.14 production path fails closed for candidate-specific theorem Certification Records; checker/soundness/bridge functionality remains available without theorem promotion.",
       "OfflineFixtures remain protocol self-tests and are not Certification Record authority.",
       "Canonical rationals: int num, strictly positive den, gcd-normalized, zero as 0/1. Floats rejected in exact mode."
     ]
diff --git a/registry/maturity-inventory.json b/registry/maturity-inventory.json
index b1cf24b4..c6d35253 100644
--- a/registry/maturity-inventory.json
+++ b/registry/maturity-inventory.json
@@ -1,8 +1,8 @@
 {
-  "schemaVersion": "0.1.0",
-  "statusAsOfCommit": "30522d70e9be0f3fda9b9b6febc7502b9ef4c34b",
+  "schemaVersion": "0.2.0",
+  "statusAsOfCommit": "d7192f749aa54481bf979e84be1498b29abd2c55",
   "program": "exact-candidate-binding",
-  "note": "Exact-candidate-binding baseline pin 30522d70. CR-eligible: ideal, rational_equality, linear_algebra (4 ops), finite_counterexample (refuted), formal_rational_calculus (4 ops soundResult), analytic_calculus (Deriv/DerivWithin/Antideriv/ODE).",
+  "note": "Audited capability baseline is main@d7192f74. Final release commit/tree is bound separately by the release provenance manifest. offline_replay_exists is retained only as a compatibility alias for offline_bundle_replay_exists; offline kernel theorem execution is tracked independently.",
   "capabilities": [
     {
       "id": "algebra.ideal_membership_witness",
@@ -13,6 +13,8 @@
       "bridge_replay_exists": true,
       "exact_candidate_binding_exists": true,
       "offline_replay_exists": true,
+      "offline_bundle_replay_exists": true,
+      "offline_kernel_replay_exists": false,
       "cr_eligible": true,
       "trusted_backend": "lean_kernel",
       "supported_assurance_modes": [
@@ -31,9 +33,9 @@
         "verifier": "mathevidence-declaration-identity"
       },
       "known_limitations": [
-        "CR eligibility enabled after local Lean exact-replay E2E ladder; OfflineFixtures are not Certification Record authority.",
+        "CR eligibility requires candidate-bound Lean exact replay; OfflineFixtures are not Certification Record authority.",
         "Witness identity only: no Groebner, non-membership, radical, or completeness claim.",
-        "Offline exact bundle may still report theorem_pending for Lean inspect; online kernel_replay is the promotion path."
+        "Offline bundle replay exists; offline kernel replay is not yet a required release maturity gate."
       ]
     },
     {
@@ -43,27 +45,21 @@
       "checker_exists": true,
       "lean_soundness_exists": true,
       "bridge_replay_exists": true,
-      "exact_candidate_binding_exists": true,
+      "exact_candidate_binding_exists": false,
       "offline_replay_exists": true,
-      "cr_eligible": true,
+      "offline_bundle_replay_exists": true,
+      "offline_kernel_replay_exists": false,
+      "cr_eligible": false,
       "trusted_backend": "lean_kernel",
-      "supported_assurance_modes": [
-        "kernel_replay"
-      ],
-      "allowed_certification_outcomes": [
-        "proved"
-      ],
+      "supported_assurance_modes": [],
+      "allowed_certification_outcomes": [],
       "exactBinding": {
-        "supported": true,
-        "generatorId": "mathevidence.exact_rational_equality",
-        "generatorVersion": "0.1.0",
-        "grammarVersion": "0.1.0",
-        "generatorPath": "scripts/generate_exact_rational_equality_replay_module.py",
-        "verifier": "mathevidence-declaration-identity"
+        "supported": false
       },
       "known_limitations": [
-        "CR eligibility enabled after local Lean exact-replay E2E; OfflineFixtures are not Certification Record authority.",
-        "Canonical rationals: int num, strictly positive den, gcd-normalized, zero as 0/1."
+        "Checker, soundness theorem, bridge, and exact-source generation remain available, but theorem-level Certification Record promotion is disabled for the pinned Lean 4.14 public preview because the candidate-specific checker proposition cannot be admitted on the production native-reduction path without an unacceptable sorryAx dependency.",
+        "Canonical rationals: int num, strictly positive den, gcd-normalized, zero as 0/1.",
+        "Offline bundle replay exists; offline kernel replay is not claimed as a release maturity property."
       ]
     },
     {
@@ -75,6 +71,8 @@
       "bridge_replay_exists": true,
       "exact_candidate_binding_exists": true,
       "offline_replay_exists": true,
+      "offline_bundle_replay_exists": true,
+      "offline_kernel_replay_exists": false,
       "cr_eligible": true,
       "trusted_backend": "lean_kernel",
       "supported_assurance_modes": [
@@ -92,8 +90,9 @@
         "verifier": "mathevidence-declaration-identity"
       },
       "known_limitations": [
-        "CR eligibility enabled after local Lean exact-replay E2E for inverse_witness, system_solution, kernel_vector, and det_identity.",
-        "Exact int/rational entries only; numerical LA is a different evidence class."
+        "CR eligibility is operation-scoped to exact-enabled inverse_witness, system_solution, kernel_vector, and det_identity.",
+        "Exact int/rational entries only; numerical LA is a different evidence class.",
+        "Offline bundle replay exists; offline kernel replay is not yet a required release maturity gate."
       ]
     },
     {
@@ -105,6 +104,8 @@
       "bridge_replay_exists": true,
       "exact_candidate_binding_exists": true,
       "offline_replay_exists": true,
+      "offline_bundle_replay_exists": true,
+      "offline_kernel_replay_exists": false,
       "cr_eligible": true,
       "trusted_backend": "lean_kernel",
       "supported_assurance_modes": [
@@ -123,7 +124,8 @@
       },
       "known_limitations": [
         "Exact witness binding yields outcome polarity refuted (never proved).",
-        "CR eligibility enabled after local Lean exact-replay E2E."
+        "Failure to find a witness is not a proof of the universal claim.",
+        "Offline bundle replay exists; offline kernel replay is not yet a required release maturity gate."
       ]
     },
     {
@@ -135,6 +137,8 @@
       "bridge_replay_exists": true,
       "exact_candidate_binding_exists": true,
       "offline_replay_exists": true,
+      "offline_bundle_replay_exists": true,
+      "offline_kernel_replay_exists": false,
       "cr_eligible": true,
       "trusted_backend": "lean_kernel",
       "supported_assurance_modes": [
@@ -152,9 +156,9 @@
         "verifier": "mathevidence-declaration-identity"
       },
       "known_limitations": [
-        "Formal/algebraic only; not analytic HasDerivAt.",
-        "CR eligibility enabled after local Lean exact-replay E2E for derivative/antiderivative/recurrence/ODE with soundResult claims.",
-        "Candidate-only requests remain evidence-only."
+        "Formal/algebraic only; not general analytic HasDerivAt semantics.",
+        "CR eligibility is restricted to the exact registered soundResult operations; candidate-only requests remain evidence-only.",
+        "Offline bundle replay exists; offline kernel replay is not yet a required release maturity gate."
       ]
     },
     {
@@ -166,6 +170,8 @@
       "bridge_replay_exists": true,
       "exact_candidate_binding_exists": true,
       "offline_replay_exists": true,
+      "offline_bundle_replay_exists": true,
+      "offline_kernel_replay_exists": false,
       "cr_eligible": true,
       "trusted_backend": "lean_kernel",
       "supported_assurance_modes": [
@@ -183,9 +189,9 @@
         "verifier": "mathevidence-declaration-identity"
       },
       "known_limitations": [
-        "Analytic calculus whitelist only: checkDeriv_sound, checkDerivWithin_sound, checkAntideriv_sound, checkODE_sound.",
-        "CR eligibility enabled after local Lean exact-replay E2E for Deriv / DerivWithin / Antideriv / ODE (empty-obligation single-IC ODE).",
-        "Exact ODE currently requires empty domain obligations and at most one initial condition; multi-IC / obligation-bearing ODE fail closed."
+        "Analytic calculus is a strict theorem-form whitelist, not arbitrary analysis.",
+        "Exact ODE currently requires empty domain obligations and at most one initial condition; unsupported forms fail closed.",
+        "Offline bundle replay exists; offline kernel replay is not yet a required release maturity gate."
       ]
     },
     {
@@ -197,6 +203,8 @@
       "bridge_replay_exists": false,
       "exact_candidate_binding_exists": false,
       "offline_replay_exists": false,
+      "offline_bundle_replay_exists": false,
+      "offline_kernel_replay_exists": false,
       "cr_eligible": false,
       "trusted_backend": "external",
       "supported_assurance_modes": [],
@@ -218,6 +226,8 @@
       "bridge_replay_exists": false,
       "exact_candidate_binding_exists": false,
       "offline_replay_exists": false,
+      "offline_bundle_replay_exists": false,
+      "offline_kernel_replay_exists": false,
       "cr_eligible": false,
       "trusted_backend": "external",
       "supported_assurance_modes": [],
@@ -239,6 +249,8 @@
       "bridge_replay_exists": false,
       "exact_candidate_binding_exists": false,
       "offline_replay_exists": false,
+      "offline_bundle_replay_exists": false,
+      "offline_kernel_replay_exists": false,
       "cr_eligible": false,
       "trusted_backend": "external",
       "supported_assurance_modes": [],
diff --git a/schemas/maturity-inventory.schema.json b/schemas/maturity-inventory.schema.json
index 91286262..b294b0bd 100644
--- a/schemas/maturity-inventory.schema.json
+++ b/schemas/maturity-inventory.schema.json
@@ -1,8 +1,8 @@
 {
   "$schema": "https://json-schema.org/draft/2020-12/schema",
-  "$id": "https://mathevidence.org/schemas/maturity-inventory-v0.json",
+  "$id": "https://mathevidence.org/schemas/maturity-inventory-v0.2.json",
   "title": "MathEvidence Assurance Maturity Inventory",
-  "description": "Machine-readable answer to: what can each adapter-exposed capability prove today, and may that result mint a Certification Record? Independent booleans are not implied by each other. cr_eligible never follows from checker or fixture existence.",
+  "description": "Machine-readable answer to: what can each adapter-exposed capability prove today, and may that result mint a Certification Record? Independent booleans are not implied by each other. cr_eligible never follows from checker or fixture existence. Offline bundle replay and offline kernel theorem execution are distinct maturity dimensions.",
   "type": "object",
   "additionalProperties": false,
   "required": [
@@ -14,12 +14,12 @@
   "properties": {
     "schemaVersion": {
       "type": "string",
-      "const": "0.1.0"
+      "const": "0.2.0"
     },
     "statusAsOfCommit": {
       "type": "string",
       "pattern": "^[0-9a-f]{40}$",
-      "description": "Git commit this inventory describes"
+      "description": "Audited baseline Git commit whose capability state this inventory describes. A release manifest binds the inventory hash to the actual release commit/tree."
     },
     "program": {
       "type": "string",
@@ -49,6 +49,8 @@
         "bridge_replay_exists",
         "exact_candidate_binding_exists",
         "offline_replay_exists",
+        "offline_bundle_replay_exists",
+        "offline_kernel_replay_exists",
         "cr_eligible",
         "exactBinding",
         "known_limitations"
@@ -67,7 +69,18 @@
         "lean_soundness_exists": { "type": "boolean" },
         "bridge_replay_exists": { "type": "boolean" },
         "exact_candidate_binding_exists": { "type": "boolean" },
-        "offline_replay_exists": { "type": "boolean" },
+        "offline_replay_exists": {
+          "type": "boolean",
+          "description": "Compatibility alias for offline_bundle_replay_exists. It does not mean the Lean theorem was re-executed offline."
+        },
+        "offline_bundle_replay_exists": {
+          "type": "boolean",
+          "description": "A sealed candidate replay bundle can be regenerated/validated without consulting the untrusted solver or the network after materialization."
+        },
+        "offline_kernel_replay_exists": {
+          "type": "boolean",
+          "description": "Release CI requires successful offline Lean/kernel theorem execution of a sealed candidate bundle; setup failure does not count as success."
+        },
         "cr_eligible": { "type": "boolean" },
         "trusted_backend": { "type": "string" },
         "supported_assurance_modes": {
diff --git a/scripts/ci/install-lean-pinned.sh b/scripts/ci/install-lean-pinned.sh
new file mode 100644
index 00000000..520c28fd
--- /dev/null
+++ b/scripts/ci/install-lean-pinned.sh
@@ -0,0 +1,114 @@
+#!/usr/bin/env bash
+# Exact Lean 4.14.0 CI bootstrap from the official leanprover/lean4 release asset.
+#
+# This transport path avoids releases.lean-lang.org, whose TLS endpoint has
+# repeatedly failed before project code can run. The source is pinned by:
+#   tag:        v4.14.0
+#   tag commit: 410fab7284703f41660ca2454218dcca9b2ec896
+#   asset id:   210336963
+#   asset name: lean-4.14.0-linux.tar.zst
+#   byte size:  249860945
+#   sha256:     320f18e7d58271d95fced740522b5a5ed41b85b2af5bf0e8ab9a8dbc380e450a
+#
+# The SHA-256 was observed from the exact official GitHub release asset after
+# independently checking asset id/name/size, archive integrity, extracted Lean
+# version, and the upstream v4.14.0 tag commit. CI fails closed on any mismatch.
+set -euo pipefail
+
+LEAN_VERSION="4.14.0"
+LEAN_TOOLCHAIN="leanprover/lean4:v${LEAN_VERSION}"
+LEAN_TAG_COMMIT="410fab7284703f41660ca2454218dcca9b2ec896"
+LEAN_ASSET_ID="210336963"
+LEAN_ASSET_NAME="lean-${LEAN_VERSION}-linux.tar.zst"
+LEAN_ASSET_SIZE="249860945"
+LEAN_ASSET_URL="https://api.github.com/repos/leanprover/lean4/releases/assets/${LEAN_ASSET_ID}"
+LEAN_SHA256="320f18e7d58271d95fced740522b5a5ed41b85b2af5bf0e8ab9a8dbc380e450a"
+
+repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)"
+actual_toolchain="$(tr -d '\r\n' < "${repo_root}/lean-toolchain")"
+if [[ "$actual_toolchain" != "$LEAN_TOOLCHAIN" ]]; then
+  echo "lean-toolchain mismatch: got '$actual_toolchain', expected '$LEAN_TOOLCHAIN'" >&2
+  exit 1
+fi
+
+tmpdir="$(mktemp -d)"
+trap 'rm -rf "$tmpdir"' EXIT
+archive="${tmpdir}/${LEAN_ASSET_NAME}"
+extract_root="${tmpdir}/extract"
+mkdir -p "$extract_root"
+
+retry_download() {
+  local attempt
+  for attempt in 1 2 3; do
+    if curl \
+      --fail \
+      --location \
+      --silent \
+      --show-error \
+      --connect-timeout 20 \
+      --max-time 900 \
+      -H 'Accept: application/octet-stream' \
+      -H 'X-GitHub-Api-Version: 2022-11-28' \
+      "$LEAN_ASSET_URL" \
+      -o "$archive"; then
+      return 0
+    fi
+    rm -f "$archive"
+    if [[ "$attempt" -eq 3 ]]; then
+      echo "official Lean release asset download failed after ${attempt} attempts" >&2
+      return 1
+    fi
+    sleep_seconds=$((5 * (2 ** (attempt - 1))))
+    echo "Lean asset download attempt ${attempt} failed; retrying in ${sleep_seconds}s" >&2
+    sleep "$sleep_seconds"
+  done
+}
+
+retry_download
+
+actual_size="$(stat -c '%s' "$archive")"
+if [[ "$actual_size" != "$LEAN_ASSET_SIZE" ]]; then
+  echo "Lean asset size mismatch: got ${actual_size}, expected ${LEAN_ASSET_SIZE}" >&2
+  exit 1
+fi
+
+observed_sha256="$(sha256sum "$archive" | awk '{print $1}')"
+echo "MATHEVIDENCE_LEAN_ASSET_ID=${LEAN_ASSET_ID}"
+echo "MATHEVIDENCE_LEAN_ASSET_SIZE=${actual_size}"
+echo "MATHEVIDENCE_LEAN_ASSET_SHA256=${observed_sha256}"
+if [[ "$observed_sha256" != "$LEAN_SHA256" ]]; then
+  echo "Lean asset SHA-256 mismatch: got ${observed_sha256}, expected ${LEAN_SHA256}" >&2
+  exit 1
+fi
+
+# Verify compressed-stream integrity before extraction.
+zstd --test "$archive" >/dev/null
+
+tar --zstd -xf "$archive" -C "$extract_root"
+toolchain_dir="${extract_root}/lean-${LEAN_VERSION}-linux"
+if [[ ! -x "${toolchain_dir}/bin/lean" || ! -x "${toolchain_dir}/bin/lake" ]]; then
+  echo "official Lean release archive layout is not the expected linux distribution" >&2
+  find "$extract_root" -maxdepth 2 \( -type f -o -type d \) >&2 || true
+  exit 1
+fi
+
+lean_version="$(${toolchain_dir}/bin/lean --version)"
+lake_version="$(${toolchain_dir}/bin/lake --version)"
+printf '%s\n' "$lean_version"
+printf '%s\n' "$lake_version"
+if [[ "$lean_version" != *"version ${LEAN_VERSION}"* ]]; then
+  echo "extracted Lean version mismatch: $lean_version" >&2
+  exit 1
+fi
+
+install_root="${HOME}/.local/share/mathevidence/lean-${LEAN_VERSION}-linux"
+rm -rf "$install_root"
+mkdir -p "$(dirname "$install_root")"
+mv "$toolchain_dir" "$install_root"
+
+if [[ -n "${GITHUB_PATH:-}" ]]; then
+  echo "${install_root}/bin" >> "$GITHUB_PATH"
+fi
+
+echo "MATHEVIDENCE_LEAN_TAG_COMMIT=${LEAN_TAG_COMMIT}"
+echo "MATHEVIDENCE_LEAN_BIN=${install_root}/bin/lean"
diff --git a/scripts/ci/probe_rational_native_compile.py b/scripts/ci/probe_rational_native_compile.py
new file mode 100644
index 00000000..bf508f7a
--- /dev/null
+++ b/scripts/ci/probe_rational_native_compile.py
@@ -0,0 +1,192 @@
+#!/usr/bin/env python3
+"""Diagnostic-only probe for staged rational native reduction.
+
+This script never emits or accepts a Certification Record. It tests the exact
+Lean 4.14 boundary required by ``Lean.reduceBool``: candidate-specific closed
+Boolean computations are elaborated first as an imported module, then a second
+theorem module consumes those imported constants through ``Lean.ofReduceBool``.
+Production acceptance remains owned by ``run_cr_exact_lean_e2e_production.py``
+and ``kernel_replay._compile_and_inspect``.
+"""
+
+from __future__ import annotations
+
+import importlib.util
+import json
+from pathlib import Path
+import sys
+
+import adapters.common.exact_replay.plugins  # noqa: F401
+from adapters.common.exact_replay.pipeline import generate_module, verify
+from adapters.common.kernel_replay import _run_process, find_lake
+
+ROOT = Path(__file__).resolve().parents[2]
+RUNNER_PATH = ROOT / "scripts" / "ci" / "run_cr_exact_lean_e2e_production.py"
+RUNNER_MODULE = "mathevidence_native_compile_probe_runner"
+BASE_MODULE = "MathEvidence.Generated.Replay.probe_rational_native_compile"
+COMPUTE_MODULE = f"{BASE_MODULE}Compute"
+THEOREM_MODULE = f"{BASE_MODULE}Theorem"
+DECL = "probe_rational_native_compile"
+
+
+def _load_runner():
+    spec = importlib.util.spec_from_file_location(RUNNER_MODULE, RUNNER_PATH)
+    if spec is None or spec.loader is None:
+        raise RuntimeError(f"cannot load production runner from {RUNNER_PATH}")
+    module = importlib.util.module_from_spec(spec)
+    previous = sys.modules.get(RUNNER_MODULE)
+    sys.modules[RUNNER_MODULE] = module
+    try:
+        spec.loader.exec_module(module)
+    except BaseException:
+        if previous is None:
+            sys.modules.pop(RUNNER_MODULE, None)
+        else:
+            sys.modules[RUNNER_MODULE] = previous
+        raise
+    return module, previous
+
+
+def _staged_sources(source: str) -> tuple[str, str]:
+    marker = "/-- Lean-side equality between reconstructed wire binding and submitted digest."
+    if marker not in source:
+        raise RuntimeError("expected rational request-binding marker not found")
+    prefix = source.split(marker, 1)[0]
+    compute = (
+        prefix
+        + f"""/-- Closed candidate-specific request-binding computation. -/\ndef {DECL}_binding_bool : Bool :=\n  decide ({DECL}_req.requestDigest = {DECL}_cert.requestDigest)\n\n/-- Closed candidate-specific checker proposition computation. -/\ndef {DECL}_checker_decide_bool : Bool :=\n  decide (checkBool {DECL}_req {DECL}_cert = true)\n"""
+    )
+    theorem = f"""/- Diagnostic theorem stage; never Certification Record authority. -/\nimport {COMPUTE_MODULE}\n\nopen MathEvidence.Core\nopen MathEvidence.IR.RationalExpr\nopen MathEvidence.Checkers.RationalEquality\n\n/-- Request digest is recomputed by Request.ofClaim! in the imported candidate module. -/\ntheorem {DECL}_request_binding :\n    {DECL}_req.requestDigest = {DECL}_cert.requestDigest :=\n  of_decide_eq_true\n    (Lean.ofReduceBool {DECL}_binding_bool true (Eq.refl true))\n\n/-- Candidate-specific semantic theorem from the independently evaluated checker. -/\ntheorem {DECL} : Claim.proposition {DECL}_req.claim {DECL}_cert.denomFactors := by\n  have hcheck : checkBool {DECL}_req {DECL}_cert = true :=\n    of_decide_eq_true\n      (Lean.ofReduceBool {DECL}_checker_decide_bool true (Eq.refl true))\n  exact replaySound {DECL}_req {DECL}_cert hcheck\n\n#print axioms {DECL}_request_binding\n#print axioms {DECL}\n"""
+    return compute, theorem
+
+
+def _path_for(module_name: str, suffix: str) -> Path:
+    return ROOT.joinpath(*module_name.split(".")).with_suffix(suffix)
+
+
+def _build_path(module_name: str, suffix: str) -> Path:
+    return (ROOT / ".lake" / "build" / "lib").joinpath(*module_name.split(".")).with_suffix(suffix)
+
+
+def main() -> int:
+    runner, previous = _load_runner()
+    try:
+        case = next(
+            item
+            for item in runner.matrix._cases()
+            if item.capability == "algebra.rational_equality"
+        )
+        request, certificate = runner._canonical_case_payload(case)
+        module = generate_module(
+            capability_id=case.capability,
+            request=request,
+            certificate=certificate,
+            candidate_bundle_digest=runner.BUNDLE_DIGEST,
+            module_name=BASE_MODULE,
+            declaration_name=DECL,
+        )
+        metadata = verify(module)
+        if not metadata.ok:
+            raise RuntimeError(f"generated module metadata failed: {metadata.detail}")
+        if f"Request.ofClaim! {DECL}_claim" not in module.source_text:
+            raise RuntimeError("probe source is not candidate-bound through Request.ofClaim!")
+        if "OfflineFixtures" in module.source_text:
+            raise RuntimeError("probe source unexpectedly references OfflineFixtures")
+
+        compute_source, theorem_source = _staged_sources(module.source_text)
+        if "Request.ofClaim!" not in compute_source:
+            raise RuntimeError("compute stage lost Lean-side request digest reconstruction")
+        if f"decide (checkBool {DECL}_req {DECL}_cert = true)" not in compute_source:
+            raise RuntimeError("compute stage does not decide the exact checker proposition")
+        if "Lean.ofReduceBool" not in theorem_source:
+            raise RuntimeError("theorem stage does not consume compiled Boolean constants")
+        if "native_decide" in theorem_source:
+            raise RuntimeError("theorem stage unexpectedly creates a fresh native_decide auxiliary")
+
+        lake = find_lake(ROOT)
+        if lake is None:
+            raise RuntimeError("lake unavailable")
+
+        compute_source_path = _path_for(COMPUTE_MODULE, ".lean")
+        theorem_source_path = _path_for(THEOREM_MODULE, ".lean")
+        compute_olean = _build_path(COMPUTE_MODULE, ".olean")
+        theorem_olean = _build_path(THEOREM_MODULE, ".olean")
+        compute_c = (ROOT / ".lake" / "build" / "ir").joinpath(
+            *COMPUTE_MODULE.split(".")
+        ).with_suffix(".c")
+        for path in (compute_source_path, theorem_source_path, compute_olean, theorem_olean, compute_c):
+            path.parent.mkdir(parents=True, exist_ok=True)
+            path.unlink(missing_ok=True)
+
+        compute_source_path.write_text(compute_source, encoding="utf-8", newline="\n")
+        theorem_source_path.write_text(theorem_source, encoding="utf-8", newline="\n")
+        compute_proc = None
+        theorem_proc = None
+        try:
+            compute_proc = _run_process(
+                [
+                    str(lake),
+                    "env",
+                    "lean",
+                    "-o",
+                    str(compute_olean),
+                    "-c",
+                    str(compute_c),
+                    str(compute_source_path),
+                ],
+                root=ROOT,
+            )
+            if compute_proc.returncode == 0:
+                theorem_proc = _run_process(
+                    [
+                        str(lake),
+                        "env",
+                        "lean",
+                        "-o",
+                        str(theorem_olean),
+                        str(theorem_source_path),
+                    ],
+                    root=ROOT,
+                )
+
+            report = {
+                "schemaVersion": "0.4.0",
+                "status": "diagnostic_only_non_authoritative",
+                "capability": case.capability,
+                "requestDigest": request["requestDigest"],
+                "generatedSourceHash": module.source_hash,
+                "probeTransformation": "precompile_decided_binding_and_checker_propositions_then_ofReduceBool",
+                "computeReturnCode": compute_proc.returncode,
+                "theoremReturnCode": None if theorem_proc is None else theorem_proc.returncode,
+                "computeOleanExists": compute_olean.is_file(),
+                "computeCExists": compute_c.is_file(),
+                "theoremOleanExists": theorem_olean.is_file(),
+                "computeStdoutTail": (compute_proc.stdout or "")[-2500:],
+                "computeStderrTail": (compute_proc.stderr or "")[-2500:],
+                "theoremStdoutTail": "" if theorem_proc is None else (theorem_proc.stdout or "")[-2500:],
+                "theoremStderrTail": "" if theorem_proc is None else (theorem_proc.stderr or "")[-2500:],
+            }
+            print(json.dumps(report, sort_keys=True))
+            if compute_proc.returncode != 0 or theorem_proc is None or theorem_proc.returncode != 0:
+                return 1
+            if not compute_olean.is_file() or not theorem_olean.is_file():
+                raise RuntimeError("staged probe reported success without both .olean files")
+            return 0
+        finally:
+            for path in (
+                compute_source_path,
+                theorem_source_path,
+                compute_olean,
+                theorem_olean,
+                compute_c,
+            ):
+                path.unlink(missing_ok=True)
+    finally:
+        if previous is None:
+            sys.modules.pop(RUNNER_MODULE, None)
+        else:
+            sys.modules[RUNNER_MODULE] = previous
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())
diff --git a/scripts/ci/run_cr_exact_lean_e2e.py b/scripts/ci/run_cr_exact_lean_e2e.py
new file mode 100644
index 00000000..fbac5ec8
--- /dev/null
+++ b/scripts/ci/run_cr_exact_lean_e2e.py
@@ -0,0 +1,458 @@
+"""Case/coverage matrix for exact-candidate Lean replay.
+
+The authoritative release executor is ``run_cr_exact_lean_e2e_production.py``.
+This module owns deterministic candidate fixtures and coverage checks derived
+from the machine-readable maturity inventory plus production operation/whitelist
+constants. Its standalone temporary-file Lean executor is diagnostic only and
+is not Certification Record or release authority.
+"""
+
+from __future__ import annotations
+
+import json
+import tempfile
+from dataclasses import dataclass
+from pathlib import Path
+from typing import Any
+
+import adapters.common.exact_replay.plugins  # noqa: F401
+from adapters.common.bounded_process import run_bounded
+from adapters.common.exact_replay.pipeline import generate_module, verify
+from adapters.common.exact_replay.plugins.analytic_calculus import WHITELIST_KINDS
+from adapters.common.exact_replay.plugins.formal_rational_calculus import (
+    OPERATIONS as FORMAL_OPERATIONS,
+)
+from adapters.common.exact_replay.plugins.linear_algebra import OPERATIONS as LA_OPERATIONS
+from adapters.common.limits import ResourceLimits
+from agent.api.assurance_policy import decide_exact_kernel_replay, load_assurance_policy
+
+ROOT = Path(__file__).resolve().parents[2]
+BUNDLE_DIGEST = "sha256:" + ("c" * 64)
+LIMITS = ResourceLimits(max_wall_time_ms=180_000, max_output_bytes=4_194_304)
+INVENTORY = ROOT / "registry" / "maturity-inventory.json"
+
+
+@dataclass(frozen=True)
+class ExactCase:
+    name: str
+    capability: str
+    form: str
+    request: dict[str, Any]
+    certificate: dict[str, Any]
+
+
+def _digest(char: str) -> str:
+    return "sha256:" + (char * 64)
+
+
+def _rat(num: str | int, den: str | int = "1") -> dict[str, Any]:
+    return {"tag": "rat", "num": str(num), "den": str(den)}
+
+
+def _matrix(rows: list[list[tuple[str | int, str | int]]]) -> dict[str, Any]:
+    return {
+        "tag": "matrix",
+        "rows": len(rows),
+        "cols": len(rows[0]),
+        "entries": [[_rat(num, den) for num, den in row] for row in rows],
+    }
+
+
+def _poly(var_count: int, coefficient: int, exponents: list[int]) -> dict[str, Any]:
+    return {
+        "varCount": var_count,
+        "terms": [{"coefficient": coefficient, "exponents": exponents}],
+    }
+
+
+def _provenance() -> dict[str, str]:
+    return {"backendId": "release-e2e", "adapterVersion": "0.1.0"}
+
+
+def _ideal_case() -> ExactCase:
+    request = {
+        "schemaVersion": "0.1.0",
+        "capability": "algebra.ideal_membership_witness",
+        "capabilityVersion": "0.1.0",
+        "target": _poly(2, 1, [1, 1]),
+        "generators": [_poly(2, 1, [1, 0]), _poly(2, 1, [0, 1])],
+        "requestedClaim": "witness",
+        "requestDigest": _digest("1"),
+    }
+    certificate = {
+        "schemaVersion": "0.1.0",
+        "capability": request["capability"],
+        "capabilityVersion": request["capabilityVersion"],
+        "requestDigest": request["requestDigest"],
+        "target": request["target"],
+        "generators": request["generators"],
+        "multipliers": [_poly(2, 1, [0, 1]), {"varCount": 2, "terms": []}],
+        "claimClass": "witness",
+    }
+    return ExactCase("ideal_membership", request["capability"], "witness", request, certificate)
+
+
+def _linear_cases() -> list[ExactCase]:
+    base = {
+        "schemaVersion": "0.1.0",
+        "capability": "algebra.linear_algebra",
+        "capabilityVersion": "0.1.0",
+        "resourcePolicy": {"maxWallTimeMs": 10000, "maxOutputBytes": 1048576},
+    }
+    cases: list[ExactCase] = []
+
+    request = {
+        **base,
+        "operation": "inverse_witness",
+        "matrix": _matrix([[("2", "1")]]),
+        "requestedClaim": "witness",
+        "requestDigest": _digest("3"),
+    }
+    cert = {
+        "schemaVersion": "0.1.0", "capability": base["capability"],
+        "capabilityVersion": base["capabilityVersion"], "requestDigest": request["requestDigest"],
+        "operation": "inverse_witness", "inverse": _matrix([[("1", "2")]]),
+        "provenance": _provenance(),
+    }
+    cases.append(ExactCase("linear_inverse", base["capability"], "inverse_witness", request, cert))
+
+    request = {
+        **base, "operation": "system_solution", "matrix": _matrix([[("2", "1")]]),
+        "rhs": [_rat("4")], "requestedClaim": "witness", "requestDigest": _digest("4"),
+    }
+    cert = {
+        "schemaVersion": "0.1.0", "capability": base["capability"],
+        "capabilityVersion": base["capabilityVersion"], "requestDigest": request["requestDigest"],
+        "operation": "system_solution", "vector": [_rat("2")], "provenance": _provenance(),
+    }
+    cases.append(ExactCase("linear_system", base["capability"], "system_solution", request, cert))
+
+    request = {
+        **base, "operation": "kernel_vector",
+        "matrix": _matrix([[("1", "1"), ("1", "1")], [("2", "1"), ("2", "1")]]),
+        "requestedClaim": "witness", "requestDigest": _digest("5"),
+    }
+    cert = {
+        "schemaVersion": "0.1.0", "capability": base["capability"],
+        "capabilityVersion": base["capabilityVersion"], "requestDigest": request["requestDigest"],
+        "operation": "kernel_vector", "vector": [_rat("1"), _rat("-1")],
+        "provenance": _provenance(),
+    }
+    cases.append(ExactCase("linear_kernel", base["capability"], "kernel_vector", request, cert))
+
+    request = {
+        **base, "operation": "det_identity",
+        "matrix": _matrix([[("1", "1"), ("2", "1")], [("3", "1"), ("4", "1")]]),
+        "claimedDet": _rat("-2"), "requestedClaim": "soundResult", "requestDigest": _digest("6"),
+    }
+    cert = {
+        "schemaVersion": "0.1.0", "capability": base["capability"],
+        "capabilityVersion": base["capabilityVersion"], "requestDigest": request["requestDigest"],
+        "operation": "det_identity", "provenance": _provenance(),
+    }
+    cases.append(ExactCase("linear_determinant", base["capability"], "det_identity", request, cert))
+    return cases
+
+
+def _counterexample_case() -> ExactCase:
+    request = {
+        "schemaVersion": "0.1.0",
+        "capability": "logic.finite_counterexample",
+        "capabilityVersion": "0.1.0",
+        "predicate": {
+            "varNames": ["x"],
+            "domains": [{"ty": "nat", "bound": 3}],
+            "pred": {
+                "tag": "eq",
+                "left": {"tag": "var", "idx": 0},
+                "right": {"tag": "lit", "v": {"tag": "nat", "v": 0}},
+            },
+        },
+        "requestedClaim": "refutation",
+        "resourcePolicy": {"maxWallTimeMs": 10000, "maxOutputBytes": 1048576},
+        "requestDigest": _digest("7"),
+    }
+    certificate = {
+        "schemaVersion": "0.1.0",
+        "capability": request["capability"],
+        "capabilityVersion": request["capabilityVersion"],
+        "requestDigest": request["requestDigest"],
+        "witness": {"assignment": [{"tag": "nat", "v": 2}]},
+        "provenance": _provenance(),
+    }
+    return ExactCase("finite_counterexample", request["capability"], "refutation", request, certificate)
+
+
+def _formal_base(operation: str, digest_char: str) -> tuple[dict[str, Any], dict[str, Any]]:
+    request: dict[str, Any] = {
+        "schemaVersion": "0.1.0",
+        "capability": "algebra.formal_rational_calculus",
+        "capabilityVersion": "0.1.0",
+        "operation": operation,
+        "variables": [{"name": "x", "type": "Rat"}],
+        "independentVar": "x",
+        "expr": {"tag": "var", "name": "x"},
+        "candidate": {"tag": "int", "value": "1"},
+        "domainConditions": [],
+        "requestedClaim": "soundResult",
+        "resourcePolicy": {"maxWallTimeMs": 10000, "maxOutputBytes": 1048576},
+        "requestDigest": _digest(digest_char),
+    }
+    certificate = {
+        "schemaVersion": "0.1.0",
+        "capability": request["capability"],
+        "capabilityVersion": request["capabilityVersion"],
+        "requestDigest": request["requestDigest"],
+        "operation": operation,
+        "domainConditions": [],
+        "provenance": _provenance(),
+    }
+    return request, certificate
+
+
+def _formal_cases() -> list[ExactCase]:
+    cases: list[ExactCase] = []
+
+    req, cert = _formal_base("derivative_candidate", "8")
+    req["expr"] = {"tag": "pow", "base": {"tag": "var", "name": "x"}, "exp": 2}
+    req["candidate"] = {
+        "tag": "mul", "left": {"tag": "int", "value": "2"},
+        "right": {"tag": "var", "name": "x"},
+    }
+    cases.append(ExactCase("formal_derivative", req["capability"], "derivative_candidate", req, cert))
+
+    req, cert = _formal_base("antiderivative_candidate", "9")
+    req["expr"] = {"tag": "var", "name": "x"}
+    req["candidate"] = {
+        "tag": "mul",
+        "left": {"tag": "rat", "num": "1", "den": "2"},
+        "right": {"tag": "pow", "base": {"tag": "var", "name": "x"}, "exp": 2},
+    }
+    cases.append(ExactCase("formal_antiderivative", req["capability"], "antiderivative_candidate", req, cert))
+
+    req, cert = _formal_base("recurrence_identity", "a")
+    req["variables"] = [{"name": "n", "type": "Rat"}, {"name": "u", "type": "Rat"}]
+    req["independentVar"] = "n"
+    req["dependentVar"] = "u"
+    req["expr"] = {"tag": "var", "name": "n"}
+    req["candidate"] = {"tag": "int", "value": "0"}
+    req["recurrenceRhs"] = {
+        "tag": "add",
+        "left": {"tag": "var", "name": "u"},
+        "right": {"tag": "int", "value": "1"},
+    }
+    cases.append(ExactCase("formal_recurrence", req["capability"], "recurrence_identity", req, cert))
+
+    req, cert = _formal_base("ode_candidate", "b")
+    req["variables"] = [{"name": "x", "type": "Rat"}, {"name": "y", "type": "Rat"}]
+    req["dependentVar"] = "y"
+    req["expr"] = {"tag": "var", "name": "x"}
+    req["candidate"] = {"tag": "int", "value": "0"}
+    req["odeRhs"] = {"tag": "int", "value": "1"}
+    req["initialConditions"] = [
+        {"point": {"tag": "int", "value": "0"}, "value": {"tag": "int", "value": "0"}}
+    ]
+    cases.append(ExactCase("formal_ode", req["capability"], "ode_candidate", req, cert))
+    return cases
+
+
+def _analytic_derivative_case(kind: str, digest_char: str) -> ExactCase:
+    source = {
+        "tag": "mul",
+        "lhs": {"tag": "variable", "idx": 0},
+        "rhs": {"tag": "variable", "idx": 0},
+    }
+    target = {
+        "tag": "add",
+        "lhs": {
+            "tag": "mul", "lhs": {"tag": "const", "value": "1"},
+            "rhs": {"tag": "variable", "idx": 0},
+        },
+        "rhs": {
+            "tag": "mul", "lhs": {"tag": "variable", "idx": 0},
+            "rhs": {"tag": "const", "value": "1"},
+        },
+    }
+    request = {
+        "schemaVersion": "0.1.0", "capability": "analysis.analytic_calculus",
+        "capabilityVersion": "0.1.0", "kind": kind, "source": source, "target": target,
+        "requestDigest": _digest(digest_char),
+    }
+    certificate = {
+        "schemaVersion": "0.1.0", "capability": request["capability"],
+        "capabilityVersion": request["capabilityVersion"], "requestDigest": request["requestDigest"],
+        "source": source, "derivative": target,
+        "proof": {"tag": "mul", "p": {"tag": "variable"}, "q": {"tag": "variable"}},
+        "obligations": [], "claimsCompleteness": False,
+    }
+    return ExactCase(f"analytic_{kind}", request["capability"], kind, request, certificate)
+
+
+def _analytic_cases() -> list[ExactCase]:
+    cases = [
+        _analytic_derivative_case("derivative", "c"),
+        _analytic_derivative_case("derivativeWithin", "d"),
+    ]
+    request = {
+        "schemaVersion": "0.1.0", "capability": "analysis.analytic_calculus",
+        "capabilityVersion": "0.1.0", "kind": "antiderivative",
+        "source": {"tag": "variable", "idx": 0},
+        "target": {"tag": "const", "value": "1"},
+        "requestDigest": _digest("e"),
+    }
+    certificate = {
+        "schemaVersion": "0.1.0", "capability": request["capability"],
+        "capabilityVersion": request["capabilityVersion"], "requestDigest": request["requestDigest"],
+        "source": request["source"], "derivative": request["target"],
+        "proof": {"tag": "variable"}, "obligations": [], "claimsCompleteness": False,
+    }
+    cases.append(ExactCase("analytic_antiderivative", request["capability"], "antiderivative", request, certificate))
+
+    request = {
+        "schemaVersion": "0.1.0", "capability": "analysis.analytic_calculus",
+        "capabilityVersion": "0.1.0", "kind": "odeCandidate",
+        "source": {"tag": "variable", "idx": 0},
+        "target": {"tag": "const", "value": "1"},
+        "initialConditions": [
+            {"point": {"tag": "const", "value": "0"}, "value": {"tag": "const", "value": "0"}}
+        ],
+        "requestDigest": _digest("f"),
+    }
+    certificate = {
+        "schemaVersion": "0.1.0", "capability": request["capability"],
+        "capabilityVersion": request["capabilityVersion"], "requestDigest": request["requestDigest"],
+        "solution": {"tag": "variable", "idx": 0}, "rhs": {"tag": "const", "value": "1"},
+        "derivProof": {"tag": "variable"}, "initialConditions": request["initialConditions"],
+        "obligations": [], "claimsCompleteness": False,
+    }
+    cases.append(ExactCase("analytic_ode", request["capability"], "odeCandidate", request, certificate))
+    return cases
+
+
+def _cases() -> list[ExactCase]:
+    return [
+        _ideal_case(),
+        *_linear_cases(),
+        _counterexample_case(),
+        *_formal_cases(),
+        *_analytic_cases(),
+    ]
+
+
+def _inventory_cr_eligible() -> set[str]:
+    data = json.loads(INVENTORY.read_text(encoding="utf-8"))
+    return {
+        str(entry["id"])
+        for entry in data.get("capabilities") or []
+        if isinstance(entry, dict) and entry.get("cr_eligible") is True
+    }
+
+
+def _assert_coverage(cases: list[ExactCase]) -> None:
+    capabilities = {case.capability for case in cases}
+    expected_capabilities = _inventory_cr_eligible()
+    if capabilities != expected_capabilities:
+        raise RuntimeError(
+            "release exact E2E capability coverage mismatch: "
+            f"got {sorted(capabilities)}, expected inventory {sorted(expected_capabilities)}"
+        )
+
+    forms_by_cap: dict[str, set[str]] = {}
+    for case in cases:
+        forms_by_cap.setdefault(case.capability, set()).add(case.form)
+
+    expected_forms = {
+        "algebra.linear_algebra": set(LA_OPERATIONS),
+        "algebra.formal_rational_calculus": set(FORMAL_OPERATIONS),
+        "analysis.analytic_calculus": set(WHITELIST_KINDS),
+    }
+    for capability, expected in expected_forms.items():
+        got = forms_by_cap.get(capability, set())
+        if got != expected:
+            raise RuntimeError(
+                f"{capability}: exact theorem-form E2E coverage mismatch: "
+                f"got {sorted(got)}, production enables {sorted(expected)}"
+            )
+
+
+def _assert_policy(case: ExactCase) -> None:
+    decision = decide_exact_kernel_replay(case.capability)
+    if not decision.ok:
+        raise RuntimeError(
+            f"{case.name}: CR E2E case has unavailable exact policy: "
+            f"{decision.code}: {decision.message}"
+        )
+    policy = load_assurance_policy(case.capability)
+    cert = policy.get("certification") or {}
+    if cert.get("crEligible") is not True:
+        raise RuntimeError(f"{case.name}: release E2E case is not CR-eligible in registry")
+
+
+def _lean_check(case: ExactCase, directory: Path) -> dict[str, Any]:
+    _assert_policy(case)
+    module = generate_module(
+        capability_id=case.capability,
+        request=case.request,
+        certificate=case.certificate,
+        candidate_bundle_digest=BUNDLE_DIGEST,
+        module_name=f"MathEvidence.Generated.Replay.release_{case.name}",
+        declaration_name=f"release_{case.name}",
+    )
+    metadata = verify(module)
+    if not metadata.ok:
+        raise RuntimeError(f"{case.name}: generated module metadata failed: {metadata.detail}")
+    if "OfflineFixtures" in module.source_text:
+        raise RuntimeError(f"{case.name}: generated exact source references OfflineFixtures")
+
+    source = directory / f"{case.name}.lean"
+    source.write_text(module.source_text, encoding="utf-8", newline="\n")
+    result = run_bounded(
+        ["lake", "env", "lean", str(source)],
+        cwd=ROOT,
+        limits=LIMITS,
+    )
+    if result.returncode != 0 or result.timed_out or result.output_truncated:
+        raise RuntimeError(
+            f"{case.name}: Lean candidate replay failed "
+            f"(rc={result.returncode}, timeout={result.timed_out}, "
+            f"truncated={result.output_truncated})\n"
+            f"stdout:\n{result.stdout}\n"
+            f"stderr:\n{result.stderr}"
+        )
+    return {
+        "case": case.name,
+        "capability": case.capability,
+        "form": case.form,
+        "declaration": module.declaration_name,
+        "sourceHash": module.source_hash,
+        "generatorId": module.generator_id,
+        "generatorVersion": module.generator_version,
+        "grammarVersion": module.grammar_version,
+        "requestDigest": module.request_digest,
+        "candidateBundleDigest": module.candidate_bundle_digest,
+        "leanWallTimeMs": result.wall_time_ms,
+        "status": "lean_candidate_verified",
+    }
+
+
+def main() -> int:
+    cases = _cases()
+    _assert_coverage(cases)
+
+    results: list[dict[str, Any]] = []
+    with tempfile.TemporaryDirectory(prefix="mathevidence-exact-e2e-") as tmp:
+        directory = Path(tmp)
+        for case in cases:
+            result = _lean_check(case, directory)
+            results.append(result)
+            print(
+                f"[exact-e2e] {case.capability}::{case.form}: "
+                f"OK ({result['sourceHash']})"
+            )
+
+    print(json.dumps({"schemaVersion": "0.2.0", "results": results}, sort_keys=True))
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())
diff --git a/scripts/ci/run_cr_exact_lean_e2e_production.py b/scripts/ci/run_cr_exact_lean_e2e_production.py
new file mode 100644
index 00000000..9794a952
--- /dev/null
+++ b/scripts/ci/run_cr_exact_lean_e2e_production.py
@@ -0,0 +1,308 @@
+#!/usr/bin/env python3
+"""Release gate: execute the CR exact matrix through the production Lean path.
+
+The case/coverage matrix lives in ``run_cr_exact_lean_e2e`` and is derived from
+registry maturity plus production plugin operation whitelists. This executor
+intentionally uses the same source staging, ``lake env lean -o`` compilation,
+and Lean.Environment declaration inspection primitive as production
+``kernel_replay``. A standalone /tmp Lean invocation is not equivalent for
+Lean 4.14 ``native_decide`` modules and must not be used as release authority.
+"""
+
+from __future__ import annotations
+
+import importlib.util
+import json
+from pathlib import Path
+import sys
+from types import ModuleType
+from typing import Any
+
+import adapters.common.exact_replay.plugins  # noqa: F401
+from adapters.common.canonical import (
+    bind_request_digest,
+    canonical_dumps,
+    request_binding_payload,
+    verify_request_digest,
+)
+from adapters.common.environment_lock import current_capability_environment_lock
+from adapters.common.exact_replay.pipeline import generate_module, verify
+from adapters.common.kernel_replay import (
+    ALLOWED_AXIOMS_DEFAULT,
+    KernelReplayError,
+    _compile_and_inspect,
+    _run_process,
+    axiom_policy_ok,
+    find_lake,
+)
+from adapters.common.theorem_identity import environment_lock_digest
+
+ROOT = Path(__file__).resolve().parents[2]
+
+
+def _load_matrix() -> ModuleType:
+    """Load the checked-in case matrix explicitly, independent of package install layout."""
+    path = ROOT / "scripts" / "ci" / "run_cr_exact_lean_e2e.py"
+    module_name = "mathevidence_cr_exact_matrix"
+    spec = importlib.util.spec_from_file_location(module_name, path)
+    if spec is None or spec.loader is None:
+        raise RuntimeError(f"cannot load exact E2E matrix from {path}")
+
+    module = importlib.util.module_from_spec(spec)
+    previous = sys.modules.get(module_name)
+    sys.modules[module_name] = module
+    try:
+        spec.loader.exec_module(module)
+    except BaseException:
+        if previous is None:
+            sys.modules.pop(module_name, None)
+        else:
+            sys.modules[module_name] = previous
+        raise
+    return module
+
+
+matrix = _load_matrix()
+BUNDLE_DIGEST = matrix.BUNDLE_DIGEST
+
+
+def _canonical_case_payload(case: Any) -> tuple[dict[str, Any], dict[str, Any]]:
+    """Bind synthetic matrix fixtures exactly as a real Candidate Bundle request.
+
+    Matrix cases use deterministic placeholder digests to keep fixture construction
+    readable. Release execution must not compile those placeholders: production
+    Candidate Bundles bind ``requestDigest`` to the canonical request payload before
+    exact replay. Recompute that binding here and synchronize the certificate so the
+    E2E gate exercises the same semantic contract rather than an invalid fixture.
+    """
+    request = bind_request_digest(case.request)
+    request_digest = verify_request_digest(request)
+    certificate = dict(case.certificate)
+    certificate["requestDigest"] = request_digest
+    return request, certificate
+
+
+def _rational_binding_diagnostic_source(case: Any, module: Any) -> str | None:
+    """Build a non-authoritative companion that prints Lean's reconstructed binding.
+
+    The production theorem source is attempted first and remains the only acceptance
+    path. This companion is generated only for diagnostics after a failure. It stops
+    before the first theorem and therefore cannot establish or inspect a theorem.
+    """
+    if case.capability != "algebra.rational_equality":
+        return None
+    decl = module.declaration_name
+    marker = f"theorem {decl}_request_binding :"
+    prefix, found, _ = module.source_text.partition(marker)
+    if not found:
+        return None
+    return (
+        prefix
+        + f"""
+/- Diagnostic-only companion: never Certification Record authority. -/
+#eval do
+  match MathEvidence.Core.JsonCanonical.canonicalString
+      (MathEvidence.Checkers.RationalEquality.Wire.claimToRequestJson {decl}_claim) with
+  | .ok s => IO.println ("MATHEVIDENCE_DIAG_CANONICAL=" ++ s)
+  | .error e => IO.println ("MATHEVIDENCE_DIAG_CANONICAL_ERROR=" ++ toString e)
+
+#eval IO.println ("MATHEVIDENCE_DIAG_DIGEST=" ++ {decl}_req.requestDigest.value)
+"""
+    )
+
+
+def _extract_prefixed_line(stdout: str, prefix: str) -> str | None:
+    for line in stdout.splitlines():
+        if line.startswith(prefix):
+            return line[len(prefix) :]
+    return None
+
+
+def _rational_binding_diagnostic(
+    *, case: Any, module: Any, request: dict[str, Any], lake: Path
+) -> dict[str, Any]:
+    """Run a failure-only Lean/Python binding comparison with no theorem authority."""
+    source = _rational_binding_diagnostic_source(case, module)
+    if source is None:
+        return {"status": "diagnostic_unavailable", "reason": "source_marker_missing"}
+
+    diagnostic_module = f"MathEvidence.Generated.Replay.diagnostic_{case.name}"
+    source_path = ROOT.joinpath(*diagnostic_module.split(".")).with_suffix(".lean")
+    source_path.parent.mkdir(parents=True, exist_ok=True)
+    source_path.write_text(source, encoding="utf-8", newline="\n")
+    try:
+        proc = _run_process([str(lake), "env", "lean", str(source_path)], root=ROOT)
+    finally:
+        source_path.unlink(missing_ok=True)
+
+    lean_canonical = _extract_prefixed_line(
+        proc.stdout or "", "MATHEVIDENCE_DIAG_CANONICAL="
+    )
+    lean_digest = _extract_prefixed_line(proc.stdout or "", "MATHEVIDENCE_DIAG_DIGEST=")
+    python_canonical = canonical_dumps(request_binding_payload(request))
+    python_digest = str(request["requestDigest"])
+    return {
+        "status": "diagnostic_only_non_authoritative",
+        "returnCode": proc.returncode,
+        "leanCanonical": lean_canonical,
+        "pythonCanonical": python_canonical,
+        "canonicalMatch": (
+            lean_canonical == python_canonical if lean_canonical is not None else None
+        ),
+        "leanRequestDigest": lean_digest,
+        "pythonRequestDigest": python_digest,
+        "digestMatch": lean_digest == python_digest if lean_digest is not None else None,
+        "stdoutTail": (proc.stdout or "")[-3000:],
+        "stderrTail": (proc.stderr or "")[-3000:],
+    }
+
+
+def _execute(case: Any) -> dict[str, Any]:
+    matrix._assert_policy(case)
+    request, certificate = _canonical_case_payload(case)
+    module = generate_module(
+        capability_id=case.capability,
+        request=request,
+        certificate=certificate,
+        candidate_bundle_digest=BUNDLE_DIGEST,
+        module_name=f"MathEvidence.Generated.Replay.release_{case.name}",
+        declaration_name=f"release_{case.name}",
+    )
+    metadata = verify(module)
+    if not metadata.ok:
+        raise RuntimeError(
+            f"{case.capability}::{case.form}: generated module metadata failed: "
+            f"{metadata.detail}"
+        )
+    if "OfflineFixtures" in module.source_text:
+        raise RuntimeError(
+            f"{case.capability}::{case.form}: generated exact source references OfflineFixtures"
+        )
+
+    lake = find_lake(ROOT)
+    if lake is None:
+        raise RuntimeError("lake is unavailable; exact release E2E cannot run")
+
+    lock = current_capability_environment_lock(ROOT, case.capability)
+    lock_digest = environment_lock_digest(lock)
+    try:
+        report, lean_stdout, lean_stderr = _compile_and_inspect(
+            root=ROOT,
+            lake=lake,
+            module_name=module.module_name,
+            declaration_name=module.declaration_name,
+            source_text=module.source_text,
+            environment_lock_digest_value=lock_digest,
+        )
+    except KernelReplayError as exc:
+        diagnostics: dict[str, Any] = {}
+        if case.capability == "algebra.rational_equality":
+            try:
+                diagnostics = _rational_binding_diagnostic(
+                    case=case,
+                    module=module,
+                    request=request,
+                    lake=lake,
+                )
+            except Exception as diagnostic_exc:  # noqa: BLE001
+                diagnostics = {
+                    "status": "diagnostic_failed",
+                    "error": f"{type(diagnostic_exc).__name__}: {diagnostic_exc}",
+                }
+
+        # Preserve the structured Lean/Lake failure context in CI. Diagnostics
+        # are explicitly non-authoritative and run only after acceptance failed.
+        print(
+            json.dumps(
+                {
+                    "schemaVersion": "0.2.0",
+                    "status": "exact_e2e_failure",
+                    "case": case.name,
+                    "capability": case.capability,
+                    "form": case.form,
+                    "requestDigest": request["requestDigest"],
+                    "errorCode": exc.code,
+                    "message": exc.message,
+                    "details": exc.details or {},
+                    "diagnostics": diagnostics,
+                },
+                sort_keys=True,
+            ),
+            file=sys.stderr,
+        )
+        raise
+
+    if report.get("authority") != "Lean.Environment ConstantInfo":
+        raise RuntimeError(
+            f"{case.capability}::{case.form}: declaration inspector authority mismatch"
+        )
+    if report.get("declarationName") != module.declaration_name:
+        raise RuntimeError(
+            f"{case.capability}::{case.form}: declaration identity mismatch: "
+            f"{report.get('declarationName')!r}"
+        )
+    if report.get("environmentLockDigest") != lock_digest:
+        raise RuntimeError(
+            f"{case.capability}::{case.form}: environment-lock identity mismatch"
+        )
+
+    axioms = report.get("axioms")
+    if not isinstance(axioms, list) or not all(isinstance(a, str) for a in axioms):
+        raise RuntimeError(f"{case.capability}::{case.form}: invalid axiom report")
+    axioms = sorted(set(axioms))
+    if not axiom_policy_ok(axioms, ALLOWED_AXIOMS_DEFAULT):
+        raise RuntimeError(
+            f"{case.capability}::{case.form}: unexpected axioms {axioms}"
+        )
+
+    theorem_type_digest = report.get("theoremTypeDigest")
+    proof_digest = report.get("proofDeclarationDigest")
+    if not isinstance(theorem_type_digest, str) or not theorem_type_digest.startswith("sha256:"):
+        raise RuntimeError(
+            f"{case.capability}::{case.form}: missing Lean theorem type digest"
+        )
+    if not isinstance(proof_digest, str) or not proof_digest.startswith("sha256:"):
+        raise RuntimeError(
+            f"{case.capability}::{case.form}: missing Lean proof declaration digest"
+        )
+
+    return {
+        "case": case.name,
+        "capability": case.capability,
+        "form": case.form,
+        "declaration": module.declaration_name,
+        "sourceHash": module.source_hash,
+        "generatorId": module.generator_id,
+        "generatorVersion": module.generator_version,
+        "grammarVersion": module.grammar_version,
+        "requestDigest": module.request_digest,
+        "candidateBundleDigest": module.candidate_bundle_digest,
+        "environmentLockDigest": lock_digest,
+        "theoremTypeDigest": theorem_type_digest,
+        "proofDeclarationDigest": proof_digest,
+        "axioms": axioms,
+        "identityAuthority": report.get("authority"),
+        "leanOutputBytes": len((lean_stdout + lean_stderr).encode("utf-8")),
+        "status": "lean_candidate_identity_verified",
+    }
+
+
+def main() -> int:
+    cases = matrix._cases()
+    matrix._assert_coverage(cases)
+
+    results: list[dict[str, Any]] = []
+    for case in cases:
+        result = _execute(case)
+        results.append(result)
+        print(
+            f"[exact-e2e-production] {case.capability}::{case.form}: "
+            f"OK ({result['theoremTypeDigest']})"
+        )
+
+    print(json.dumps({"schemaVersion": "0.3.0", "results": results}, sort_keys=True))
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())
diff --git a/scripts/generate_release_provenance.py b/scripts/generate_release_provenance.py
index db530246..b2169d4d 100644
--- a/scripts/generate_release_provenance.py
+++ b/scripts/generate_release_provenance.py
@@ -1,10 +1,11 @@
 #!/usr/bin/env python3
-"""Emit release provenance manifest: evidence digests + Lean toolchain / lake pins."""
+"""Emit release provenance binding the exact release tree and trust surface."""
 
 from __future__ import annotations
 
 import hashlib
 import json
+import os
 import subprocess
 import sys
 from datetime import UTC, datetime
@@ -22,13 +23,39 @@ def _sha256_file(path: Path) -> str:
     return "sha256:" + h.hexdigest()
 
 
+def _git_output(*args: str) -> str:
+    try:
+        return subprocess.check_output(
+            ["git", *args],
+            cwd=ROOT,
+            text=True,
+            stderr=subprocess.DEVNULL,
+        ).strip()
+    except (subprocess.CalledProcessError, FileNotFoundError, OSError):
+        return "unknown"
+
+
 def _git_rev() -> str:
+    return _git_output("rev-parse", "HEAD")
+
+
+def _git_tree() -> str:
+    return _git_output("rev-parse", "HEAD^{tree}")
+
+
+def _git_clean() -> bool | None:
     try:
-        return (
-            subprocess.check_output(["git", "rev-parse", "HEAD"], cwd=ROOT, text=True).strip()
+        result = subprocess.run(
+            ["git", "status", "--porcelain", "--untracked-files=normal"],
+            cwd=ROOT,
+            text=True,
+            stdout=subprocess.PIPE,
+            stderr=subprocess.DEVNULL,
+            check=True,
         )
     except (subprocess.CalledProcessError, FileNotFoundError, OSError):
-        return "unknown"
+        return None
+    return not bool(result.stdout.strip())
 
 
 def _lean_toolchain() -> str:
@@ -53,41 +80,169 @@ def _lake_pins() -> dict[str, Any]:
                 "inputRev": pkg.get("inputRev"),
             }
         )
+    packages.sort(key=lambda item: str(item.get("name") or ""))
     return {"manifestVersion": data.get("version"), "packages": packages}
 
 
+def _hashed_files(
+    root: Path,
+    *,
+    suffixes: frozenset[str] | None = None,
+) -> list[dict[str, str]]:
+    if not root.is_dir():
+        return []
+    rows: list[dict[str, str]] = []
+    for path in sorted(root.rglob("*")):
+        if not path.is_file():
+            continue
+        if suffixes is not None and path.suffix.lower() not in suffixes:
+            continue
+        rows.append(
+            {
+                "path": path.relative_to(ROOT).as_posix(),
+                "digest": _sha256_file(path),
+            }
+        )
+    return rows
+
+
+def _hashed_paths(paths: list[str]) -> list[dict[str, str]]:
+    rows: list[dict[str, str]] = []
+    for rel in paths:
+        path = ROOT / rel
+        if path.is_file():
+            rows.append({"path": rel, "digest": _sha256_file(path)})
+    return rows
+
+
+def _maturity_binding() -> dict[str, Any]:
+    path = ROOT / "registry" / "maturity-inventory.json"
+    if not path.is_file():
+        return {}
+    data = json.loads(path.read_text(encoding="utf-8"))
+    return {
+        "path": path.relative_to(ROOT).as_posix(),
+        "digest": _sha256_file(path),
+        "schemaVersion": data.get("schemaVersion"),
+        "auditedBaselineCommit": data.get("statusAsOfCommit"),
+        "program": data.get("program"),
+    }
+
+
+def _workflow_context() -> dict[str, str]:
+    names = {
+        "repository": "GITHUB_REPOSITORY",
+        "runId": "GITHUB_RUN_ID",
+        "runAttempt": "GITHUB_RUN_ATTEMPT",
+        "workflow": "GITHUB_WORKFLOW",
+        "eventName": "GITHUB_EVENT_NAME",
+        "ref": "GITHUB_REF",
+        "refName": "GITHUB_REF_NAME",
+        "refType": "GITHUB_REF_TYPE",
+        "sha": "GITHUB_SHA",
+        "actor": "GITHUB_ACTOR",
+    }
+    return {
+        key: os.environ[value]
+        for key, value in names.items()
+        if os.environ.get(value)
+    }
+
+
 def main() -> int:
     out_dir = Path(sys.argv[1]) if len(sys.argv) > 1 else ROOT / "dist" / "provenance"
     out_dir.mkdir(parents=True, exist_ok=True)
 
+    commit = _git_rev()
+    tree = _git_tree()
+    workflow = _workflow_context()
+    workflow_sha = workflow.get("sha")
+    if workflow_sha and commit != "unknown" and workflow_sha != commit:
+        raise SystemExit(
+            f"release provenance SHA mismatch: GITHUB_SHA={workflow_sha} HEAD={commit}"
+        )
+
     evidence_files: list[dict[str, str]] = []
     for root_name in ("evidence", "benchmarks"):
-        root = ROOT / root_name
-        if not root.is_dir():
-            continue
-        for path in sorted(root.rglob("*")):
-            if not path.is_file():
-                continue
-            if path.suffix.lower() not in {".json", ".md"}:
-                continue
-            rel = path.relative_to(ROOT).as_posix()
-            evidence_files.append({"path": rel, "digest": _sha256_file(path)})
+        # Bind every committed file under the release evidence trees.  A suffix
+        # allowlist could silently omit a future proof/evidence format and make
+        # the provenance manifest weaker than the released repository tree.
+        evidence_files.extend(_hashed_files(ROOT / root_name))
+    evidence_files.sort(key=lambda item: item["path"])
+
+    lock_files = _hashed_paths(
+        [
+            "lean-toolchain",
+            "lake-manifest.json",
+            "uv.lock",
+            "pyproject.toml",
+            "requirements-freeze.txt",
+        ]
+    )
+    trust_documents = _hashed_paths(
+        [
+            "README.md",
+            "docs/STATUS.md",
+            "docs/security/KNOWN_TRUST_GAPS.md",
+            "docs/adr/0005-exact-candidate-binding.md",
+            "GOVERNANCE.md",
+            "SECURITY.md",
+        ]
+    )
+    registry_files = _hashed_files(
+        ROOT / "registry",
+        suffixes=frozenset({".json"}),
+    )
+    schema_files = _hashed_files(
+        ROOT / "schemas",
+        suffixes=frozenset({".json"}),
+    )
+    workflow_files = _hashed_files(
+        ROOT / ".github" / "workflows",
+        suffixes=frozenset({".yml", ".yaml"}),
+    )
 
     manifest = {
-        "schemaVersion": "0.1.0",
+        "schemaVersion": "0.2.0",
         "generatedAt": datetime.now(UTC).strftime("%Y-%m-%dT%H:%M:%SZ"),
-        "gitCommit": _git_rev(),
+        # Compatibility fields retained for existing release consumers.
+        "gitCommit": commit,
         "leanToolchain": _lean_toolchain(),
         "lake": _lake_pins(),
         "evidenceAndBenchmarkFiles": evidence_files,
+        # Release-grade bindings.
+        "gitTree": tree,
+        "gitWorkingTreeCleanAtGeneration": _git_clean(),
+        "workflowRun": workflow,
+        "maturityInventory": _maturity_binding(),
+        "lockFiles": lock_files,
+        "registryFiles": registry_files,
+        "schemaFiles": schema_files,
+        "workflowFiles": workflow_files,
+        "trustDocuments": trust_documents,
         "notes": [
-            "Lean commit pin is lean-toolchain + lake-manifest package revs.",
-            "Evidence digests are content hashes of committed JSON/MD under evidence/ and benchmarks/.",
+            "The release commit/tree bind the complete checked-out source state.",
+            "The maturity inventory names an audited baseline commit; its digest is "
+            "bound here to the actual release commit/tree.",
+            "Lean is pinned by lean-toolchain plus lake-manifest package revisions.",
+            "Python dependency state is bound by uv.lock and requirements-freeze.txt.",
+            "Every file under evidence/ and benchmarks/ is individually digest-bound; "
+            "these hashes are release evidence, not a substitute for capability-specific "
+            "checker soundness.",
+            "Stable promotion and human/external review gates are not implied by "
+            "this experimental-release provenance record.",
         ],
     }
     out_path = out_dir / "provenance-manifest.json"
-    out_path.write_text(json.dumps(manifest, indent=2) + "\n", encoding="utf-8")
-    print(f"wrote {out_path} ({len(evidence_files)} files)")
+    out_path.write_text(
+        json.dumps(manifest, indent=2, sort_keys=True) + "\n",
+        encoding="utf-8",
+    )
+    print(
+        f"wrote {out_path} "
+        f"(evidence={len(evidence_files)}, registry={len(registry_files)}, "
+        f"schemas={len(schema_files)}, workflows={len(workflow_files)})"
+    )
     return 0
 
 
diff --git a/scripts/run_ideal_membership_benchmark.py b/scripts/run_ideal_membership_benchmark.py
old mode 100644
new mode 100755
index dd3e0f2e..02ba203a
--- a/scripts/run_ideal_membership_benchmark.py
+++ b/scripts/run_ideal_membership_benchmark.py
@@ -4,8 +4,9 @@
 Tiers
 -----
 ``candidate``:
-  pass iff backend proposes + arity decodes + the Python mirror of
-  ``checkMembership`` accepts. This tier never reports theorem authority.
+  pass iff backend proposes + arity decodes + the independently recomputed
+  Python mirror of ``checkMembership`` accepts. Adapter self-reports are
+  diagnostic only. This tier never reports theorem authority.
 
 ``release``:
   pass iff the candidate gates succeed and the *exact proposed witness* is
@@ -48,7 +49,8 @@
 
 # Keep PR/nightly theorem compilation bounded while the exact path is new.
 # These are task IDs, not OfflineFixtures: the backend's proposed multipliers
-# are the certificate that Lean compiles and certifies.
+# are the certificate that Lean compiles and certifies. The complete frozen
+# corpus is evaluated separately at candidate/checker tier.
 RELEASE_CERTIFICATION_TASKS = frozenset(
     {
         "IM01_linear_combination_xy",
@@ -78,7 +80,7 @@ def _candidate_status(task: dict[str, Any], proposed: list[dict[str, Any]]) -> d
         "assuranceClaim": "native_checked_candidate_only",
         "resultStatus": None,
         "note": (
-            "Candidate tier accepted only by the Python checker mirror; "
+            "Candidate tier accepted only by the independently recomputed Python checker mirror; "
             "no theorem-level status is claimed."
         ),
         "taskId": task.get("id"),
@@ -259,6 +261,14 @@ def _score_task(task: dict[str, Any], backend: str, *, tier: str) -> dict[str, A
             decode_error = str(exc)
     check_ms = (time.perf_counter() - start) * 1000.0
 
+    adapter_reported_accepts = proposal.get("pythonMirrorAccepts")
+    adapter_checker_agreement = (
+        adapter_reported_accepts == proposed_ok
+        if isinstance(adapter_reported_accepts, bool)
+        else None
+    )
+    critical_false_accept = expected_status == "xfail" and proposed_ok
+
     if not proposed_ok:
         lean = {
             "leanCheckStatus": "not_attempted",
@@ -274,7 +284,9 @@ def _score_task(task: dict[str, Any], backend: str, *, tier: str) -> dict[str, A
     if expected_status == "skip":
         status = "skip"
     elif expected_status == "xfail":
-        status = "xfail_ok" if not proposal.get("pythonMirrorAccepts") else "xfail_unexpected_accept"
+        # A negative-corpus outcome is decided only by the independently
+        # recomputed checker result. Adapter self-report is untrusted telemetry.
+        status = "xfail_unexpected_accept" if critical_false_accept else "xfail_ok"
     elif not decode_ok:
         status = "fail_decode_arity"
     elif not proposed:
@@ -305,7 +317,9 @@ def _score_task(task: dict[str, Any], backend: str, *, tier: str) -> dict[str, A
         "decodeOk": decode_ok,
         "decodeError": decode_error,
         "proposedAccepts": proposed_ok,
-        "adapterPythonMirrorAccepts": proposal.get("pythonMirrorAccepts"),
+        "criticalFalseAccept": critical_false_accept,
+        "adapterPythonMirrorAccepts": adapter_reported_accepts,
+        "adapterCheckerAgreement": adapter_checker_agreement,
         "adapterBackend": proposal.get("backend"),
         "nativeWitnessMs": round(generation_ms, 3),
         "mathEvidenceCheckMs": round(check_ms, 3),
@@ -352,6 +366,13 @@ def main(argv: list[str] | None = None) -> int:
     if tier == TIER_CANDIDATE and soundness_claims:
         raise SystemExit("candidate tier produced soundness_verified; refusing report")
 
+    critical_false_accept_tasks = [
+        str(row["id"]) for row in rows if row.get("criticalFalseAccept") is True
+    ]
+    adapter_checker_disagreement_tasks = [
+        str(row["id"]) for row in rows if row.get("adapterCheckerAgreement") is False
+    ]
+
     by_stratum: dict[str, dict[str, int]] = {}
     for row in rows:
         bucket = by_stratum.setdefault(str(row.get("stratum") or "unit"), {"total": 0, "passed": 0})
@@ -367,9 +388,9 @@ def main(argv: list[str] | None = None) -> int:
         "capability": CAPABILITY_ID,
         "tier": tier,
         "scoringRule": (
-            "pass iff propose + arity-decode + Python mirror check; never theorem authority"
+            "pass iff propose + arity-decode + independently recomputed Python mirror check; adapter self-report is diagnostic only; never theorem authority"
             if tier == TIER_CANDIDATE
-            else "pass iff backend proposal passes mirror and that exact proposal obtains Lean.Environment-derived kernel Certification Record"
+            else "pass iff backend proposal passes independently recomputed mirror and that exact proposal obtains Lean.Environment-derived kernel Certification Record"
         ),
         "backend": backend,
         "declaredBaselines": manifest.get("baselines") or [],
@@ -378,6 +399,10 @@ def main(argv: list[str] | None = None) -> int:
         "scoredTasks": len(scored),
         "passed": passed,
         "skipped": sum(row["status"] == "skip" for row in rows),
+        "criticalFalseAcceptCount": len(critical_false_accept_tasks),
+        "criticalFalseAcceptTasks": critical_false_accept_tasks,
+        "adapterCheckerDisagreementCount": len(adapter_checker_disagreement_tasks),
+        "adapterCheckerDisagreementTasks": adapter_checker_disagreement_tasks,
         "byStratum": by_stratum,
         "honestyNote": manifest.get("honestyNote"),
         "externalHeldOutNote": (
@@ -403,7 +428,13 @@ def main(argv: list[str] | None = None) -> int:
         "tasks": rows,
     }
     print(json.dumps(out, indent=2))
-    return 0 if scored and passed == len(scored) else 1
+    return (
+        0
+        if scored
+        and passed == len(scored)
+        and not critical_false_accept_tasks
+        else 1
+    )
 
 
 if __name__ == "__main__":
diff --git a/scripts/scaffold_env_audits.py b/scripts/scaffold_env_audits.py
old mode 100644
new mode 100755
index ade2aa20..a931856c
--- a/scripts/scaffold_env_audits.py
+++ b/scripts/scaffold_env_audits.py
@@ -4,7 +4,10 @@
 Runs Lake executables ``mathevidence-import-graph`` /
 ``mathevidence-axiom-report`` via ``lake env`` so ``LEAN_PATH`` includes built
 oleans. Drivers load trusted roots with ``Lean.importModules`` and emit
-Environment-level JSON under ``docs/validation/ci/``.
+Environment-level JSON. By default reports are written under
+``docs/validation/ci/``; release workflows can redirect them with
+``MATHEVIDENCE_ENV_AUDIT_OUT_DIR`` so runtime evidence does not mutate the
+checked-out release tree.
 
 Exit non-zero if either driver fails or reports ``environmentLevel: false``.
 """
@@ -12,13 +15,31 @@
 from __future__ import annotations
 
 import json
+import os
 import subprocess
 import sys
 from datetime import UTC, datetime
 from pathlib import Path
 
 ROOT = Path(__file__).resolve().parents[1]
-OUT_DIR = ROOT / "docs" / "validation" / "ci"
+
+
+def _resolve_out_dir() -> Path:
+    raw = os.environ.get("MATHEVIDENCE_ENV_AUDIT_OUT_DIR", "").strip()
+    if not raw:
+        return ROOT / "docs" / "validation" / "ci"
+    path = Path(raw).expanduser()
+    return path if path.is_absolute() else ROOT / path
+
+
+def _display_path(path: Path) -> str:
+    try:
+        return path.relative_to(ROOT).as_posix()
+    except ValueError:
+        return str(path)
+
+
+OUT_DIR = _resolve_out_dir()
 TRUSTED_ROOTS = [
     "MathEvidence/Core",
     "MathEvidence/IR",
@@ -29,6 +50,7 @@
 
 def _run_lake_exe(name: str, out_path: Path) -> dict:
     out_path.parent.mkdir(parents=True, exist_ok=True)
+
     def _run(cmd: list[str]) -> subprocess.CompletedProcess[str]:
         return subprocess.run(
             cmd,
@@ -156,7 +178,7 @@ def main() -> int:
         }
         bundle_path = OUT_DIR / "environment_audit_scaffold.json"
         bundle_path.write_text(json.dumps(results, indent=2) + "\n", encoding="utf-8")
-        print(f"wrote {bundle_path.relative_to(ROOT).as_posix()}")
+        print(f"wrote {_display_path(bundle_path)}")
         return 1
 
     if not (bin_dir / "mathevidence-import-graph").is_file() and not (
@@ -177,7 +199,7 @@ def main() -> int:
         }
         bundle_path = OUT_DIR / "environment_audit_scaffold.json"
         bundle_path.write_text(json.dumps(results, indent=2) + "\n", encoding="utf-8")
-        print(f"wrote {bundle_path.relative_to(ROOT).as_posix()}")
+        print(f"wrote {_display_path(bundle_path)}")
         print("env audits: pending (binaries missing)", file=sys.stderr)
         return 1
 
@@ -199,7 +221,7 @@ def main() -> int:
 
     bundle_path = OUT_DIR / "environment_audit_scaffold.json"
     bundle_path.write_text(json.dumps(results, indent=2) + "\n", encoding="utf-8")
-    print(f"wrote {bundle_path.relative_to(ROOT).as_posix()}")
+    print(f"wrote {_display_path(bundle_path)}")
 
     rc = 0
     for key, label in (("importAudit", "import"), ("axiomAudit", "axiom")):
diff --git a/scripts/validate_maturity_inventory.py b/scripts/validate_maturity_inventory.py
index 2d9f1bd9..10bc2e76 100644
--- a/scripts/validate_maturity_inventory.py
+++ b/scripts/validate_maturity_inventory.py
@@ -7,6 +7,7 @@
 - duplicate capability/version keys appear;
 - ``cr_eligible=true`` without exact-binding generator/verifier metadata;
 - exact binding is claimed without generator metadata / generator path;
+- the legacy offline-replay alias disagrees with offline bundle replay;
 - federated capabilities are marked CR-eligible;
 - ``docs/STATUS.md`` claims CR eligibility the inventory denies, or its
   machine-readable maturity table drifts from the inventory.
@@ -32,24 +33,28 @@
 STATUS_PATH = ROOT / "docs" / "STATUS.md"
 SCHEMA_NAME = "maturity-inventory.schema.json"
 
+# Displayed independent maturity dimensions. ``offline_replay_exists`` remains
+# in the schema as a compatibility alias for offline_bundle_replay_exists but is
+# deliberately not shown as an independent dimension.
 MATURITY_BOOLS = (
     "adapter_exists",
     "checker_exists",
     "lean_soundness_exists",
     "bridge_replay_exists",
     "exact_candidate_binding_exists",
-    "offline_replay_exists",
+    "offline_bundle_replay_exists",
+    "offline_kernel_replay_exists",
     "cr_eligible",
 )
 
 TABLE_BEGIN = "<!-- maturity-inventory-table:begin -->"
 TABLE_END = "<!-- maturity-inventory-table:end -->"
-ROW_RE = re.compile(r"^\|\s*`([^`]+)`\s*\|" + r"\s*(true|false)\s*\|" * 7 + r"\s*$")
+ROW_RE = re.compile(r"^\|\s*`([^`]+)`\s*\|" + r"\s*(true|false)\s*\|" * 8 + r"\s*$")
 CR_ELIGIBLE_TRUE_RE = re.compile(r"(?i)(?:cr_eligible|crEligible)\s*[:=]\s*true\b")
 TABLE_HEADER = (
     "| Capability | adapter_exists | checker_exists | lean_soundness_exists | "
     "bridge_replay_exists | exact_candidate_binding_exists | "
-    "offline_replay_exists | cr_eligible |"
+    "offline_bundle_replay_exists | offline_kernel_replay_exists | cr_eligible |"
 )
 
 _EXACT_META_KEYS = (
@@ -88,6 +93,9 @@ def validate_entry_policy(entry: dict[str, Any], *, repo_root: Path = ROOT) -> l
     supported = binding.get("supported") is True
     exact_exists = entry.get("exact_candidate_binding_exists") is True
     cr_eligible = entry.get("cr_eligible") is True
+    offline_legacy = entry.get("offline_replay_exists") is True
+    offline_bundle = entry.get("offline_bundle_replay_exists") is True
+    offline_kernel = entry.get("offline_kernel_replay_exists") is True
 
     if exact_exists != supported:
         errors.append(
@@ -95,6 +103,21 @@ def validate_entry_policy(entry: dict[str, Any], *, repo_root: Path = ROOT) -> l
             f"with exactBinding.supported={supported}"
         )
 
+    if offline_legacy != offline_bundle:
+        errors.append(
+            f"{cap_id}: offline_replay_exists is a compatibility alias and must equal "
+            f"offline_bundle_replay_exists ({offline_legacy} != {offline_bundle})"
+        )
+    if offline_kernel and not offline_bundle:
+        errors.append(
+            f"{cap_id}: offline_kernel_replay_exists=true requires "
+            "offline_bundle_replay_exists=true"
+        )
+    if offline_kernel and not exact_exists:
+        errors.append(
+            f"{cap_id}: offline_kernel_replay_exists=true requires exact candidate binding"
+        )
+
     if supported or cr_eligible or exact_exists:
         missing = [key for key in _EXACT_META_KEYS if not binding.get(key)]
         if missing:
@@ -127,9 +150,10 @@ def validate_entry_policy(entry: dict[str, Any], *, repo_root: Path = ROOT) -> l
                 f"{cap_id}: inventory cr_eligible={cr_eligible} disagrees with "
                 f"capability assurancePolicy.certification.crEligible={live_cr}"
             )
-        live_exact = False
-        binding = policy.get("exactBinding") if isinstance(policy.get("exactBinding"), dict) else {}
-        live_exact = binding.get("supported") is True
+        live_binding = (
+            policy.get("exactBinding") if isinstance(policy.get("exactBinding"), dict) else {}
+        )
+        live_exact = live_binding.get("supported") is True
         inv_exact = entry.get("exact_candidate_binding_exists") is True
         if live_exact != inv_exact:
             errors.append(
@@ -186,7 +210,7 @@ def format_status_table(inventory: dict[str, Any]) -> str:
     lines = [
         TABLE_BEGIN,
         TABLE_HEADER,
-        "| --- | --- | --- | --- | --- | --- | --- | --- |",
+        "| --- | --- | --- | --- | --- | --- | --- | --- | --- |",
     ]
     for entry in inventory.get("capabilities") or []:
         if not isinstance(entry, dict):
diff --git a/temp_audit_specs/README.md b/temp_audit_specs/README.md
deleted file mode 100644
index aadb809d..00000000
--- a/temp_audit_specs/README.md
+++ /dev/null
@@ -1,8 +0,0 @@
-# Audit specs moved
-
-The normative real-vision re-audit package lives at:
-
-[`docs/audits/2026-07-26-real-vision/`](../docs/audits/2026-07-26-real-vision/)
-
-This directory is retained only as a pointer so older references keep resolving.
-Do not edit specs here; edit the docs path above.
diff --git a/tests/forensic/test_assurance_adversarial_corpus.py b/tests/forensic/test_assurance_adversarial_corpus.py
index 4495ba3b..beffca15 100644
--- a/tests/forensic/test_assurance_adversarial_corpus.py
+++ b/tests/forensic/test_assurance_adversarial_corpus.py
@@ -1,8 +1,9 @@
-"""Assurance adversarial corpus for every exact-bound capability.
+"""Assurance adversarial corpus for exact-bound capability implementations.
 
 Covers candidate mismatch, fixture substitution, hash/source mutation, wrong
 capability/generator/declaration, unsupported exact mode, legacy-as-exact, and
-omitted side conditions — without requiring Lake.
+omitted side conditions — without requiring Lake. Plugin availability is kept
+separate from current theorem/Certification Record eligibility.
 """
 
 from __future__ import annotations
@@ -33,7 +34,6 @@
 _CR_ELIGIBLE = frozenset(
     {
         "algebra.ideal_membership_witness",
-        "algebra.rational_equality",
         "algebra.linear_algebra",
         "logic.finite_counterexample",
         "algebra.formal_rational_calculus",
@@ -53,9 +53,10 @@ def test_exact_binding_supported_cr_eligibility_honest(capability_id: str) -> No
     policy = load_assurance_policy(capability_id)
     assert policy is not None
     decision = decide_exact_kernel_replay(capability_id)
-    assert decision.ok is True
     cert = policy.get("certification") or {}
+
     if capability_id in _CR_ELIGIBLE:
+        assert decision.ok is True
         assert cert.get("crEligible") is True
         outcomes = cert.get("allowedOutcomes") or []
         if capability_id == "logic.finite_counterexample":
@@ -63,11 +64,21 @@ def test_exact_binding_supported_cr_eligibility_honest(capability_id: str) -> No
         else:
             assert "proved" in outcomes
     else:
+        assert capability_id == "algebra.rational_equality"
+        assert decision.ok is False
         assert cert.get("crEligible") is False
+        assert cert.get("allowedOutcomes") == []
+        assert policy.get("supportedAssuranceModes") == []
+        assert (policy.get("exactBinding") or {}).get("supported") is False
 
 
 def test_unsupported_exact_mode_fail_closed() -> None:
-    for cap in ("logic.sat_unsat", "logic.smt", "logic.pseudo_boolean"):
+    for cap in (
+        "algebra.rational_equality",
+        "logic.sat_unsat",
+        "logic.smt",
+        "logic.pseudo_boolean",
+    ):
         decision = decide_exact_kernel_replay(cap)
         assert decision.ok is False
 
diff --git a/tests/forensic/test_assurance_policy.py b/tests/forensic/test_assurance_policy.py
index 23749800..0bfa1ef8 100644
--- a/tests/forensic/test_assurance_policy.py
+++ b/tests/forensic/test_assurance_policy.py
@@ -3,7 +3,6 @@
 from __future__ import annotations
 
 import copy
-import json
 from pathlib import Path
 
 import pytest
@@ -17,15 +16,16 @@
     load_assurance_policy,
     validate_assurance_policy_object,
 )
-from adapters.common.kernel_replay import EXACT_REPLAY_CAPABILITIES, KernelReplayError, run_kernel_replay
+from adapters.common.kernel_replay import EXACT_REPLAY_CAPABILITIES
 from adapters.common.schema_validate import SchemaStore
 
 ROOT = Path(__file__).resolve().parents[2]
 
+# Release-authorized theorem/CR cohort. Rational equality deliberately remains
+# candidate-only until its exact candidate-identity representation is closed.
 _CR_ELIGIBLE = frozenset(
     {
         "algebra.ideal_membership_witness",
-        "algebra.rational_equality",
         "algebra.linear_algebra",
         "logic.finite_counterexample",
         "algebra.formal_rational_calculus",
@@ -54,32 +54,42 @@ def test_all_capabilities_have_assurance_policy() -> None:
             assert cr is False
 
 
-def test_exact_binding_phase2_set() -> None:
-    supported = {cid for cid, p in load_all_assurance_policies().items() if p["exactBinding"]["supported"]}
-    assert supported == set(historical_exact_replay_capabilities())
+def test_exact_binding_current_and_historical_sets_are_distinct() -> None:
+    policies = load_all_assurance_policies()
+    supported = {
+        cid for cid, policy in policies.items() if policy["exactBinding"]["supported"]
+    }
+    historical = set(historical_exact_replay_capabilities())
+
+    assert supported == set(_CR_ELIGIBLE)
+    assert historical == set(EXACT_REPLAY_CAPABILITIES)
+    assert supported < historical
+    assert historical - supported == {"algebra.rational_equality"}
+
     assert exact_binding_supported("algebra.ideal_membership_witness") is True
-    assert exact_binding_supported("algebra.rational_equality") is True
+    assert exact_binding_supported("algebra.rational_equality") is False
     assert exact_binding_supported("logic.smt") is False
 
 
-def test_differential_matches_historical_exact_set() -> None:
-    historical = historical_exact_replay_capabilities()
-    assert historical == EXACT_REPLAY_CAPABILITIES
-    registry_exact = {
+def test_policy_decisions_match_current_release_cohort() -> None:
+    current = {
         cid
-        for cid, policy in load_all_assurance_policies().items()
+        for cid in load_all_assurance_policies()
         if decide_exact_kernel_replay(cid).ok
     }
-    assert registry_exact == set(historical)
+    assert current == set(_CR_ELIGIBLE)
+
+    # The compatibility cohort records implementation history only; it is not
+    # release authority and may therefore be a strict superset of current CR.
+    historical = historical_exact_replay_capabilities()
+    assert historical == EXACT_REPLAY_CAPABILITIES
+    assert "algebra.rational_equality" in historical
+    assert "algebra.rational_equality" not in current
 
 
 @pytest.mark.parametrize(
     "capability_id",
-    sorted(
-        cid
-        for cid in load_all_assurance_policies()
-        if cid not in historical_exact_replay_capabilities()
-    ),
+    sorted(cid for cid in load_all_assurance_policies() if cid not in _CR_ELIGIBLE),
 )
 def test_unsupported_exact_is_assurance_mode_unavailable(capability_id: str) -> None:
     decision = decide_exact_kernel_replay(capability_id)
@@ -98,9 +108,7 @@ def test_cr_eligible_without_generator_rejected_by_policy_validator() -> None:
     policy = copy.deepcopy(load_assurance_policy("logic.smt"))
     assert policy is not None
     policy["certification"]["crEligible"] = True
-    errors = validate_assurance_policy_object(
-        policy, capability_id="logic.smt"
-    )
+    errors = validate_assurance_policy_object(policy, capability_id="logic.smt")
     assert any("crEligible=true" in message for message in errors)
 
 
@@ -114,31 +122,25 @@ def test_exact_mode_without_binding_metadata_rejected() -> None:
     assert any("exactBinding.supported requires fields" in message for message in errors)
 
 
-def test_kernel_replay_rational_uses_exact_generator_not_fixtures() -> None:
-    """Exact binding is enabled; OfflineFixtures must never be the authority."""
-    example = ROOT / "evidence" / "examples" / "rational_equality_basic"
+def test_rational_theorem_replay_is_explicitly_fail_closed() -> None:
+    policy = load_assurance_policy("algebra.rational_equality")
+    assert policy is not None
+    assert policy["exactBinding"]["supported"] is False
+    assert policy["certification"]["crEligible"] is False
+    assert policy["certification"]["allowedOutcomes"] == []
+    assert policy["supportedAssuranceModes"] == []
+
     decision = decide_exact_kernel_replay("algebra.rational_equality")
-    assert decision.ok is True
-    try:
-        result = run_kernel_replay(
-            bundle_dir=example,
-            repo_root=ROOT,
-            declaration_name="forensic_exact_rational",
-            require_lean=False,
-        )
-    except KernelReplayError as exc:
-        assert "OfflineFixtures" not in str(exc.message)
-        return
-    assert result["ok"] is True
-    assert "OfflineFixtures" not in (result.get("detail") or "")
-    assert result.get("identityAuthority") == "Lean.Environment ConstantInfo"
-
-
-def test_validate_registry_accepts_phase1_policies() -> None:
+    assert decision.ok is False
+    assert decision.code == ASSURANCE_MODE_UNAVAILABLE
+    assert "crEligible" in decision.message
+
+
+def test_validate_registry_accepts_current_policies() -> None:
     import importlib.util
 
     path = ROOT / "scripts" / "validate_registry.py"
-    spec = importlib.util.spec_from_file_location("validate_registry_phase1", path)
+    spec = importlib.util.spec_from_file_location("validate_registry_release", path)
     assert spec and spec.loader
     mod = importlib.util.module_from_spec(spec)
     spec.loader.exec_module(mod)
diff --git a/tests/forensic/test_bundle_v03.py b/tests/forensic/test_bundle_v03.py
index f8255ca6..ba7a4518 100644
--- a/tests/forensic/test_bundle_v03.py
+++ b/tests/forensic/test_bundle_v03.py
@@ -106,12 +106,7 @@ def test_duplicate_role_rejects(tmp_path: Path) -> None:
     request = _minimal_rational_request()
     cert = _minimal_certificate(request["requestDigest"])
     out = tmp_path / "dup"
-    write_candidate_bundle(
-        out, request=request, candidate={}, certificate=cert
-    )
-    # Plant a second request role path with different name but same role via
-    # forged manifest entry after write — verify should catch duplicate roles
-    # when we add a second file with role=request.
+    write_candidate_bundle(out, request=request, candidate={}, certificate=cert)
     shutil.copy(out / "request.cjson", out / "request-copy.cjson")
     manifest = json.loads((out / "manifest.cjson").read_text(encoding="utf-8"))
     manifest["files"].append(
@@ -134,9 +129,7 @@ def test_extra_unlisted_file_rejects(tmp_path: Path) -> None:
     request = _minimal_rational_request()
     cert = _minimal_certificate(request["requestDigest"])
     out = tmp_path / "extra"
-    write_candidate_bundle(
-        out, request=request, candidate={}, certificate=cert
-    )
+    write_candidate_bundle(out, request=request, candidate={}, certificate=cert)
     (out / "evil.txt").write_text("nope\n", encoding="utf-8")
     with pytest.raises(ValueError, match="unlisted"):
         verify_bundle_offline(out, strict=True)
@@ -154,9 +147,7 @@ def test_same_request_different_backends_distinct_digests(tmp_path: Path) -> Non
         tmp_path / "b",
         request=request,
         candidate={},
-        certificate=_minimal_certificate(
-            request["requestDigest"], backend_id="sage"
-        ),
+        certificate=_minimal_certificate(request["requestDigest"], backend_id="sage"),
     )
     assert a["requestDigest"] == b["requestDigest"]
     assert a["bundleDigest"] != b["bundleDigest"]
@@ -210,8 +201,6 @@ def test_content_store_collision_rejects(tmp_path: Path) -> None:
         request_digest=manifest["requestDigest"],
         bundle_digest=manifest["bundleDigest"],
     )
-    # Same digest path, different bytes: forge by writing into a clone then
-    # forcing commit with the same digest key.
     clone = tmp_path / "clone"
     shutil.copytree(bundle, clone)
     (clone / "README.md").write_text("# tampered\n", encoding="utf-8")
@@ -245,10 +234,7 @@ def test_certification_receipt_coherence_native_checked(tmp_path: Path) -> None:
         "proofDeclarationDigest": digest,
         "axiomReportDigest": digest,
         "environmentLockDigest": digest,
-        "capability": {
-            "id": "algebra.rational_equality",
-            "version": "0.1.0",
-        },
+        "capability": {"id": "algebra.rational_equality", "version": "0.1.0"},
         "checker": {
             "package": "MathEvidence.Checkers.RationalEquality",
             "module": "Check",
@@ -273,7 +259,10 @@ def test_certification_receipt_coherence_native_checked(tmp_path: Path) -> None:
             result_status="soundness_verified",
             assurance_mode="native_checked",
             replay_target={"schemaVersion": "0.3.0", "detail": "stub"},
-            checker_evaluation={"schemaVersion": "0.3.0", "resultStatus": "checker_accepted"},
+            checker_evaluation={
+                "schemaVersion": "0.3.0",
+                "resultStatus": "checker_accepted",
+            },
             theorem_identity={
                 "schemaVersion": "0.3.0",
                 "theoremTypeDigest": digest,
@@ -289,7 +278,7 @@ def test_certification_receipt_coherence_native_checked(tmp_path: Path) -> None:
         )
 
 
-def test_certification_record_structural_roundtrip_does_not_imply_verification(
+def test_rational_theorem_certification_is_rejected_even_when_structurally_coherent(
     tmp_path: Path,
 ) -> None:
     from adapters.common.theorem_identity import (
@@ -383,18 +372,13 @@ def test_certification_record_structural_roundtrip_does_not_imply_verification(
         },
         certification_receipt=receipt,
     )
-    result = verify_certification_record(cert_dir, candidate_dir=cand)
-    assert result.candidate_bundle_digest == cand_manifest["bundleDigest"]
-    assert result.assurance_mode == "kernel_replay"
-    assert result.claim_established == "soundResult"
-    assert result.record_integrity_verified is True
-    assert result.environment_lock_current is False
-    assert result.environment_lock_stale is True
-    assert result.kernel_replay_verified is False
-    assert result.verified is False
-
-
-def test_migration_script_deterministic(tmp_path: Path, monkeypatch: pytest.MonkeyPatch) -> None:
+    with pytest.raises(ValueError, match="allowedOutcomes"):
+        verify_certification_record(cert_dir, candidate_dir=cand)
+
+
+def test_migration_script_deterministic(
+    tmp_path: Path, monkeypatch: pytest.MonkeyPatch
+) -> None:
     """Two dry-run migrations over the same tree produce identical reports."""
     import scripts.migrate_bundles_v03 as mig
 
@@ -406,13 +390,8 @@ def test_migration_script_deterministic(tmp_path: Path, monkeypatch: pytest.Monk
         candidate={},
         certificate=_minimal_certificate(request["requestDigest"]),
     )
-    # Downgrade version marker to force migrate path interest; script rewrites anyway.
     monkeypatch.setattr(mig, "ROOT", tmp_path)
-    monkeypatch.setattr(
-        mig,
-        "collect_targets",
-        lambda: [src],
-    )
+    monkeypatch.setattr(mig, "collect_targets", lambda: [src])
     r1 = mig.migrate_one(src, dry_run=True)
     r2 = mig.migrate_one(src, dry_run=True)
     assert r1 == r2
diff --git a/tests/forensic/test_cr_exact_lean_e2e_loader.py b/tests/forensic/test_cr_exact_lean_e2e_loader.py
new file mode 100644
index 00000000..3024de7a
--- /dev/null
+++ b/tests/forensic/test_cr_exact_lean_e2e_loader.py
@@ -0,0 +1,90 @@
+from __future__ import annotations
+
+import importlib.util
+from pathlib import Path
+import sys
+from types import ModuleType
+
+from adapters.common.canonical import verify_request_digest
+from agent.api.assurance_policy import decide_exact_kernel_replay
+
+ROOT = Path(__file__).resolve().parents[2]
+RUNNER_PATH = ROOT / "scripts" / "ci" / "run_cr_exact_lean_e2e_production.py"
+RUNNER_MODULE_NAME = "mathevidence_cr_exact_production_loader_test"
+MATRIX_MODULE_NAME = "mathevidence_cr_exact_matrix"
+
+
+def _restore_module(name: str, previous: ModuleType | None) -> None:
+    if previous is None:
+        sys.modules.pop(name, None)
+    else:
+        sys.modules[name] = previous
+
+
+def _load_runner() -> tuple[ModuleType, ModuleType | None, ModuleType | None]:
+    previous_runner = sys.modules.get(RUNNER_MODULE_NAME)
+    previous_matrix = sys.modules.get(MATRIX_MODULE_NAME)
+
+    spec = importlib.util.spec_from_file_location(RUNNER_MODULE_NAME, RUNNER_PATH)
+    assert spec is not None
+    assert spec.loader is not None
+    runner = importlib.util.module_from_spec(spec)
+    sys.modules[RUNNER_MODULE_NAME] = runner
+    spec.loader.exec_module(runner)
+    return runner, previous_runner, previous_matrix
+
+
+def test_production_runner_registers_dataclass_matrix_module_and_binds_requests() -> None:
+    """The production runner must load and canonically bind its synthetic matrix.
+
+    Python 3.12 dataclasses resolve postponed annotations through
+    ``sys.modules[cls.__module__]`` while the class is created. Executing a
+    module returned by ``module_from_spec`` without registering it first makes
+    that lookup fail before the production Lean gate can run.
+
+    The checked-in E2E cases also use readable placeholder request digests.
+    Production execution must replace those placeholders with the canonical
+    request binding used by real Candidate Bundles and synchronize the exact
+    certificate before Lean compilation.
+    """
+    runner, previous_runner, previous_matrix = _load_runner()
+
+    try:
+        matrix = runner.matrix
+        assert matrix.__name__ == MATRIX_MODULE_NAME
+        assert sys.modules.get(MATRIX_MODULE_NAME) is matrix
+        assert matrix.ExactCase.__module__ == MATRIX_MODULE_NAME
+
+        cases = matrix._cases()
+        assert cases
+        for case in cases:
+            request, certificate = runner._canonical_case_payload(case)
+            digest = verify_request_digest(request)
+            assert request["requestDigest"] == digest
+            assert certificate["requestDigest"] == digest
+    finally:
+        _restore_module(RUNNER_MODULE_NAME, previous_runner)
+        _restore_module(MATRIX_MODULE_NAME, previous_matrix)
+
+
+def test_rational_equality_is_excluded_from_production_release_matrix() -> None:
+    """A disabled theorem policy must not leak into the production CR matrix."""
+    runner, previous_runner, previous_matrix = _load_runner()
+
+    try:
+        matrix = runner.matrix
+        cases = matrix._cases()
+        matrix._assert_coverage(cases)
+
+        capabilities = {case.capability for case in cases}
+        expected = matrix._inventory_cr_eligible()
+        assert capabilities == expected
+        assert "algebra.rational_equality" not in capabilities
+        assert "algebra.rational_equality" not in expected
+
+        decision = decide_exact_kernel_replay("algebra.rational_equality")
+        assert decision.ok is False
+        assert "crEligible" in decision.message
+    finally:
+        _restore_module(RUNNER_MODULE_NAME, previous_runner)
+        _restore_module(MATRIX_MODULE_NAME, previous_matrix)
diff --git a/tests/forensic/test_env_audit_output_path.py b/tests/forensic/test_env_audit_output_path.py
new file mode 100644
index 00000000..c94b55ec
--- /dev/null
+++ b/tests/forensic/test_env_audit_output_path.py
@@ -0,0 +1,20 @@
+from __future__ import annotations
+
+from pathlib import Path
+
+import scripts.scaffold_env_audits as env_audits
+
+
+def test_environment_audit_output_can_be_redirected_outside_repo(
+    monkeypatch,
+    tmp_path: Path,
+) -> None:
+    out_dir = tmp_path / "release-env-audits"
+    monkeypatch.setenv("MATHEVIDENCE_ENV_AUDIT_OUT_DIR", str(out_dir))
+    assert env_audits._resolve_out_dir() == out_dir
+    assert env_audits._display_path(out_dir / "report.json") == str(out_dir / "report.json")
+
+
+def test_environment_audit_relative_override_is_repo_relative(monkeypatch) -> None:
+    monkeypatch.setenv("MATHEVIDENCE_ENV_AUDIT_OUT_DIR", "_tmp_release_env_audits")
+    assert env_audits._resolve_out_dir() == env_audits.ROOT / "_tmp_release_env_audits"
diff --git a/tests/forensic/test_exact_phase2_plugins.py b/tests/forensic/test_exact_phase2_plugins.py
index 245e05fd..82e29705 100644
--- a/tests/forensic/test_exact_phase2_plugins.py
+++ b/tests/forensic/test_exact_phase2_plugins.py
@@ -74,7 +74,7 @@ def _rat_request_cert(
     return request, certificate
 
 
-def test_rational_equal_reduced_and_unreduced_canonicalize() -> None:
+def test_rational_exact_wire_binding_and_scope_rejections() -> None:
     # (x^2-1)/(x-1) = x+1
     lhs = {
         "tag": "div",
@@ -106,23 +106,53 @@ def test_rational_equal_reduced_and_unreduced_canonicalize() -> None:
     assert "replaySound" in text
     assert "Expr.div" in text
     assert DIGEST_A in text
+    assert "Request.ofClaim! rat_eq_claim" in text
+    assert "rat_eq_request_binding" in text
 
-    # Unreduced rat literal 2/4 -> 1/2 in source
+    # Exact theorem replay must not silently rewrite a request behind its digest.
     request2, cert2 = _rat_request_cert(
         lhs={"tag": "rat", "num": "2", "den": "4"},
         rhs={"tag": "rat", "num": "1", "den": "2"},
         factors=[],
         digest=DIGEST_B,
     )
-    text2 = generate_exact_rational_equality_module(
-        module_name="MathEvidence.Generated.Replay.rat_canon",
-        declaration_name="rat_canon",
-        request=request2,
-        certificate=cert2,
-        candidate_bundle_digest=BUNDLE,
-    )
-    assert "Expr.rat (1 : Int) 2" in text2
-    assert "Expr.rat (2 : Int) 4" not in text2
+    with pytest.raises(ValueError, match="canonical exact RationalExpr"):
+        generate_exact_rational_equality_module(
+            module_name="MathEvidence.Generated.Replay.rat_noncanonical",
+            declaration_name="rat_noncanonical",
+            request=request2,
+            certificate=cert2,
+            candidate_bundle_digest=BUNDLE,
+        )
+
+    unsupported_policy = copy.deepcopy(request)
+    unsupported_policy["resourcePolicy"] = {
+        "maxWallTimeMs": 20000,
+        "maxOutputBytes": 1048576,
+    }
+    with pytest.raises(ValueError, match="resourcePolicy"):
+        generate_module(
+            capability_id="algebra.rational_equality",
+            request=unsupported_policy,
+            certificate=certificate,
+            candidate_bundle_digest=BUNDLE,
+            module_name="MathEvidence.Generated.Replay.rat_policy",
+            declaration_name="rat_policy",
+        )
+
+    unsupported_version = copy.deepcopy(request)
+    unsupported_version["capabilityVersion"] = "0.2.0"
+    unsupported_version_cert = copy.deepcopy(certificate)
+    unsupported_version_cert["capabilityVersion"] = "0.2.0"
+    with pytest.raises(ValueError, match="supports capabilityVersion 0.1.0 only"):
+        generate_module(
+            capability_id="algebra.rational_equality",
+            request=unsupported_version,
+            certificate=unsupported_version_cert,
+            candidate_bundle_digest=BUNDLE,
+            module_name="MathEvidence.Generated.Replay.rat_version",
+            declaration_name="rat_version",
+        )
 
 
 def test_rational_negatives_zero_unequal_den0_float() -> None:
@@ -141,7 +171,7 @@ def test_rational_negatives_zero_unequal_den0_float() -> None:
     assert "Expr.neg" in text
 
     request0, cert0 = _rat_request_cert(
-        lhs={"tag": "rat", "num": "0", "den": "5"},
+        lhs={"tag": "rat", "num": "0", "den": "1"},
         rhs={"tag": "int", "value": "0"},
         factors=[],
         digest=DIGEST_B,
@@ -217,6 +247,7 @@ def test_rational_field_and_operator_mutation_change_hash() -> None:
         module_name="MathEvidence.Generated.Replay.rat_op",
         declaration_name="rat_op",
     )
+    assert other.source_hash != base.source_hash
     assert op_other.source_hash != base.source_hash
     assert "OfflineFixtures" not in base.source_text
 
@@ -226,7 +257,9 @@ def _matrix(rows: list[list[tuple[str, str]]]) -> dict:
         "tag": "matrix",
         "rows": len(rows),
         "cols": len(rows[0]),
-        "entries": [[{"tag": "rat", "num": n, "den": d} for n, d in row] for row in rows],
+        "entries": [
+            [{"tag": "rat", "num": n, "den": d} for n, d in row] for row in rows
+        ],
     }
 
 
@@ -241,7 +274,9 @@ def test_linear_algebra_ops_true_false_and_mutations() -> None:
         "capability": "algebra.linear_algebra",
         "capabilityVersion": "0.1.0",
         "operation": "inverse_witness",
-        "matrix": _matrix([[("1", "2"), ("0", "1")], [("0", "1"), ("2", "1")]]),
+        "matrix": _matrix(
+            [[("1", "2"), ("0", "1")], [("0", "1"), ("2", "1")]]
+        ),
         "requestedClaim": "witness",
         "resourcePolicy": {"maxWallTimeMs": 10000, "maxOutputBytes": 1048576},
         "requestDigest": DIGEST_A,
@@ -252,7 +287,9 @@ def test_linear_algebra_ops_true_false_and_mutations() -> None:
         "capabilityVersion": "0.1.0",
         "requestDigest": DIGEST_A,
         "operation": "inverse_witness",
-        "inverse": _matrix([[("2", "1"), ("0", "1")], [("0", "1"), ("1", "2")]]),
+        "inverse": _matrix(
+            [[("2", "1"), ("0", "1")], [("0", "1"), ("1", "2")]]
+        ),
         "provenance": {"backendId": "test", "adapterVersion": "0.1.0"},
     }
     text = generate_exact_linear_algebra_module(
@@ -317,7 +354,11 @@ def test_linear_algebra_ops_true_false_and_mutations() -> None:
         )
 
     float_req = copy.deepcopy(req)
-    float_req["matrix"]["entries"][0][0] = {"tag": "rat", "num": 1.5, "den": "1"}
+    float_req["matrix"]["entries"][0][0] = {
+        "tag": "rat",
+        "num": 1.5,
+        "den": "1",
+    }
     with pytest.raises(ValueError, match="float"):
         generate_module(
             capability_id="algebra.linear_algebra",
@@ -334,7 +375,9 @@ def test_linear_algebra_ops_true_false_and_mutations() -> None:
         "capability": "algebra.linear_algebra",
         "capabilityVersion": "0.1.0",
         "operation": "system_solution",
-        "matrix": _matrix([[("1", "1"), ("1", "1")], [("0", "1"), ("1", "1")]]),
+        "matrix": _matrix(
+            [[("1", "1"), ("1", "1")], [("0", "1"), ("1", "1")]]
+        ),
         "rhs": [_rat("3"), _rat("2")],
         "requestedClaim": "witness",
         "resourcePolicy": {"maxWallTimeMs": 10000, "maxOutputBytes": 1048576},
@@ -394,7 +437,12 @@ def test_counterexample_refutation_polarity_and_guards() -> None:
     assert "outcome = refuted" in text
     assert "claimClass := .refutation" in text
     assert "OfflineFixtures" not in text
-    assert map_claim_to_outcome(claim_class="refutation", claim_established="refutation") == "refuted"
+    assert (
+        map_claim_to_outcome(
+            claim_class="refutation", claim_established="refutation"
+        )
+        == "refuted"
+    )
 
     # non-violating / out-of-domain rejected at parse (type/domain checks)
     ood = copy.deepcopy(certificate)
@@ -463,7 +511,11 @@ def test_formal_calculus_binds_tree_and_rejects_candidate_only() -> None:
         "operation": "derivative_candidate",
         "variables": [{"name": "x", "type": "Rat"}],
         "independentVar": "x",
-        "expr": {"tag": "pow", "base": {"tag": "var", "name": "x"}, "exp": 2},
+        "expr": {
+            "tag": "pow",
+            "base": {"tag": "var", "name": "x"},
+            "exp": 2,
+        },
         "candidate": {
             "tag": "mul",
             "left": {"tag": "int", "value": "2"},
@@ -514,7 +566,11 @@ def test_analytic_whitelist_and_unsupported_fail_closed() -> None:
         "capability": "analysis.analytic_calculus",
         "capabilityVersion": "0.1.0",
         "kind": "derivative",
-        "source": {"tag": "mul", "lhs": {"tag": "variable", "idx": 0}, "rhs": {"tag": "variable", "idx": 0}},
+        "source": {
+            "tag": "mul",
+            "lhs": {"tag": "variable", "idx": 0},
+            "rhs": {"tag": "variable", "idx": 0},
+        },
         "target": {
             "tag": "add",
             "lhs": {
@@ -537,7 +593,11 @@ def test_analytic_whitelist_and_unsupported_fail_closed() -> None:
         "requestDigest": DIGEST_A,
         "source": request["source"],
         "derivative": request["target"],
-        "proof": {"tag": "mul", "p": {"tag": "variable"}, "q": {"tag": "variable"}},
+        "proof": {
+            "tag": "mul",
+            "p": {"tag": "variable"},
+            "q": {"tag": "variable"},
+        },
         "obligations": [],
         "claimsCompleteness": False,
     }
@@ -681,7 +741,6 @@ def test_analytic_antideriv_and_ode_generate() -> None:
 
 def test_phase2_exact_binding_decisions() -> None:
     for cap in (
-        "algebra.rational_equality",
         "algebra.linear_algebra",
         "logic.finite_counterexample",
         "algebra.formal_rational_calculus",
@@ -689,5 +748,12 @@ def test_phase2_exact_binding_decisions() -> None:
     ):
         decision = decide_exact_kernel_replay(cap)
         assert decision.ok is True, cap
+
+    # The rational plugin remains directly testable above, but theorem/CR replay
+    # is intentionally disabled until candidate identity is closed.
+    rational = decide_exact_kernel_replay("algebra.rational_equality")
+    assert rational.ok is False
+    assert "crEligible" in rational.message
+
     # federated remain closed
     assert decide_exact_kernel_replay("logic.smt").ok is False
diff --git a/tests/forensic/test_formal_calculus_binding_codegen.py b/tests/forensic/test_formal_calculus_binding_codegen.py
new file mode 100644
index 00000000..647b98f4
--- /dev/null
+++ b/tests/forensic/test_formal_calculus_binding_codegen.py
@@ -0,0 +1,112 @@
+"""Regression coverage for formal-calculus exact request binding and proof mode."""
+
+from __future__ import annotations
+
+from adapters.common.canonical import bind_request_digest
+from adapters.common.exact_replay.pipeline import generate_module
+
+
+def _generate(operation: str, *, antiderivative: bool) -> str:
+    request = {
+        "schemaVersion": "0.1.0",
+        "capability": "algebra.formal_rational_calculus",
+        "capabilityVersion": "0.1.0",
+        "operation": operation,
+        "variables": [{"name": "x", "type": "Rat"}],
+        "independentVar": "x",
+        "domainConditions": [],
+        "requestedClaim": "soundResult",
+        "resourcePolicy": {"maxWallTimeMs": 10000, "maxOutputBytes": 1048576},
+    }
+    if antiderivative:
+        request["expr"] = {"tag": "var", "name": "x"}
+        request["candidate"] = {
+            "tag": "mul",
+            "left": {"tag": "rat", "num": "1", "den": "2"},
+            "right": {
+                "tag": "pow",
+                "base": {"tag": "var", "name": "x"},
+                "exp": 2,
+            },
+        }
+    else:
+        request["expr"] = {
+            "tag": "pow",
+            "base": {"tag": "var", "name": "x"},
+            "exp": 2,
+        }
+        request["candidate"] = {
+            "tag": "mul",
+            "left": {"tag": "int", "value": "2"},
+            "right": {"tag": "var", "name": "x"},
+        }
+
+    bound = bind_request_digest(request)
+    certificate = {
+        "schemaVersion": "0.1.0",
+        "capability": bound["capability"],
+        "capabilityVersion": bound["capabilityVersion"],
+        "requestDigest": bound["requestDigest"],
+        "operation": bound["operation"],
+        "domainConditions": [],
+        "provenance": {"backendId": "test", "adapterVersion": "0.1.0"},
+    }
+    declaration = f"formal_{operation}_proof_mode_regression"
+    module = generate_module(
+        capability_id=bound["capability"],
+        request=bound,
+        certificate=certificate,
+        candidate_bundle_digest="sha256:" + ("c" * 64),
+        module_name=f"MathEvidence.Generated.Replay.{declaration}",
+        declaration_name=declaration,
+    )
+    return module.source_text
+
+
+def _binding_and_theorem(source: str, declaration: str) -> tuple[str, str]:
+    binding = f"theorem {declaration}_request_binding :"
+    theorem = f"theorem {declaration} :"
+    assert binding in source
+    assert theorem in source
+    binding_body = source.split(binding, 1)[1].split(theorem, 1)[0]
+    theorem_body = source.split(theorem, 1)[1]
+    return binding_body, theorem_body
+
+
+def test_formal_antiderivative_stages_exact_checker_proof() -> None:
+    declaration = "formal_antiderivative_candidate_proof_mode_regression"
+    source = _generate("antiderivative_candidate", antiderivative=True)
+    binding_body, theorem_body = _binding_and_theorem(source, declaration)
+
+    assert "\n  rfl\n" in binding_body
+    assert "native_decide" not in binding_body
+
+    # Preserve replaySound over the exact production checkBool proposition while
+    # separating metadata/domain computations from the mathematical operation.
+    # The operation proof explicitly unfolds the production symbolic computation
+    # so kernel simplification is authoritative and no native bridge is used for it.
+    assert f"show checkBool {declaration}_req {declaration}_cert = true from by" in theorem_body
+    assert f"digestOk {declaration}_req {declaration}_cert" in theorem_body
+    assert f"wellFormedOk {declaration}_req" in theorem_body
+    assert f"domainCoverOk {declaration}_req {declaration}_cert" in theorem_body
+    assert f"opOk {declaration}_req" in theorem_body
+    assert theorem_body.count("native_decide") == 3
+    assert "have hOp" in theorem_body
+    assert "simp [opOk" in theorem_body
+    assert "MathEvidence.IR.RationalExpr.polyEqual" in theorem_body
+    assert "MathEvidence.IR.RationalExpr.Poly.combineLike" in theorem_body
+    assert "have hOp" in theorem_body and ":= by decide" not in theorem_body
+    assert "simp [checkBool, hDigest, hWellFormed, hDomain, hOp]" in theorem_body
+
+
+def test_formal_derivative_retains_validated_native_checker_path() -> None:
+    declaration = "formal_derivative_candidate_proof_mode_regression"
+    source = _generate("derivative_candidate", antiderivative=False)
+    binding_body, theorem_body = _binding_and_theorem(source, declaration)
+
+    assert "\n  rfl\n" in binding_body
+    assert "native_decide" not in binding_body
+    assert f"checkBool {declaration}_req {declaration}_cert" in theorem_body
+    assert "by native_decide" in theorem_body
+    assert "show checkBool" not in theorem_body
+    assert "by decide" not in theorem_body
diff --git a/tests/forensic/test_ideal_benchmark_scoring.py b/tests/forensic/test_ideal_benchmark_scoring.py
new file mode 100644
index 00000000..fb90f6cb
--- /dev/null
+++ b/tests/forensic/test_ideal_benchmark_scoring.py
@@ -0,0 +1,59 @@
+from __future__ import annotations
+
+import pytest
+
+import scripts.run_ideal_membership_benchmark as benchmark
+
+
+def _negative_task() -> dict:
+    return {
+        "id": "negative_scoring_regression",
+        "target": {"varCount": 1, "terms": []},
+        "generators": [{"varCount": 1, "terms": []}],
+        "expectedMultipliers": None,
+        "expectedStatus": "xfail",
+        "claimClass": "membership",
+        "stratum": "adversarial",
+    }
+
+
+@pytest.mark.parametrize(
+    ("adapter_claim", "independent_accepts", "expected_status", "false_accept"),
+    [
+        (False, True, "xfail_unexpected_accept", True),
+        (True, False, "xfail_ok", False),
+    ],
+)
+def test_negative_scoring_uses_independent_checker_not_adapter_self_report(
+    monkeypatch: pytest.MonkeyPatch,
+    adapter_claim: bool,
+    independent_accepts: bool,
+    expected_status: str,
+    false_accept: bool,
+) -> None:
+    """Negative-corpus scoring must not trust an adapter's acceptance Boolean."""
+
+    def propose_membership_witness(**_: object) -> dict:
+        return {
+            "multipliers": [{"varCount": 1, "terms": []}],
+            "pythonMirrorAccepts": adapter_claim,
+            "backend": "adversarial-test",
+        }
+
+    def independent_checker(*_: object) -> bool:
+        return independent_accepts
+
+    monkeypatch.setattr(benchmark, "propose_membership_witness", propose_membership_witness)
+    monkeypatch.setattr(benchmark, "check_membership_python", independent_checker)
+
+    row = benchmark._score_task(
+        _negative_task(),
+        backend="adversarial-test",
+        tier=benchmark.TIER_CANDIDATE,
+    )
+
+    assert row["status"] == expected_status
+    assert row["proposedAccepts"] is independent_accepts
+    assert row["adapterPythonMirrorAccepts"] is adapter_claim
+    assert row["adapterCheckerAgreement"] is False
+    assert row["criticalFalseAccept"] is false_accept
diff --git a/tests/forensic/test_maturity_inventory.py b/tests/forensic/test_maturity_inventory.py
index 36179247..c2f943c0 100644
--- a/tests/forensic/test_maturity_inventory.py
+++ b/tests/forensic/test_maturity_inventory.py
@@ -13,7 +13,6 @@
 _CR_ELIGIBLE = frozenset(
     {
         "algebra.ideal_membership_witness",
-        "algebra.rational_equality",
         "algebra.linear_algebra",
         "logic.finite_counterexample",
         "algebra.formal_rational_calculus",
@@ -50,6 +49,15 @@ def test_catalog_coverage_matches_disk() -> None:
         if entry["id"] not in _CR_ELIGIBLE:
             assert entry["cr_eligible"] is False
 
+    rational = next(
+        entry
+        for entry in inventory["capabilities"]
+        if entry["id"] == "algebra.rational_equality"
+    )
+    assert rational["cr_eligible"] is False
+    assert rational["exact_candidate_binding_exists"] is False
+    assert rational["exactBinding"]["supported"] is False
+
 
 def test_cr_eligible_without_exact_binding_is_rejected() -> None:
     mod = _mod()
@@ -134,7 +142,9 @@ def test_inventory_cr_eligible_must_match_capability_json() -> None:
 def test_federated_cr_eligible_is_rejected() -> None:
     mod = _mod()
     inventory = copy.deepcopy(mod.load_inventory())
-    target = next(entry for entry in inventory["capabilities"] if entry["id"] == "logic.sat_unsat")
+    target = next(
+        entry for entry in inventory["capabilities"] if entry["id"] == "logic.sat_unsat"
+    )
     target["cr_eligible"] = True
     target["exact_candidate_binding_exists"] = True
     target["exactBinding"] = {
diff --git a/tests/forensic/test_rational_cr_fail_closed.py b/tests/forensic/test_rational_cr_fail_closed.py
new file mode 100644
index 00000000..75333deb
--- /dev/null
+++ b/tests/forensic/test_rational_cr_fail_closed.py
@@ -0,0 +1,87 @@
+from __future__ import annotations
+
+import importlib.util
+import json
+from pathlib import Path
+import sys
+
+from agent.api.assurance_policy import (
+    ASSURANCE_MODE_UNAVAILABLE,
+    cr_eligible,
+    decide_exact_kernel_replay,
+    exact_binding_supported,
+    load_assurance_policy,
+)
+
+ROOT = Path(__file__).resolve().parents[2]
+
+
+def test_rational_theorem_certification_fails_closed_under_pinned_release_policy() -> None:
+    capability = "algebra.rational_equality"
+    policy = load_assurance_policy(capability)
+    assert policy is not None
+
+    certification = policy.get("certification") or {}
+    maturity = policy.get("maturity") or {}
+
+    assert certification.get("crEligible") is False
+    assert certification.get("allowedOutcomes") == []
+    assert policy.get("supportedAssuranceModes") == []
+    assert exact_binding_supported(capability) is False
+    assert cr_eligible(capability) is False
+
+    # The capability is not deleted: checker/soundness/bridge maturity remains
+    # explicit while theorem-level Certification Record promotion is disabled.
+    assert maturity.get("adapterExists") is True
+    assert maturity.get("checkerExists") is True
+    assert maturity.get("leanSoundnessExists") is True
+    assert maturity.get("bridgeReplayExists") is True
+    assert maturity.get("exactCandidateBindingExists") is False
+
+    decision = decide_exact_kernel_replay(capability)
+    assert decision.ok is False
+    assert decision.code == ASSURANCE_MODE_UNAVAILABLE
+    assert "crEligible" in decision.message
+
+    inventory = json.loads(
+        (ROOT / "registry" / "maturity-inventory.json").read_text(encoding="utf-8")
+    )
+    row = next(
+        entry for entry in inventory["capabilities"] if entry["id"] == capability
+    )
+    assert row["adapter_exists"] is True
+    assert row["checker_exists"] is True
+    assert row["lean_soundness_exists"] is True
+    assert row["bridge_replay_exists"] is True
+    assert row["exact_candidate_binding_exists"] is False
+    assert row["cr_eligible"] is False
+    assert row["supported_assurance_modes"] == []
+    assert row["allowed_certification_outcomes"] == []
+    assert row["exactBinding"] == {"supported": False}
+
+
+def test_release_exact_matrix_is_exactly_live_cr_eligible_set() -> None:
+    """A disabled theorem path must disappear from release execution coverage."""
+    path = ROOT / "scripts" / "ci" / "run_cr_exact_lean_e2e.py"
+    module_name = "mathevidence_test_cr_exact_matrix"
+    spec = importlib.util.spec_from_file_location(module_name, path)
+    assert spec is not None and spec.loader is not None
+
+    module = importlib.util.module_from_spec(spec)
+    previous = sys.modules.get(module_name)
+    sys.modules[module_name] = module
+    try:
+        spec.loader.exec_module(module)
+        cases = module._cases()
+        module._assert_coverage(cases)
+        covered = {case.capability for case in cases}
+        expected = module._inventory_cr_eligible()
+    finally:
+        if previous is None:
+            sys.modules.pop(module_name, None)
+        else:
+            sys.modules[module_name] = previous
+
+    assert covered == expected
+    assert "algebra.rational_equality" not in covered
+    assert len(covered) == 5
diff --git a/tests/forensic/test_rational_exact_kernel_decision.py b/tests/forensic/test_rational_exact_kernel_decision.py
new file mode 100644
index 00000000..f77d6aa5
--- /dev/null
+++ b/tests/forensic/test_rational_exact_kernel_decision.py
@@ -0,0 +1,44 @@
+from __future__ import annotations
+
+from adapters.common.exact_replay.plugins.rational_equality import (
+    generate_exact_rational_equality_module,
+)
+
+
+def test_rational_exact_source_uses_native_decision_for_bound_request() -> None:
+    digest = "sha256:" + ("a" * 64)
+    request = {
+        "schemaVersion": "0.1.0",
+        "capability": "algebra.rational_equality",
+        "capabilityVersion": "0.1.0",
+        "variables": [],
+        "lhs": {"tag": "rat", "num": "1", "den": "2"},
+        "rhs": {"tag": "rat", "num": "1", "den": "2"},
+        "knownAssumptions": [],
+        "requestedClaim": "soundResult",
+        "resourcePolicy": {"maxWallTimeMs": 10000, "maxOutputBytes": 1048576},
+        "requestDigest": digest,
+    }
+    certificate = {
+        "schemaVersion": "0.1.0",
+        "capability": "algebra.rational_equality",
+        "capabilityVersion": "0.1.0",
+        "requestDigest": digest,
+        "differenceNumerator": {"tag": "int", "value": "0"},
+        "denominatorFactors": [],
+        "provenance": {"backendId": "test", "adapterVersion": "0.1.0"},
+    }
+
+    source = generate_exact_rational_equality_module(
+        module_name="MathEvidence.Generated.Replay.rat_native_decision",
+        declaration_name="rat_native_decision",
+        request=request,
+        certificate=certificate,
+        candidate_bundle_digest="sha256:" + ("b" * 64),
+    )
+
+    assert "Request.ofClaim! rat_native_decision_claim" in source
+    assert "rat_native_decision_request_binding" in source
+    assert "\n  native_decide\n" in source
+    assert "(by native_decide : checkBool rat_native_decision_req rat_native_decision_cert = true)" in source
+    assert "OfflineFixtures" not in source
diff --git a/tests/forensic/test_release_provenance.py b/tests/forensic/test_release_provenance.py
new file mode 100644
index 00000000..27890194
--- /dev/null
+++ b/tests/forensic/test_release_provenance.py
@@ -0,0 +1,58 @@
+"""Release-provenance regressions for complete evidence binding."""
+
+from __future__ import annotations
+
+import json
+import sys
+from pathlib import Path
+
+import scripts.generate_release_provenance as release_provenance
+
+
+def test_release_provenance_binds_complete_evidence_and_benchmark_trees(
+    tmp_path: Path, monkeypatch
+) -> None:
+    """Every committed file in evidence/ and benchmarks/ must be digest-bound."""
+
+    root = tmp_path / "repo"
+    evidence = root / "evidence" / "examples" / "example"
+    benchmark = root / "benchmarks" / "suite"
+    evidence.mkdir(parents=True)
+    benchmark.mkdir(parents=True)
+
+    canonical = evidence / "manifest.cjson"
+    canonical.write_text('{"bundleVersion":"0.3.0"}\n', encoding="utf-8")
+    readme = evidence / "README.md"
+    readme.write_text("example\n", encoding="utf-8")
+    theorem = evidence / "theorem.lean"
+    theorem.write_text("theorem example : True := by trivial\n", encoding="utf-8")
+    benchmark_manifest = benchmark / "manifest.json"
+    benchmark_manifest.write_text("{}\n", encoding="utf-8")
+
+    monkeypatch.setattr(release_provenance, "ROOT", root)
+    monkeypatch.setattr(release_provenance, "_git_rev", lambda: "a" * 40)
+    monkeypatch.setattr(release_provenance, "_git_tree", lambda: "b" * 40)
+    monkeypatch.setattr(release_provenance, "_git_clean", lambda: True)
+    monkeypatch.delenv("GITHUB_SHA", raising=False)
+
+    out_dir = tmp_path / "provenance"
+    monkeypatch.setattr(sys, "argv", ["generate_release_provenance.py", str(out_dir)])
+
+    assert release_provenance.main() == 0
+    manifest = json.loads(
+        (out_dir / "provenance-manifest.json").read_text(encoding="utf-8")
+    )
+    rows = {
+        row["path"]: row["digest"]
+        for row in manifest["evidenceAndBenchmarkFiles"]
+    }
+
+    expected = {
+        "evidence/examples/example/manifest.cjson": canonical,
+        "evidence/examples/example/README.md": readme,
+        "evidence/examples/example/theorem.lean": theorem,
+        "benchmarks/suite/manifest.json": benchmark_manifest,
+    }
+    assert set(rows) == set(expected)
+    for relative_path, path in expected.items():
+        assert rows[relative_path] == release_provenance._sha256_file(path)