From d43446866a129a607b891ab29e7f0aa58da3bdd6 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 14:15:42 +0000
Subject: [PATCH 1/2] feat(verification): re-home the Lean engineering proofs
 to Idris2; ledger rows now proven

Third PR of the proof-ledger stack. The owner decided (2026-11-09) to
re-home the Lean engineering proofs now rather than record their kernel
axioms as necessary. That is PROOF-POLICY section 3: interface and
engineering statements live in Idris2.

- verification/proofs/idris2/ gains RateLimiting, BayesianUpdate,
  ParserTotality, PageRankInvariants and ESNSpectralScaling, theorem for
  theorem, with the Lean names in camelCase. All are under
  `%default total`, with no believe_me, assert_total or holes.
- Four of the Lean files had rested on propext, or on propext and
  Quot.sound, per Lean.collectAxioms. Idris2 has neither. Their ledger
  rows (now rate-limiting, bayesian-update, parser-totality,
  pagerank-preconditions and esn-preconditions) are proven. The census
  moves from 18 to 22 proven of 42, with 0 proven-with-postulates.
- verification/proofs/lean4/ is removed. The `lake build` job becomes
  `Lean hole re-check (HYP-01 control)`: the pinned Lean stays, only for
  the verdict fixture. That job is not a required check.
- README, AFFIRMATION, EXPLAINME, PROOF-STATUS and needs.adoc describe the
  move. The `claims` gate caught all four stale census quotes before they
  were updated.
- tests/proof-ledger-test.sh: the axiom contracts target rows that exist,
  and `mutate` now fails when its target row is missing. A vanished row
  would otherwise make a contract pass for the wrong reason.

Local receipt, Idris2 0.7.0 built from source with Chez:
- all 12 verification/proofs/idris2/*.idr pass idris2 --check;
- the hypatia-abi and hypatia-verify ipkgs build (exit 0);
- check-verdicts passes (2 positive controls, 5 expected rejections);
- check-trusted-base is OK.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CYR5bf5FBLS7cXQK72aVNM
---
 .github/workflows/verify-proofs.yml           |  44 ++--
 .machine_readable/testing/blitz.a2ml          |   2 +-
 AFFIRMATION.adoc                              |  12 +-
 CHANGELOG.adoc                                |  12 +
 EXPLAINME.adoc                                |  20 +-
 README.adoc                                   |   8 +-
 docs/proofs/gap-analysis.adoc                 |   6 +
 docs/proofs/needs.adoc                        |   6 +-
 tests/proof-ledger-test.sh                    |   9 +-
 verification/PROOF-STATUS.adoc                |  63 ++---
 verification/proof-ledger.jsonl               |  12 +-
 verification/proofs/idris2/BayesianUpdate.idr | 189 +++++++++++++++
 .../proofs/idris2/ESNSpectralScaling.idr      | 126 ++++++++++
 .../proofs/idris2/PageRankInvariants.idr      |  89 +++++++
 verification/proofs/idris2/ParserTotality.idr | 145 ++++++++++++
 verification/proofs/idris2/RateLimiting.idr   | 222 +++++++++++++++++
 verification/proofs/lean4/.gitignore          |   4 -
 verification/proofs/lean4/BayesianUpdate.lean | 188 ---------------
 .../proofs/lean4/ESNSpectralScaling.lean      | 148 ------------
 .../proofs/lean4/PageRankInvariants.lean      | 120 ----------
 verification/proofs/lean4/ParserTotality.lean | 191 ---------------
 verification/proofs/lean4/RateLimiting.lean   | 223 ------------------
 verification/proofs/lean4/lakefile.lean       |  12 -
 verification/proofs/lean4/lean-toolchain      |   1 -
 24 files changed, 874 insertions(+), 978 deletions(-)
 create mode 100644 verification/proofs/idris2/BayesianUpdate.idr
 create mode 100644 verification/proofs/idris2/ESNSpectralScaling.idr
 create mode 100644 verification/proofs/idris2/PageRankInvariants.idr
 create mode 100644 verification/proofs/idris2/ParserTotality.idr
 create mode 100644 verification/proofs/idris2/RateLimiting.idr
 delete mode 100644 verification/proofs/lean4/.gitignore
 delete mode 100644 verification/proofs/lean4/BayesianUpdate.lean
 delete mode 100644 verification/proofs/lean4/ESNSpectralScaling.lean
 delete mode 100644 verification/proofs/lean4/PageRankInvariants.lean
 delete mode 100644 verification/proofs/lean4/ParserTotality.lean
 delete mode 100644 verification/proofs/lean4/RateLimiting.lean
 delete mode 100644 verification/proofs/lean4/lakefile.lean
 delete mode 100644 verification/proofs/lean4/lean-toolchain

diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml
index 7fa7acf4..eea9c8e2 100644
--- a/.github/workflows/verify-proofs.yml
+++ b/.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,8 +229,11 @@ 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:
@@ -240,25 +241,20 @@ jobs:
 
     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:
diff --git a/.machine_readable/testing/blitz.a2ml b/.machine_readable/testing/blitz.a2ml
index cba82d31..25f3e6ba 100644
--- a/.machine_readable/testing/blitz.a2ml
+++ b/.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
 
diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc
index 5defac9a..7b8eee48 100644
--- a/AFFIRMATION.adoc
+++ b/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
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index e705a9b7..16d8e368 100644
--- a/CHANGELOG.adoc
+++ b/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
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
index ec95ac8b..c473c572 100644
--- a/EXPLAINME.adoc
+++ b/EXPLAINME.adoc
@@ -84,7 +84,7 @@ 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
@@ -92,20 +92,22 @@ pseudo-counts, not Elixir floats.
 [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.
 
@@ -267,7 +269,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
 |===
 
@@ -283,7 +285,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`;
diff --git a/README.adoc b/README.adoc
index b4c34733..8647158e 100644
--- a/README.adoc
+++ b/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.
diff --git a/docs/proofs/gap-analysis.adoc b/docs/proofs/gap-analysis.adoc
index dddf4b28..4332b9fd 100644
--- a/docs/proofs/gap-analysis.adoc
+++ b/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.
 
diff --git a/docs/proofs/needs.adoc b/docs/proofs/needs.adoc
index 99360ad3..079917ce 100644
--- a/docs/proofs/needs.adoc
+++ b/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+`).
diff --git a/tests/proof-ledger-test.sh b/tests/proof-ledger-test.sh
index be137ba3..c9af3000 100755
--- a/tests/proof-ledger-test.sh
+++ b/tests/proof-ledger-test.sh
@@ -22,6 +22,11 @@ expect() { # <label> <want-exit> <command...>
 
 # 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"
 }
 
@@ -31,10 +36,10 @@ expect "the committed PROOF-STATUS block is the ledger's rendering" 0 bash "$scr
 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
diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc
index 02981167..f8fe7d02 100644
--- a/verification/PROOF-STATUS.adoc
+++ b/verification/PROOF-STATUS.adoc
@@ -41,12 +41,13 @@ neurosymbolic CI/CD platform.
   need their own correspondence evidence and tests, and the ledger gives
   them their own rows.
 
-NOTE: This repo verifies Idris2, Lean and TLA+ artefacts in CI, and carries
-one narrowly scoped Agda artefact (`+LogtalkMigration.agda+`) gated by the
-same workflow. It does not yet run an Agda + Rocq + Lean reconciliation
-pipeline. The Lean files state engineering properties; they stay in Lean,
-labelled as such, until they are next touched (PROOF-POLICY §3). They are not
-recheck legs of any Agda proof.
+NOTE: This repo verifies Idris2 and TLA+ artefacts in CI, and carries one
+narrowly scoped Agda artefact (`+LogtalkMigration.agda+`) gated by the same
+workflow. It does not yet run an Agda + Rocq + Lean reconciliation pipeline.
+The engineering proofs that were in Lean (rate limiting, Bayesian update, VCL
+parser, PageRank and ESN preconditions) moved to Idris2 on 2026-11-09
+(PROOF-POLICY §3). Lean still runs in CI, but only for the HYP-01 control
+fixture.
 
 // BEGIN GENERATED: scripts/proof-ledger.sh render (do not edit by hand)
 [[proof-ledger]]
@@ -55,7 +56,7 @@ recheck legs of any Agda proof.
 Rendered from `+verification/proof-ledger.jsonl+`, which is canonical: where this table and the
 ledger disagree, the ledger wins and this table is regenerated.
 
-*Census:* 18 proven of 42; 4 proven-with-postulates, 11 tested-only, 2 argued, 7 open. Theory rows: 3 (PWG-1 0, PWG-2ii 0, PWG-2i 0, PWG-3 1, ungraded 2).
+*Census:* 22 proven of 42; 0 proven-with-postulates, 11 tested-only, 2 argued, 7 open. Theory rows: 3 (PWG-1 0, PWG-2ii 0, PWG-2i 0, PWG-3 1, ungraded 2).
 
 [cols="3,1,2,2,2",options="header"]
 |===
@@ -242,34 +243,34 @@ ledger disagree, the ledger wins and this table is regenerated.
 |There is no Signalbox repository to apply the criterion to
 
 |The rate-limit counter never exceeds its bound: tryAccept, prune and event sequences preserve the invariant, and an at-limit event is rejected (P7)
-|proven-with-postulates (Quot.sound, propext)
-|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
-|`+verification/proofs/lean4/RateLimiting.lean+`: `+tryAccept_preserves_invariant+`, `+prune_preserves_invariant+`, `+processEvents_preserves_invariant+`, `+at_limit_rejects+`, `+count_bounded_after_accepts+`
-|Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Interface engineering in Lean: moves to Idris2 when next touched (PROOF-POLICY section 3)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/RateLimiting.idr+`: `+tryAcceptPreservesInvariant+`, `+prunePreservesInvariant+`, `+processEventsPreservesInvariant+`, `+atLimitRejects+`, `+countBoundedAfterAccepts+`
+|Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)
 
 |The Beta posterior stays in (0,1), rises with successes, falls with failures, is the prior with no observations, and clamps to [floor, cap] (H7)
-|proven-with-postulates (Quot.sound, propext)
-|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
-|`+verification/proofs/lean4/BayesianUpdate.lean+`: `+posterior_lt_one+`, `+posterior_pos+`, `+more_successes_raises+`, `+more_failures_lowers+`, `+clamp_ge_floor+`, `+clamp_le_cap+`, `+bayesian_update_sound+`
-|Over Nat pseudo-counts; Elixir floats are not modelled. Moves to Idris2 when next touched (PROOF-POLICY section 3)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/BayesianUpdate.idr+`: `+posteriorLtOne+`, `+posteriorPos+`, `+moreSuccessesRaises+`, `+moreFailuresLowers+`, `+clampGeFloor+`, `+clampLeCap+`, `+bayesianUpdateSound+`
+|Over Nat pseudo-counts; Elixir floats are not modelled. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)
 
 |The VCL FROM-clause parser is total and deterministic, passes the remainder on, and rejects malformed input
-|proven-with-postulates (propext)
-|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
-|`+verification/proofs/lean4/ParserTotality.lean+`: `+parseFrom_deterministic+`, `+parseFrom_passes_remainder+`, `+parseFrom_orphan_from+`, `+parseFrom_no_from_keyword+`
-|FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moves to Idris2 when next touched (PROOF-POLICY section 3)
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/ParserTotality.idr+`: `+parseFromDeterministic+`, `+parseFromPassesRemainder+`, `+parseFromOrphanFrom+`, `+parseFromNoFromKeyword+`
+|FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)
 
 |PageRank inputs are well formed: edge weights and in/out weight sums are non-negative
 |proven
-|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
-|`+verification/proofs/lean4/PageRankInvariants.lean+`: `+edge_weight_nonneg+`, `+outWeightSum_nonneg+`, `+inWeightSum_nonneg+`, `+pagerank_preconditions_sound+`
-|Preconditions only; convergence is row pagerank-convergence
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/PageRankInvariants.idr+`: `+edgeWeightNonneg+`, `+outWeightSumNonneg+`, `+inWeightSumNonneg+`, `+pagerankPreconditionsSound+`
+|Preconditions only; convergence is row pagerank-convergence. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)
 
 |ESN spectral scaling is well defined: the floor-clamped denominator is positive and bounds both inputs
-|proven-with-postulates (propext)
-|Lean 4.30.0, lake build; axioms by Lean.collectAxioms
-|`+verification/proofs/lean4/ESNSpectralScaling.lean+`: `+denom_pos_when_floor_pos+`, `+denom_ge_maxAbs+`, `+denom_ge_floor+`, `+esn_scaling_preconditions_sound+`
-|Preconditions only; echo-state stability is row esn-echo-state
+|proven
+|Idris2 0.7.0, idris2 --check (--total)
+|`+verification/proofs/idris2/ESNSpectralScaling.idr+`: `+denomPosWhenFloorPos+`, `+denomGeMaxAbs+`, `+denomGeFloor+`, `+esnScalingPreconditionsSound+`
+|Preconditions only; the echo-state property is row esn-echo-state. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)
 
 |Kin-gate atomicity: mutual exclusion by type and in the bot view, view coherent with locks, no orphan view, well-bracketed grants, and every request processed (H8)
 |tested-only
@@ -311,7 +312,7 @@ ledger disagree, the ledger wins and this table is regenerated.
 |open
 |-
 |`+lib/vcl/query.ex+`: `+fetch_scans+`
-|Only FROM-clause parsing is modelled (row lean-parser-totality)
+|Only FROM-clause parsing is modelled (row parser-totality)
 |===
 // END GENERATED: proof ledger
 
@@ -386,7 +387,7 @@ snapshot
 * *P6.3* Fault Tolerance: even partially failed batches are reversible
 to original state
 
-==== 7. Rate Limiting (`+RateLimiting.lean+`)
+==== 7. Rate Limiting (`+RateLimiting.idr+`)
 
 * *P7.1* Empty state satisfies invariant (base case)
 * *P7.2* `+tryAccept+` preserves invariant (inductive step)
@@ -397,9 +398,9 @@ list)
 rejected
 * *P7.6* Count bounded after any sequence of accepts
 
-Status for all of P7: `proven-with-postulates`. The proofs rest on the Lean
-kernel axioms `propext` and `Quot.sound` (`at_limit_rejects` on
-`propext` only), as `Lean.collectAxioms` reports under Lean 4.30.0.
+Status for all of P7: `proven` (Idris2 0.7.0, `%default total`). Moved
+from Lean on 2026-11-09; the Lean proofs rested on the kernel axioms
+`propext` and `Quot.sound`, which Idris2 does not have.
 
 ==== 8. Logtalk Migration Correspondence (`+LogtalkMigration.agda+`)
 
diff --git a/verification/proof-ledger.jsonl b/verification/proof-ledger.jsonl
index cb028d0c..aa37d92d 100644
--- a/verification/proof-ledger.jsonl
+++ b/verification/proof-ledger.jsonl
@@ -28,15 +28,15 @@
 {"axioms":[],"bounds":"","checker":"-","file":"lib/safety/quarantine.ex","id":"retraction-runtime-wiring","kind":"engineering","names":["retract_dependents"],"obligation":"Quarantine.retract_dependents/1 is called by a scan or dispatch path","status":"open","trust_boundary":"Not wired, like the rest of the safety systems (CLAUDE.md Known Gap 2)"}
 {"axioms":[],"bounds":"ExUnit cases","checker":"ExUnit (mix test)","file":"test/dispatch_manifest_test.exs","id":"dispatch-manifest-steps","kind":"engineering","names":["DispatchManifest"],"obligation":"Every dispatch-manifest step names the verdict it derives from, and a factless step refuses the whole manifest before anything is written","status":"tested-only","trust_boundary":"Hypatia's own derived workflow only"}
 {"axioms":[],"bounds":"","checker":"-","file":"test/dispatch_manifest_test.exs","id":"signalbox","kind":"engineering","names":["DispatchManifest"],"obligation":"The Signalbox derived-workflow criterion holds","status":"open","trust_boundary":"There is no Signalbox repository to apply the criterion to"}
-{"axioms":["Quot.sound","propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/RateLimiting.lean","id":"lean-rate-limiting","kind":"engineering","names":["tryAccept_preserves_invariant","prune_preserves_invariant","processEvents_preserves_invariant","at_limit_rejects","count_bounded_after_accepts"],"obligation":"The rate-limit counter never exceeds its bound: tryAccept, prune and event sequences preserve the invariant, and an at-limit event is rejected (P7)","status":"proven-with-postulates","trust_boundary":"Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Interface engineering in Lean: moves to Idris2 when next touched (PROOF-POLICY section 3)"}
-{"axioms":["Quot.sound","propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/BayesianUpdate.lean","id":"lean-bayesian-update","kind":"engineering","names":["posterior_lt_one","posterior_pos","more_successes_raises","more_failures_lowers","clamp_ge_floor","clamp_le_cap","bayesian_update_sound"],"obligation":"The Beta posterior stays in (0,1), rises with successes, falls with failures, is the prior with no observations, and clamps to [floor, cap] (H7)","status":"proven-with-postulates","trust_boundary":"Over Nat pseudo-counts; Elixir floats are not modelled. Moves to Idris2 when next touched (PROOF-POLICY section 3)"}
-{"axioms":["propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/ParserTotality.lean","id":"lean-parser-totality","kind":"engineering","names":["parseFrom_deterministic","parseFrom_passes_remainder","parseFrom_orphan_from","parseFrom_no_from_keyword"],"obligation":"The VCL FROM-clause parser is total and deterministic, passes the remainder on, and rejects malformed input","status":"proven-with-postulates","trust_boundary":"FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moves to Idris2 when next touched (PROOF-POLICY section 3)"}
-{"axioms":[],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/PageRankInvariants.lean","id":"lean-pagerank-preconditions","kind":"engineering","names":["edge_weight_nonneg","outWeightSum_nonneg","inWeightSum_nonneg","pagerank_preconditions_sound"],"obligation":"PageRank inputs are well formed: edge weights and in/out weight sums are non-negative","status":"proven","trust_boundary":"Preconditions only; convergence is row pagerank-convergence"}
-{"axioms":["propext"],"bounds":"","checker":"Lean 4.30.0, lake build; axioms by Lean.collectAxioms","file":"verification/proofs/lean4/ESNSpectralScaling.lean","id":"lean-esn-preconditions","kind":"engineering","names":["denom_pos_when_floor_pos","denom_ge_maxAbs","denom_ge_floor","esn_scaling_preconditions_sound"],"obligation":"ESN spectral scaling is well defined: the floor-clamped denominator is positive and bounds both inputs","status":"proven-with-postulates","trust_boundary":"Preconditions only; echo-state stability is row esn-echo-state"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/RateLimiting.idr","id":"rate-limiting","kind":"engineering","names":["tryAcceptPreservesInvariant","prunePreservesInvariant","processEventsPreservesInvariant","atLimitRejects","countBoundedAfterAccepts"],"obligation":"The rate-limit counter never exceeds its bound: tryAccept, prune and event sequences preserve the invariant, and an at-limit event is rejected (P7)","status":"proven","trust_boundary":"Over Nat counters; lib/safety/rate_limiter.ex is not called by any dispatch path. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/BayesianUpdate.idr","id":"bayesian-update","kind":"engineering","names":["posteriorLtOne","posteriorPos","moreSuccessesRaises","moreFailuresLowers","clampGeFloor","clampLeCap","bayesianUpdateSound"],"obligation":"The Beta posterior stays in (0,1), rises with successes, falls with failures, is the prior with no observations, and clamps to [floor, cap] (H7)","status":"proven","trust_boundary":"Over Nat pseudo-counts; Elixir floats are not modelled. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/ParserTotality.idr","id":"parser-totality","kind":"engineering","names":["parseFromDeterministic","parseFromPassesRemainder","parseFromOrphanFrom","parseFromNoFromKeyword"],"obligation":"The VCL FROM-clause parser is total and deterministic, passes the remainder on, and rejects malformed input","status":"proven","trust_boundary":"FROM-clause subset over a token model; lib/vcl/ is not shown to follow it. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/PageRankInvariants.idr","id":"pagerank-preconditions","kind":"engineering","names":["edgeWeightNonneg","outWeightSumNonneg","inWeightSumNonneg","pagerankPreconditionsSound"],"obligation":"PageRank inputs are well formed: edge weights and in/out weight sums are non-negative","status":"proven","trust_boundary":"Preconditions only; convergence is row pagerank-convergence. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"}
+{"axioms":[],"bounds":"","checker":"Idris2 0.7.0, idris2 --check (--total)","file":"verification/proofs/idris2/ESNSpectralScaling.idr","id":"esn-preconditions","kind":"engineering","names":["denomPosWhenFloorPos","denomGeMaxAbs","denomGeFloor","esnScalingPreconditionsSound"],"obligation":"ESN spectral scaling is well defined: the floor-clamped denominator is positive and bounds both inputs","status":"proven","trust_boundary":"Preconditions only; the echo-state property is row esn-echo-state. Moved from Lean 2026-11-09 (PROOF-POLICY section 3)"}
 {"axioms":[],"bounds":"3 bots x 2 repos, MaxRequests = 4: 444715 distinct states, depth 13, no error","checker":"TLC 2.19 (rev 5a47802), -workers auto -config KinGate.cfg","file":"verification/proofs/tlaplus/KinGate.tla","id":"kin-gate","kind":"engineering","names":["KinGateSafe","MutualExclusionByType","MutualExclusionBotView","ViewCoherentWithLocks","NoOrphanView","GrantsAreWellBracketed","EveryRequestProcessed"],"obligation":"Kin-gate atomicity: mutual exclusion by type and in the bot view, view coherent with locks, no orphan view, well-bracketed grants, and every request processed (H8)","status":"tested-only","trust_boundary":"One bounded instance; the Elixir kin gate is not shown to follow the spec"}
 {"axioms":[],"bounds":"","checker":"Agda 2.8.0.2, builtins only, --safe --without-K --cubical-compatible","file":"verification/proofs/agda/LogtalkMigration.agda","foundation_diverse":false,"id":"logtalk-migration","kind":"theory","legs":[],"names":["categoriesAgree","severitiesAgree","autoFixableAgrees","fixPresenceAgrees","preventionBranchSource","preventionCodeReviewTarget"],"obligation":"The 18 transcribed alert types agree between security_learning.lgt and Hypatia.Rules.SecurityErrors on category, severity, auto-fixability and fix presence; prevention agrees except the two ledgered non-equalities","pwg":"3","status":"proven","trust_boundary":"The finite table as transcribed; fix strings and Elixir runtime behaviour are outside the model. No Rocq or Lean leg yet"}
 {"axioms":[],"bounds":"ExUnit cases over the migrated alert types","checker":"ExUnit (mix test)","file":"test/security_errors_test.exs","id":"logtalk-runtime","kind":"engineering","names":["SecurityErrors"],"obligation":"Hypatia.Rules.SecurityErrors at runtime follows the table the Agda model states","status":"tested-only","trust_boundary":"Example-based; the transcription into the Agda table is not itself checked"}
 {"axioms":[],"bounds":"","checker":"-","file":"-","foundation_diverse":false,"id":"pagerank-convergence","kind":"theory","legs":[],"names":[],"obligation":"Damped PageRank iteration converges to a unique stationary vector","pwg":"ungraded","status":"open","trust_boundary":"Not stated in any prover. Agda statement first (PROOF-POLICY section 2), over constructive reals, then Rocq and Lean legs; no Mathlib"}
 {"axioms":[],"bounds":"","checker":"-","file":"-","foundation_diverse":false,"id":"esn-echo-state","kind":"theory","legs":[],"names":[],"obligation":"With leak rate 0 < a <= 1 and the reservoir scaled to infinity-norm at most 0.95, two state trajectories under the same input converge geometrically (echo-state property), and [-1,1]^n is invariant","pwg":"ungraded","status":"open","trust_boundary":"Not stated in any prover. Agda statement first (PROOF-POLICY section 2), over constructive reals, then Rocq and Lean legs; no Mathlib. The runtime scales by the induced infinity-norm, not the spectral radius"}
 {"axioms":[],"bounds":"","checker":"-","file":"-","id":"models-runtime-refinement","kind":"engineering","names":[],"obligation":"The Elixir runtime follows the Idris2, Lean and TLA+ models above","status":"open","trust_boundary":"No correspondence evidence beyond the rows that name a runtime test; a model row proves its model only (README-EXPLAINME section 5 rule 3)"}
-{"axioms":[],"bounds":"","checker":"-","file":"lib/vcl/query.ex","id":"vcl-query-correctness","kind":"engineering","names":["fetch_scans"],"obligation":"VCL queries return what their semantics says beyond the FROM clause","status":"open","trust_boundary":"Only FROM-clause parsing is modelled (row lean-parser-totality)"}
+{"axioms":[],"bounds":"","checker":"-","file":"lib/vcl/query.ex","id":"vcl-query-correctness","kind":"engineering","names":["fetch_scans"],"obligation":"VCL queries return what their semantics says beyond the FROM clause","status":"open","trust_boundary":"Only FROM-clause parsing is modelled (row parser-totality)"}
diff --git a/verification/proofs/idris2/BayesianUpdate.idr b/verification/proofs/idris2/BayesianUpdate.idr
new file mode 100644
index 00000000..69dd6c73
--- /dev/null
+++ b/verification/proofs/idris2/BayesianUpdate.idr
@@ -0,0 +1,189 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- BayesianUpdate.idr — Bayesian confidence update soundness (H7).
+--
+-- Re-homed from verification/proofs/lean4/BayesianUpdate.lean (PROOF-POLICY
+-- section 3). The statements are the Lean file's; the Lean proofs rested on
+-- the kernel axioms propext and Quot.sound, which Idris2 does not have.
+--
+-- Models the Beta-conjugate update in lib/outcome_tracker.ex
+-- (prior_strength = 10):
+--   alpha_post = alpha_prior + successes, beta_post = beta_prior + failures,
+--   posterior  = alpha_post / (alpha_post + beta_post),
+--   result     = clamp(posterior, floor = 10%, cap = 99%).
+-- Ratios are compared by cross-multiplication over Nat; Elixir floats are
+-- not modelled.
+
+module BayesianUpdate
+
+import Control.Relation
+import Data.Nat
+
+%default total
+
+------------------------------------------------------------------------
+-- Section 1: fraction comparison over Nat (a/b <= c/d iff a*d <= c*b)
+------------------------------------------------------------------------
+
+||| alpha / (alpha + beta) < 1 when beta > 0: alpha < alpha + beta.
+export
+fracLtOne : (alpha, beta : Nat) -> LT 0 beta -> LT alpha (alpha + beta)
+fracLtOne alpha (S b) _ =
+  rewrite sym (plusSuccRightSucc alpha b) in LTESucc (lteAddRight alpha)
+
+||| alpha / (alpha + beta) > 0 when alpha > 0.
+export
+fracPos : (alpha : Nat) -> LT 0 alpha -> LT 0 alpha
+fracPos _ h = h
+
+||| The denominator alpha + beta is positive when alpha is.
+export
+denomPos : (alpha, beta : Nat) -> LT 0 alpha -> LT 0 (alpha + beta)
+denomPos alpha beta h = transitive h (lteAddRight alpha)
+
+------------------------------------------------------------------------
+-- Section 2: the Beta update
+------------------------------------------------------------------------
+
+||| Posterior parameters: alpha = alpha_prior + successes, beta = beta_prior
+||| + failures, both positive.
+public export
+record BayesParams where
+  constructor MkBayesParams
+  alpha    : Nat
+  beta     : Nat
+  alphaPos : LT 0 alpha
+  betaPos  : LT 0 beta
+
+||| The denominator alpha + beta.
+public export
+denom : BayesParams -> Nat
+denom p = p.alpha + p.beta
+
+||| The denominator is positive.
+export
+paramsDenomPos : (p : BayesParams) -> LT 0 (denom p)
+paramsDenomPos p = denomPos p.alpha p.beta p.alphaPos
+
+------------------------------------------------------------------------
+-- Section 3: the posterior is in (0, 1)
+------------------------------------------------------------------------
+
+||| H7, property 1: alpha / (alpha + beta) < 1.
+export
+posteriorLtOne : (p : BayesParams) -> LT p.alpha (denom p)
+posteriorLtOne p = fracLtOne p.alpha p.beta p.betaPos
+
+||| H7, property 2: alpha / (alpha + beta) > 0.
+export
+posteriorPos : (p : BayesParams) -> LT 0 p.alpha
+posteriorPos p = p.alphaPos
+
+------------------------------------------------------------------------
+-- Section 4: monotonicity
+------------------------------------------------------------------------
+
+||| Multiplication by k is monotone.
+export
+multLteMonotoneLeft : {m, n : Nat} -> (k : Nat) -> LTE m n -> LTE (k * m) (k * n)
+multLteMonotoneLeft Z _ = LTEZero
+multLteMonotoneLeft (S k) h = plusLteMonotone h (multLteMonotoneLeft k h)
+
+||| H7, property 3: a success weakly raises the ratio:
+||| alpha * (alpha + 1 + beta) <= (alpha + 1) * (alpha + beta).
+export
+moreSuccessesRaises : (p : BayesParams) ->
+                      LTE (p.alpha * (p.alpha + 1 + p.beta)) ((p.alpha + 1) * (p.alpha + p.beta))
+moreSuccessesRaises p =
+  rewrite hs1 in rewrite hs2 in
+    plusLteMonotoneLeft (p.alpha * (p.alpha + p.beta)) p.alpha (p.alpha + p.beta)
+                        (lteAddRight p.alpha)
+  where
+    reassoc : p.alpha + 1 + p.beta = (p.alpha + p.beta) + 1
+    reassoc = rewrite sym (plusAssociative p.alpha 1 p.beta) in
+              rewrite plusCommutative 1 p.beta in
+              plusAssociative p.alpha p.beta 1
+    hs1 : p.alpha * (p.alpha + 1 + p.beta) = p.alpha * (p.alpha + p.beta) + p.alpha
+    hs1 = rewrite reassoc in
+          rewrite multDistributesOverPlusRight p.alpha (p.alpha + p.beta) 1 in
+          rewrite multOneRightNeutral p.alpha in Refl
+    hs2 : (p.alpha + 1) * (p.alpha + p.beta) = p.alpha * (p.alpha + p.beta) + (p.alpha + p.beta)
+    hs2 = rewrite multDistributesOverPlusLeft p.alpha 1 (p.alpha + p.beta) in
+          rewrite multOneLeftNeutral (p.alpha + p.beta) in Refl
+
+||| H7, property 4: a failure weakly lowers the ratio:
+||| alpha * (alpha + beta) <= alpha * (alpha + beta + 1).
+export
+moreFailuresLowers : (p : BayesParams) ->
+                     LTE (p.alpha * (p.alpha + p.beta)) (p.alpha * (p.alpha + p.beta + 1))
+moreFailuresLowers p = multLteMonotoneLeft p.alpha (lteAddRight (p.alpha + p.beta))
+
+------------------------------------------------------------------------
+-- Section 5: zero observations return the prior
+------------------------------------------------------------------------
+
+||| A prior as a fraction (alpha_p = prior * 10, beta_p = (1 - prior) * 10).
+public export
+record Prior where
+  constructor MkPrior
+  alphaP    : Nat
+  betaP     : Nat
+  alphaPPos : LT 0 alphaP
+  betaPPos  : LT 0 betaP
+
+||| The posterior after no successes and no failures.
+public export
+fromPrior : Prior -> BayesParams
+fromPrior p = MkBayesParams p.alphaP p.betaP p.alphaPPos p.betaPPos
+
+||| H7, property 5: with no observations the posterior alpha is the prior's.
+export
+zeroObsAlpha : (p : Prior) -> (fromPrior p).alpha = p.alphaP
+zeroObsAlpha _ = Refl
+
+||| H7, property 6: with no observations the posterior beta is the prior's.
+export
+zeroObsBeta : (p : Prior) -> (fromPrior p).beta = p.betaP
+zeroObsBeta _ = Refl
+
+||| H7, property 7: with no observations the denominator is unchanged.
+export
+zeroObsDenom : (p : Prior) -> denom (fromPrior p) = p.alphaP + p.betaP
+zeroObsDenom _ = Refl
+
+------------------------------------------------------------------------
+-- Section 6: floor (10%) and cap (99%)
+------------------------------------------------------------------------
+
+||| minimum m n never exceeds n.
+export
+minimumLTERight : (m, n : Nat) -> LTE (minimum m n) n
+minimumLTERight Z n = LTEZero
+minimumLTERight (S m) Z = LTEZero
+minimumLTERight (S m) (S n) = LTESucc (minimumLTERight m n)
+
+||| H7, property 8: the clamped result is at least the floor.
+export
+clampGeFloor : (raw : Nat) -> LTE 1 (maximum 1 raw)
+clampGeFloor raw = maximumLeftUpperBound 1 raw
+
+||| H7, property 9: the clamped result is at most the cap.
+export
+clampLeCap : (raw : Nat) -> LTE (minimum raw 99) 99
+clampLeCap raw = minimumLTERight raw 99
+
+------------------------------------------------------------------------
+-- Section 7: composite validity
+------------------------------------------------------------------------
+
+||| H7, main theorem: a BayesParams with alpha, beta > 0 satisfies all four
+||| validity conditions.
+export
+bayesianUpdateSound : (p : BayesParams) ->
+  ( LT 0 p.alpha
+  , LT p.alpha (denom p)
+  , LTE (p.alpha * (p.alpha + 1 + p.beta)) ((p.alpha + 1) * (p.alpha + p.beta))
+  , LTE (p.alpha * (p.alpha + p.beta)) (p.alpha * (p.alpha + p.beta + 1)) )
+bayesianUpdateSound p =
+  (posteriorPos p, posteriorLtOne p, moreSuccessesRaises p, moreFailuresLowers p)
diff --git a/verification/proofs/idris2/ESNSpectralScaling.idr b/verification/proofs/idris2/ESNSpectralScaling.idr
new file mode 100644
index 00000000..e41ad134
--- /dev/null
+++ b/verification/proofs/idris2/ESNSpectralScaling.idr
@@ -0,0 +1,126 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- ESNSpectralScaling.idr — the reservoir scaling step is well defined, over Nat.
+--
+-- Re-homed from verification/proofs/lean4/ESNSpectralScaling.lean
+-- (PROOF-POLICY section 3). The statements are the Lean file's; the Lean
+-- proofs rested on the kernel axiom propext, which Idris2 does not have.
+--
+-- lib/neural/echo_state_network.ex scales the reservoir by
+--   scale = reservoir_norm / max(max_row_sum, 0.001),
+-- the induced infinity-norm (largest absolute row sum), not the spectral
+-- radius. This file shows, over a Nat model, that the floor-guarded
+-- denominator is positive whenever the floor is, so the scaling never
+-- divides by zero. The echo-state property itself is a theory theorem,
+-- planned in Agda over constructive reals
+-- (docs/proofs/HANDOVER-neural-convergence.adoc); it is not proved here.
+
+module ESNSpectralScaling
+
+import Control.Relation
+import Data.Nat
+
+%default total
+
+------------------------------------------------------------------------
+-- Section 1: the model (entries are Nat magnitudes)
+------------------------------------------------------------------------
+
+||| A matrix as a list of rows.
+public export
+Matrix : Type
+Matrix = List (List Nat)
+
+||| Each row's sum of entry magnitudes (Enum.map(row, &abs/1) |> Enum.sum()).
+public export
+rowSums : Matrix -> List Nat
+rowSums m = map sum m
+
+||| The largest element, or the floor for an empty list
+||| (Enum.max(fn -> 1.0 end)).
+public export
+maxAbsOr : List Nat -> (floor : Nat) -> Nat
+maxAbsOr xs floor = foldl (\acc, x => if x > acc then x else acc) floor xs
+
+||| The induced infinity-norm (largest row sum), with a floor.
+public export
+matrixMaxAbs : Matrix -> (floor : Nat) -> Nat
+matrixMaxAbs m floor = maxAbsOr (rowSums m) floor
+
+||| The scaling ratio of the target to the floor-clamped norm.
+public export
+scaleRatio : (target, maxAbs, floor : Nat) -> Nat
+scaleRatio target maxAbs floor = div target (maximum maxAbs floor)
+
+------------------------------------------------------------------------
+-- Section 2: the empty matrix
+------------------------------------------------------------------------
+
+||| Property 1: an empty matrix has no row sums.
+export
+rowSumsNil : rowSums [] = []
+rowSumsNil = Refl
+
+||| Property 2: maxAbsOr of an empty list is the floor.
+export
+maxAbsOrNil : (floor : Nat) -> maxAbsOr [] floor = floor
+maxAbsOrNil _ = Refl
+
+||| Property 3: an empty matrix's norm is its floor.
+export
+matrixMaxAbsNil : (floor : Nat) -> matrixMaxAbs [] floor = floor
+matrixMaxAbsNil _ = Refl
+
+------------------------------------------------------------------------
+-- Section 3: non-negativity
+------------------------------------------------------------------------
+
+||| Property 4: the norm is non-negative.
+export
+matrixMaxAbsNonneg : (m : Matrix) -> (floor : Nat) -> LTE 0 (matrixMaxAbs m floor)
+matrixMaxAbsNonneg _ _ = LTEZero
+
+||| Property 5: the scaling ratio is non-negative.
+export
+scaleRatioNonneg : (target, maxAbs, floor : Nat) -> LTE 0 (scaleRatio target maxAbs floor)
+scaleRatioNonneg _ _ _ = LTEZero
+
+------------------------------------------------------------------------
+-- Section 4: the denominator is positive
+------------------------------------------------------------------------
+
+||| Property 6: a positive floor makes the clamped denominator positive, so
+||| the scaling never divides by zero.
+export
+denomPosWhenFloorPos : (maxAbs, floor : Nat) -> LT 0 floor -> LT 0 (maximum maxAbs floor)
+denomPosWhenFloorPos maxAbs floor hf = transitive hf (maximumRightUpperBound maxAbs floor)
+
+||| Property 7: the clamped denominator is at least maxAbs.
+export
+denomGeMaxAbs : (maxAbs, floor : Nat) -> LTE maxAbs (maximum maxAbs floor)
+denomGeMaxAbs = maximumLeftUpperBound
+
+||| Property 8: the clamped denominator is at least the floor.
+export
+denomGeFloor : (maxAbs, floor : Nat) -> LTE floor (maximum maxAbs floor)
+denomGeFloor = maximumRightUpperBound
+
+------------------------------------------------------------------------
+-- Section 5: composite
+------------------------------------------------------------------------
+
+||| Main theorem: for any reservoir and any positive floor, the norm is
+||| non-negative and the clamped denominator is positive and bounds both
+||| the norm and the floor.
+export
+esnScalingPreconditionsSound : (m : Matrix) -> (maxAbs, floor : Nat) -> LT 0 floor ->
+  ( LTE 0 (matrixMaxAbs m floor)
+  , LT 0 (maximum maxAbs floor)
+  , LTE maxAbs (maximum maxAbs floor)
+  , LTE floor (maximum maxAbs floor) )
+esnScalingPreconditionsSound m maxAbs floor hf =
+  ( matrixMaxAbsNonneg m floor
+  , denomPosWhenFloorPos maxAbs floor hf
+  , denomGeMaxAbs maxAbs floor
+  , denomGeFloor maxAbs floor )
diff --git a/verification/proofs/idris2/PageRankInvariants.idr b/verification/proofs/idris2/PageRankInvariants.idr
new file mode 100644
index 00000000..b48b7057
--- /dev/null
+++ b/verification/proofs/idris2/PageRankInvariants.idr
@@ -0,0 +1,89 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- PageRankInvariants.idr — preconditions of the PageRank iteration, over Nat.
+--
+-- Re-homed from verification/proofs/lean4/PageRankInvariants.lean
+-- (PROOF-POLICY section 3: these are engineering preconditions, so they live
+-- in Idris2). The statements are the Lean file's.
+--
+-- lib/neural/graph_of_trust.ex (build_edges/1) keeps edge weights
+-- non-negative, divides each source's contributions by its outgoing-weight
+-- sum, and keeps the damping factor in [0, 1]. This file states the first
+-- two over a Nat model. Convergence of the iteration is a theory theorem,
+-- planned in Agda over constructive reals
+-- (docs/proofs/HANDOVER-neural-convergence.adoc); it is not proved here.
+
+module PageRankInvariants
+
+import Data.List
+import Data.Nat
+
+%default total
+
+------------------------------------------------------------------------
+-- Section 1: the model
+------------------------------------------------------------------------
+
+||| A weighted directed edge; weights are absolute counts on a shared scale.
+public export
+record Edge where
+  constructor MkEdge
+  src    : Nat
+  tgt    : Nat
+  weight : Nat
+
+||| The sum of the weights of the edges leaving `src`.
+public export
+outWeightSum : List Edge -> (src : Nat) -> Nat
+outWeightSum edges s = foldl (\acc, e => acc + e.weight) 0 (filter (\e => e.src == s) edges)
+
+||| The sum of the weights of the edges entering `tgt`.
+public export
+inWeightSum : List Edge -> (tgt : Nat) -> Nat
+inWeightSum edges t = foldl (\acc, e => acc + e.weight) 0 (filter (\e => e.tgt == t) edges)
+
+------------------------------------------------------------------------
+-- Section 2: non-negativity
+------------------------------------------------------------------------
+
+||| Property 1: edge weights are non-negative.
+export
+edgeWeightNonneg : (e : Edge) -> LTE 0 e.weight
+edgeWeightNonneg _ = LTEZero
+
+||| Property 2: every outgoing-weight sum is non-negative.
+export
+outWeightSumNonneg : (edges : List Edge) -> (s : Nat) -> LTE 0 (outWeightSum edges s)
+outWeightSumNonneg _ _ = LTEZero
+
+||| Property 3: every incoming-weight sum is non-negative.
+export
+inWeightSumNonneg : (edges : List Edge) -> (t : Nat) -> LTE 0 (inWeightSum edges t)
+inWeightSumNonneg _ _ = LTEZero
+
+------------------------------------------------------------------------
+-- Section 3: the empty graph
+------------------------------------------------------------------------
+
+||| Property 4: with no edges, every outgoing-weight sum is 0.
+export
+outWeightSumNil : (s : Nat) -> outWeightSum [] s = 0
+outWeightSumNil _ = Refl
+
+||| Property 5: with no edges, every incoming-weight sum is 0.
+export
+inWeightSumNil : (t : Nat) -> inWeightSum [] t = 0
+inWeightSumNil _ = Refl
+
+------------------------------------------------------------------------
+-- Section 4: composite
+------------------------------------------------------------------------
+
+||| Main theorem: the step preconditions build_edges/1 maintains hold for
+||| every graph.
+export
+pagerankPreconditionsSound : (edges : List Edge) -> (e : Edge) -> (t : Nat) ->
+  (LTE 0 e.weight, LTE 0 (outWeightSum edges e.src), LTE 0 (inWeightSum edges t))
+pagerankPreconditionsSound edges e t =
+  (edgeWeightNonneg e, outWeightSumNonneg edges e.src, inWeightSumNonneg edges t)
diff --git a/verification/proofs/idris2/ParserTotality.idr b/verification/proofs/idris2/ParserTotality.idr
new file mode 100644
index 00000000..a45f3194
--- /dev/null
+++ b/verification/proofs/idris2/ParserTotality.idr
@@ -0,0 +1,145 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- ParserTotality.idr — totality and round trips of the VCL FROM-clause parser.
+--
+-- Re-homed from verification/proofs/lean4/ParserTotality.lean (PROOF-POLICY
+-- section 3). The statements are the Lean file's; the Lean proofs rested on
+-- the kernel axiom propext, which Idris2 does not have.
+--
+-- Models a representative subset of `parse_from/1` in lib/vcl/: FROM STORE,
+-- FROM FEDERATION and FROM HEXAD, each followed by a bare identifier or (for
+-- STORE and FEDERATION) a quoted literal; anything else is an error. The
+-- model omits unquoted URLs, WITH DRIFT and multi-URL sources. It does not
+-- show that the Elixir parser follows it.
+
+module ParserTotality
+
+%default total
+
+------------------------------------------------------------------------
+-- Section 1: tokens, sources, errors, results
+------------------------------------------------------------------------
+
+||| Tokens from the VCL tokenizer; quoted literals are kept apart from bare
+||| identifiers so the parser's two paths can be modelled separately.
+public export
+data Token
+  = KwFrom
+  | KwStore
+  | KwFederation
+  | KwHexad
+  | Ident String
+  | Quoted String
+  | Other String
+
+||| The parsed source: {:store, id}, {:federation, pattern}, {:hexad, uuid}.
+public export
+data Source = Store String | Federation String | Hexad String
+
+||| Parser errors, structured for the proofs.
+public export
+data ParseError = ExpectedFromClause | EmptyInput | Malformed
+
+||| A result: a value and the tokens left over, or an error.
+public export
+data ParseResult a = Ok a (List Token) | Err ParseError
+
+------------------------------------------------------------------------
+-- Section 2: the parser
+------------------------------------------------------------------------
+
+||| Parse a FROM clause. `%default total` makes the checker refuse this
+||| definition unless it covers every input and terminates: the
+||| definition checking is the totality proof.
+public export
+parseFrom : List Token -> ParseResult Source
+parseFrom (KwFrom :: KwStore :: Ident id :: rest)        = Ok (Store id) rest
+parseFrom (KwFrom :: KwStore :: Quoted id :: rest)       = Ok (Store id) rest
+parseFrom (KwFrom :: KwFederation :: Ident pat :: rest)  = Ok (Federation pat) rest
+parseFrom (KwFrom :: KwFederation :: Quoted pat :: rest) = Ok (Federation pat) rest
+parseFrom (KwFrom :: KwHexad :: Ident u :: rest)         = Ok (Hexad u) rest
+parseFrom []                                             = Err EmptyInput
+parseFrom _                                              = Err ExpectedFromClause
+
+------------------------------------------------------------------------
+-- Section 3: totality as a structural property
+------------------------------------------------------------------------
+
+||| Property 1: parseFrom is a function: equal inputs give equal results.
+export
+parseFromDeterministic : (ts : List Token) -> parseFrom ts = parseFrom ts
+parseFromDeterministic _ = Refl
+
+||| Property 2: empty input gives the empty-input error.
+export
+parseFromEmpty : parseFrom [] = Err EmptyInput
+parseFromEmpty = Refl
+
+------------------------------------------------------------------------
+-- Section 4: round trips on well-formed input
+------------------------------------------------------------------------
+
+||| Property 4: FROM STORE <ident> gives a store.
+export
+parseFromStoreBare : parseFrom [KwFrom, KwStore, Ident "scans"] = Ok (Store "scans") []
+parseFromStoreBare = Refl
+
+||| Property 5: FROM STORE "quoted" gives a store.
+export
+parseFromStoreQuoted : parseFrom [KwFrom, KwStore, Quoted "scans"] = Ok (Store "scans") []
+parseFromStoreQuoted = Refl
+
+||| Property 6: FROM FEDERATION <ident> gives a federation, pattern kept.
+export
+parseFromFederation : parseFrom [KwFrom, KwFederation, Ident "/scans/*"]
+                      = Ok (Federation "/scans/*") []
+parseFromFederation = Refl
+
+||| Property 7: FROM HEXAD <uuid> gives a hexad.
+export
+parseFromHexad : parseFrom [KwFrom, KwHexad, Ident "abc-123"] = Ok (Hexad "abc-123") []
+parseFromHexad = Refl
+
+||| Property 8: tokens after a valid FROM clause are passed on, so the
+||| WHERE / LIMIT / OFFSET parsers still see them.
+export
+parseFromPassesRemainder :
+  parseFrom [KwFrom, KwStore, Ident "scans", Other "WHERE", Other "FIELD"]
+  = Ok (Store "scans") [Other "WHERE", Other "FIELD"]
+parseFromPassesRemainder = Refl
+
+------------------------------------------------------------------------
+-- Section 5: malformed input is rejected
+------------------------------------------------------------------------
+
+||| Property 9: FROM with no STORE / FEDERATION / HEXAD is rejected.
+export
+parseFromOrphanFrom : parseFrom [KwFrom] = Err ExpectedFromClause
+parseFromOrphanFrom = Refl
+
+||| Property 10: a clause without FROM is rejected.
+export
+parseFromNoFromKeyword : parseFrom [KwStore, Ident "scans"] = Err ExpectedFromClause
+parseFromNoFromKeyword = Refl
+
+------------------------------------------------------------------------
+-- Section 6: a Bool view of success
+------------------------------------------------------------------------
+
+||| Did the parse succeed?
+public export
+parseFromSucceeded : List Token -> Bool
+parseFromSucceeded ts = case parseFrom ts of
+  Ok _ _ => True
+  Err _  => False
+
+||| Property 11: the predicate agrees with the parser on FROM STORE.
+export
+parseFromSucceededStore : parseFromSucceeded [KwFrom, KwStore, Ident "scans"] = True
+parseFromSucceededStore = Refl
+
+||| Property 12: the predicate is false on empty input.
+export
+parseFromSucceededEmpty : parseFromSucceeded [] = False
+parseFromSucceededEmpty = Refl
diff --git a/verification/proofs/idris2/RateLimiting.idr b/verification/proofs/idris2/RateLimiting.idr
new file mode 100644
index 00000000..e9cbd803
--- /dev/null
+++ b/verification/proofs/idris2/RateLimiting.idr
@@ -0,0 +1,222 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- RateLimiting.idr — the sliding-window rate limiter never exceeds its bound.
+--
+-- Re-homed from verification/proofs/lean4/RateLimiting.lean (PROOF-POLICY
+-- section 3: interface and engineering statements live in Idris2). The
+-- statements are the Lean file's, theorem for theorem; the Lean proofs rested
+-- on the kernel axioms propext and Quot.sound, which Idris2 does not have.
+--
+-- Models lib/safety/rate_limiter.ex, which enforces
+--   per-bot 50 / 60 s, global 200 / 60 s, burst 10 / 5 s.
+-- Over Nat timestamps and counts. The model does not show that the Elixir
+-- GenServer follows it, and the GenServer is not on any dispatch path
+-- (CLAUDE.md Known Gap 2).
+
+module RateLimiting
+
+import Control.Relation
+import Data.Nat
+import Data.List
+import Data.List.Quantifiers
+
+%default total
+
+------------------------------------------------------------------------
+-- Section 1: window-based counter model
+------------------------------------------------------------------------
+
+||| A rate-limiter configuration: the most events allowed in a window.
+public export
+record RateLimitConfig where
+  constructor MkRateLimitConfig
+  maxEvents      : Nat
+  windowSize     : Nat
+  windowPositive : LT 0 windowSize
+
+||| A timestamped event.
+public export
+record Event where
+  constructor MkEvent
+  timestamp : Nat
+
+||| The limiter's state: its configuration and the events it has accepted.
+public export
+record RateLimiterState where
+  constructor MkRateLimiterState
+  config : RateLimitConfig
+  events : List Event
+
+||| Is the event inside a window that starts at `windowStart`?
+public export
+inWindow : (windowStart : Nat) -> Event -> Bool
+inWindow windowStart e = windowStart <= e.timestamp
+
+||| Events within [windowStart, now].
+public export
+countEventsInWindow : List Event -> (windowStart : Nat) -> Nat
+countEventsInWindow es windowStart = length (filter (inWindow windowStart) es)
+
+||| The start of the window that ends at `now`.
+public export
+windowStart : RateLimiterState -> (now : Nat) -> Nat
+windowStart state now = minus now state.config.windowSize
+
+||| The in-window count at `now`.
+public export
+currentCount : RateLimiterState -> (now : Nat) -> Nat
+currentCount state now = countEventsInWindow state.events (windowStart state now)
+
+||| Accept the event only if the in-window count is below the maximum.
+public export
+tryAccept : RateLimiterState -> Event -> (RateLimiterState, Bool)
+tryAccept (MkRateLimiterState cfg evs) e
+  with (isLT (countEventsInWindow evs (minus e.timestamp cfg.windowSize)) cfg.maxEvents)
+  _ | Yes _ = (MkRateLimiterState cfg (e :: evs), True)
+  _ | No _  = (MkRateLimiterState cfg evs, False)
+
+||| Drop the events outside the window (garbage collection).
+public export
+prune : RateLimiterState -> (now : Nat) -> RateLimiterState
+prune state@(MkRateLimiterState cfg evs) now = MkRateLimiterState cfg (filter (inWindow (windowStart state now)) evs)
+
+------------------------------------------------------------------------
+-- Section 2: the invariant
+------------------------------------------------------------------------
+
+||| The in-window count never exceeds maxEvents.
+public export
+InvariantHolds : RateLimiterState -> (now : Nat) -> Type
+InvariantHolds state now = LTE (currentCount state now) state.config.maxEvents
+
+||| An empty limiter satisfies the invariant.
+export
+emptySatisfiesInvariant : (config : RateLimitConfig) -> (now : Nat) ->
+                          InvariantHolds (MkRateLimiterState config []) now
+emptySatisfiesInvariant _ _ = LTEZero
+
+||| Filtering never lengthens a list.
+export
+filterLengthLTE : (p : a -> Bool) -> (xs : List a) -> LTE (length (filter p xs)) (length xs)
+filterLengthLTE p [] = LTEZero
+filterLengthLTE p (x :: xs) with (p x)
+  _ | True  = LTESucc (filterLengthLTE p xs)
+  _ | False = lteSuccRight (filterLengthLTE p xs)
+
+------------------------------------------------------------------------
+-- Section 3: tryAccept preserves the invariant
+------------------------------------------------------------------------
+
+||| One more event at the front raises the in-window count by at most one.
+export
+countConsLTE : (e : Event) -> (es : List Event) -> (ws : Nat) ->
+               LTE (countEventsInWindow (e :: es) ws) (S (countEventsInWindow es ws))
+countConsLTE e es ws with (inWindow ws e)
+  _ | True  = reflexive
+  _ | False = lteSuccRight reflexive
+
+||| After tryAccept the invariant still holds: a rejected event leaves the
+||| state unchanged, and an accepted one was admitted below the maximum.
+export
+tryAcceptPreservesInvariant : (state : RateLimiterState) -> (e : Event) ->
+                              InvariantHolds state e.timestamp ->
+                              InvariantHolds (fst (tryAccept state e)) e.timestamp
+tryAcceptPreservesInvariant (MkRateLimiterState cfg evs) e h
+  with (isLT (countEventsInWindow evs (minus e.timestamp cfg.windowSize)) cfg.maxEvents)
+  _ | Yes below =
+        transitive (countConsLTE e evs (minus e.timestamp cfg.windowSize)) below
+  _ | No _ = h
+
+------------------------------------------------------------------------
+-- Section 4: prune preserves the invariant
+------------------------------------------------------------------------
+
+||| Pruning only removes events, so the count can only fall.
+export
+prunePreservesInvariant : (state : RateLimiterState) -> (now : Nat) ->
+                          InvariantHolds state now ->
+                          InvariantHolds (prune state now) now
+prunePreservesInvariant state@(MkRateLimiterState cfg evs) now h =
+  transitive (filterLengthLTE (inWindow (windowStart state now))
+                              (filter (inWindow (windowStart state now)) evs)) h
+
+------------------------------------------------------------------------
+-- Section 5: a sequence of events
+------------------------------------------------------------------------
+
+||| Offer each event in turn; keep the state tryAccept returns.
+public export
+processEvents : RateLimiterState -> List Event -> RateLimiterState
+processEvents state [] = state
+processEvents state (e :: es) = processEvents (fst (tryAccept state e)) es
+
+||| The invariant holds after any sequence of simultaneous events (the
+||| worst-case burst), if it held at the start.
+export
+processEventsPreservesInvariant : (state : RateLimiterState) -> (es : List Event) ->
+                                  (t : Nat) -> All (\e => e.timestamp = t) es ->
+                                  InvariantHolds state t ->
+                                  InvariantHolds (processEvents state es) t
+processEventsPreservesInvariant state [] t [] h = h
+processEventsPreservesInvariant state (e :: es) t (prf :: prfs) h =
+  processEventsPreservesInvariant (fst (tryAccept state e)) es t prfs step
+  where
+    step : InvariantHolds (fst (tryAccept state e)) t
+    step = rewrite sym prf in
+             tryAcceptPreservesInvariant state e (rewrite prf in h)
+
+------------------------------------------------------------------------
+-- Section 6: the deployed configurations
+------------------------------------------------------------------------
+
+||| Per-bot: 50 events per 60 s.
+public export
+perBotConfig : RateLimitConfig
+perBotConfig = MkRateLimitConfig 50 60 (LTESucc LTEZero)
+
+||| Global: 200 events per 60 s.
+public export
+globalConfig : RateLimitConfig
+globalConfig = MkRateLimitConfig 200 60 (LTESucc LTEZero)
+
+||| Burst: 10 events per 5 s.
+public export
+burstConfig : RateLimitConfig
+burstConfig = MkRateLimitConfig 10 5 (LTESucc LTEZero)
+
+export
+perBotInitialValid : (now : Nat) -> InvariantHolds (MkRateLimiterState RateLimiting.perBotConfig []) now
+perBotInitialValid = emptySatisfiesInvariant perBotConfig
+
+export
+globalInitialValid : (now : Nat) -> InvariantHolds (MkRateLimiterState RateLimiting.globalConfig []) now
+globalInitialValid = emptySatisfiesInvariant globalConfig
+
+export
+burstInitialValid : (now : Nat) -> InvariantHolds (MkRateLimiterState RateLimiting.burstConfig []) now
+burstInitialValid = emptySatisfiesInvariant burstConfig
+
+------------------------------------------------------------------------
+-- Section 7: the rejection guarantee
+------------------------------------------------------------------------
+
+||| At the limit, the next event is rejected.
+export
+atLimitRejects : (state : RateLimiterState) -> (e : Event) ->
+                 currentCount state e.timestamp = state.config.maxEvents ->
+                 snd (tryAccept state e) = False
+atLimitRejects (MkRateLimiterState cfg evs) e full
+  with (isLT (countEventsInWindow evs (minus e.timestamp cfg.windowSize)) cfg.maxEvents)
+  _ | Yes below = absurd (succNotLTEpred (replace {p = \m => LT (countEventsInWindow evs (minus e.timestamp cfg.windowSize)) m} (sym full) below))
+  _ | No _ = Refl
+
+||| From an empty limiter, any burst of simultaneous offers keeps the count
+||| within the bound.
+export
+countBoundedAfterAccepts : (config : RateLimitConfig) -> (es : List Event) -> (t : Nat) ->
+                           All (\e => e.timestamp = t) es ->
+                           InvariantHolds (processEvents (MkRateLimiterState config []) es) t
+countBoundedAfterAccepts config es t times =
+  processEventsPreservesInvariant (MkRateLimiterState config []) es t times
+    (emptySatisfiesInvariant config t)
diff --git a/verification/proofs/lean4/.gitignore b/verification/proofs/lean4/.gitignore
deleted file mode 100644
index d13c5071..00000000
--- a/verification/proofs/lean4/.gitignore
+++ /dev/null
@@ -1,4 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-# Lake build artifacts
-/.lake/
-/lake-manifest.json
diff --git a/verification/proofs/lean4/BayesianUpdate.lean b/verification/proofs/lean4/BayesianUpdate.lean
deleted file mode 100644
index bcdbcafe..00000000
--- a/verification/proofs/lean4/BayesianUpdate.lean
+++ /dev/null
@@ -1,188 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
---
--- BayesianUpdate.lean — Formal proof of Bayesian confidence update soundness (H7).
---
--- REQUIREMENTS-MASTER.md: H7 | Bayesian confidence update soundness | ALG | L4 | P1
---
--- Models the Beta-conjugate prior update in lib/outcome_tracker.ex.
--- No external dependencies (no Mathlib required).
---
--- We represent confidence as a pair (α : Nat, β : Nat) where:
---   α > 0, β > 0 (ensures the fraction is in (0,1))
---   confidence = α / (α + β)   (real value, but we prove properties via ℕ cross-mult)
---
--- The production update (prior_strength = 10):
---   α_prior  = prior_confidence * 10
---   β_prior  = (1 - prior_confidence) * 10
---   α_post   = α_prior + successes
---   β_post   = β_prior + failures
---   posterior = α_post / (α_post + β_post)
---   result   = clamp(posterior, floor=10%, cap=99%)
---
--- All ratio comparisons are done by cross-multiplication over ℕ to avoid
--- floating-point and to stay within the standard library.
-
-------------------------------------------------------------------------
--- Section 1: Fraction comparison over ℕ
---
--- a/b ≤ c/d  (with b,d > 0)  iff  a*d ≤ c*b
-------------------------------------------------------------------------
-
-/-- α / (α+β) < 1  iff  β > 0.
-    Proof: α / (α+β) < 1  iff  α < α+β  iff  0 < β. -/
-theorem frac_lt_one (α β : Nat) (hβ : 0 < β) : α < α + β := Nat.lt_add_of_pos_right hβ
-
-/-- α / (α+β) > 0  iff  α > 0.
-    Proof: 0 < α / (α+β)  iff  0 * (α+β) < α * 1  iff  0 < α. -/
-theorem frac_pos (α : Nat) (hα : 0 < α) : 0 < α := hα
-
-/-- Denominator α+β > 0 when both α,β ≥ 0 and α > 0. -/
-theorem denom_pos (α β : Nat) (hα : 0 < α) : 0 < α + β := Nat.lt_of_lt_of_le hα (Nat.le_add_right α β)
-
-------------------------------------------------------------------------
--- Section 2: The beta update
-------------------------------------------------------------------------
-
-/-- Parameters for the Bayesian update. -/
-structure BayesParams where
-  α     : Nat    -- alpha_posterior = alpha_prior + successes
-  β     : Nat    -- beta_posterior  = beta_prior + failures
-  hα    : 0 < α  -- α > 0
-  hβ    : 0 < β  -- β > 0
-
-namespace BayesParams
-
-/-- Denominator α + β. -/
-def denom (p : BayesParams) : Nat := p.α + p.β
-
-/-- Denominator is positive. -/
-theorem denom_pos (p : BayesParams) : 0 < p.denom :=
-  Nat.lt_of_lt_of_le p.hα (Nat.le_add_right p.α p.β)
-
-------------------------------------------------------------------------
--- Section 3: Posterior is in (0, 1)
---
--- We prove this via the cross-multiplication inequality:
---   0 < α/(α+β) < 1  iff  0 < α  and  α < α+β
-------------------------------------------------------------------------
-
-/-- H7 — PROPERTY 1: α/(α+β) is strictly less than 1.
-    Cross-multiplication: α < α + β  iff  0 < β. -/
-theorem posterior_lt_one (p : BayesParams) : p.α < p.denom :=
-  Nat.lt_add_of_pos_right p.hβ
-
-/-- H7 — PROPERTY 2: α/(α+β) is strictly greater than 0.
-    (α > 0 by construction.) -/
-theorem posterior_pos (p : BayesParams) : 0 < p.α := p.hα
-
-------------------------------------------------------------------------
--- Section 4: Monotonicity theorems
---
--- We prove via cross-multiplication:
---   α/(α+β) ≤ (α+1)/(α+1+β)
---   iff  α * (α+1+β) ≤ (α+1) * (α+β)
---   iff  α²+αβ+α ≤ α²+αβ+α+β
---   iff  0 ≤ β  ✓
-------------------------------------------------------------------------
-
-/-- H7 — PROPERTY 3: Adding a success (α+1) weakly increases the ratio.
-    Cross-multiplication proof: α*(α+1+β) ≤ (α+1)*(α+β).
-    Key identity: (α+1)*(α+β) = α*(α+β) + (α+β)  and  α*(α+1+β) = α*(α+β) + α.
-    Since α ≤ α+β, the claim follows. -/
-theorem more_successes_raises (p : BayesParams) :
-    p.α * (p.α + 1 + p.β) ≤ (p.α + 1) * (p.α + p.β) := by
-  -- Step 1: α*(α+1+β) = α*(α+β) + α
-  have hs1 : p.α * (p.α + 1 + p.β) = p.α * (p.α + p.β) + p.α := by
-    have : p.α + 1 + p.β = (p.α + p.β) + 1 := by omega
-    rw [this, Nat.mul_add, Nat.mul_one]
-  -- Step 2: (α+1)*(α+β) = α*(α+β) + (α+β)
-  have hs2 : (p.α + 1) * (p.α + p.β) = p.α * (p.α + p.β) + (p.α + p.β) := by
-    rw [Nat.add_mul, Nat.one_mul]
-  rw [hs1, hs2]
-  -- Goal: α*(α+β) + α ≤ α*(α+β) + (α+β)
-  exact Nat.add_le_add_left (Nat.le_add_right p.α p.β) _
-
-/-- H7 — PROPERTY 4: Adding a failure (β+1) weakly decreases the ratio.
-    α*(α+β) ≤ α*(α+β+1)  since α+β ≤ α+β+1. -/
-theorem more_failures_lowers (p : BayesParams) :
-    p.α * (p.α + p.β) ≤ p.α * (p.α + p.β + 1) :=
-  Nat.mul_le_mul_left p.α (Nat.le_add_right _ 1)
-
-------------------------------------------------------------------------
--- Section 5: Zero observations returns prior
---
--- With no observations: α_post = α_prior, β_post = β_prior.
--- So the ratio α_post/(α_post+β_post) = α_prior/(α_prior+β_prior) = prior.
--- This is a definitional equality — represented by Refl below.
-------------------------------------------------------------------------
-
-/-- Represent the prior as a fraction. -/
-structure Prior where
-  α_p : Nat    -- prior alpha  (e.g., prior_confidence * 10)
-  β_p : Nat    -- prior beta   (e.g., (1 - prior_confidence) * 10)
-  hα  : 0 < α_p
-  hβ  : 0 < β_p
-
-/-- Construct a BayesParams with zero successes and zero failures. -/
-def fromPrior (p : Prior) : BayesParams where
-  α  := p.α_p
-  β  := p.β_p
-  hα := p.hα
-  hβ := p.hβ
-
-/-- H7 — PROPERTY 5: Zero observations — posterior alpha = prior alpha. -/
-theorem zero_obs_alpha (p : Prior) :
-    (fromPrior p).α = p.α_p := rfl
-
-/-- H7 — PROPERTY 6: Zero observations — posterior beta = prior beta. -/
-theorem zero_obs_beta (p : Prior) :
-    (fromPrior p).β = p.β_p := rfl
-
-/-- H7 — PROPERTY 7: Zero observations — denominator unchanged. -/
-theorem zero_obs_denom (p : Prior) :
-    (fromPrior p).denom = p.α_p + p.β_p := rfl
-
-------------------------------------------------------------------------
--- Section 6: Floor and cap (10% and 99%)
---
--- The production clamp is: max(0.10, min(0.99, posterior)).
--- We represent:
---   floor = 1/10  (10%)  ↔  cross-mult: α/(α+β) ≥ 1/10  iff  10α ≥ α+β  iff  9α ≥ β
---   cap   = 99/100 (99%) ↔  cross-mult: α/(α+β) ≤ 99/100 iff  100α ≤ 99(α+β) iff  α ≤ 99β
---
--- After clamping with max and min, the result is definitionally in [floor, cap].
-------------------------------------------------------------------------
-
-/-- H7 — PROPERTY 8: The clamped result is ≥ floor (1/10).
-    Proof: max(1/10, x) ≥ 1/10 by definition of max. -/
-theorem clamp_ge_floor (raw : Nat) : max 1 raw ≥ 1 := Nat.le_max_left 1 raw
-
-/-- H7 — PROPERTY 9: The clamped result is ≤ cap (99/100).
-    Proof: min(99, x) ≤ 99 by definition of min. -/
-theorem clamp_le_cap (raw : Nat) : min raw 99 ≤ 99 := Nat.min_le_right raw 99
-
-------------------------------------------------------------------------
--- Section 7: Composite validity theorem
---
--- The Bayesian update is valid if:
---   1. α_post > 0  (posterior numerator positive)
---   2. β_post > 0  (posterior denominator positive → ratio < 1)
---   3. Adding successes doesn't decrease the ratio (monotonicity)
---   4. Adding failures doesn't increase the ratio (monotonicity)
--- All four hold constructively by the theorems above.
-------------------------------------------------------------------------
-
-/-- H7 — MAIN THEOREM: Bayesian update soundness.
-    A BayesParams with α,β > 0 satisfies all validity conditions. -/
-theorem bayesian_update_sound (p : BayesParams) :
-    0 < p.α                                              -- numerator positive
-    ∧ p.α < p.denom                                      -- fraction < 1
-    ∧ p.α * (p.α + 1 + p.β) ≤ (p.α + 1) * (p.α + p.β) -- more successes ↑
-    ∧ p.α * (p.α + p.β) ≤ p.α * (p.α + p.β + 1) :=    -- more failures ↓
-  ⟨p.posterior_pos,
-   p.posterior_lt_one,
-   more_successes_raises p,
-   more_failures_lowers p⟩
-
-end BayesParams
diff --git a/verification/proofs/lean4/ESNSpectralScaling.lean b/verification/proofs/lean4/ESNSpectralScaling.lean
deleted file mode 100644
index ff65c34d..00000000
--- a/verification/proofs/lean4/ESNSpectralScaling.lean
+++ /dev/null
@@ -1,148 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
---
--- ESNSpectralScaling.lean — Structural preconditions for ESN echo-state
--- stability, proven over ℕ.
---
--- PROOFS-GAP.md: Neural Property 2 — ESN spectral-radius stability.
---
--- Context: `lib/neural/echo_state_network.ex` scales the reservoir
--- matrix so its induced infinity-norm (the largest absolute row sum) is
--- a configured `@reservoir_norm` (default 0.95):
---
---     max_row_sum = matrix |> map(row -> sum(map(row, abs))) |> max(1.0)
---     scale       = @reservoir_norm / max(max_row_sum, 0.001)
---     scaled      = Enum.map(matrix, fn row -> Enum.map(row, &(&1 * scale)) end)
---
--- That scaling is the runtime enforcement of the echo-state property.
--- With ‖R‖∞ < 1, leak rate a and tanh (1-Lipschitz), the update
--- `x ↦ (1 - a)·x + a·tanh(R·x + w·u)` is a contraction in the sup norm
--- with modulus `1 - a + a·‖R‖∞`, so the state trajectory forgets its
--- initial state exponentially. (Until 2026-10 the runtime scaled the
--- largest single entry instead, which does not bound ‖R‖∞: the 80-node
--- reservoir had a spectral radius near 2 and the property failed.) The
--- analytical half of that statement needs Mathlib — out of scope for
--- the Mathlib-free proof set (see the header note in
--- BayesianUpdate.lean).
---
--- What this file proves, over ℕ, is that the **scaling operation is
--- well-defined**: the floor-guarded `max(max_row_sum, floor)`
--- denominator is strictly positive whenever the floor is, which is the
--- load-bearing precondition for avoiding divide-by-zero in the
--- runtime. The Mathlib follow-up is tracked in
--- docs/proofs/HANDOVER-neural-convergence.adoc.
-
-------------------------------------------------------------------------
--- Section 1: The model
---
--- Reservoir entries are ℕ (scaled integer magnitudes; negatives and
--- rationals would require Mathlib). The norm is the max over rows of
--- each row's sum of entry magnitudes. Scaling is integer division by
--- the ratio (norm / target).
-------------------------------------------------------------------------
-
-/-- Matrix as a list of rows. -/
-def Matrix := List (List Nat)
-
-/-- Each row's sum of entry magnitudes. Mirrors
-    `Enum.map(row, &abs/1) |> Enum.sum()` in Elixir. -/
-def rowSums (m : Matrix) : List Nat := m.map List.sum
-
-/-- Pointwise max of a list of ℕ with a provided floor for the empty
-    case. Mirrors `Enum.max(fn -> 1.0 end)` in Elixir. -/
-def maxAbsOr (xs : List Nat) (floor : Nat) : Nat :=
-  xs.foldl (fun acc x => if x > acc then x else acc) floor
-
-/-- Induced infinity-norm (largest row sum) of a matrix, with a floor. -/
-def matrixMaxAbs (m : Matrix) (floor : Nat) : Nat :=
-  maxAbsOr (rowSums m) floor
-
-/-- Scaling ratio of target to the norm under a positive floor.
-    Models `scale = reservoir_norm / max(max_row_sum, 0.001)` in Elixir. -/
-def scaleRatio (target maxAbs floor : Nat) : Nat :=
-  target / (max maxAbs floor)
-
-------------------------------------------------------------------------
--- Section 2: Empty-matrix base cases
-------------------------------------------------------------------------
-
-/-- ESN — PROPERTY 1: An empty matrix has no row sums. -/
-theorem rowSums_nil : rowSums [] = [] := rfl
-
-/-- ESN — PROPERTY 2: `maxAbsOr` on an empty list returns the floor. -/
-theorem maxAbsOr_nil (floor : Nat) : maxAbsOr [] floor = floor := rfl
-
-/-- ESN — PROPERTY 3: An empty matrix has norm equal to its floor. -/
-theorem matrixMaxAbs_nil (floor : Nat) : matrixMaxAbs [] floor = floor := rfl
-
-------------------------------------------------------------------------
--- Section 3: Non-negativity — ℕ-trivial but load-bearing downstream
-------------------------------------------------------------------------
-
-/-- ESN — PROPERTY 4: The norm is non-negative for any matrix. -/
-theorem matrixMaxAbs_nonneg (m : Matrix) (floor : Nat) :
-    0 ≤ matrixMaxAbs m floor := Nat.zero_le _
-
-/-- ESN — PROPERTY 5: The scaling ratio itself is non-negative. -/
-theorem scaleRatio_nonneg (target maxAbs floor : Nat) :
-    0 ≤ scaleRatio target maxAbs floor := Nat.zero_le _
-
-------------------------------------------------------------------------
--- Section 4: The denominator is strictly positive
---
--- The runtime uses `max(max_row_sum, 0.001)` precisely to keep the
--- denominator above zero. In ℕ land the positive floor is any
--- non-zero constant. This is the load-bearing precondition: without
--- it the scaling operation would divide by zero at runtime.
-------------------------------------------------------------------------
-
-/-- ESN — PROPERTY 6: When the floor is strictly positive, so is the
-    floor-clamped max. This guarantees the scaling ratio's denominator
-    is non-zero. -/
-theorem denom_pos_when_floor_pos (maxAbs floor : Nat) (hf : 0 < floor) :
-    0 < max maxAbs floor :=
-  Nat.lt_of_lt_of_le hf (Nat.le_max_right maxAbs floor)
-
-/-- ESN — PROPERTY 7: If the raw `maxAbs` happens to be positive, the
-    clamped denominator is at least `maxAbs`. Lets downstream proofs
-    reason about the ratio without relying on the floor. -/
-theorem denom_ge_maxAbs (maxAbs floor : Nat) :
-    maxAbs ≤ max maxAbs floor := Nat.le_max_left maxAbs floor
-
-/-- ESN — PROPERTY 8: The clamped denominator is at least the floor.
-    Symmetric to PROPERTY 7; completes the "max is an upper-bound of
-    both" lemma. -/
-theorem denom_ge_floor (maxAbs floor : Nat) :
-    floor ≤ max maxAbs floor := Nat.le_max_right maxAbs floor
-
-------------------------------------------------------------------------
--- Section 5: Composite soundness theorem
-------------------------------------------------------------------------
-
-/-- ESN — MAIN THEOREM: The scaling preconditions that
-    `lib/neural/echo_state_network.ex` `generate_reservoir/1` enforces
-    are structurally sound.
-
-    For any reservoir matrix and any strictly-positive floor:
-
-      1. Max-abs is non-negative (ℕ-trivial).
-      2. The floor-clamped denominator is strictly positive, so the
-         scaling ratio is well-defined.
-      3. The clamped denominator is bounded below by both `max_row_sum`
-         and `floor`.
-
-    These are the preconditions a Mathlib-based echo-state-property
-    proof (trajectory boundedness + exponential forgetting) would
-    take as hypotheses. The analytical half is deferred until
-    Mathlib joins the Lean proof set — tracked as PR 5 in
-    PROOFS-GAP.md. -/
-theorem esn_scaling_preconditions_sound
-    (m : Matrix) (maxAbs floor : Nat) (hf : 0 < floor) :
-    (0 ≤ matrixMaxAbs m floor) ∧
-    (0 < max maxAbs floor) ∧
-    (maxAbs ≤ max maxAbs floor) ∧
-    (floor ≤ max maxAbs floor) :=
-  ⟨matrixMaxAbs_nonneg m floor,
-   denom_pos_when_floor_pos maxAbs floor hf,
-   denom_ge_maxAbs maxAbs floor,
-   denom_ge_floor maxAbs floor⟩
diff --git a/verification/proofs/lean4/PageRankInvariants.lean b/verification/proofs/lean4/PageRankInvariants.lean
deleted file mode 100644
index 48c258fe..00000000
--- a/verification/proofs/lean4/PageRankInvariants.lean
+++ /dev/null
@@ -1,120 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
---
--- PageRankInvariants.lean — Algebraic preconditions for PageRank
--- convergence, proven over ℕ.
---
--- PROOFS-GAP.md: Neural Property 1 — PageRank power-iteration convergence.
---
--- Context: `lib/neural/graph_of_trust.ex` (after the quality-gates
--- fix) enforces:
---
---   1. Every edge weight is non-negative.
---   2. Each source's outgoing contributions are divided by its
---      outgoing-weight sum — column-stochastic normalisation.
---   3. The damping factor α lies in [0, 1].
---
--- A full analytical convergence theorem (Banach contraction
--- mapping on ℝⁿ with α < 1) requires real analysis, which pulls in
--- Mathlib — out of scope for the Mathlib-free proof set (see the
--- header note in BayesianUpdate.lean).
---
--- What this file proves, over a ℕ model, are the structural
--- invariants the Elixir runtime now upholds and an analytical
--- proof would take as hypotheses:
---
---   • Edge weights are non-negative.
---   • Outgoing-weight sums are non-negative.
---   • For a graph with no edges, every outgoing-weight sum is 0.
---
--- The Mathlib-backed follow-up is tracked as PR 4 in PROOFS-GAP.md.
-
-------------------------------------------------------------------------
--- Section 1: The model
---
--- Scores and weights are ℕ with a shared scale. Weights on edges are
--- absolute integer counts; normalisation is handled by dividing by
--- the source's outgoing-weight sum. This sidesteps rational
--- arithmetic entirely while still capturing the load-bearing
--- properties.
-------------------------------------------------------------------------
-
-/-- A weighted directed edge. -/
-structure Edge where
-  src    : Nat
-  tgt    : Nat
-  weight : Nat
-  deriving Repr, DecidableEq
-
-/-- Sum of outgoing edge weights from a given source. -/
-def outWeightSum (edges : List Edge) (src : Nat) : Nat :=
-  (edges.filter (fun e => e.src = src)).foldl (fun acc e => acc + e.weight) 0
-
-/-- Total incoming weight into a given target. -/
-def inWeightSum (edges : List Edge) (tgt : Nat) : Nat :=
-  (edges.filter (fun e => e.tgt = tgt)).foldl (fun acc e => acc + e.weight) 0
-
-------------------------------------------------------------------------
--- Section 2: Non-negativity
---
--- ℕ has no negative values, so these are definitional. Stating them
--- here pins the preconditions the Elixir fix (`build_edges/1`) now
--- maintains.
-------------------------------------------------------------------------
-
-/-- PAGERANK — PROPERTY 1: Edge weights are non-negative. -/
-theorem edge_weight_nonneg (e : Edge) : 0 ≤ e.weight := Nat.zero_le _
-
-/-- PAGERANK — PROPERTY 2: The outgoing-weight sum is non-negative
-    for every source, regardless of graph shape. -/
-theorem outWeightSum_nonneg (edges : List Edge) (src : Nat) :
-    0 ≤ outWeightSum edges src := Nat.zero_le _
-
-/-- PAGERANK — PROPERTY 3: The incoming-weight sum is non-negative
-    for every target. -/
-theorem inWeightSum_nonneg (edges : List Edge) (tgt : Nat) :
-    0 ≤ inWeightSum edges tgt := Nat.zero_le _
-
-------------------------------------------------------------------------
--- Section 3: Empty-graph base cases
---
--- An empty graph has zero outgoing and incoming weight at every
--- node. The Elixir runtime uses this to short-circuit the iteration
--- — a node with no outgoing edges contributes only through the
--- teleport term `(1 - α) / n`.
-------------------------------------------------------------------------
-
-/-- PAGERANK — PROPERTY 4: An empty edge list has zero outgoing
-    weight at every source. -/
-theorem outWeightSum_nil (src : Nat) :
-    outWeightSum [] src = 0 := rfl
-
-/-- PAGERANK — PROPERTY 5: An empty edge list has zero incoming
-    weight at every target. -/
-theorem inWeightSum_nil (tgt : Nat) :
-    inWeightSum [] tgt = 0 := rfl
-
-------------------------------------------------------------------------
--- Section 4: Composite soundness theorem
-------------------------------------------------------------------------
-
-/-- PAGERANK — MAIN THEOREM: The PageRank iteration-step
-    preconditions enforced by `build_edges/1` in
-    `lib/neural/graph_of_trust.ex` are structurally sound.
-
-    For any graph:
-      1. Every edge weight is non-negative (ℕ-typed).
-      2. Every outgoing-weight sum is non-negative.
-      3. Every incoming-weight sum is non-negative.
-
-    These are the load-bearing preconditions for Banach-style
-    convergence. The analytical half (contraction + unique fixed
-    point) is deferred until Mathlib joins the Lean proof set. -/
-theorem pagerank_preconditions_sound
-    (edges : List Edge) (e : Edge) (tgt : Nat) :
-    (0 ≤ e.weight) ∧
-    (0 ≤ outWeightSum edges e.src) ∧
-    (0 ≤ inWeightSum edges tgt) :=
-  ⟨edge_weight_nonneg e,
-   outWeightSum_nonneg edges e.src,
-   inWeightSum_nonneg edges tgt⟩
diff --git a/verification/proofs/lean4/ParserTotality.lean b/verification/proofs/lean4/ParserTotality.lean
deleted file mode 100644
index 3bef09c7..00000000
--- a/verification/proofs/lean4/ParserTotality.lean
+++ /dev/null
@@ -1,191 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
---
--- ParserTotality.lean — Parser totality for the VCL `FROM` clause.
---
--- REQUIREMENTS-MASTER.md / PROOFS-GAP.md: VCL parser totality | L3 | P1
---
--- Hypatia's VCL query parser lives in `lib/vcl/client.ex` and dispatches on
--- pattern match against a token list. Clauses like:
---
---     defp parse_from(["FROM", "STORE", store_id | rest]) do ...
---     defp parse_from(["FROM", "FEDERATION", pattern | rest]) do ...
---     defp parse_from(_), do: {:error, ...}
---
--- The catch-all returns `{:error, _}` so the function is total in the
--- sense that every token stream produces a result — either a parsed
--- source tuple or an error.
---
--- This file formalises a representative subset of that dispatch,
--- shows it is total (Lean's default — the elaborator refuses
--- non-terminating functions without `partial`), and then establishes
--- a few concrete round-trip properties against well-formed inputs.
--- No external dependencies (no Mathlib required).
---
--- The model omits unquoted-URL, WITH-DRIFT, and multi-URL cases; the
--- pattern is identical and the shape of the proof scales linearly.
-
-------------------------------------------------------------------------
--- Section 1: Token / Source datatypes
-------------------------------------------------------------------------
-
-/-- Tokens produced by `Hypatia.VCL.Client.tokenize/1`. Quoted strings
-    are distinguished so the parser's two code paths (bare identifier
-    vs. quoted literal) can be modelled separately. -/
-inductive Token where
-  | kwFrom
-  | kwStore
-  | kwFederation
-  | kwHexad
-  | ident (s : String)
-  | quoted (s : String)
-  | other (s : String)
-  deriving Repr, DecidableEq
-
-/-- Parsed source tuple, mirroring what `parse_from/1` emits in Elixir:
-
-      {:store, store_id}
-      {:federation, pattern, drift_policy}
-      {:hexad, uuid}
-
-    `DriftPolicy` is left abstract here (always `none` in the subset
-    we model). -/
-inductive Source where
-  | store (id : String)
-  | federation (pattern : String)
-  | hexad (uuid : String)
-  deriving Repr, DecidableEq
-
-/-- Parser errors. The Elixir side returns a string; we keep it
-    structured for the proofs. -/
-inductive ParseError where
-  | expectedFromClause
-  | emptyInput
-  | malformed
-  deriving Repr, DecidableEq
-
-/-- A parse result either succeeds (with remaining tokens) or fails. -/
-inductive ParseResult (α : Type) where
-  | ok (value : α) (rest : List Token)
-  | err (e : ParseError)
-  deriving Repr
-
-------------------------------------------------------------------------
--- Section 2: The `parse_from` subset
---
--- Mirrors lib/vcl/client.ex `parse_from/1` for the three canonical
--- source shapes. Lean refuses non-total functions without `partial`,
--- so the very fact that this `def` elaborates is the totality proof.
-------------------------------------------------------------------------
-
-/-- Parse a FROM clause. Total over every input by construction
-    (Lean would reject a partial definition without the keyword). -/
-def parseFrom : List Token → ParseResult Source
-  | Token.kwFrom :: Token.kwStore :: Token.ident id :: rest =>
-      .ok (.store id) rest
-  | Token.kwFrom :: Token.kwStore :: Token.quoted id :: rest =>
-      .ok (.store id) rest
-  | Token.kwFrom :: Token.kwFederation :: Token.ident pat :: rest =>
-      .ok (.federation pat) rest
-  | Token.kwFrom :: Token.kwFederation :: Token.quoted pat :: rest =>
-      .ok (.federation pat) rest
-  | Token.kwFrom :: Token.kwHexad :: Token.ident u :: rest =>
-      .ok (.hexad u) rest
-  | [] => .err .emptyInput
-  | _ => .err .expectedFromClause
-
-------------------------------------------------------------------------
--- Section 3: Totality as a structural property
---
--- Totality is definitionally true — `parseFrom` is a `def`, not a
--- `partial def`, so Lean's termination checker has already approved
--- it. The theorems below pin concrete reference-transparency and
--- base-case properties without leaving tactic safety.
-------------------------------------------------------------------------
-
-/-- VCL PARSER — PROPERTY 1: `parseFrom` is deterministic.
-    Pattern matching is confluent; the same input always produces the
-    same output. -/
-theorem parseFrom_deterministic (ts : List Token) :
-    parseFrom ts = parseFrom ts := rfl
-
-/-- VCL PARSER — PROPERTY 2: Empty input produces the canonical
-    error, never a spurious success. -/
-theorem parseFrom_empty : parseFrom [] = .err .emptyInput := rfl
-
-------------------------------------------------------------------------
--- Section 4: Round-trip correctness against well-formed inputs
---
--- These are end-to-end assertions that the three happy-path clauses
--- produce the expected source tuples. If the parser's dispatch order
--- were ever reshuffled such that (say) `FROM STORE ident` matched
--- the `hexad` clause first, these theorems would fail to type-check.
-------------------------------------------------------------------------
-
-/-- VCL PARSER — PROPERTY 4: `FROM STORE <ident>` produces `:store`. -/
-theorem parseFrom_store_bare :
-    parseFrom [Token.kwFrom, Token.kwStore, Token.ident "scans"]
-      = .ok (.store "scans") [] := rfl
-
-/-- VCL PARSER — PROPERTY 5: `FROM STORE "quoted"` produces `:store`. -/
-theorem parseFrom_store_quoted :
-    parseFrom [Token.kwFrom, Token.kwStore, Token.quoted "scans"]
-      = .ok (.store "scans") [] := rfl
-
-/-- VCL PARSER — PROPERTY 6: `FROM FEDERATION <ident>` produces
-    `:federation` with the pattern preserved. -/
-theorem parseFrom_federation :
-    parseFrom [Token.kwFrom, Token.kwFederation, Token.ident "/scans/*"]
-      = .ok (.federation "/scans/*") [] := rfl
-
-/-- VCL PARSER — PROPERTY 7: `FROM HEXAD <uuid>` produces `:hexad`. -/
-theorem parseFrom_hexad :
-    parseFrom [Token.kwFrom, Token.kwHexad, Token.ident "abc-123"]
-      = .ok (.hexad "abc-123") [] := rfl
-
-/-- VCL PARSER — PROPERTY 8: Tokens after a valid FROM clause are
-    passed through as remainder. The downstream WHERE / LIMIT / OFFSET
-    parsers consume them; dropping the remainder would silently lose
-    clauses. -/
-theorem parseFrom_passes_remainder :
-    parseFrom [Token.kwFrom, Token.kwStore, Token.ident "scans",
-               Token.other "WHERE", Token.other "FIELD"]
-      = .ok (.store "scans") [Token.other "WHERE", Token.other "FIELD"] := rfl
-
-------------------------------------------------------------------------
--- Section 5: Malformed-input rejection
-------------------------------------------------------------------------
-
-/-- VCL PARSER — PROPERTY 9: A FROM token with no following STORE /
-    FEDERATION / HEXAD keyword is rejected, never silently matched. -/
-theorem parseFrom_orphan_from :
-    parseFrom [Token.kwFrom] = .err .expectedFromClause := rfl
-
-/-- VCL PARSER — PROPERTY 10: A bare identifier list without FROM is
-    rejected. Guards against the token pipeline accidentally skipping
-    the FROM keyword. -/
-theorem parseFrom_no_from_keyword :
-    parseFrom [Token.kwStore, Token.ident "scans"]
-      = .err .expectedFromClause := rfl
-
-------------------------------------------------------------------------
--- Section 6: A convenience helper
-------------------------------------------------------------------------
-
-/-- Test whether a parse succeeded. Usable in downstream theorems
-    that need a Bool-valued predicate. -/
-def parseFrom_succeeded (ts : List Token) : Bool :=
-  match parseFrom ts with
-  | .ok _ _ => true
-  | .err _  => false
-
-/-- VCL PARSER — PROPERTY 11: The `parseFrom_succeeded` predicate
-    agrees with the `parseFrom` dispatch for the canonical STORE
-    clause. -/
-theorem parseFrom_succeeded_store :
-    parseFrom_succeeded [Token.kwFrom, Token.kwStore, Token.ident "scans"] = true := rfl
-
-/-- VCL PARSER — PROPERTY 12: The `parseFrom_succeeded` predicate
-    is false on malformed input. -/
-theorem parseFrom_succeeded_empty :
-    parseFrom_succeeded [] = false := rfl
diff --git a/verification/proofs/lean4/RateLimiting.lean b/verification/proofs/lean4/RateLimiting.lean
deleted file mode 100644
index fae3ab2d..00000000
--- a/verification/proofs/lean4/RateLimiting.lean
+++ /dev/null
@@ -1,223 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
---
--- RateLimiting.lean — Formal proof that sliding window rate limiter
--- never exceeds configured bounds.
---
--- Models the Hypatia rate limiter (lib/safety/rate_limiter.ex) which
--- enforces:
---   - Per-bot limit:  50 dispatches per 60-second window
---   - Global limit:   200 dispatches per 60-second window
---   - Burst limit:    10 dispatches per 5-second window
---
--- The proof shows that the counter can never exceed the configured
--- maximum, regardless of the arrival pattern.
---
--- Corresponds to:
---   - lib/safety/rate_limiter.ex   (RateLimiter GenServer)
-
-------------------------------------------------------------------------
--- Section 1: Window-based counter model
-------------------------------------------------------------------------
-
-/-- A rate limiter configuration: maximum allowed events in a window. -/
-structure RateLimitConfig where
-  maxEvents : Nat
-  windowSize : Nat
-  windowPositive : windowSize > 0
-
-/-- A timestamped event. -/
-structure Event where
-  timestamp : Nat
-
-/-- The state of a rate limiter: a list of events within the current window. -/
-structure RateLimiterState where
-  config : RateLimitConfig
-  events : List Event
-
-/-- Count events within a time window [windowStart, now]. -/
-def countEventsInWindow (events : List Event) (windowStart : Nat) : Nat :=
-  events.filter (fun e => e.timestamp >= windowStart) |>.length
-
-/-- Check whether a new event would be allowed (counter < max). -/
-def isAllowed (state : RateLimiterState) (now : Nat) : Bool :=
-  let windowStart := now - state.config.windowSize
-  let currentCount := countEventsInWindow state.events windowStart
-  currentCount < state.config.maxEvents
-
-/-- Accept an event: add it to the list only if allowed. -/
-def tryAccept (state : RateLimiterState) (event : Event) : RateLimiterState × Bool :=
-  if isAllowed state event.timestamp then
-    ({ state with events := event :: state.events }, true)
-  else
-    (state, false)
-
-/-- Prune events outside the window (garbage collection). -/
-def prune (state : RateLimiterState) (now : Nat) : RateLimiterState :=
-  let windowStart := now - state.config.windowSize
-  { state with events := state.events.filter (fun e => e.timestamp >= windowStart) }
-
-------------------------------------------------------------------------
--- Section 2: Core invariant — counter never exceeds bound
-------------------------------------------------------------------------
-
-/-- The fundamental invariant: the number of events in any window
-    never exceeds maxEvents. -/
-def invariantHolds (state : RateLimiterState) (now : Nat) : Prop :=
-  let windowStart := now - state.config.windowSize
-  countEventsInWindow state.events windowStart ≤ state.config.maxEvents
-
-/-- An empty rate limiter trivially satisfies the invariant. -/
-theorem empty_satisfies_invariant (config : RateLimitConfig) (now : Nat) :
-    invariantHolds { config := config, events := [] } now := by
-  simp [invariantHolds, countEventsInWindow]
-
-/-- Helper: List.filter never increases length. -/
-theorem filter_length_le {α : Type} (p : α → Bool) (xs : List α) :
-    (xs.filter p).length ≤ xs.length := by
-  induction xs with
-  | nil => simp
-  | cons x xs ih =>
-    rw [List.filter_cons]
-    split
-    · exact Nat.succ_le_succ ih
-    · exact Nat.le_succ_of_le ih
-
-------------------------------------------------------------------------
--- Section 3: Proof that tryAccept preserves the invariant
-------------------------------------------------------------------------
-
-/-- Adding one event to the front raises the in-window count by at most 1. -/
-theorem count_cons_le (e : Event) (es : List Event) (ws : Nat) :
-    countEventsInWindow (e :: es) ws ≤ countEventsInWindow es ws + 1 := by
-  unfold countEventsInWindow
-  rw [List.filter_cons]
-  split
-  · rw [List.length_cons]
-    omega
-  · omega
-
-/-- After tryAccept, the invariant is preserved.
-    If the event is rejected, state is unchanged (trivially preserves).
-    If the event is accepted, count was < max before, so count+1 <= max. -/
-theorem tryAccept_preserves_invariant
-    (state : RateLimiterState) (event : Event)
-    (h : invariantHolds state event.timestamp) :
-    invariantHolds (tryAccept state event).1 event.timestamp := by
-  unfold tryAccept
-  split
-  · -- accepted: events become event :: state.events; event is in its own window,
-    -- and isAllowed gave count < maxEvents, so count + 1 ≤ maxEvents.
-    rename_i hAllowed
-    simp only [invariantHolds] at h ⊢
-    simp only [isAllowed, decide_eq_true_eq] at hAllowed
-    have hc := count_cons_le event state.events (event.timestamp - state.config.windowSize)
-    omega
-  · -- rejected: state unchanged
-    exact h
-
-------------------------------------------------------------------------
--- Section 4: Proof that prune preserves the invariant
-------------------------------------------------------------------------
-
-/-- Pruning only removes events, so it can only decrease the count. -/
-theorem prune_preserves_invariant
-    (state : RateLimiterState) (now : Nat)
-    (h : invariantHolds state now) :
-    invariantHolds (prune state now) now := by
-  -- prune filters the events; counting re-filters with the same predicate, so the
-  -- post-prune count is ≤ the pre-prune count, which h bounds by maxEvents.
-  simp only [invariantHolds, countEventsInWindow, prune] at h ⊢
-  exact Nat.le_trans (filter_length_le _ _) h
-
-------------------------------------------------------------------------
--- Section 5: Sequence of events — invariant holds inductively
-------------------------------------------------------------------------
-
-/-- Process a sequence of events, accepting only those that don't violate
-    the rate limit. Returns the final state. -/
-def processEvents (state : RateLimiterState) : List Event → RateLimiterState
-  | [] => state
-  | e :: es =>
-    let (state', _) := tryAccept state e
-    processEvents state' es
-
-/-- The invariant holds after processing any sequence of events,
-    provided it held initially and all events have the same timestamp
-    (worst case: all events arrive simultaneously). -/
-theorem processEvents_preserves_invariant
-    (state : RateLimiterState) (events : List Event) (t : Nat)
-    (hTime : ∀ e, e ∈ events → e.timestamp = t)
-    (h : invariantHolds state t) :
-    invariantHolds (processEvents state events) t := by
-  -- Generalize `state`: each step processes one event from a possibly-different
-  -- state, so the induction hypothesis must hold for any starting state.
-  induction events generalizing state with
-  | nil => exact h
-  | cons e es ih =>
-    simp only [processEvents]
-    apply ih (tryAccept state e).1
-    · intro e' he'
-      exact hTime e' (List.mem_cons_of_mem e he')
-    · have hET : e.timestamp = t := hTime e List.mem_cons_self
-      have hpre : invariantHolds state e.timestamp := by rw [hET]; exact h
-      have hstep := tryAccept_preserves_invariant state e hpre
-      rwa [hET] at hstep
-
-------------------------------------------------------------------------
--- Section 6: Concrete configurations
-------------------------------------------------------------------------
-
-/-- Per-bot rate limit: 50 events per 60s window. -/
-def perBotConfig : RateLimitConfig :=
-  { maxEvents := 50, windowSize := 60, windowPositive := by omega }
-
-/-- Global rate limit: 200 events per 60s window. -/
-def globalConfig : RateLimitConfig :=
-  { maxEvents := 200, windowSize := 60, windowPositive := by omega }
-
-/-- Burst rate limit: 10 events per 5s window. -/
-def burstConfig : RateLimitConfig :=
-  { maxEvents := 10, windowSize := 5, windowPositive := by omega }
-
-/-- Per-bot limiter starts in a valid state. -/
-theorem perBot_initial_valid (now : Nat) :
-    invariantHolds { config := perBotConfig, events := [] } now :=
-  empty_satisfies_invariant perBotConfig now
-
-/-- Global limiter starts in a valid state. -/
-theorem global_initial_valid (now : Nat) :
-    invariantHolds { config := globalConfig, events := [] } now :=
-  empty_satisfies_invariant globalConfig now
-
-/-- Burst limiter starts in a valid state. -/
-theorem burst_initial_valid (now : Nat) :
-    invariantHolds { config := burstConfig, events := [] } now :=
-  empty_satisfies_invariant burstConfig now
-
-------------------------------------------------------------------------
--- Section 7: Rejection guarantee
-------------------------------------------------------------------------
-
-/-- When the counter equals maxEvents, the next event is always rejected. -/
-theorem at_limit_rejects
-    (state : RateLimiterState) (event : Event)
-    (hFull : countEventsInWindow state.events
-               (event.timestamp - state.config.windowSize)
-             = state.config.maxEvents) :
-    (tryAccept state event).2 = false := by
-  simp [tryAccept, isAllowed]
-  rw [hFull]
-  simp [Nat.lt_irrefl]
-
-/-- The count after any sequence of simultaneous tryAccept calls is bounded.
-    All events must share the same timestamp (worst-case burst scenario). -/
-theorem count_bounded_after_accepts
-    (config : RateLimitConfig) (events : List Event) (t : Nat)
-    (hTime : ∀ e, e ∈ events → e.timestamp = t) :
-    let finalState := processEvents { config := config, events := [] } events
-    invariantHolds finalState t :=
-  processEvents_preserves_invariant
-    { config := config, events := [] }
-    events t hTime
-    (empty_satisfies_invariant config t)
diff --git a/verification/proofs/lean4/lakefile.lean b/verification/proofs/lean4/lakefile.lean
deleted file mode 100644
index 3b0ac34d..00000000
--- a/verification/proofs/lean4/lakefile.lean
+++ /dev/null
@@ -1,12 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
-import Lake
-open Lake DSL
-
-package hypatia_proofs
-
--- @[default_target] so a bare `lake build` actually compiles (and thus
--- type-checks) the proof library. Without it, `lake build` reports success
--- having built 0 targets — the verify-proofs.yml gate would pass vacuously.
-@[default_target]
-lean_lib HypatiaProofs where
-  roots := #[`BayesianUpdate, `RateLimiting, `ParserTotality, `PageRankInvariants, `ESNSpectralScaling]
diff --git a/verification/proofs/lean4/lean-toolchain b/verification/proofs/lean4/lean-toolchain
deleted file mode 100644
index af9e5d33..00000000
--- a/verification/proofs/lean4/lean-toolchain
+++ /dev/null
@@ -1 +0,0 @@
-leanprover/lean4:v4.30.0

From c6327ecd8d112faccbb3c665968652f3950f658d Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 16:08:29 +0000
Subject: [PATCH 2/2] fix(proofs): word the RateLimiting doc comment without
 the trusted-base marker

check-trusted-base.sh matches 'admit' anywhere, so 'admitted' in an
Idris ||| doc comment failed Verify Proofs on this branch. The comment now
says 'let in'; no proof text changes (idris2 --check RateLimiting.idr OK).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CYR5bf5FBLS7cXQK72aVNM
---
 verification/proofs/idris2/RateLimiting.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/verification/proofs/idris2/RateLimiting.idr b/verification/proofs/idris2/RateLimiting.idr
index e9cbd803..77db2a87 100644
--- a/verification/proofs/idris2/RateLimiting.idr
+++ b/verification/proofs/idris2/RateLimiting.idr
@@ -117,7 +117,7 @@ countConsLTE e es ws with (inWindow ws e)
   _ | False = lteSuccRight reflexive
 
 ||| After tryAccept the invariant still holds: a rejected event leaves the
-||| state unchanged, and an accepted one was admitted below the maximum.
+||| state unchanged, and an accepted one was let in below the maximum.
 export
 tryAcceptPreservesInvariant : (state : RateLimiterState) -> (e : Event) ->
                               InvariantHolds state e.timestamp ->