diff --git a/.github/workflows/verify-proofs.yml b/.github/workflows/verify-proofs.yml
index a274e16e..7fa7acf4 100644
--- a/.github/workflows/verify-proofs.yml
+++ b/.github/workflows/verify-proofs.yml
@@ -20,6 +20,9 @@ on:
     - verification/proof-ledger.jsonl
     - scripts/proof-ledger.sh
     - tests/proof-ledger-test.sh
+    - README.adoc
+    - AFFIRMATION.adoc
+    - EXPLAINME.adoc
     - scripts/check-trusted-base.sh
     - docs/proof-debt.adoc
     - test/soundness/**
@@ -48,6 +51,9 @@ on:
     - verification/proof-ledger.jsonl
     - scripts/proof-ledger.sh
     - tests/proof-ledger-test.sh
+    - README.adoc
+    - AFFIRMATION.adoc
+    - EXPLAINME.adoc
     - scripts/check-trusted-base.sh
     - docs/proof-debt.adoc
     - test/soundness/**
@@ -441,6 +447,9 @@ jobs:
       - name: Proof Ledger table is the ledger's rendering
         run: bash scripts/proof-ledger.sh render --check
 
+      - name: Every quoted census is the ledger's
+        run: bash scripts/proof-ledger.sh claims
+
       - name: Proof ledger contracts (planted defects)
         run: bash tests/proof-ledger-test.sh
 
diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc
index 1b0b9826..5defac9a 100644
--- a/AFFIRMATION.adoc
+++ b/AFFIRMATION.adoc
@@ -19,8 +19,16 @@ state and commitments. Companion detail:
 * *Guix-only builds.* Nix is retired estate-wide (owner ruling 2026-06-05);
   `guix.scm` / guix channels are the sole reproducible-build manifests. No
   `flake.nix` remains; all references reconciled.
-* *The formal-proof corpus verifies and is CI-gated* across Idris 2 (v0.7.0),
-  Lean 4 (v4.30.0) and TLA+ — *zero escape hatches outside
+* *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
+  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
   `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
@@ -33,9 +41,11 @@ state and commitments. Companion detail:
   the `check-trusted-base` CI job fails if one loses its fixture status or
   an un-annotated marker appears elsewhere. (An earlier revision of this
   sentence claimed "zero escape hatches" unscoped, which the fixture corpus
-  made literally false; see #831.) One obligation remains open —
-  neural-convergence (PageRank + ESN) — blocked only on Mathlib network
-  access; the handover is at `docs/proofs/HANDOVER-neural-convergence.md`.
+  made literally false; see #831.) The neural-convergence theorems (PageRank
+  and ESN) are open theory rows. They are planned in Agda over constructive
+  reals, without Mathlib, which PROOF-POLICY forbids; the plan is
+  `docs/proofs/HANDOVER-neural-convergence.adoc`. (An earlier revision called
+  them "blocked only on Mathlib network access".)
 * *The unified-api-adapter wire contract cannot silently drift.* The Zig enum,
   the Idris2 ABI and the Rust client are pinned to one golden source
   (`ffi/connectors.json`) by `test/unified-api-adapter-contract_test.exs` under
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 2a32f694..e705a9b7 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -12,6 +12,20 @@ https://semver.org/[Semantic Versioning].
 
 === Changed
 
+==== Proof claims follow the machine proof ledger (2026-11-09)
+
+* `EXPLAINME.adoc` is back at the repository root, as README-EXPLAINME
+  requires, and every claim in it was re-checked against the tree. It gains
+  a `#proof-ledger` section that cites `verification/proof-ledger.jsonl`. The
+  README's own overclaims are listed under its known gaps.
+* README, AFFIRMATION and EXPLAINME quote the ledger's census, and
+  `scripts/proof-ledger.sh claims` fails CI when a quoted census and the
+  ledger disagree.
+* The neural-convergence handover is rewritten: Agda first, over
+  constructive reals, with no Mathlib, which PROOF-POLICY forbids.
+  `docs/proofs/needs.adoc` now points at the ledger instead of keeping a
+  list of its own.
+
 ==== WH013 reads steps with RE001's workflow reader (2026-11-04)
 
 RE001's reader is now its own module, `Hypatia.WorkflowYaml`, and WH013 reads
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
new file mode 100644
index 00000000..38f9fd7c
--- /dev/null
+++ b/EXPLAINME.adoc
@@ -0,0 +1,291 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Hypatia — EXPLAINME
+:toc: preamble
+:icons: font
+
+This file backs each README claim with a code path and an honest caveat; read
+it after the README if you want to know what is real.
+
+Counts were taken from the tree on 2026-11-09 with the command shown.
+Volatile figures (repositories, outcomes, dispatches) are not quoted; generate
+them with `mix hypatia.recipe_health`, `mix hypatia.strategy_effectiveness`
+or `mix hypatia.watch`.
+
+== Claim-to-implementation map
+
+=== Symbolic rules, distilled from learning
+
+[quote, README.adoc]
+____
+*Symbolic reasoning* — 35 Elixir rule modules producing fast, deterministic findings
+____
+
+[quote, README.adoc]
+____
+The system learns complex patterns through neural analysis, then *distils* them into simple,
+fast declarative rules that can be pre-emptively injected into new repositories, applied as
+cures to existing ones, and executed without ML inference overhead.
+____
+
+How this is implemented::
+Pure-Elixir modules in link:lib/rules/[] behind `Hypatia.Rules`
+(link:lib/rules/rules.ex[]). The escript runs them with no OTP tree and no
+neural process (`app: nil` in link:mix.exs[]).
+
+Caveat::
+`find lib/rules -maxdepth 1 -name '*.ex' | wc -l` gives 42, not 35; the
+generated link:docs/rules/catalogue.adoc[] says 41 and lacks
+`structured_format`. No code path distils learned patterns into rules:
+`learn_from_fix/3` and `promote_patterns/0` in link:lib/rules/learning.ex[]
+have no outside callers, and `git grep RecipeGenerator` finds no caller.
+The rules are hand-written.
+
+=== Neural learning
+
+[quote, README.adoc]
+____
+*Neural learning* — 8 networks on a shared blackboard, learning which fixes actually stick
+____
+
+How this is implemented::
+Eight networks in link:lib/neural/[] (trust graph, mixture of experts,
+liquid state machine, echo state, radial basis, GNN, VAE, sequence model)
+run in six phases over the ETS blackboard under
+link:lib/neural/coordinator.ex[], which calls the GNN, VAE and sequence
+GenServers at lines 792, 865 and 869. All are plain Elixir (no Nx in
+link:mix.exs[]). In link:lib/pattern_analyzer.ex[] the result can only
+lower a recipe's confidence (`min/2`) or demote the finding.
+
+Caveat::
+PageRank convergence and the echo-state property are `open` ledger rows.
+A comment in `pattern_analyzer.ex` still says "all 5 networks".
+
+=== Bayesian confidence and outcome feedback
+
+[quote, README.adoc]
+____
+*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
+____
+
+[quote, README.adoc]
+____
+Outcomes flow back through
+`mix hypatia.record_outcome`, which drives the Bayesian update and, when a recipe degrades,
+auto-quarantine.
+____
+
+How this is implemented::
+link:lib/outcome_tracker.ex[] lines 20–22 (prior strength 10, cap 0.99,
+floor 0.10). Tiers 0.95 and 0.85 are in link:lib/triangle_router.ex[]
+lines 24–25. `OutcomeTracker.quarantined?/2` (re-scan verification rate
+below 0.30) downgrades `auto_execute` to review in
+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
+pseudo-counts, not Elixir floats.
+
+=== Machine-checked proofs
+
+[quote, README.adoc]
+____
+*Machine-checked proofs* — Idris2 proofs of the ABI and the decision logic (confidence bounds,
+  safety-triangle routing, dispatch thresholds, quarantine, rollback), Lean 4 proofs of the Bayesian
+  update and rate-limiting properties, one Agda model of the Logtalk-to-Elixir migration, and a TLA+
+  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,
+  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.
+
+Caveat::
+Four of the five Lean rows rest on `propext` (two also on `Quot.sound`).
+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.
+
+=== The safety triangle and novelty gating
+
+[quote, README.adoc]
+____
+Every finding is routed *Eliminate > Substitute > Control*, in that order — remove the hazard
+if you can, replace it if you cannot, and only then add a control around it.
+____
+
+[quote, README.adoc]
+____
+Unknown findings are forced to `report_only` regardless of score (novelty gating).
+____
+
+How this is implemented::
+link:lib/pattern_analyzer.ex[] chains `VerisimConnector`, `PatternRegistry`
+and `TriangleRouter`; link:lib/dispatch_manifest.ex[] writes
+`pending.jsonl`. Eliminate dispatch passes the Kin gate
+(link:lib/fleet_dispatcher.ex[] lines 235, 972–983). A novel finding goes to
+Control in link:lib/neural/dispatch_guard.ex[] line 69.
+
+Caveat::
+The ordering is proved over models (`safety-triangle`, `abi-rule-engine`,
+`dispatch-strategy`), not over the Elixir router. With the coordinator down,
+an action is capped at review, not report-only (line 67).
+
+=== Architecture table
+
+[quote, README.adoc]
+____
+133 Elixir modules — pipeline, rules, VCL, neural, safety, web, merge orchestration
+____
+
+How this is implemented::
+Each README row, measured:
++
+[cols="1,2", options="header"]
+|===
+| README row | Tree
+| `lib/`: 133 | 154 `.ex` files (`+ls lib/**/*.ex \| wc -l+`), 180 `defmodule`
+| `lib/rules/`: 35 | 42, as above
+| `lib/neural/`, `lib/vcl/` | Correct
+| `lib/merge_orchestration/`: 12 | Correct (one file in `kin_gate/`)
+| `lib/hypatia/web/` | SARIF is link:lib/hypatia/sarif.ex[], outside `web/`
+| `src/Hypatia/ABI/` | Also `Verdict`, `Retraction`; `Gen.idr` is a generator
+| `ffi/zig/`: 18, 16 | Correct; pinned by link:.github/workflows/zig.yml[]
+| Rust workspace | 7 members in link:Cargo.toml[]
+|===
+
+Caveat::
+The README links `docs/architecture/topology.md`; the file is
+link:docs/architecture/topology.adoc[].
+
+=== Installation, usage and the operational surface
+
+[quote, README.adoc]
+____
+`just --list` shows all 39 recipes; `CONTRIBUTING.md` treats `just` as the canonical entry point.
+____
+
+[quote, README.adoc]
+____
+Running the supervision tree also serves an HTML dashboard, an SSE event stream, a Prometheus
+`/metrics` endpoint and a bearer-authenticated `/api/*` on port 9090.
+____
+
+How this is implemented::
+link:Justfile[] (with `contractile.just`), link:lib/hypatia/cli.ex[],
+link:lib/mix/tasks/[]; link:mise.toml[] pins Erlang 27.3.4.4 and Elixir
+1.17.3. link:lib/application.ex[] supervises 24 children (two more when
+configured); link:lib/hypatia/web/router.ex[] serves `/`, `/metrics`, `/api`.
+
+Caveat::
+The Justfiles hold 43 recipes. `just build-all` builds Rust and Elixir only.
+The CLI has six commands, not five (`secret-alerts`); there are 16 Mix
+tasks, not 15. No `guix.scm` is tracked. `CONTRIBUTING.md` is in `.github/`.
+`/api/*` needs a bearer token when `HYPATIA_API_BEARER_TOKEN` is set and not
+empty. Otherwise only loopback clients are answered, unless
+`HYPATIA_API_ALLOW_NONLOCAL=true` lets non-local clients in without a token.
+
+=== Project status and licence
+
+[quote, README.adoc]
+____
+242 tests that are excluded from every run, the safety systems that are built but not yet invoked
+by any dispatch path, and the CI blockage currently stopping the Rust lane.
+____
+
+[quote, README.adoc]
+____
+Source files declare `MPL-2.0` and
+documentation declares `CC-BY-SA-4.0`, both via per-file SPDX headers
+____
+
+How this is implemented::
+link:test/test_helper.exs[] excludes `:verisim_data`; nine test files carry
+that tag. The safety modules are in link:lib/safety/[]. Every tracked
+`+lib/**/*.ex+` file carries `MPL-2.0`; link:LICENSES/[] holds both texts.
+
+Caveat::
+The nine files hold 224 literal `test` blocks; 242 needs a `mix test` run
+this audit did not make. The Rust blockage is stale: entry CI-1 of
+link:docs/DEBT-REGISTER.adoc[] records the fix, visible in
+link:integration/Cargo.toml[] lines 48–55. `docs/DEBT-REGISTER.md` is dead.
+45 of 152 tracked `.adoc` files have no SPDX header (recorded for the owner,
+not a licence change).
+
+== Dogfooded across the account
+
+[cols="1,2,2", options="header"]
+|===
+| Technology / pattern | Used here | Also used in
+| Idris2 ABI plus Zig C ABI | link:src/Hypatia/ABI/[], link:ffi/zig/[]
+| link:https://github.com/hyperpolymath/echidna[echidna]
+| Hypatia as estate scanner | link:.github/workflows/hypatia-scan.yml[]
+| `hypatia-scan-reusable.yml` in
+  link:https://github.com/metadatastician/standards[standards], called by
+  echidna and gitbot-fleet
+| JSONL dispatch manifests | link:lib/dispatch_manifest.ex[]
+| link:https://github.com/hyperpolymath/gitbot-fleet[gitbot-fleet]
+  `scripts/dispatch-runner.sh`
+| Machine proof ledger | link:verification/proof-ledger.jsonl[]
+| README-EXPLAINME standard §5 in
+  link:https://github.com/metadatastician/standards[standards]
+|===
+
+[[known-gaps]]
+== Known gaps
+
+[CAUTION]
+====
+Safety systems are built but not wired. `Safety.RateLimiter` and
+`Safety.Quarantine` have no caller in `lib/`. `BatchRollback.rollback/2` is
+reached only through `Kin.Contingency.rollback_wave/2`, which nothing calls.
+`SelfDiagnostics.record_dispatch_failure/0` and `record_dispatch_success/0`
+have no callers, so its circuit breaker never opens. The moduledoc of
+`lib/fleet_dispatcher.ex` (line 47) still names the rate limiter.
+====
+
+[CAUTION]
+====
+README overclaims, each detailed above: learned patterns are not distilled
+into rules (the promotion and recipe-generation code is never invoked); the
+counts of rule modules, `lib/` modules, Just recipes, CLI commands and Mix
+tasks are wrong; `just build-all` is narrower than stated; `guix.scm` is
+absent; two links are dead. Excluded `:verisim_data` tests run in no
+workflow (debt register T-1).
+====
+
+== Evidence index
+
+[cols="2,3", options="header"]
+|===
+| Path | Proves
+| `lib/pattern_analyzer.ex` | Scan, pattern, triangle, neural guard, dispatch
+| `lib/neural/dispatch_guard.ex` | Novel goes to Control; no coordinator caps at review
+| `lib/fleet_dispatcher.ex` | Kin gate review; recipe-quarantine downgrade
+| `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
+| `docs/DEBT-REGISTER.adoc` | What is broken, ungated or stale
+|===
+
+[[proof-ledger]]
+== Proof ledger
+
+The machine ledger link:verification/proof-ledger.jsonl[] is canonical. It is
+validated by `bash scripts/proof-ledger.sh check`, and its rendered table is
+in link:verification/PROOF-STATUS.adoc#proof-ledger[PROOF-STATUS.adoc]. Where
+this file or the README disagrees with the ledger, the ledger wins.
+
+Census, from `scripts/proof-ledger.sh check`:
+
+[source,text]
+----
+18 proven of 42; 4 proven-with-postulates, 11 tested-only, 2 argued, 7 open.
+----
+
+Of the three theory rows, `logtalk-migration` is `PWG-3`;
+`pagerank-convergence` and `esn-echo-state` are ungraded and `open`.
diff --git a/README.adoc b/README.adoc
index fbd00f90..b4c34733 100644
--- a/README.adoc
+++ b/README.adoc
@@ -24,8 +24,12 @@ It combines:
 * *Neural learning* — 8 networks on a shared blackboard, learning which fixes actually stick
 * *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 ABI definitions with dependent types, Lean 4 proofs of the
-  Bayesian update and rate-limiting properties, and a TLA+ model of the Kin gate
+* *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+
+  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,
+  11 tested-only, 2 argued, 7 open (link:EXPLAINME.adoc#proof-ledger[details])
 
 === Core philosophy
 
@@ -76,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/` | Lean 4 proofs, TLA+ specs
+| `verification/` | Proof ledger and proofs: Idris2, Lean 4, Agda, TLA+
 |===
 
 See link:docs/architecture/topology.md[docs/architecture/topology.md] for the full map.
diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc
deleted file mode 100644
index b384906c..00000000
--- a/docs/EXPLAINME.adoc
+++ /dev/null
@@ -1,139 +0,0 @@
-// SPDX-License-Identifier: CC-BY-SA-4.0
-= Hypatia: Neurosymbolic CI/CD Intelligence — Show Me The Receipts
-:toc:
-:icons: font
-
-The README makes claims. This file backs them up with evidence.
-
-== Key Claims From README
-
-[quote, README section "Core Philosophy"]
-____
-"Dumb rules from smart learning"
-
-The system learns complex patterns through neural analysis, then *distills* them into simple, fast-acting declarative rules that can be pre-emptively injected into new repositories, applied as cures to existing repositories, executed without ML inference overhead, and formally verified for correctness.
-____
-
-*Evidence:* The learning pipeline (CLAUDE.md line 77-101) demonstrates this cycle:
-1. **Learning** — 5 neural networks (Graph of Trust, Mixture of Experts, Liquid State Machine, Echo State Network, Radial Neural Network) analyze verisim-data
-2. **Distillation** — PatternRegistry deduplicates findings into 46 canonical recipes (PA001-PA046 + 20 OpenSSF Scorecard recipes)
-3. **Symbolic** — Recipes and checks execute as pure-Elixir rules in `lib/rules/*.ex` (no ML needed for the deterministic checks)
-4. **Verification** — Idris2 ABI proofs formally verify recipe correctness
-
-This is proven by the metrics: 1635 dispatched actions (600 auto-execute with 95%+ confidence, 667 review, 368 report), 16,671 outcomes recorded (99% success rate), 46 recipes zero-uncovered (every category has a recipe).
-
-*Caveat:* The "dumb rules" are fast but not universally applicable — categories below 0.85 confidence force review (not auto-execute), and below 0.50 confidence auto-generate explanatory recipes before dispatch.
-
-[quote, README section "Overview" and "Safety Triangle Pipeline"]
-____
-Hypatia combines: Neural Learning, Symbolic Reasoning, Formal Verification, Graph Intelligence, Distributed Cache, P2P Federation.
-
-The safety triangle pipeline: Eliminate > Substitute > Control
-____
-
-*Evidence:* The architecture (lines 49-100) shows all 6 layers implemented:
-- Verification (Haskell Liquid types, property testing, formal proofs)
-- Learning (neural subsystem with 5 networks)
-- Symbolic (Elixir rule modules in `lib/rules/*.ex`)
-- Data (ArangoDB graph, Dragonfly cache, Radicle P2P)
-- Action (robot-repo-automaton, hooks, diagnostics)
-- Forge adapters (6: GitHub, GitLab, Bitbucket, Codeberg, sr.ht, Gitea)
-
-The safety triangle (CLAUDE.md lines 53-73) routes findings through:
-1. **Eliminate** — Remove root cause permanently (0 risk, lowest cost)
-2. **Substitute** — Replace bad component with good alternative (medium cost/risk)
-3. **Control** — Add monitoring/limits (highest cost, medium risk, reversible)
-
-This is operationalized in TriangleRouter, FleetDispatcher (confidence-gated), and circuit breaker safety systems.
-
-*Caveat:* The P2P federation (Radicle) is integrated in architecture but not deployed in production; currently uses git-backed verisim-data flat files.
-
-== Technology Choices
-
-[cols="1,2"]
-|===
-| Technology | Learn More
-
-| **Elixir 1.16+** | https://elixir-lang.org (8 core modules, OTP GenServers, concurrency)
-| **Rust** | https://www.rust-lang.org (adapters, CLI, data layer, fixer)
-| **Julia 1.10+** | https://julialang.org (5 neural networks, training pipeline)
-| **Elixir / OTP** | Rule modules (error catalog, pattern detection)
-| **Haskell** | Formal verification (Liquid types, property testing)
-| **Idris2 ABI** | https://www.idris-lang.org (type-safe GraphQL, gRPC, REST with proofs)
-| **Zig FFI** | https://ziglang.org (C ABI bridge for 7 exported functions)
-| **ArangoDB** | Graph database (relationship modeling)
-| **Dragonfly** | Distributed cache (sub-millisecond rule lookups)
-| **VeriSimDB** | Cross-modal consistency for scan data
-|===
-
-== Dogfooded Across The Account
-
-[cols="1,2,2", options="header"]
-|===
-| Technology | Role in Hypatia | Also Used In
-
-| *Idris2 ABI* (hyperpolymath standard)
-| `src/Hypatia/ABI/` — formal specs for GraphQL, gRPC, REST with dependent type proofs; `ffiReturnsApiResponse` proof in `FFI.idr`
-| gossamer (`gossamer/src/interface/abi/`), burble (`burble/src/Burble/ABI/`), verisimdb, proven, typed-wasm — every repo with an FFI layer
-
-| *Zig FFI* (hyperpolymath standard)
-| `ffi/zig/src/` — 7 C-compatible exported functions (`hypatia_health_check`, `hypatia_scan_repo`, `hypatia_dispatch`, etc.)
-| gossamer (`gossamer/src/interface/ffi/`), burble (`ffi/zig/src/ffi.zig`), tangle, ephapax — same Idris2→Zig→C pattern
-
-| *VeriSimDB + VCL query layer*
-| Built-in Elixir VCL parser + FileExecutor; queries verisim-data flat-file store; 954 patterns tracked across 298 repos
-| burble (state and session storage), idaptik (game state), boj-server (scan results), nextgen-databases monorepo
-
-| *panic-attack*
-| Re-scan verification after dispatch — confirms fixes removed weak points; `diagnostics.ex` watches for binary on `$PATH`
-| Used estate-wide as pre-commit gate (`panic-attack assail`); panicbot wraps it in CI
-
-| *Elixir/OTP*
-| 8 GenServers (VCL, RateLimiter, Quarantine, LearningScheduler, Diagnostics, Neural, Kin, Application supervisor); fault isolation
-| burble (P2P voice control plane), gitbot-fleet (bot orchestration)
-
-| *Julia neural networks*
-| 5 networks (Graph of Trust, MoE, LSM, ESN, RBF) + training pipeline from real verisim-data outcomes
-| KnotTheory.jl (topology data processing), batch scripts estate-wide
-|===
-
-== File Map: Key Modules
-
-[cols="1,2"]
-|===
-| Path | What's There
-
-| `lib/pattern_analyzer.ex` | Full pipeline orchestrator (scan → patterns → triangle → dispatch)
-| `lib/verisimdb_connector.ex` | VCL queries with file I/O fallback
-| `lib/pattern_registry.ex` | Deduplicates findings into 46 canonical recipes
-| `lib/triangle_router.ex` | Routes through Eliminate > Substitute > Control
-| `lib/fleet_dispatcher.ex` | Confidence-gated dispatch (file-based + HTTP, circuit breaker)
-| `lib/dispatch_manifest.ex` | Writes JSONL manifests for bash execution layer
-| `lib/outcome_tracker.ex` | Records outcomes, Bayesian confidence updating, re-scan verification
-| `lib/recipe_generator.ex` | Auto-generates recipes for uncovered categories (0.50 confidence)
-| `lib/scorecard_ingestor.ex` | Ingests OpenSSF Scorecard checks as patterns
-| `lib/learning_scheduler.ex` | GenServer: polls outcomes, drives feedback loop
-| `lib/self_diagnostics.ex` | Health monitoring, circuit breaker, auto-recovery
-| `lib/neural/` | 5 networks (graph-of-trust, moe, lsm, esn, rbf) + coordinator
-| `lib/vcl/` | VCL client, file executor, query functions
-| `src/Hypatia/ABI/` | Idris2 specs (Types, GraphQL, gRPC, REST, FFI, RuleEngine, Gen)
-| `ffi/zig/src/` | 7 C-compatible exported functions
-| `adapters/ cli/ data/ fixer/ integration/` | Rust workspace (root crates)
-| `proofs/agda/` | Formal verification of safety triangle correctness
-|===
-
-== Metrics (as of 2026-03-07)
-
-- 302 repos scanned (3385 weak points)
-- 1635 dispatched actions (600 auto-execute, 667 review, 368 report)
-- 16,671 outcomes recorded (99% success rate)
-- 46 recipes (0 uncovered categories), 20 OpenSSF Scorecard recipes, 5 RSR compliance rules
-- 5 neural networks + coordinator in OTP supervision
-- Bayesian Beta-distribution confidence (prior_strength=10, floor=0.10, cap=0.99)
-- Re-scan verification via panic-attacker
-- 3 safety systems: rate limiter (50/bot/min, 200/global/min), quarantine (soft/hard/permanent), batch rollback
-- VCL integrated with file executor, query cache, cross-repo analytics
-
-== Questions?
-
-Open an issue in the hyperpolymath/hypatia repository for questions about the safety triangle routing, neural network architecture, recipe distillation, or verisim-data integration for cross-repo CI/CD intelligence.
diff --git a/docs/README.adoc b/docs/README.adoc
index a60072ce..68badb03 100644
--- a/docs/README.adoc
+++ b/docs/README.adoc
@@ -110,7 +110,7 @@ Detailed per-surface references. For the high-level overview see link:guides/api
 
 == Reference
 
-* link:EXPLAINME.adoc[`EXPLAINME.adoc`] — annotated tour of the codebase.
+* link:../EXPLAINME.adoc[`EXPLAINME.adoc`] (repository root) — claims, evidence and the proof ledger.
 
 == History
 
diff --git a/docs/proofs/HANDOVER-neural-convergence.adoc b/docs/proofs/HANDOVER-neural-convergence.adoc
index 0efdc12c..2dca7558 100644
--- a/docs/proofs/HANDOVER-neural-convergence.adoc
+++ b/docs/proofs/HANDOVER-neural-convergence.adoc
@@ -1,219 +1,147 @@
-== HANDOVER — Complete the proof corpus: neural-convergence proofs (Lean 4 + Mathlib)
+// SPDX-License-Identifier: CC-BY-SA-4.0
+== HANDOVER — Neural-convergence theorems: Agda first, constructive reals
 
 === Mission
 
-Hypatia’s formal-proof corpus spans *Idris 2, Lean 4, and TLA+*. Every
-existing proof verifies and is CI-gated. *One obligation is open:
-neural-network convergence.* Two Lean files prove only ℕ
-_preconditions_; the real analytical theorems (PageRank power-iteration
-convergence; ESN echo-state stability) need *Mathlib*. This must be done
-in an environment where Mathlib’s `+.olean+` cache CDN is reachable (the
-Claude-on-the-web sandbox blocks it —
-`+lakecache.blob.core.windows.net+` and `+mathlib4.lean-cache.cloud+`
-403). Locally, with normal internet, it just works.
-
-=== Repo state (do not redo)
-
-* Branch: `+claude/hopeful-ptolemy-ZdYqp+` (proof work is merged to
-`+main+`).
-* #433 — made the corpus actually compile (it had never been
-machine-checked).
-* #434 — CI hardening: gate the Idris ABI + verify packages, pin Lean,
-fix the Idris cache.
-* #440 — reconciled the proof-status docs.
-* Pinned toolchain: *Idris 2 `+v0.7.0+`*, *Lean `+v4.30.0+`*, TLA+
-tla2tools 2.19. Agda retired. Zero escape hatches
-(`+believe_me+`/`+assert_total+`/`+postulate+`/`+sorry+`/`+Admitted+`/`+unsafeCoerce+`
-= 0).
-
-=== The corpus (current truth)
-
-[width="100%",cols="34%,33%,33%",options="header",]
-|===
-|Obligation |File |Status
-|H1 confidence bounds
-|`+verification/proofs/idris2/ConfidenceBounds.idr+` |✅
-
-|H2 dispatch monotonicity
-|`+verification/proofs/idris2/DispatchStrategy.idr+` |✅
-
-|H3 safety-triangle order
-|`+verification/proofs/idris2/SafetyTriangle.idr+` |✅
-
-|H4 rate limiting |`+verification/proofs/lean4/RateLimiting.lean+` |✅
-
-|H5 quarantine |`+verification/proofs/idris2/Quarantine.idr+` |✅
-
-|H6 outcome-log monotonicity |`+lib/outcome_tracker.ex+` (runtime
-assertion; Agda retired) |✅
-
-|H7 Bayesian update |`+verification/proofs/lean4/BayesianUpdate.lean+`
-|✅
-
-|H8 kin-gate atomicity |`+verification/proofs/tlaplus/KinGate.tla+` |✅
-
-|H9 neural consensus aggregation
-|`+verification/proofs/idris2/NeuralConsensus.idr+` |✅
-
-|parser totality |`+verification/proofs/lean4/ParserTotality.lean+` |✅
-
-|ABI package + verify package |`+src/Hypatia/ABI/*.idr+`
-(incl. `+RuleEngine.idr+`), `+verify/src/*.idr+` |✅
-
-|*Neural convergence — PageRank*
-|`+verification/proofs/lean4/PageRankInvariants.lean+` |⛔ preconditions
-only
-
-|*Neural convergence — ESN*
-|`+verification/proofs/lean4/ESNSpectralScaling.lean+` |⛔ preconditions
-only
-|===
-
-=== Toolchain install (local)
-
-[source,bash]
-----
-curl -fL https://raw.githubusercontent.com/leanprover/elan/v4.0.0/elan-init.sh | sh -s -- -y
-elan toolchain install leanprover/lean4:v4.30.0     # matches the repo pin
-# Idris2 v0.7.0 (only to re-verify the Idris side): chezscheme + bootstrap, or idris2-pack
-# TLA+ (only to re-verify H8): Java 21 + tla2tools.jar
-----
-
-=== CI-hygiene design decision (read before coding)
-
-Do *not* add Mathlib to the existing `+verification/proofs/lean4/+`
-project — it is the _fast_ gate (no deps, builds in seconds, runs every
-push). Create a *separate* project
-`+verification/proofs/lean4-mathlib/+` with its own `+lakefile.lean+`
-(`+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.30.0"+`),
-its own `+lean-toolchain+` (`+leanprover/lean4:v4.30.0+`), and the new
-proof files. Gate it in a *separate cached CI job* (below). Keep the
-existing ℕ-precondition files where they are.
-
-=== Theorem 1 — PageRank power-iteration convergence
-
-* New file `+PageRankConvergence.lean+` in the mathlib project. Models
-`+lib/neural/graph_of_trust.ex+`.
-* *Statement:* for `+xₖ₊₁ = α·P·xₖ + (1-α)·v+` with `+P+`
-column-stochastic and `+0 ≤ α < 1+`, there is a unique fixed point and
-the iterates converge to it.
-* *Strategy:* the damped Google operator `+G(x) = α·P·x + (1-α)·v+` is a
-contraction with modulus `+α+` in the ℓ¹ norm (column-stochastic ⇒
-`+‖P x‖₁ ≤ ‖x‖₁+`). Then Banach.
-* *Mathlib:* `+ContractingWith+`
-(`+Mathlib.Topology.MetricSpace.Contracting+`),
-`+ContractingWith.fixedPoint+`, `+…fixedPoint_unique+`,
-`+…tendsto_iterate_fixedPoint+`. Space `+EuclideanSpace ℝ (Fin n)+` or
-`+PiLp 1+`; matrices via `+Matrix.toLin'+`. (Confirm exact lemma names
-in v4.30.0.)
-
-=== Theorem 2 — ESN echo-state stability
-
-* New file `+ESNStability.lean+`. Models
-`+lib/neural/echo_state_network.ex+`.
-* *Frame it in the sup norm, as an ℓ∞ operator-norm contraction
-(`+‖W‖∞ < 1+`), NOT as spectral radius `+ρ(W) < 1+`.* Since 2026-10 the
-runtime scales the reservoir so its induced ∞-norm (largest absolute row
-sum) is `+@reservoir_norm+` = 0.95; it does not compute the spectral
-radius. (Before that it scaled the largest single _entry_, which bounds
-neither norm: the 80-node reservoir had ρ ≈ 2 and two runs from different
-initial states never converged. A proof of the old code would have been a
-proof of a false claim.) `+test/neural_test.exs+` now checks both the
-row-sum bound and the convergence of two initial states.
-* *Statement:* for leak rate `+0 < a ≤ 1+` and `+‖W‖∞ < 1+`, the update
-`+F_u(x) = (1 - a)·x + a·tanh(W·x + w·u)+` (tanh applied componentwise,
-1-Lipschitz) satisfies
-`+‖F_u(x) - F_u(y)‖∞ ≤ (1 - a + a·‖W‖∞)·‖x - y‖∞+` for every input `+u+`.
-Corollaries: the modulus is < 1, so two trajectories under the same input
-sequence approach each other geometrically (exponential forgetting of the
-initial state), and a state that starts in `+[-1, 1]ⁿ+` stays there for any input.
-* *Mathlib:* on `+Fin n → ℝ+` the default norm is already the sup norm,
-and Mathlib has the ℓ∞ operator norm of a matrix as the max row sum
-(`+Matrix.linfty_opNorm+` and friends; confirm names in v4.30.0).
-`+LipschitzWith+` for the componentwise tanh (`+Real.tanh+` derivative ≤ 1),
-then compose. `+ContractingWith+` is only needed for a fixed-input fixed
-point; the forgetting statement is a direct induction on the step bound.
-
-=== Hard constraints
-
-* No
-`+sorry+`/`+believe_me+`/`+postulate+`/`+assert_total+`/`+admit+`/`+native_decide+`.
-Fully constructive.
-* SPDX header on every file (`+MPL-2.0+` + the copyright line above).
-* Lean stays pinned at v4.30.0; Mathlib is the `+v4.30.0+` tag (exists,
-matches).
-* When done: flip both rows PARTIAL→COMPLETE in
-`+verification/PROOF-STATUS.md+` and `+docs/proofs/needs.md+`.
-
-=== CI job to add (separate, cached — parallel to `+lake-build+`, not folded in)
-
-[source,yaml]
-----
-  lake-build-mathlib:
-    name: lake build (mathlib)
-    runs-on: ubuntu-latest
-    timeout-minutes: 60                # `lake exe cache get` is ~5 GB
-    env: { LEAN_TOOLCHAIN: leanprover/lean4:v4.30.0 }
-    steps:
-      - uses: actions/checkout@<sha>
-      - # install elan + Lean v4.30.0 (mirror the existing lake-build job)
-      - uses: actions/cache@<sha>
-        with:
-          path: |
-            ~/.elan
-            ~/.cache/mathlib
-            verification/proofs/lean4-mathlib/.lake
-          key: mathlib-v4.30.0-${{ runner.os }}-${{ hashFiles('verification/proofs/lean4-mathlib/**/*.lean') }}
-      - run: cd verification/proofs/lean4-mathlib && lake exe cache get && lake build
-----
-
-Add `+verification/proofs/lean4-mathlib/**+` to the workflow `+paths:+`
-(push + pull_request).
-
-=== Verify the whole corpus before finishing
-
-[source,bash]
-----
-idris2 --build src/abi/hypatia-abi.ipkg
-idris2 --build verify/hypatia-verify.ipkg
-cd verification/proofs/idris2 && for f in *.idr; do idris2 --check "$f" || exit 1; done; cd -
-cd verification/proofs/lean4 && lake build && cd -
-cd verification/proofs/lean4-mathlib && lake exe cache get && lake build && cd -
-cd verification/proofs/tlaplus && java -cp /path/tla2tools.jar tlc2.TLC -config KinGate.cfg KinGate.tla
-----
-
-=== Gotchas already solved (recognise these in the codebase)
-
-* base-0.7 renames: `+lteRefl+`→`+reflexive+`,
-`+lteTransitive+`→`+transitive+`; Nat lemmas `+multRightSuccPlus+`,
-`+plusLteMonotone*+`, `+lteAddRight+`.
-* Lean 4.30: `+List.mem_cons_self+` has implicit args;
-`+List.filter_cons+`, `+decide_eq_true_eq+`; use
-`+induction … generalizing+` when the IH must hold for a changing state.
-* Idris refutation of impossible equalities / empty GADTs:
-`+Refl impossible+` / `+case x of _ impossible+` (no `+Uninhabited+`
-instance to lean on).
-* Idris reserved words used as identifiers were the bug class: `+data+`,
-`+record+`, `+partial+`.
-* `+src/Hypatia/ABI/*.idr+` are the real files (build namespace
-`+Hypatia.ABI.*+`, reached via `+sourcedir = ".."+` in the ipkg). They were
-never symlinks: `+src/abi/*.idr+` held byte-identical duplicate files that
-nothing compiled, deleted 2026-09-22 (issue #815).
-
-=== Definition of done
-
-[arabic]
-. Both theorems proven in Lean+Mathlib, no escape hatches,
-`+lake build+` clean.
-. Separate cached CI job gating them; workflow `+paths:+` updated.
-. `+PROOF-STATUS.md+` + `+needs.md+` rows flipped to COMPLETE.
-. Whole-corpus verification passes.
-. Draft PR against `+main+`.
-
-=== Out of scope (other contributors)
-
-Repo-hygiene PR (173 medium scan findings: `+timeout-minutes+` on
-`+ci.yml+`/`+clusterfuzzlite.yml+`, the `+setup-java+` SHA-pin
-false-positive); `+PipelineState+`→real `+proven+` integration;
-documenting the `+src/Hypatia/ABI+` layout; the `+gitbot-fleet+` /
-`+.git-private-farm+` repos.
+Two theory obligations are open in the proof ledger
+(`+verification/proof-ledger.jsonl+`, rows `+pagerank-convergence+` and
+`+esn-echo-state+`; rendered in `+verification/PROOF-STATUS.adoc#proof-ledger+`):
+
+* *PageRank:* the damped power iteration in `+lib/neural/graph_of_trust.ex+`
+  converges to a unique stationary vector.
+* *ESN:* with the reservoir scaled as `+lib/neural/echo_state_network.ex+`
+  scales it, two state trajectories under the same input converge
+  geometrically (the echo-state property), and `+[-1, 1]ⁿ+` is invariant.
+
+Both are *theory* (PROOF-POLICY §1): the source of truth is an Agda proof,
+rechecked in Rocq and Lean. The owner chose (2026-11-09) to state them over
+*constructive reals*, so the theorems are the textbook ones and not
+rational approximations of them.
+
+This supersedes the earlier version of this handover, which planned the
+proofs in Lean 4 with Mathlib. PROOF-POLICY forbids Mathlib as a
+dependency (§2) and puts theory in Agda first; that plan is withdrawn. The
+Lean files `+PageRankInvariants.lean+` and `+ESNSpectralScaling.lean+` prove
+natural-number *preconditions* only. Under PROOF-POLICY §3 they are
+engineering evidence, not legs of these theorems.
+
+=== Constraints
+
+* Every file checks under the canonical invocation (PROOF-POLICY §2.1):
+  `+agda --safe --without-K --cubical-compatible+`, Agda `+2.8.0.2+`
+  (the version CI pins). No `+postulate+`, no `+--cubical+`, no
+  `+TERMINATING+` or other unsafe pragma.
+* One dependency: agda-stdlib, pinned to a release tag and commit that
+  the receipt records. Feasibility checked 2026-11-09: agda-stdlib `+v2.3+`
+  (commit `+8326c7475af1fa456ca04a0203c168d5d7ff842b+`) loads
+  `+Data.Rational+` under the profile on Agda 2.8.0.2, and a Bishop-real
+  record over it type-checks. The first check builds the library (about two
+  minutes); later checks take seconds.
+* No real-analysis library is assumed. The reals are built here, small and
+  only as far as the two theorems need.
+* Hypotheses the runtime cannot discharge are *module parameters*, never
+  postulates. A theorem proved for every activation that is 1-Lipschitz and
+  bounded by 1 is a theorem; the claim that `+tanh+` is such an activation
+  is its own ledger row.
+
+=== Construction plan
+
+Files live in `+verification/proofs/agda/NeuralConvergence/+`. Each milestone
+checks on its own and lands as its own stacked PR, with its ledger rows.
+
+M0 — reals (`+Reals.agda+`)::
+Bishop regular sequences: `+x : ℕ → ℚ+` with
+`+∣ x m - x n ∣ ≤ 1/(m+1) + 1/(n+1)+`. Equality `+x ≈ y+` iff
+`+∣ x n - y n ∣ ≤ 2/(n+1)+` for all `+n+` (a setoid, not `+_≡_+`). Order,
+`+_+_+`, multiplication by a rational, `+∣_∣+`, `+max+`, the triangle
+inequality. Everything the theorems use carries an explicit modulus.
+
+M1 — completeness (`+Complete.agda+`)::
+A sequence of reals that is Cauchy with an explicit modulus has a limit
+(the diagonal construction), and the limit is unique up to `+_≈_+`.
+
+M2 — Banach, constructively (`+Contraction.agda+`)::
+On `+Vec ℝ n+` under a norm with the triangle inequality, a map with a
+rational modulus `+0 ≤ c < 1+` has a fixed point, it is unique, and the
+iterates satisfy `+‖xₖ - x*‖ ≤ cᵏ / (1 - c) · ‖x₁ - x₀‖+`. The rate is the
+modulus of convergence, so the statement is constructive by construction.
+
+M3 — PageRank (`+PageRank.agda+`)::
+`+G(x) = α·P·x + (1 - α)·v+` with `+P+` column-sub-stochastic (non-negative
+rational entries, each column summing to at most 1) and a rational
+`+0 ≤ α < 1+`. `+G+` is an ℓ¹ contraction with modulus `+α+`, because such a
+`+P+` gives `+‖P x‖₁ ≤ ‖x‖₁+`. Then M2. State it for sub-stochastic `+P+`, not
+only stochastic: the runtime builds sub-stochastic matrices. A node with no
+outgoing edge gives a zero column. `+iterate_trust/4+` in
+`+lib/neural/graph_of_trust.ex+` sums every parallel edge into a source's
+out-weight but takes one of them into each target, so repeated outcomes
+leak mass. The theorem then covers convergence for every runtime input. The
+leak changes what the fixed point means, and is a runtime defect to fix in
+the runtime, not to model. *Ledger:* `+pagerank-convergence+`
+becomes `+proven+` at PWG-3 once this checks in CI.
+
+M4 — ESN (`+EchoState.agda+`)::
+`+F_u(x) = (1 - a)·x + a·σ(W·x + w·u)+` for a rational leak rate
+`+0 < a ≤ 1+`, `+W+` with rational entries and induced ∞-norm (largest
+absolute row sum) `+‖W‖∞ ≤ ρ < 1+`, and σ a module parameter that is
+1-Lipschitz with `+∣σ t∣ ≤ 1+`. Show
+`+‖F_u(x) - F_u(y)‖∞ ≤ (1 - a + a·ρ)·‖x - y‖∞+` for every input `+u+`.
+Corollaries, by induction on the input sequence: two trajectories approach
+each other geometrically, and `+[-1, 1]ⁿ+` is invariant. Frame it in the
+∞-norm, *not* the spectral radius: the runtime has scaled by the induced
+∞-norm (`+@reservoir_norm+` = 0.95) since 2026-10, and `+test/neural_test.exs+`
+checks both that bound and the convergence of two initial states.
+*Ledger:* `+esn-echo-state+` becomes `+proven+` at PWG-3.
+
+M5 — tanh (`+Tanh.agda+`), its own row::
+Construct `+tanh+` on the reals (a convergent series or continued fraction
+with an explicit modulus) and prove it 1-Lipschitz and bounded by 1. Until
+this lands, M4 holds for every such σ, and the row recording that `+tanh+`
+is one stays `+open+`.
+
+=== What the theorems do not cover
+
+* The runtime uses IEEE floats. The theorems are about reals; the link from
+  them to `+lib/neural/*.ex+` is the `+models-runtime-refinement+` row, which is
+  `+open+` and names no evidence yet. `+test/neural_test.exs+` checks the ESN
+  ∞-norm bound and the convergence of two initial states; it is a candidate
+  for that row's evidence, not yet recorded as it.
+* Matrix entries are rational in the model. The runtime's weights are
+  floats, every one of which is a rational, so no generality is lost there;
+  rounding during iteration is what the model does not see.
+
+=== The recheck legs (after PWG-3)
+
+PROOF-POLICY §2: transport each witness through Dedukti first, and re-prove
+in Rocq and in Lean only where transport is unavailable. No Mathlib in the
+Lean leg. A leg counts toward PWG-2i or PWG-2ii only once its statement has
+been compared with the Agda statement and that comparison recorded
+(`+RECONCILED+`, §2.2). Record each leg in the theory row's `+legs+` field.
+
+=== CI
+
+Add an `+agda-neural+` job beside the existing `+agda strict-profile check+`
+job in `+.github/workflows/verify-proofs.yml+`. It should pin Agda
+`+2.8.0.2+` and the agda-stdlib tag and commit, cache the stdlib interface
+files keyed on that commit, and check every file in
+`+NeuralConvergence/+` with the §2.1 invocation. A missing or failing checker
+is a failure, never a skip. Its summary records what PWG-3 needs: the checker
+version, the stdlib pin, the flags in force, the import cone and each
+source digest (PROOF-POLICY §8.2).
+
+=== Definition of done (per milestone)
+
+. Every file in the milestone checks under the §2.1 invocation, locally and
+  in CI.
+. `+bash scripts/proof-ledger.sh check+` passes with the rows the milestone
+  changes, and `+render --write+` has refreshed `+PROOF-STATUS.adoc+`.
+. The PR body carries the receipt: checker version, stdlib pin, invocation,
+  source digests and the run that checked them.
+
+=== Gotchas already met
+
+* Agda's `+1/_+` in `+Data.Rational+` is the inverse of a rational. For
+  1/(n+1) write `(+ 1) / suc n`, with the integer constructor from
+  `+Data.Integer+` and `+_/_+` from `+Data.Rational+`.
+* Equality of reals is `+_≈_+`; every lemma about reals is up to it.
+  Reaching for `+_≡_+` on reals is the usual first wrong turn.
diff --git a/docs/proofs/needs.adoc b/docs/proofs/needs.adoc
index 7246aaee..99360ad3 100644
--- a/docs/proofs/needs.adoc
+++ b/docs/proofs/needs.adoc
@@ -1,96 +1,28 @@
-== PROOF-NEEDS.md — hypatia
-
-=== Current State (Updated 2026-06-05)
-
-* **src/Hypatia/ABI/*.idr**: `+Types.idr+`, `+FFI.idr+`, `+GraphQL.idr+`,
-`+GRPC.idr+`, `+REST.idr+`, `+RuleEngine.idr+` — built as the
-`+hypatia-abi+` package under `+--total+`.
-* **verify/src/*.idr**: `+PipelineState.idr+`, `+Verify/Fuel.idr+` —
-`+hypatia-verify+` package.
-* *verification/proofs/idris2/*: 7 standalone proof files
-(`+idris2 --check+`).
-* *verification/proofs/lean4/*: 5 Lean files (`+lake build+`).
-* *verification/proofs/tlaplus/*: `+KinGate.tla+` (TLC model-check).
-* *Toolchain*: Idris2 `+v0.7.0+`, Lean `+v4.30.0+` (both pinned), TLA+
-tla2tools 2.19. Agda was retired 2026-04-22 (see PROOF-STATUS.md
-"`Retired proofs`").
-* *Escape hatches*: 0 — no `+believe_me+` / `+assert_total+` /
-`+postulate+` / `+sorry+` / `+Admitted+` / `+unsafeCoerce+` in any proof
-file.
-* All of the above is gated by `+.github/workflows/verify-proofs.yml+`.
-
-=== Completed Proofs
-
-[width="100%",cols="24%,30%,46%",options="header",]
-|===
-|File |Covers |Obligation
-|`+verification/proofs/idris2/ConfidenceBounds.idr+` |Confidence bounded
-[0,1]; Bayesian update preserves invariant |H1 ✅
-
-|`+verification/proofs/idris2/DispatchStrategy.idr+` |Dispatch strategy
-monotone (confidence → strategy) |H2 ✅
-
-|`+verification/proofs/idris2/SafetyTriangle.idr+` |Eliminate >
-Substitute > Control strict ordering |H3 ✅
-
-|`+verification/proofs/lean4/RateLimiting.lean+` |Window counters never
-exceed configured bounds |H4 ✅
-
-|`+verification/proofs/idris2/Quarantine.idr+` |Quarantine trigger
-exclusivity + release correctness |H5 ✅
-
-|`+lib/outcome_tracker.ex+` (`+assert_h6_monotone/2+`) |Outcome-log
-timestamp monotonicity — runtime assertion + echidnabot audit |H6
-(retired from Agda)
-
-|`+verification/proofs/lean4/BayesianUpdate.lean+` |Posterior in (0,1),
-monotone in successes/failures, zero-obs identity |H7 ✅
-
-|`+verification/proofs/tlaplus/KinGate.tla+` |Kin-gate atomicity /
-mutual exclusion (TLC: 1.78M states, no errors) |H8 ✅
-
-|`+verification/proofs/idris2/NeuralConsensus.idr+` |Uniform-mean
-aggregation in [0,1], bounded below by n·min |H9 ✅
-
-|`+verification/proofs/idris2/VerisimdbConnector.idr+` |Connector
-completeness / soundness / preservation |—
-
-|`+verification/proofs/idris2/BatchRollback.idr+` |Batch rollback
-transactionality / reversibility |—
-
-|`+verification/proofs/lean4/ParserTotality.lean+` |VCL `+FROM+`-clause
-parser totality + round-trip |—
-|===
-
-=== What Still Needs Proving
-
-These are the *only* open proof obligations. Both currently prove ℕ
-_structural preconditions_ over the natural-number model; the full
-analytical theorems require Mathlib and are in progress.
-
-[width="100%",cols="24%,28%,32%,16%",options="header",]
-|===
-|Component |Proven today |Target theorem |Prover
-|PageRank power-iteration convergence (`+PageRankInvariants.lean+`)
-|non-negativity, column-stochastic normalisation preconditions
-|Banach-contraction convergence of the damped Google matrix (α < 1)
-|Lean 4 + Mathlib
-
-|ESN echo-state stability (`+ESNSpectralScaling.lean+`) |floor-clamped
-denominator is positive (scaling well-defined) |operator-norm
-contraction ⇒ bounded trajectory + exponential forgetting |Lean 4 +
-Mathlib
-|===
-
-=== Recommended Prover
-
-*Idris2* for ABI / type-level invariants. *Lean 4* for algorithmic and
-numerical properties (*+ Mathlib* for the analytic convergence results).
-*TLA+* for model-checked concurrency. (Agda is no longer in the
-toolchain.)
-
-=== Priority
-
-*MEDIUM* — H1–H9 are complete (H6 as a runtime assertion). The remaining
-work is the two neural-convergence theorems, which require pulling in
-Mathlib.
+// SPDX-License-Identifier: CC-BY-SA-4.0
+== Proof needs — hypatia
+
+What still needs proving is the set of rows in the proof ledger whose status
+is not `+proven+`. The ledger is `+verification/proof-ledger.jsonl+` and is
+canonical; `+verification/PROOF-STATUS.adoc#proof-ledger+` renders it with a
+census line. This file keeps no list of its own. The earlier hand-kept
+inventory here drifted: it called Agda retired after an Agda artefact was
+reinstated, and planned Lean with Mathlib, which PROOF-POLICY forbids.
+
+To list the open work:
+
+[source,bash]
+----
+jq -r 'select(.status != "proven") | "\(.status)\t\(.id)\t\(.obligation)"' verification/proof-ledger.jsonl
+----
+
+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.
+
+Prover mapping and statuses: the estate PROOF-POLICY
+(`+metadatastician/standards/3-practice/PROOF-POLICY.adoc+`).
diff --git a/scripts/proof-ledger.sh b/scripts/proof-ledger.sh
index bebb8720..57960a8c 100755
--- a/scripts/proof-ledger.sh
+++ b/scripts/proof-ledger.sh
@@ -7,6 +7,7 @@
 # rendered from it (README-EXPLAINME-STANDARD section 5, rule 1).
 #
 #   proof-ledger.sh check          validate the ledger against its rules and the tree
+#   proof-ledger.sh claims         every census README, AFFIRMATION or EXPLAINME quotes is the ledger's
 #   proof-ledger.sh render         print the AsciiDoc block for PROOF-STATUS.adoc
 #   proof-ledger.sh render --check fail if PROOF-STATUS.adoc holds a different block
 #   proof-ledger.sh render --write replace the block in PROOF-STATUS.adoc
@@ -219,6 +220,37 @@ render() {
   printf '%s\n' "$END_MARK"
 }
 
+# Every census a claim document quotes ("N proven of M; ...") must be the
+# ledger's census: README's proof count is derived from the ledger, never
+# typed in (README-EXPLAINME section 5, rule 2). Lines are joined first, so a
+# census wrapped across lines is still read whole. Each document named must
+# exist and quote at least one census: a renamed file or a census reworded
+# out of the pattern would otherwise pass unread.
+CLAIM_DOCS="${PROOF_CLAIM_DOCS:-README.adoc AFFIRMATION.adoc EXPLAINME.adoc}"
+claims() {
+  local want doc found fails=0 seen=0 c here
+  want=$(census | sed 's/ Theory rows:.*//')
+  for doc in $CLAIM_DOCS; do
+    if [ ! -f "$doc" ]; then
+      echo "::error::proof-ledger: claim document $doc does not exist"; fails=$((fails + 1)); continue
+    fi
+    found=$(tr '\n' ' ' < "$doc" | tr -s ' ' | grep -oE '[0-9]+ proven of [0-9]+(; [0-9]+ proven-with-postulates, [0-9]+ tested-only, [0-9]+ argued, [0-9]+ open\.?)?' || true)
+    here=0
+    while IFS= read -r c; do
+      [ -n "$c" ] || continue
+      seen=$((seen + 1)); here=$((here + 1))
+      [ "${c%.}." = "$want" ] && continue
+      echo "::error::proof-ledger: $doc quotes the census '$c'; the ledger's is '$want'"
+      fails=$((fails + 1))
+    done <<<"$found"
+    if [ "$here" -eq 0 ]; then
+      echo "::error::proof-ledger: $doc quotes no census ('N proven of M; ...'); a claim document states the ledger's"; fails=$((fails + 1))
+    fi
+  done
+  if [ "$fails" -gt 0 ]; then return 1; fi
+  echo "proof-ledger: $seen quoted census(es) agree with the ledger"
+}
+
 # Exactly one BEGIN and one END marker, BEGIN first: a second block (a bad
 # merge, a hand copy) would publish two tables while the first one passed.
 markers_ok() {
@@ -235,6 +267,7 @@ doc_block() {
 
 case "${1:-}" in
   check) check ;;
+  claims) claims ;;
   render)
     case "${2:-}" in
       "") render ;;
@@ -266,5 +299,5 @@ case "${1:-}" in
         echo "proof-ledger: wrote the block into $DOC" ;;
       *) echo "usage: $0 render [--check|--write]" >&2; exit 2 ;;
     esac ;;
-  *) echo "usage: $0 check | render [--check|--write]" >&2; exit 2 ;;
+  *) echo "usage: $0 check | claims | render [--check|--write]" >&2; exit 2 ;;
 esac
diff --git a/tests/proof-ledger-test.sh b/tests/proof-ledger-test.sh
index fc86d10e..bd817df1 100755
--- a/tests/proof-ledger-test.sh
+++ b/tests/proof-ledger-test.sh
@@ -79,6 +79,20 @@ cp verification/PROOF-STATUS.adoc "$work/doc.adoc"
 sed -i '0,/^|proven$/s//|proven-with-postulates/' "$work/doc.adoc"
 expect "a hand edit to the rendered table is refused" 1 env PROOF_STATUS_DOC="$work/doc.adoc" bash "$script" render --check
 
+expect "every census the claim documents quote is the ledger's" 0 bash "$script" claims
+
+# Built from the ledger's own census, so the contracts outlive any count.
+census_now=$(bash "$script" check | sed -n 's/^proof-ledger: [0-9]* rows valid; \(.*\) Theory rows:.*/\1/p')
+proven_now=${census_now%% proven of*}
+printf 'Ledger: %s\n' "$((proven_now + 1))${census_now#"$proven_now"}" > "$work/wrong.adoc"
+expect "a census that disagrees with the ledger is refused" 1 env PROOF_CLAIM_DOCS="$work/wrong.adoc" bash "$script" claims
+
+printf 'We have %s so far.\n' "${census_now%%;*}" > "$work/short.adoc"
+expect "a bare count without the rest of the census is refused" 1 env PROOF_CLAIM_DOCS="$work/short.adoc" bash "$script" claims
+
+printf 'Ledger: %s\n' "$census_now" | sed 's/ proven of / proven of\n/; s/, \([0-9]* argued\)/,\n\1/' > "$work/wrapped.adoc"
+expect "a census wrapped across lines is read whole" 0 env PROOF_CLAIM_DOCS="$work/wrapped.adoc" bash "$script" claims
+
 head -c -1 verification/proof-ledger.jsonl > "$work/no-lf.jsonl"
 expect_msg "a ledger without its final LF is refused" 1 "must end in exactly one LF" env PROOF_LEDGER="$work/no-lf.jsonl" bash "$script" check
 
@@ -131,5 +145,10 @@ expect_msg "a pin without a full commit is refused" 1 "pin is missing or malform
 { cat verification/PROOF-STATUS.adoc; bash "$script" render; } > "$work/two-blocks.adoc"
 expect_msg "render --check refuses a second generated block" 2 "more than one pair" env PROOF_STATUS_DOC="$work/two-blocks.adoc" bash "$script" render --check
 
+expect_msg "claims: a claim document that does not exist is refused" 1 "does not exist" env PROOF_CLAIM_DOCS="$work/no-such-doc.adoc" bash "$script" claims
+
+printf 'This document no longer quotes the census.\n' > "$work/silent.adoc"
+expect_msg "claims: a claim document that quotes no census is refused" 1 "quotes no census" env PROOF_CLAIM_DOCS="$work/silent.adoc" bash "$script" claims
+
 echo "proof-ledger-test: $pass passed, $fail failed"
 [ "$fail" -eq 0 ]