release: final assurance closure and experimental 0.x readiness

.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
 

.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
 

.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)."

.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
+          print("ideal bounded exact subset OK:", p.get("passed"), "Certification Records")
+          PY

.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

.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

.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