docs(proofs): align the neural-convergence plan and proof ledger with PROOF-POLICY

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

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

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+`).

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.

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
 

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:

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

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 =

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