feat(verification): re-home the Lean engineering proofs to Idris2; ledger rows now proven

.github/workflows/verify-proofs.yml

@@ -12,7 +12,6 @@ on:
     - Justfile
     - pack.toml
     - verification/proofs/idris2/**
-    - verification/proofs/lean4/**
     - verification/proofs/tlaplus/**
     - verification/proofs/agda/**
     - verification/PROOF-STATUS.adoc
@@ -43,7 +42,6 @@ on:
     - Justfile
     - pack.toml
     - verification/proofs/idris2/**
-    - verification/proofs/lean4/**
     - verification/proofs/tlaplus/**
     - verification/proofs/agda/**
     - verification/PROOF-STATUS.adoc
@@ -231,34 +229,32 @@ jobs:
             done
           } >> "$GITHUB_STEP_SUMMARY"
 
-  lake-build:
-    name: lake build
+  # Lean is no longer a proof lane here: the engineering proofs it held moved
+  # to Idris2 (PROOF-POLICY section 3; verification/proofs/idris2/). It stays
+  # for the HYP-01 positive control, which re-runs Lean on a fixture.
+  lean-hole-recheck:
+    name: Lean hole re-check (HYP-01 control)
     runs-on: ubuntu-latest
     timeout-minutes: 20
     permissions:
       contents: read
 
     env:
       ELAN_VERSION: v4.0.0
-      # Pinned (not :stable) so the proofs are checked against the exact Lean
-      # they were verified with. Matches verification/proofs/lean4/lean-toolchain;
-      # bump both together. A moving :stable can break version-sensitive lemmas.
+      # Pinned (not :stable): tests/accept/LeanHoleRecheckSound.idr records
+      # the Lean version whose output it digests.
       LEAN_TOOLCHAIN: leanprover/lean4:v4.30.0
 
     steps:
       - name: Checkout
         uses: actions/checkout@v7.0.1
 
-      - name: Cache Lean toolchain and build
+      - name: Cache Lean toolchain
         id: cache-lean
         uses: actions/cache@v6.1.0
         with:
-          path: |
-            ~/.elan
-            verification/proofs/lean4/.lake
-          key: lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}-${{ hashFiles('verification/proofs/lean4/lakefile.lean', 'verification/proofs/lean4/*.lean') }}
-          restore-keys: |
-            lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}-
+          path: ~/.elan
+          key: lean-${{ env.ELAN_VERSION }}-${{ env.LEAN_TOOLCHAIN }}-toolchain
 
       - name: Install elan + Lean 4
         if: steps.cache-lean.outputs.cache-hit != 'true'
@@ -270,33 +266,23 @@ jobs:
       - name: Put elan on PATH
         run: echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
-      - name: lake build
-        working-directory: verification/proofs/lean4
-        run: |
-          set -euo pipefail
-          lean --version
-          lake --version
-          lake build
-
       # HYP-01 positive control: the SoundVerdict in
       # tests/accept/LeanHoleRecheckSound.idr records digests of a Lean run.
       # Re-run Lean on the fixture from the repository root (where the
       # control's paths are relative to) and require both digests to match.
       - name: Re-check the Lean proof-hole fixture against the HYP-01 control
-        run: bash scripts/recheck-lean-hole.sh
+        run: |
+          set -euo pipefail
+          lean --version
+          bash scripts/recheck-lean-hole.sh
 
       - name: Summary
         if: always()
         run: |
           {
-            echo "## Lean proof verification"
+            echo "## Lean (HYP-01 positive control)"
             echo ""
             echo "- Toolchain: \`${LEAN_TOOLCHAIN}\` via elan \`${ELAN_VERSION}\`"
-            echo "- Proof files:"
-            for f in verification/proofs/lean4/*.lean; do
-              [ "$(basename "$f")" = "lakefile.lean" ] && continue
-              echo "  - \`$(basename "$f")\`"
-            done
           } >> "$GITHUB_STEP_SUMMARY"
 
   # Estate PROOF-POLICY / Mathesis Grade 3 gate for the one Agda artefact:

.machine_readable/testing/blitz.a2ml

@@ -267,7 +267,7 @@ evidence = [
 
 [aspects.safety]
 status = "strong"
-evidence = ["verification/proofs/tlaplus/", "verification/proofs/idris2/", "verification/proofs/lean4/"]
+evidence = ["verification/proofs/tlaplus/", "verification/proofs/idris2/"]
 banned-patterns-clean = true
 default-total-idris = true
 

AFFIRMATION.adoc

@@ -20,15 +20,15 @@ state and commitments. Companion detail:
   `guix.scm` / guix channels are the sole reproducible-build manifests. No
   `flake.nix` remains; all references reconciled.
 * *The formal-proof corpus checks in CI* across Idris 2 (v0.7.0),
-  Lean 4 (v4.30.0), Agda (2.8.0.2, one artefact) and TLA+ (bounded TLC
+  Agda (2.8.0.2, one artefact) and TLA+ (bounded TLC
   model checking, which is `tested-only`, not a proof). What each artefact
   proves, and how strongly, is the proof ledger
   (`verification/proof-ledger.jsonl`, rendered in
-  `verification/PROOF-STATUS.adoc#proof-ledger`): 18 proven of 42;
-  4 proven-with-postulates, 11 tested-only, 2 argued, 7 open. The four
-  `proven-with-postulates` rows are Lean proofs that rest on the Lean kernel
-  axioms `propext` and `Quot.sound`. A source scan does not see those
-  axioms; `Lean.collectAxioms` does. *Zero escape hatches outside
+  `verification/PROOF-STATUS.adoc#proof-ledger`): 22 proven of 42;
+  0 proven-with-postulates, 11 tested-only, 2 argued, 7 open. Four of the
+  Lean proofs rested on the Lean kernel axioms `propext` and `Quot.sound`,
+  which a source scan does not see and `Lean.collectAxioms` does; they moved
+  to Idris2 on 2026-11-09, which has no such axioms. *Zero escape hatches outside
   `test/soundness/fixtures/`* (`believe_me` / `sorry` / `postulate` /
   `assert_total` / `admit` / `native_decide`). Re-measured 2026-09-26 over
   the git-tracked tree by `scripts/check-trusted-base.sh`: outside that

CHANGELOG.adoc

@@ -12,6 +12,18 @@ https://semver.org/[Semantic Versioning].
 
 === Changed
 
+==== Lean engineering proofs move to Idris2 (2026-11-09)
+
+* `RateLimiting`, `BayesianUpdate`, `ParserTotality`, `PageRankInvariants`
+  and `ESNSpectralScaling` are now Idris2 (`verification/proofs/idris2/`,
+  `%default total`), theorem for theorem (PROOF-POLICY §3; owner decision).
+  Four of them had rested on the Lean kernel axioms `propext` and
+  `Quot.sound`; the ledger rows are now `proven`, which makes the census
+  22 proven of 42.
+* `verification/proofs/lean4/` is removed. The `lake build` job becomes
+  `Lean hole re-check (HYP-01 control)`, which keeps the pinned Lean only for
+  the verdict fixture.
+
 ==== Proof claims follow the machine proof ledger (2026-11-09)
 
 * `EXPLAINME.adoc` is back at the repository root, as README-EXPLAINME

EXPLAINME.adoc

@@ -84,28 +84,30 @@ link:lib/fleet_dispatcher.ex[] line 267.
 
 Caveat::
 That recipe quarantine is not `Hypatia.Safety.Quarantine`, which nothing
-calls (<<known-gaps>>). The Lean model of the update uses natural-number
+calls (<<known-gaps>>). The Idris2 model of the update uses natural-number
 pseudo-counts, not Elixir floats.
 
 === Machine-checked proofs
 
 [quote, README.adoc]
 ____
 *Machine-checked proofs* — Idris2 proofs of the ABI and the decision logic (confidence bounds,
-  safety-triangle routing, dispatch thresholds, quarantine, rollback), Lean 4 proofs of the Bayesian
-  update and rate-limiting properties, one Agda model of the Logtalk-to-Elixir migration, and a TLA+
+  safety-triangle routing, dispatch thresholds, quarantine, rollback, the Bayesian update and rate
+  limiting), one Agda model of the Logtalk-to-Elixir migration, and a TLA+
   model of the Kin gate that is model-checked on a bounded instance. The proofs are about models of
-  the code, not the Elixir runtime itself. Proof ledger: 18 proven of 42; 4 proven-with-postulates,
+  the code, not the Elixir runtime itself. Proof ledger: 22 proven of 42; 0 proven-with-postulates,
   11 tested-only, 2 argued, 7 open
 ____
 
 How this is implemented::
 See <<proof-ledger>>. link:.github/workflows/verify-proofs.yml[] runs
-`idris2 --check` per proof file, `idris2 --build` of both ipkgs, `lake
-build`, Agda in its strict profile and TLC.
+`idris2 --check` per proof file, `idris2 --build` of both ipkgs, Agda in
+its strict profile and TLC; Lean runs only for the HYP-01 control.
 
 Caveat::
-Four of the five Lean rows rest on `propext` (two also on `Quot.sound`).
+The Bayesian-update, rate-limiting, parser and neural-precondition proofs moved
+from Lean to Idris2 on 2026-11-09, which removed the Lean kernel axioms
+(`propext`, `Quot.sound`) four of them rested on.
 The TLA+ row is `tested-only`: one bounded instance. The modelled rate
 limiter is not called by any dispatch path. The census matches the ledger.
 
@@ -268,7 +270,7 @@ workflow (debt register T-1).
 | `lib/outcome_tracker.ex` | Beta update; re-scan with `panic-attack assail`
 | `lib/application.ex` | What is supervised
 | `.github/workflows/zig.yml` | FFI tests run; exactly 18 `hypatia_*` exports
-| `.github/workflows/verify-proofs.yml` | Idris2, Lean, Agda and TLC in CI
+| `.github/workflows/verify-proofs.yml` | Idris2, Agda and TLC in CI; Lean for the HYP-01 control
 | `docs/DEBT-REGISTER.adoc` | What is broken, ungated or stale
 |===
 
@@ -284,7 +286,7 @@ Census, from `scripts/proof-ledger.sh check`:
 
 [source,text]
 ----
-18 proven of 42; 4 proven-with-postulates, 11 tested-only, 2 argued, 7 open.
+22 proven of 42; 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open.
 ----
 
 Of the three theory rows, `logtalk-migration` is `PWG-3`;

README.adoc

@@ -25,10 +25,10 @@ It combines:
 * *Bayesian confidence* — every recipe carries a Beta-distributed confidence updated from real
   outcomes, which gates whether a fix is applied automatically, proposed as a PR, or merely reported
 * *Machine-checked proofs* — Idris2 proofs of the ABI and the decision logic (confidence bounds,
-  safety-triangle routing, dispatch thresholds, quarantine, rollback), Lean 4 proofs of the Bayesian
-  update and rate-limiting properties, one Agda model of the Logtalk-to-Elixir migration, and a TLA+
+  safety-triangle routing, dispatch thresholds, quarantine, rollback, the Bayesian update and rate
+  limiting), one Agda model of the Logtalk-to-Elixir migration, and a TLA+
   model of the Kin gate that is model-checked on a bounded instance. The proofs are about models of
-  the code, not the Elixir runtime itself. Proof ledger: 18 proven of 42; 4 proven-with-postulates,
+  the code, not the Elixir runtime itself. Proof ledger: 22 proven of 42; 0 proven-with-postulates,
   11 tested-only, 2 argued, 7 open (link:EXPLAINME.adoc#proof-ledger[details])
 
 === Core philosophy
@@ -80,7 +80,7 @@ PatternRegistry ──> TriangleRouter ──> FleetDispatcher ──> DispatchM
 | `src/Hypatia/ABI/` | Idris2 ABI — Types, GraphQL, gRPC, REST, FFI, RuleEngine
 | `ffi/zig/` | Zig C ABI bridge — 18 exports + 16 protocol connectors
 | `adapters/ cli/ data/ fixer/ integration/` | Rust workspace
-| `verification/` | Proof ledger and proofs: Idris2, Lean 4, Agda, TLA+
+| `verification/` | Proof ledger and proofs: Idris2, Agda, TLA+
 |===
 
 See link:docs/architecture/topology.md[docs/architecture/topology.md] for the full map.

docs/proofs/gap-analysis.adoc

@@ -1,5 +1,11 @@
 == Proofs Gap Analysis
 
+NOTE: Historical (2026-04-22), kept as the record of that analysis. Since then
+the Lean engineering proofs moved to Idris2 (2026-11-09), an Agda artefact
+returned, and every prover runs in CI. The current state is the proof ledger
+(`+verification/proof-ledger.jsonl+`); the convergence plan is
+`+docs/proofs/HANDOVER-neural-convergence.adoc+`.
+
 *Date:* 2026-04-22 *Scope:* VCL query correctness + neural ensemble
 convergence *Status:* Inventory + prioritised plan. No code changes yet.
 

docs/proofs/needs.adoc

@@ -20,9 +20,9 @@ Plans:
 * Neural convergence (rows `+pagerank-convergence+` and `+esn-echo-state+`):
   `+docs/proofs/HANDOVER-neural-convergence.adoc+`. Agda first, over
   constructive reals, then the Rocq and Lean legs.
-* Lean engineering proofs (rows `+lean-*+`): moving to Idris2 (PROOF-POLICY
-  §3; owner decision 2026-11-09). The move also removes the Lean kernel
-  axioms (`+propext+`, `+Quot.sound+`) that four of them rest on.
+* The Lean engineering proofs moved to Idris2 on 2026-11-09 (PROOF-POLICY §3;
+  owner decision), which removed the Lean kernel axioms (`+propext+`,
+  `+Quot.sound+`) four of them rested on.
 
 Prover mapping and statuses: the estate PROOF-POLICY
 (`+metadatastician/standards/3-practice/PROOF-POLICY.adoc+`).

tests/proof-ledger-test.sh

@@ -32,6 +32,11 @@
 }
 # mutate <name> <jq filter applied to the row whose id is $id> <id>
 mutate() {
+  # A mutant whose target row is gone would mutate nothing and pass for the
+  # wrong reason: refuse it.
+  if ! jq -e --arg id "$3" "select(.id == \$id)" verification/proof-ledger.jsonl >/dev/null; then
+    fail=$((fail + 1)); echo "  FAIL mutant $1 targets row $3, which the ledger does not have" >&2
+  fi
   jq -cS --arg id "$3" "if .id == \$id then $2 else . end" verification/proof-ledger.jsonl > "$work/$1.jsonl"
 }
 
@@ -41,10 +46,10 @@
 mutate status-escape '.status = "COMPLETE"' abi-types
 expect "a status outside the closed vocabulary is refused" 1 env PROOF_LEDGER="$work/status-escape.jsonl" bash "$script" check
 
-mutate hidden-axioms '.status = "proven"' lean-rate-limiting
+mutate hidden-axioms '.axioms = ["propext"]' rate-limiting
 expect "proven with axioms listed is refused (it is proven-with-postulates)" 1 env PROOF_LEDGER="$work/hidden-axioms.jsonl" bash "$script" check
 
-mutate unnamed-axioms '.axioms = []' lean-parser-totality
+mutate unnamed-axioms '.status = "proven-with-postulates"' parser-totality
 expect "proven-with-postulates without its axioms is refused" 1 env PROOF_LEDGER="$work/unnamed-axioms.jsonl" bash "$script" check
 
 mutate renamed-proof '.names += ["noSuchTheorem"]' safety-triangle