diff --git a/.machine_readable/testing/blitz.a2ml b/.machine_readable/testing/blitz.a2ml
index cba82d31..8ca5241c 100644
--- a/.machine_readable/testing/blitz.a2ml
+++ b/.machine_readable/testing/blitz.a2ml
@@ -371,5 +371,5 @@ items = [
   "external-user-feedback (can't be manufactured)",
   "formal WCAG/GDPR audit (needs external domain expert)",
   "energy profiling (tooling gap for BEAM+Rust hybrid)",
-  "full PageRank convergence proof (tracked in PROOFS-GAP.md PR 4 — needs Mathlib)",
+  "PageRank contraction proof (T-PR, docs/proofs/HANDOVER-neural-convergence.adoc — Agda, rechecked in Rocq and Lean; fixed-point existence is a separate, unplanned theorem)",
 ]
diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc
index 1b0b9826..ddc19a1e 100644
--- a/AFFIRMATION.adoc
+++ b/AFFIRMATION.adoc
@@ -33,9 +33,16 @@ 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.) _Amended 2026-11-09 (#1025), after the
+  `affirmed-at` timestamp above, which does not cover the rest of this
+  item:_ one theorem obligation remains open —
+  neural contraction (PageRank, ESN and LSM) — two theory theorems, to be
+  proved in Agda and rechecked in Rocq and Lean without Mathlib (estate
+  PROOF-POLICY §§1–2); the handover is at
+  `docs/proofs/HANDOVER-neural-convergence.adoc`. Separately, the
+  PROOF-POLICY §6 deviation records for the proof toolchains CI installs
+  outside Guix are not yet written (`verification/PROOF-STATUS.adoc`,
+  "Toolchain deviations").
 * *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/docs/proofs/HANDOVER-neural-convergence.adoc b/docs/proofs/HANDOVER-neural-convergence.adoc
index 0efdc12c..b7054022 100644
--- a/docs/proofs/HANDOVER-neural-convergence.adoc
+++ b/docs/proofs/HANDOVER-neural-convergence.adoc
@@ -1,219 +1,173 @@
-== HANDOVER — Complete the proof corpus: neural-convergence proofs (Lean 4 + Mathlib)
-
-=== 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",]
+// SPDX-License-Identifier: CC-BY-SA-4.0
+== HANDOVER — neural-convergence theorems (Agda, rechecked in Rocq and Lean)
+
+=== What changed, and why
+
+Until 2026-11-09 this handover planned the PageRank and ESN convergence
+proofs in Lean 4 *with Mathlib*, in a separate `+lean4-mathlib/+` project.
+That plan is withdrawn. The estate
+https://github.com/metadatastician/standards/blob/9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5/3-practice/PROOF-POLICY.adoc[PROOF-POLICY]
+(owner rulings of 2026-10-26 and 2026-11-04, pinned here at
+`+9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5+`) says:
+
+* *§1:* a statement that would be true of any implementation is *theory*.
+  Convergence is the policy's own example. Theory lives in *Agda*, under
+  `+agda --safe --without-K --cubical-compatible+` (§2.1).
+* *§2:* every Agda theory proof is rechecked in *Rocq* and in *Lean*,
+  transported through Dedukti where that works and re-proved by hand
+  where it does not. *No Mathlib*: a missing lemma is re-proved in the
+  core library.
+* *§8:* the result is graded `+PWG-3+` (Agda checked), `+PWG-2i+` (one leg
+  counted), `+PWG-2ii+` (both legs) or `+PWG-1+` (current receipts for
+  every witness). A leg counts only when its kernel accepted it *and* its
+  statement is `+RECONCILED+` with the Agda statement.
+
+The inventory, with each artefact's current status, is the
+`+neural-convergence+` section of `+verification/PROOF-STATUS.adoc+`.
+
+=== The two theorems
+
+Both are stated over an *abstract ordered commutative ring*: a record of
+carrier, operations and the order and absolute-value laws the proof uses,
+taken as a module parameter. That is not a postulate, so `+--safe+`
+accepts it. Agda, Rocq and Lean all have no real numbers without a large
+library, and real analysis is not needed: the activation and the matrix
+enter only through hypotheses. Use the *bound* form of the sup norm
+(`+∀ j, |x_j − y_j| ≤ δ+`) rather than defining a maximum.
+
+==== T-RC — reservoir contraction (ESN and LSM)
+
+Setting: `+0 ≤ a ≤ 1+`; `+ρ ≥ 0+`; an `+n × n+` matrix `+W+` with
+`+Σ_j |W_ij| ≤ ρ+` for every row `+i+`; any `+σ+` with
+`+|σ s − σ t| ≤ |s − t|+`; input weights `+b+`. The update is
+
+  F_u(x)_i = (1 − a)·x_i + a·σ(Σ_j W_ij·x_j + b_i·u)
+
+*Statement:* if `+|x_j − y_j| ≤ δ+` for every `+j+`, then
+`+|F_u(x)_i − F_u(y)_i| ≤ ((1 − a) + a·ρ)·δ+` for every `+i+` and every
+input `+u+`.
+
+*Corollary (forgetting):* for an input sequence of length `+k+`, the two
+trajectories from `+x+` and `+y+` stay within `+q^k·δ+`, where
+`+q = (1 − a) + a·ρ+`. Prove it by induction on the sequence. This is
+forgetting only when `+q < 1+`, that is when `+0 < a+` and `+ρ < 1+`; with
+`+a = 0+` or `+ρ ≥ 1+` the bound is non-expansive at best. State the
+contraction claim with those strict premises. Hypatia's values give
+`+q+` = 0.99 for the ESN (`+a+` 0.2, `+ρ+` 0.95) and 0.97 for the LSM
+(`+a+` 0.3, `+ρ+` 0.9).
+
+*Proof outline:* the input term cancels. The recurrent difference is
+`+Σ_j W_ij·(x_j − y_j)+` (distributivity), bounded by
+`+Σ_j |W_ij|·δ ≤ ρ·δ+` (triangle inequality over a finite sum, `+|xy| = |x||y|+`,
+monotonicity of multiplication by a non-negative). Then
+`+|(1 − a)·d + a·e| ≤ (1 − a)·|d| + a·|e|+` for `+0 ≤ a ≤ 1+`.
+
+==== T-PR — damped PageRank contraction (Graph of Trust)
+
+Setting: `+0 ≤ d ≤ 1+`; an `+n × n+` matrix `+P+` with `+P_ij ≥ 0+` and
+`+Σ_i P_ij ≤ 1+` for every column `+j+`; any constant vector `+c+`. The
+map is `+G(x) = c + d·P·x+`.
+
+*Statement:* `+Σ_i |G(x)_i − G(y)_i| ≤ d·Σ_j |x_j − y_j|+`.
+
+*Corollary:* iterates from any two starts approach each other by `+d+` per
+step in ℓ¹. That is a contraction only when `+d < 1+`; with `+d = 1+` the
+statement is non-expansiveness (`+P+` the identity keeps the distance
+fixed). State the contraction claim with `+0 ≤ d < 1+`. Hypatia uses
+`+d+` = 0.85.
+
+The premise is column-*sub*stochastic, `+≤ 1+`, not `+= 1+`. The earlier
+handover assumed a column-stochastic `+P+`, which hypatia's code does not
+produce: a node with no positive out-edges contributes a zero column.
+Existence and uniqueness of the fixed point need completeness, which an
+ordered ring does not provide; they are out of scope.
+
+=== How hypatia meets the premises (engineering, not graded)
+
+[cols="2,3,1",options="header"]
+|===
+|Premise |Where |Status
+|ESN `+ρ+` = 0.95, LSM `+ρ+` = 0.9: the largest absolute row sum after
+scaling is at most `+ρ+` (exactly `+ρ+` unless sparsity leaves the
+reservoir all zero, which is common at `+reservoir_size: 1+`)
+|`+generate_reservoir/1+` in `+lib/neural/echo_state_network.ex+` and
+`+lib/neural/liquid_state_machine.ex+`; row-sum tests in
+`+test/neural_test.exs+` |`+TESTED+`
+
+|Trajectories converge at the T-RC rate (0.99 ESN, 0.97 LSM)
+|Convergence tests in `+test/neural_test.exs+` |`+TESTED+`
+
+|`+σ = tanh+` is 1-Lipschitz; IEEE-754 doubles behave as the ring
+|Not modelled |`+ASSUMED+`
+
+|Graph of Trust edge weights are non-negative
+|`+test/graph_of_trust_convergence_test.exs+` |`+TESTED+`
+
+|Graph of Trust is `+G+` with `+c_i = (1 − d)/n+`, `+d = 0.85+`,
+`+P_ij = w_ji / Σ_k max(w_jk, 0)+` over positive edges
+|`+iterate_trust/4+` in `+lib/neural/graph_of_trust.ex+` |`+ASSUMED+`
+(a transcription; no test pins the column sums yet)
 |===
-|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+` |✅
+The ℕ precondition files `+PageRankInvariants.lean+` and
+`+ESNSpectralScaling.lean+` are engineering proofs in Lean. Under
+PROOF-POLICY §3 they move to Idris2 when they are next touched. Their
+header comments still describe the withdrawn Mathlib plan; correct them
+in that move.
 
-|*Neural convergence — PageRank*
-|`+verification/proofs/lean4/PageRankInvariants.lean+` |⛔ preconditions
-only
+=== Files to write
 
-|*Neural convergence — ESN*
-|`+verification/proofs/lean4/ESNSpectralScaling.lean+` |⛔ preconditions
-only
+[cols="2,3",options="header"]
+|===
+|File |Content
+|`+verification/proofs/agda/ReservoirContraction.agda+` |T-RC and its
+corollary. Builtins only (as `+LogtalkMigration.agda+`), or the agda-stdlib
+at a recorded pin if it is used.
+|`+verification/proofs/agda/PageRankContraction.agda+` |T-PR and its
+corollary.
+|Rocq leg for each |Re-proved by hand unless an Agda → Dedukti → Rocq
+transport of the term works; record which.
+|Lean leg for each (`+verification/proofs/lean4/+`, core only) |Re-proved:
+check the pinned Lambdapi release for a Lean exporter first (§2).
 |===
 
-=== 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).
+For each leg record, in `+verification/PROOF-STATUS.adoc+`: the exact
+proposition and premises, the route (`+transported+` / `+re-proved+`), how
+the statement was compared with the Agda one, the checker version, the
+invocation, the result, the source commit, and the axioms reported
+(`+#print axioms+` for Lean, `+Print Assumptions+` for Rocq).
+
+=== CI
+
+* Agda: extend the existing `+agda-check+` job in
+  `+.github/workflows/verify-proofs.yml+` to check the two new modules
+  with the same pinned Agda 2.8.0.2 and the same flags.
+* Lean: add the new modules to `+roots+` in
+  `+verification/proofs/lean4/lakefile.lean+`; the `+lake build+` job
+  already gates them.
+* Rocq: there is no Rocq job yet. Add one with a pinned `+coqc+`/`+rocq+`.
+* Every job that installs a toolchain outside Guix or the container needs
+  a PROOF-POLICY §6 `+deviation+` record. None of the current jobs has
+  one yet.
 
 === 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.
+. T-RC and T-PR checked in Agda under the §2.1 invocation: `+PROVEN+`,
+  `+AGDA-VERIFIED+`, `+PWG-3+`.
+. Rocq and Lean legs kernel-checked and `+RECONCILED+`: `+PWG-2ii+`, at
+  which point §2's recheck obligation is discharged.
+. CI receipts for every witness at one source commit: `+PWG-1+`.
+. `+verification/PROOF-STATUS.adoc+` rows updated from the receipts, not by
+  hand.
+. The two Lean precondition files moved to Idris2 with corrected headers.
+
+=== Toolchain notes
+
+* Agda: the official 2.8.0.2 Linux release tarball, as the `+agda-check+`
+  job installs it.
+* Lean: v4.30.0 per `+verification/proofs/lean4/lean-toolchain+`. elan's
+  download host may be blocked in agent sandboxes; the GitHub release
+  tarball plus `+elan toolchain link+` works.
+* Lean 4.30 gotchas met in this corpus: `+List.mem_cons_self+` has implicit
+  arguments; use `+induction … generalizing+` when the hypothesis must hold
+  for a changing state.
diff --git a/docs/proofs/gap-analysis.adoc b/docs/proofs/gap-analysis.adoc
index dddf4b28..a2f102bb 100644
--- a/docs/proofs/gap-analysis.adoc
+++ b/docs/proofs/gap-analysis.adoc
@@ -263,15 +263,18 @@ parser-adjacent proofs. *✅ Landed 2026-04-22 via
 *PR 4 — Prove PageRank convergence (1 day).* Net-new mathematical
 assurance over the neural layer, only after PR 2. *⚠ Partially landed
 2026-04-22 via `+claude/lean-proofs-parser-pagerank+` — preconditions
-only (non-negativity, column-stochastic scaling premises) in
-`+PageRankInvariants.lean+`. Full analytical convergence requires
-Mathlib; still open.*
+only (non-negativity of edge weights and weight sums over ℕ; no
+normalisation or column-sum bound) in
+`+PageRankInvariants.lean+`. The contraction theorem (T-PR: two runs approach
+each other; fixed-point existence is separate and needs completeness) is theory: Agda,
+rechecked in Rocq and Lean without Mathlib (PROOF-POLICY §§1–2); still open,
+see `+docs/proofs/HANDOVER-neural-convergence.adoc+`.*
 
 *PR 5 — Prove ESN stability (3 days).* Same shape as PR 4. *⚠ Partially
 landed (awaiting merge) via `+claude/esn-spectral-scaling+` —
 `+ESNSpectralScaling.lean+` proves scaling preconditions (well-defined
-denominator, floor-clamping). Full analytical echo-state property also
-blocked on Mathlib.*
+denominator, floor-clamping). The echo-state property (T-RC) is theory, as
+for PR 4; still open, see `+docs/proofs/HANDOVER-neural-convergence.adoc+`.*
 
 *PR 6+ — Pick from:* query-result determinism, cache coherence, k-means
 convergence, federation consistency. Each is its own branch.
@@ -290,5 +293,5 @@ VeriSimDB federation executor being live.
 *2026-04-22 update:* the half-day CI PR landed; Lean and Idris proofs
 are now merge-blocking. 11 proof files gated in CI (2 original Lean + 3
 new Lean + 7 Idris — awaiting one Idris stamp cycle). Remaining
-tractable work is mathlib integration for the analytical halves of
-PageRank + ESN convergence.
+work is the two theory theorems T-PR and T-RC (2026-11-09: Agda source,
+Rocq and Lean rechecks, no Mathlib; see `+docs/proofs/HANDOVER-neural-convergence.adoc+`).
diff --git a/docs/proofs/needs.adoc b/docs/proofs/needs.adoc
index 7246aaee..d1eec00c 100644
--- a/docs/proofs/needs.adoc
+++ b/docs/proofs/needs.adoc
@@ -11,15 +11,23 @@
 (`+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`").
+* *verification/proofs/agda/*: `+LogtalkMigration.agda+` (since
+2026-11-01; `+agda --safe --without-K --cubical-compatible+`, `+PWG-3+`).
+* *Toolchain*: Idris2 `+v0.7.0+`, Lean `+v4.30.0+`, Agda `+2.8.0.2+` (all
+pinned); TLA+ tla2tools is *not* pinned (CI fetches the latest release;
+the recorded 2026-04-17 run used 2.19). The 2026-04-22 retirement of Agda covered
+only `+OutcomeLog.agda+` (see `+verification/PROOF-STATUS.adoc+`,
+"`Retired proofs`"); Agda is the estate's theory prover (PROOF-POLICY §1).
 * *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
+=== Completed Proofs and Tested Models
+
+Each row is a kernel-checked proof except two: H6 is a runtime assertion
+with an echidnabot audit (its Agda proof was retired), and H8 is a bounded
+TLC model check, `+TESTED+` rather than `+PROVEN+` (PROOF-POLICY §4).
 
 [width="100%",cols="24%,30%,46%",options="header",]
 |===
@@ -47,7 +55,8 @@ timestamp monotonicity — runtime assertion + echidnabot audit |H6
 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 ✅
+mutual exclusion (TLC: 3 bots × 2 repos × 4 requests, 1.78M states, no
+errors) |H8 `+TESTED+` (bounded model check, not a proof)
 
 |`+verification/proofs/idris2/NeuralConsensus.idr+` |Uniform-mean
 aggregation in [0,1], bounded below by n·min |H9 ✅
@@ -59,38 +68,44 @@ completeness / soundness / preservation |—
 transactionality / reversibility |—
 
 |`+verification/proofs/lean4/ParserTotality.lean+` |VCL `+FROM+`-clause
-parser totality + round-trip |—
+parser totality and determinism; round-trip on fixed examples only |—
 |===
 
 === 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.
+Two *theory* obligations are open. The Lean files below prove only ℕ
+_structural preconditions_; the theorems themselves are stated, with the
+route and the definition of done, in
+`+docs/proofs/HANDOVER-neural-convergence.adoc+` and inventoried in the
+`+neural-convergence+` section of `+verification/PROOF-STATUS.adoc+`.
 
 [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
+|PageRank (`+lib/neural/graph_of_trust.ex+`; preconditions in
+`+PageRankInvariants.lean+`) |non-negativity of edge weights and of in/out
+weight sums over ℕ (no normalisation or column-sum bound)
+|T-PR: the damped map with a column-substochastic `+P+` is an ℓ¹
+contraction with modulus `+d+` |Agda, rechecked in Rocq and Lean (no
+Mathlib)
+
+|ESN and LSM reservoirs (preconditions in `+ESNSpectralScaling.lean+`)
+|floor-clamped denominator is positive (scaling well-defined); the row-sum
+bound and runtime forgetting are `+TESTED+` |T-RC: the leaky update with
+absolute row sums ≤ `+ρ+` is a sup-norm contraction with modulus
+`+(1 − a) + a·ρ+` |Agda, rechecked in Rocq and Lean (no 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.)
+Per https://github.com/metadatastician/standards/blob/9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5/3-practice/PROOF-POLICY.adoc[PROOF-POLICY]
+§1: *Idris2* for APIs, ABIs and engineering properties of hypatia's own
+code; *Agda* for theory, rechecked in *Rocq* and *Lean* without Mathlib;
+*TLA+* as a recorded §4 exception for model-checked concurrency (reported
+as `+TESTED+`).
 
 === 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.
+*MEDIUM* — H1–H5, H7 and H9 are proved, H6 is a runtime assertion and H8
+is `+TESTED+` by a bounded model check. The remaining
+work is the two neural-convergence theorems, T-RC and T-PR.
diff --git a/docs/testing/audit.adoc b/docs/testing/audit.adoc
index 83e62755..f6f09fc6 100644
--- a/docs/testing/audit.adoc
+++ b/docs/testing/audit.adoc
@@ -303,8 +303,10 @@ items in the aspect table. *Effort: 2 weeks each.*
 
 * *Observability upgrade (OpenTelemetry / Prometheus).* Already tracked
 in CLAUDE.md "`Planned`" — orthogonal to test grading.
-* *Full PageRank convergence proof (Mathlib).* Tracked in
-`+PROOFS-GAP.md+` PR 4.
+* *PageRank contraction proof (T-PR).* Tracked in
+`+docs/proofs/HANDOVER-neural-convergence.adoc+`. T-PR proves that two runs
+approach each other; that the iteration converges to a fixed point needs
+completeness and is a separate theorem, not planned.
 
 === 7. Out of scope
 
diff --git a/lib/neural/echo_state_network.ex b/lib/neural/echo_state_network.ex
index 1fd93196..61c2c660 100644
--- a/lib/neural/echo_state_network.ex
+++ b/lib/neural/echo_state_network.ex
@@ -21,7 +21,6 @@ defmodule Hypatia.Neural.EchoStateNetwork do
     is 0.95. That makes the leaky-tanh update a contraction in the sup norm
     (modulus `1 - leak + leak * 0.95`), which gives the echo state property and
     fading memory, and it bounds the spectral radius by the same value
-  - Teacher forcing during training for faster convergence
   - Washout period discards initial transients
 
   This enables:
diff --git a/lib/neural/graph_of_trust.ex b/lib/neural/graph_of_trust.ex
index 3909fc7d..7f4e6bc1 100644
--- a/lib/neural/graph_of_trust.ex
+++ b/lib/neural/graph_of_trust.ex
@@ -238,8 +238,9 @@ defmodule Hypatia.Neural.GraphOfTrust do
     # to its neighbours sum to at most the source's score). Dividing by
     # out-degree (count) only achieves this when all edges have equal
     # weight; with mixed weights we divide by the total weight instead
-    # so the per-source contribution is conserved. See PROOFS-GAP.md
-    # for why this premise matters for PageRank convergence.
+    # so the per-source contribution is conserved. See
+    # docs/proofs/HANDOVER-neural-convergence.adoc (T-PR) for why this
+    # premise matters for PageRank convergence.
     out_weight_sum =
       Map.new(adjacency, fn {src, targets} ->
         total = Enum.reduce(targets, 0.0, fn {_t, w}, acc -> acc + max(w, 0.0) end)
@@ -331,7 +332,7 @@ defmodule Hypatia.Neural.GraphOfTrust do
     # half of the signal is a post-processing anti-trust subtraction
     # from the converged scores; that change is out of scope for this
     # fix, which is purely about making the math correct. See
-    # PROOFS-GAP.md — Section "Neural / PageRank".
+    # docs/proofs/gap-analysis.adoc (PR 2, graph_of_trust normalisation).
     Enum.flat_map(outcomes, fn outcome ->
       case Map.get(outcome, "outcome") do
         "success" ->
diff --git a/lib/neural/liquid_state_machine.ex b/lib/neural/liquid_state_machine.ex
index 20337c17..56408204 100644
--- a/lib/neural/liquid_state_machine.ex
+++ b/lib/neural/liquid_state_machine.ex
@@ -189,7 +189,7 @@ defmodule Hypatia.Neural.LiquidStateMachine do
   defp update_reservoir(%__MODULE__{reservoir_weights: w, input_weights: iw, state: state}, input) do
     size = length(state)
 
-    # Leaky integrate-and-fire update
+    # Leaky tanh update
     for i <- 0..(size - 1) do
       # Recurrent input
       recurrent =
diff --git a/test/graph_of_trust_convergence_test.exs b/test/graph_of_trust_convergence_test.exs
index ff31f53f..9ffa0e6d 100644
--- a/test/graph_of_trust_convergence_test.exs
+++ b/test/graph_of_trust_convergence_test.exs
@@ -3,7 +3,7 @@
 defmodule Hypatia.Neural.GraphOfTrustConvergenceTest do
   @moduledoc """
   Regression test for the PageRank stochastic-matrix fix
-  (`PROOFS-GAP.md` — "graph_of_trust normalisation").
+  (`docs/proofs/gap-analysis.adoc` — PR 2, "graph_of_trust normalisation").
 
   Before the fix:
     * `build_edges/1` emitted negative weights for failure
diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc
index ea95851c..a7b8b634 100644
--- a/verification/PROOF-STATUS.adoc
+++ b/verification/PROOF-STATUS.adoc
@@ -27,15 +27,26 @@ neurosymbolic CI/CD platform.
 * Canonical estate policy:
   https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[Proof and Verification Policy].
   This file is a proof inventory, not an independent alternative policy.
-* Proof *grades* follow hyperpolymath/mathesis,
-  `+estate-mathematical-architecture+` §§5–6: *Grade 3* is an Agda proof
-  formulated and type-checking under the strict profile; *Grade 2*
-  requires translation(s) into independent foundational system(s);
-  *Grade 1* additionally requires those translated witnesses to compile
-  in headless, isolated CI via verified checker APIs. A target grade is
-  not a status. This inventory records exact statuses (Open / Claimed /
-  `+AGDA-PENDING+` / `+AGDA-VERIFIED+` / Grade 3 …) and never flattens
-  them into a confidence percentage.
+* Theory theorems carry a *Proof Witness Grade* as defined in
+  https://github.com/metadatastician/standards/blob/9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5/3-practice/PROOF-POLICY.adoc#proof-witness-grades[PROOF-POLICY §8]
+  (pinned at `+9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5+`):
+  `+PWG-3+` is an Agda source checked under the §2.1 invocation;
+  `+PWG-2i+` adds one counted recheck leg (Rocq or Lean, kernel-checked
+  *and* `+RECONCILED+`); `+PWG-2ii+` adds both legs; `+PWG-1+` adds a
+  current pinned-checker receipt for every witness at the exact source
+  commit. A theory theorem below `+PWG-3+` is `+ungraded+`. The grade
+  ladder first proposed in hyperpolymath/mathesis
+  `+docs/proposals/estate-mathematical-architecture.adoc+` §§5–6 is
+  provenance only; §8 supersedes it.
+* Each record keeps three separate fields and never writes one into
+  another: the §5 status token (`+PROVEN+` / `+PROVEN-WITH-AXIOMS+` /
+  `+TESTED+` / `+ASSUMED+` / `+OPEN+`), the §2.2 correspondence state
+  (`+AGDA-PENDING+`, `+AGDA-VERIFIED+`, `+LEAN-CHECKED+`,
+  `+BRIDGE-PENDING+`, `+RECONCILED+` …) and the PWG. Engineering proofs
+  (Idris2, Lean or TLA+ models of hypatia's own code) carry the status
+  token only. Grades are never flattened into a percentage.
+* No Mathlib (PROOF-POLICY §2). A missing Lean lemma is re-proved in the
+  core library.
 * A checked model proves its stated proposition only. In particular it
   does not prove runtime refinement of Elixir/BEAM code; such claims
   need their own correspondence evidence and tests.
@@ -48,6 +59,23 @@ pre-existing Lean files below retain their documented scope; they must
 not be represented as independently rechecking Agda proofs until
 checked Agda sources and correspondence evidence actually exist.
 
+NOTE: Until 2026-11-09 the Status columns below used `+COMPLETE+` and
+`+PARTIAL+`, which are not PROOF-POLICY §5 tokens. Every `+COMPLETE+` row
+names a file that a `+Verify Proofs+` job kernel-checks on every change
+(`+idris2 --check+` over `+verification/proofs/idris2/*.idr+`, the ABI and
+verify packages, `+lake build+`), so it now reads `+PROVEN+`, except
+`+GRPC.idr+` and `+REST.idr+`, which hold declarations and state no
+proposition, so no token applies to them. The two
+`+PARTIAL+` rows were split into what is proved and what is `+OPEN+`, and
+the TLA+ row is `+TESTED+` with its bounds, as PROOF-POLICY §4 requires of
+a finite model check.
+
+The Lean files `+BayesianUpdate+`, `+RateLimiting+`, `+ParserTotality+`,
+`+PageRankInvariants+` and `+ESNSpectralScaling+` state properties of
+hypatia's own functions, which makes them *engineering* proofs
+(PROOF-POLICY §1). Under §3 each moves to Idris2 when it is next touched;
+until then it stays here, labelled Lean.
+
 === Proof Inventory
 
 ==== Existing Proofs (pre-2026-04-04)
@@ -64,26 +92,33 @@ that happened to land within two lines; the column was still not worth keeping.)
 |`+src/Hypatia/ABI/Types.idr+` |Idris2 |Confidence refined type
 (`+So (value >= 0.0 && value <= 1.0)+` auto-proof), core data types,
 and the wire-contract pin `+connectorCount : length allConnectors = 16+`
-|COMPLETE
+|PROVEN
 
 |`+src/Hypatia/ABI/RuleEngine.idr+` |Idris2 |Safety triangle ordering,
 route totality, dispatch correctness, Bayesian monotonicity, annealing
-caps, end-to-end composition |COMPLETE
+caps, end-to-end composition |PROVEN
 
-|`+src/Hypatia/ABI/GraphQL.idr+` |Idris2 |Query/Mutation/Subscription
-type safety |COMPLETE
+|`+src/Hypatia/ABI/GraphQL.idr+` |Idris2 |Every query and every mutation
+returns an ApiResponse-wrapped type (queryReturnsApiResponse,
+mutationReturnsApiResponse). Subscriptions are declared, with no proof
+about them |PROVEN (queries and mutations)
 
 |`+src/Hypatia/ABI/GRPC.idr+` |Idris2 |gRPC service type definitions
-|COMPLETE
+|Not a proof: the module type-checks in the ABI package build, but it
+states no proposition, so no status token applies
 
 |`+src/Hypatia/ABI/REST.idr+` |Idris2 |REST endpoint type definitions
-|COMPLETE
+|Not a proof: the module type-checks, but it states no proposition
+(totalEndpointCount is a count, not a theorem), so no status token
+applies
 
 |`+src/Hypatia/ABI/FFI.idr+` |Idris2 |GADT constructors,
-`+ffiReturnsApiResponse+` proof |COMPLETE
+`+ffiReturnsApiResponse+` proof |PROVEN
 
-|`+verify/src/PipelineState.idr+` |Idris2 |Pipeline state machine
-(ValidTransition GADT), terminal/active classification |COMPLETE
+|`+verify/src/PipelineState.idr+` |Idris2 |Pipeline state machine: only the
+transitions listed in the ValidTransition GADT can be constructed (by
+construction). The terminal/active classification is defined, not proved
+|PROVEN (transitions by construction)
 |===
 
 ==== New Proofs (2026-04-04)
@@ -93,17 +128,17 @@ type safety |COMPLETE
 |File |Language |Properties Proven |Status
 |`+verification/proofs/idris2/ConfidenceBounds.idr+` |Idris2
 |[0,1] bounds preserved by construction, Bayesian update,
-success/failure monotonicity, clamping, weighted average |COMPLETE
+success/failure monotonicity, clamping, weighted average |PROVEN
 
 |`+verification/proofs/idris2/SafetyTriangle.idr+` |Idris2 |Strict
 total order (irreflexive, asymmetric, transitive), trichotomy, routing
 respects hierarchy, optimality (highest available), completeness (all
-tiers reachable) |COMPLETE
+tiers reachable) |PROVEN
 
 |`+verification/proofs/idris2/DispatchStrategy.idr+` |Idris2
 |Confidence-to-strategy monotonicity, boundary proofs (high/mid/low),
 annealing clamp bounds, nascent-never-auto, veteran-unrestricted
-|COMPLETE
+|PROVEN
 
 |`+verification/proofs/idris2/VerisimdbConnector.idr+` |Idris2
 |Completeness (mandatory fields), Soundness (missing fields rejected),
@@ -113,46 +148,52 @@ canonical JSON finding record (`+FindingFact+`). *Statement superseded
 (`+LogtalkFact+`); the equality proof term is unchanged, the target is
 now `+FindingFact+`, and the corresponding module is
 `+lib/verisim_connector.ex+`. Runtime refinement is not claimed.
-|COMPLETE (superseded statement; re-checked 2026-11-01 in Verify Proofs run 41328302925, idris2 --check job 124912804086, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331)
+|PROVEN (superseded statement; re-checked 2026-11-01 in Verify Proofs run 41328302925, idris2 --check job 124912804086, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331)
 
 |`+verification/proofs/idris2/Quarantine.idr+` |Idris2 |State
-transitions (ok/soft/hard/permanent), Auto-quarantine triggers, Release
-restoration, Routing blockage |COMPLETE
+transitions Ok to Soft and Ok to Hard, idempotence once quarantined,
+Auto-quarantine triggers, Release restoration, Routing blockage
+(including Permanent). No transition into Permanent is modelled, so none
+is proved |PROVEN
 
 |`+verification/proofs/idris2/BatchRollback.idr+` |Idris2
 |Transactionality (all-or-nothing), Reversibility (snapshot
-restoration), Fault tolerance (failure handling) |COMPLETE
+restoration), Fault tolerance (failure handling) |PROVEN
 
 |`+verification/proofs/lean4/RateLimiting.lean+` |Lean 4 |Counter
 never exceeds configured bound, tryAccept preserves invariant, prune
 preserves invariant, inductive sequence processing, rejection guarantee,
-concrete configs (per-bot/global/burst) |COMPLETE
+concrete configs (per-bot/global/burst) |PROVEN
 
 |`+verification/proofs/lean4/BayesianUpdate.lean+` |Lean 4 |H7:
 posterior in (0,1), monotone in successes/failures, zero-observation
-identity, floor/cap clamp |COMPLETE
+identity, floor/cap clamp |PROVEN
 
 |`+verification/proofs/lean4/ParserTotality.lean+` |Lean 4 |VCL
-`+FROM+`-clause parser totality, determinism, round-trip,
-malformed-input rejection |COMPLETE
+`+FROM+`-clause parser totality, determinism, malformed-input rejection.
+Round-trip is checked only on fixed example token lists (STORE, FEDERATION,
+HEXAD), not as a general theorem |PROVEN (round-trip: examples only)
 
 |`+verification/proofs/lean4/PageRankInvariants.lean+` |Lean 4
-|PageRank preconditions (edge-weight / out-degree non-negativity).
-*Convergence theorem in progress (Mathlib).* |PARTIAL
+|PageRank preconditions (edge-weight / out-degree non-negativity). The
+convergence theorem is not here: it is theory, see
+<<neural-convergence>> |PROVEN (preconditions only)
 
 |`+verification/proofs/lean4/ESNSpectralScaling.lean+` |Lean 4
-|ESN scaling preconditions (floor-clamped denominator positive).
-*Echo-state stability in progress (Mathlib).* |PARTIAL
+|ESN scaling preconditions over ℕ (floor-clamped denominator positive).
+The file's header still plans the stability proof in Mathlib; that plan
+is withdrawn, see <<neural-convergence>> |PROVEN (preconditions only)
 
 |`+verification/proofs/idris2/NeuralConsensus.idr+` |Idris2 |H9:
 uniform-mean aggregation of Vect n Prediction is in [0,1], bounded below
 by n * min(inputs), denominator > 0 for non-empty ensembles, 8-network
-specialization |COMPLETE
+specialization |PROVEN
 
 |`+verification/proofs/tlaplus/KinGate.tla+` |TLA+ |H8: Kin gate
 atomicity. Acquire/Release/Expire transitions + MutualExclusionByType +
 MutualExclusionBotView + ViewCoherentWithLocks + NoOrphanView +
-GrantsAreWellBracketed + EveryRequestProcessed (liveness) |COMPLETE —
+GrantsAreWellBracketed + EveryRequestProcessed (liveness) |TESTED
+(PROOF-POLICY §4 exception; a finite model check, not a proof) —
 TLC model-check 2026-04-17 passed on 3 bots × 2 repos × MaxRequests=4:
 1,778,860 distinct states, depth 13, no errors in 51s (Eclipse Temurin
 21 JRE, tla2tools 2.19)
@@ -170,10 +211,11 @@ JSONL for violations. See commit history.
 Finite, implementation-independent table correspondence for the retired
 ECHIDNA `+security_learning.lgt+` alert semantics versus
 `+Hypatia.Rules.SecurityErrors+`. Per the estate verifier mapping this
-is Agda territory; per Mathesis this is now *Grade 3* on the
+is Agda territory. It is `+PWG-3+` (PROOF-POLICY §8) on the
 strict-profile receipt recorded in the row below (checker version,
 library discipline, exact invocation, result, source digest, and
-verification commit). Fix *strings* and Elixir
+verification commit). Its import cone is Agda's builtins only: no
+standard library, `+--safe+` in force, zero postulates. Fix *strings* and Elixir
 runtime behaviour are outside the model and are pinned by the migration
 ledger and ExUnit tests respectively.
 
@@ -190,11 +232,13 @@ entries; the two ledgered non-equalities stated exactly
 former severity catch-all members explicit (`+catchAllSastLow+`,
 `+catchAllCiTestsLow+`, `+catchAllUnmaintainedLow+`). Source SHA-256
 (at authoring): bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0.
-|Grade 3 — AGDA-VERIFIED. Receipt: official pinned Agda 2.8.0.2 Linux
-release, builtins only/no stdlib; invocation `agda --safe --without-K
+|Status PROVEN; correspondence AGDA-VERIFIED; PWG-3, no
+axioms. Receipt: official pinned Agda 2.8.0.2 Linux release, builtins
+only/no stdlib; invocation `agda --safe --without-K
 --cubical-compatible LogtalkMigration.agda`; success in Verify Proofs
-run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331. No Grade 2/1,
-reconciliation, or runtime-refinement claim.
+run 41328302925, job 124912804344, at commit 4018290eaa3265b82209e2a45b6917a4bb0a0331.
+Rocq and Lean legs OPEN (none written), so no PWG-2i/PWG-2ii/PWG-1,
+reconciliation or runtime-refinement claim.
 |===
 
 ==== Verdict support (2026-10-14, HYP-01)
@@ -294,6 +338,106 @@ the Signalbox criterion has no Signalbox repository to apply to |TESTED
 (Signalbox: OPEN)
 |===
 
+[[neural-convergence]]
+==== Neural convergence: reservoir and PageRank contraction (2026-11-09)
+
+The ESN, the LSM and the Graph of Trust each iterate a map, and each is
+meant to forget where it started. Whether a map of that shape contracts
+is true of *any* implementation, so it is *theory* (PROOF-POLICY §1): the
+source of truth is Agda under the §2.1 invocation, rechecked in Rocq and
+in Lean (core library, no Mathlib). How hypatia's code meets the
+theorem's premises is *engineering* and is recorded separately. The full
+plan is `+docs/proofs/HANDOVER-neural-convergence.adoc+`.
+
+Statements, over an abstract ordered commutative ring (so that no real
+analysis and no postulate is needed; the activation and the matrix enter
+as hypotheses):
+
+* *T-RC (reservoir contraction).* For `+0 ≤ a ≤ 1+`, `+ρ ≥ 0+`, an `+n × n+` matrix
+  `+W+` whose absolute row sums are all at most `+ρ+`, and any `+σ+` with
+  `+|σ s − σ t| ≤ |s − t|+`: if `+|x_j − y_j| ≤ δ+` for every `+j+`, then
+  for every `+i+` and input `+u+`,
+  `+|F_u(x)_i − F_u(y)_i| ≤ ((1 − a) + a·ρ)·δ+`, where
+  `+F_u(x)_i = (1 − a)·x_i + a·σ(Σ_j W_ij·x_j + b_i·u)+`. Corollary:
+  under the same input sequence, two trajectories stay within
+  `+q^k·δ+` after `+k+` steps, `+q = (1 − a) + a·ρ+`. That is a
+  contraction, and forgetting, only when `+0 < a+` and `+ρ < 1+` (so
+  `+q < 1+`); otherwise it is non-expansive at best.
+* *T-PR (damped PageRank contraction).* For `+0 ≤ d ≤ 1+` and an
+  `+n × n+` matrix `+P+` with non-negative entries and every column sum
+  at most 1 (column-*sub*stochastic, as hypatia's dangling nodes make
+  it), the map `+G(x) = c + d·P·x+` satisfies
+  `+Σ_i |G(x)_i − G(y)_i| ≤ d·Σ_j |x_j − y_j|+`. Corollary: iterates from
+  any two starts approach each other by `+d+` per step, a contraction only
+  when `+d < 1+` (with `+d = 1+` and `+P+` the identity the distance stays
+  fixed). Existence of a
+  fixed point needs completeness, which an ordered ring does not have;
+  it is out of scope.
+
+[width="100%",cols="28%,14%,42%,16%",options="header",]
+|===
+|Artefact |Language |Claim |Status
+|T-RC Agda source (planned as ReservoirContraction in
+verification/proofs/agda/; not yet written)
+|Agda |The T-RC statement above |`+OPEN+`; `+AGDA-PENDING+`; `+ungraded+`
+
+|T-RC Rocq and Lean legs |Rocq, Lean 4 |Re-proofs of the same statement
+|`+OPEN+` (both)
+
+|T-PR Agda source (planned as PageRankContraction in
+verification/proofs/agda/; not yet written)
+|Agda |The T-PR statement above |`+OPEN+`; `+AGDA-PENDING+`; `+ungraded+`
+
+|T-PR Rocq and Lean legs |Rocq, Lean 4 |Re-proofs of the same statement
+|`+OPEN+` (both)
+
+|Reservoir scaling, `+lib/neural/echo_state_network.ex+`,
+`+lib/neural/liquid_state_machine.ex+` |Elixir |After scaling, the largest
+absolute row sum is at most `+@reservoir_norm+` (ESN 0.95, LSM 0.9), i.e.
+T-RC's `+ρ+`. It equals it unless sparsity leaves the reservoir all zero,
+which is common at `+reservoir_size: 1+` (seeds 1–4 for the ESN, 1–5 for
+the LSM) and still satisfies the bound. Equality for non-degenerate
+reservoirs: `+test/neural_test.exs+` "reservoir's largest absolute row sum
+is 0.95 / 0.9 for any size and seed" (ESN sizes 10/20/80, LSM 10/20/100,
+seeds 1–5) |`+TESTED+`
+
+|Reservoir forgetting at runtime |Elixir |Two runs from different
+initial states converge within the T-RC bound, whose factor is
+`+(1 − a) + a·ρ+` = 0.99 for the ESN (`+a+` 0.2, `+ρ+` 0.95) and 0.97 for
+the LSM (`+a+` 0.3, `+ρ+` 0.9): `+test/neural_test.exs+` "two different
+initial states converge under the same inputs / events" (300 steps or
+events, seeds 1–3) |`+TESTED+`
+
+|T-RC premises for the runtime |— |`+:math.tanh/1+` is 1-Lipschitz, and
+IEEE-754 doubles stand in for the ring (rounding is not modelled)
+|`+ASSUMED+`
+
+|T-PR premises for the runtime: edge weights, `+lib/neural/graph_of_trust.ex+`
+|Elixir |Every edge weight is a non-negative number:
+`+test/graph_of_trust_convergence_test.exs+` "every edge has a non-negative
+numeric weight" |`+TESTED+`
+
+|T-PR premises for the runtime: the map |— |The iteration is `+G+` with
+`+c_i = (1 − d)/n+`, `+d = 0.85+`, and
+`+P_ij = w_ji / Σ_k max(w_jk, 0)+` over positive edges, so column sums
+are at most 1 (a transcription of `+iterate_trust/4+`; no test pins the
+column sums) |`+ASSUMED+`
+|===
+
+==== Toolchain deviations (PROOF-POLICY §6)
+
+`+verify-proofs.yml+` installs Lean through elan, Idris2 from source, Agda
+from the upstream release archive and TLC from the tla2tools jar, none of
+them through a Guix manifest or the container. §6 requires a `+deviation+`
+record for each (leg, tool, asserted version, digest of what was
+installed, why Guix or the container was not used, state). Those records
+have not been written, and the jobs do not yet record installer digests.
+TLC is not even version-pinned: the job fetches
+`+releases/latest/download/tla2tools.jar+` and caches it under a fixed key,
+so the 2.19 named in the KinGate row is the version of the recorded
+2026-04-17 run, not a guarantee for later runs:
+`+OPEN+`.
+
 === Properties Proven
 
 ==== 1. Confidence Bounds (`+ConfidenceBounds.idr+`)
@@ -378,8 +522,8 @@ rejected
 
 ==== 8. Logtalk Migration Correspondence (`+LogtalkMigration.agda+`)
 
-Status for all of P8: *Grade 3 — AGDA-VERIFIED* on the strict-profile
-receipt in the inventory row above (Agda 2.8.0.2, Verify Proofs run
+Status for all of P8: PROVEN, correspondence AGDA-VERIFIED, PWG-3, on
+the strict-profile receipt in the inventory row above (Agda 2.8.0.2, Verify Proofs run
 41328302925, job 124912804344, commit 4018290eaa3265b82209e2a45b6917a4bb0a0331). This grades the finite
 model only.
 
@@ -437,8 +581,9 @@ model only.
 |Annealing stage caps |`+DispatchStrategy.idr+`, `+RuleEngine.idr+`
 |Full
 
-|API type safety |`+Types.idr+`, `+GraphQL.idr+`, `+REST.idr+`,
-`+GRPC.idr+`, `+FFI.idr+` |Full
+|API type safety |`+Types.idr+`, `+GraphQL.idr+`, `+FFI.idr+` (proofs);
+`+REST.idr+`, `+GRPC.idr+` (type-checked declarations only) |Full for
+the proved properties
 
 |Quarantine logic |`+Quarantine.idr+` |Full
 
@@ -448,8 +593,8 @@ model only.
 superseded 2026-11-01)
 
 |Logtalk → Elixir alert-table correspondence
-|`+LogtalkMigration.agda+` |Finite model only — Grade 3 /
-AGDA-VERIFIED (receipt above); fix text and runtime refinement excluded
+|`+LogtalkMigration.agda+` |Finite model only — PWG-3, AGDA-VERIFIED
+(receipt above); fix text and runtime refinement excluded
 
 |Neural ensemble aggregation |`+NeuralConsensus.idr+` |Full (bounds +
 min-lower-bound)
@@ -459,8 +604,9 @@ min-lower-bound)
 |VCL query correctness |- |Partial
 
 |Neural network convergence |`+PageRankInvariants.lean+`,
-`+ESNSpectralScaling.lean+` |Preconditions proven; full
-convergence/stability in progress (Lean + Mathlib)
+`+ESNSpectralScaling.lean+`, `+test/neural_test.exs+` |Preconditions
+`+PROVEN+`; runtime scaling and convergence `+TESTED+`; the two theory
+theorems `+OPEN+` and `+ungraded+` (<<neural-convergence>>)
 |===
 
 === File Locations
diff --git a/verification/README.adoc b/verification/README.adoc
index 6cb675c1..471a7c59 100644
--- a/verification/README.adoc
+++ b/verification/README.adoc
@@ -9,7 +9,7 @@ Idris2, Lean 4, TLA+ and Agda proof sources for Hypatia's type-level guarantees.
   normative ABI in `src/Hypatia/ABI/`
 * `proofs/lean4/`, `proofs/tlaplus/` — Lean 4 and TLA+ proofs
 * `proofs/agda/` — Agda correspondence model for the Logtalk → Elixir
-  rule migration (`LogtalkMigration.agda`; Mathesis Grade 3 receipt in
+  rule migration (`LogtalkMigration.agda`; `PWG-3` receipt in
   `PROOF-STATUS.adoc`)
 * `PROOF-STATUS.adoc` — Current proof completion status
 
diff --git a/verification/proofs/tlaplus/KinGate.tla b/verification/proofs/tlaplus/KinGate.tla
index f6217d3b..4170e25a 100644
--- a/verification/proofs/tlaplus/KinGate.tla
+++ b/verification/proofs/tlaplus/KinGate.tla
@@ -20,6 +20,19 @@
 \*   - grantHistory: an append-only log of (bot, repo) grants used to
 \*     state the non-trivial "no interleaved re-grant without release"
 \*     safety property NoReGrantWithoutRelease.
+\*
+\* PROOF-POLICY section 4 exception record
+\* (metadatastician/standards 3-practice/PROOF-POLICY.adoc @ 9bdf864cc7f2):
+\*   Obligation: H8, kin-gate mutual exclusion under any interleaving of
+\*               Acquire / Release / Expire.
+\*   Tool:       TLA+ with the TLC model checker.
+\*   Why not the mapped prover (Idris2): the property is about every
+\*               interleaving of a concurrent protocol; exhaustive model
+\*               checking states and checks that directly, where an Idris2
+\*               proof would take far longer. PROOF-POLICY section 4 names
+\*               this file as its worked example.
+\*   Status:     TESTED, bounded by KinGate.cfg (3 bots x 2 repos x 4
+\*               requests); not PROVEN. Ledger: verification/PROOF-STATUS.adoc.
 
 EXTENDS Naturals, FiniteSets, Sequences, TLC