From ea10d4c5efd876f1b65bf7b104b0e55aed58e378 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:00:20 +0000 Subject: [PATCH 1/8] docs(proofs): align the neural-convergence plan and proof ledger with PROOF-POLICY The neural-convergence plan (HANDOVER, needs, gap-analysis, AFFIRMATION) put the PageRank and ESN theorems in Lean with Mathlib. The estate PROOF-POLICY (owner rulings 2026-10-26 and 2026-11-04) makes convergence theory: Agda source under --safe --without-K --cubical-compatible, rechecked in Rocq and Lean, no Mathlib, graded by Proof Witness Grades. - HANDOVER-neural-convergence.adoc rewritten: two theory theorems over an abstract ordered commutative ring. T-RC is the reservoir sup-norm contraction with modulus (1 - a) + a*rho, covering both ESN and LSM. T-PR is the damped PageRank l1 contraction for a column-substochastic P; the old plan assumed column-stochastic, which dangling nodes break. Separately, the engineering premises hypatia meets are listed as TESTED or ASSUMED. - PROOF-STATUS.adoc: grades cite PROOF-POLICY section 8, pinned by commit, instead of the superseded mathesis brief. The status, the correspondence state and the PWG are kept in separate fields. COMPLETE/PARTIAL become section 5 tokens. The KinGate TLC row becomes TESTED, per the policy's worked example. LogtalkMigration is recorded as PROVEN / AGDA-VERIFIED / PWG-3. New neural-convergence section with T-RC and T-PR OPEN and ungraded. The missing section 6 toolchain deviation records are now recorded as OPEN. - needs.adoc no longer says Agda is retired, since only OutcomeLog.agda was. - Replace dangling PROOFS-GAP.md references in Elixir comments and a test moduledoc. - Drop the ESN moduledoc's teacher-forcing claim (feedback_weights is never used) and the LSM's stale integrate-and-fire comment. No proof, test or runtime behaviour changes. mix test test/neural_test.exs test/graph_of_trust_convergence_test.exs: 31 tests, 0 failures; mix format --check-formatted clean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --- .machine_readable/testing/blitz.a2ml | 2 +- AFFIRMATION.adoc | 6 +- docs/proofs/HANDOVER-neural-convergence.adoc | 348 ++++++++----------- docs/proofs/gap-analysis.adoc | 13 +- docs/proofs/needs.adoc | 49 +-- docs/testing/audit.adoc | 4 +- lib/neural/echo_state_network.ex | 1 - lib/neural/graph_of_trust.ex | 7 +- lib/neural/liquid_state_machine.ex | 2 +- test/graph_of_trust_convergence_test.exs | 2 +- verification/PROOF-STATUS.adoc | 202 ++++++++--- verification/README.adoc | 2 +- 12 files changed, 356 insertions(+), 282 deletions(-) diff --git a/.machine_readable/testing/blitz.a2ml b/.machine_readable/testing/blitz.a2ml index cba82d31..adec8ef7 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)", + "full PageRank convergence proof (T-PR, docs/proofs/HANDOVER-neural-convergence.adoc — Agda, rechecked in Rocq and Lean)", ] diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 1b0b9826..50bf8216 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -34,8 +34,10 @@ state and commitments. Companion detail: 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`. + neural-convergence (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`. * *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..bc81069b 100644 --- a/docs/proofs/HANDOVER-neural-convergence.adoc +++ b/docs/proofs/HANDOVER-neural-convergence.adoc @@ -1,219 +1,163 @@ -== 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",] -|=== -|Obligation |File |Status -|H1 confidence bounds -|`+verification/proofs/idris2/ConfidenceBounds.idr+` |✅ +// 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+`; 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 -|H2 dispatch monotonicity -|`+verification/proofs/idris2/DispatchStrategy.idr+` |✅ + F_u(x)_i = (1 − a)·x_i + a·σ(Σ_j W_ij·x_j + b_i·u) -|H3 safety-triangle order -|`+verification/proofs/idris2/SafetyTriangle.idr+` |✅ +*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+`. -|H4 rate limiting |`+verification/proofs/lean4/RateLimiting.lean+` |✅ +*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. -|H5 quarantine |`+verification/proofs/idris2/Quarantine.idr+` |✅ +*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+`. -|H6 outcome-log monotonicity |`+lib/outcome_tracker.ex+` (runtime -assertion; Agda retired) |✅ +==== T-PR — damped PageRank contraction (Graph of Trust) -|H7 Bayesian update |`+verification/proofs/lean4/BayesianUpdate.lean+` -|✅ +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+`. -|H8 kin-gate atomicity |`+verification/proofs/tlaplus/KinGate.tla+` |✅ +*Statement:* `+Σ_i |G(x)_i − G(y)_i| ≤ d·Σ_j |x_j − y_j|+`. -|H9 neural consensus aggregation -|`+verification/proofs/idris2/NeuralConsensus.idr+` |✅ +*Corollary:* iterates from any two starts approach each other by `+d+` per +step in ℓ¹. -|parser totality |`+verification/proofs/lean4/ParserTotality.lean+` |✅ +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. -|ABI package + verify package |`+src/Hypatia/ABI/*.idr+` -(incl. `+RuleEngine.idr+`), `+verify/src/*.idr+` |✅ +=== How hypatia meets the premises (engineering, not graded) -|*Neural convergence — PageRank* -|`+verification/proofs/lean4/PageRankInvariants.lean+` |⛔ preconditions -only +[cols="2,3,1",options="header"] +|=== +|Premise |Where |Status +|ESN `+ρ+` = 0.95, LSM `+ρ+` = 0.9 (largest absolute row sum after scaling) +|`+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+` -|*Neural convergence — ESN* -|`+verification/proofs/lean4/ESNSpectralScaling.lean+` |⛔ preconditions -only +|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) +|=== + +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. + +=== Files to write + +[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@ - - # install elan + Lean v4.30.0 (mirror the existing lake-build job) - - uses: actions/cache@ - 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..2e79c0c8 100644 --- a/docs/proofs/gap-analysis.adoc +++ b/docs/proofs/gap-analysis.adoc @@ -264,14 +264,15 @@ parser-adjacent proofs. *✅ Landed 2026-04-22 via 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.* +`+PageRankInvariants.lean+`. The convergence theorem (T-PR) 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 +291,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..dd2567d5 100644 --- a/docs/proofs/needs.adoc +++ b/docs/proofs/needs.adoc @@ -11,9 +11,12 @@ (`+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 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. @@ -64,33 +67,37 @@ 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. +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, normalisation preconditions +|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. +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..1333f7d9 100644 --- a/docs/testing/audit.adoc +++ b/docs/testing/audit.adoc @@ -303,8 +303,8 @@ 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. +* *Full PageRank convergence proof (T-PR).* Tracked in +`+docs/proofs/HANDOVER-neural-convergence.adoc+`. === 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..4cb9d5e5 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,21 @@ 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+`. 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 +90,26 @@ 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 +type safety |PROVEN |`+src/Hypatia/ABI/GRPC.idr+` |Idris2 |gRPC service type definitions -|COMPLETE +|PROVEN |`+src/Hypatia/ABI/REST.idr+` |Idris2 |REST endpoint type definitions -|COMPLETE +|PROVEN |`+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 +(ValidTransition GADT), terminal/active classification |PROVEN |=== ==== New Proofs (2026-04-04) @@ -93,17 +119,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 +139,49 @@ 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 +restoration, Routing blockage |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 +malformed-input rejection |PROVEN |`+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 +<> |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 <> |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 +199,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 +220,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 +326,93 @@ 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+`, 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 approach each other by + the factor `+(1 − a) + a·ρ+` per step. +* *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. 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 `+verification/proofs/agda/ReservoirContraction.agda+`) +|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 `+verification/proofs/agda/PageRankContraction.agda+`) +|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 `+@reservoir_norm+` (ESN 0.95, LSM 0.9), i.e. T-RC's +`+ρ+`: `+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: +`+OPEN+`. + === Properties Proven ==== 1. Confidence Bounds (`+ConfidenceBounds.idr+`) @@ -378,8 +497,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. @@ -459,8 +578,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+` (<>) |=== === 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 From f2838274021c4de67f17c56347d5a23959e41a0e Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:09:14 +0000 Subject: [PATCH 2/8] fix(docs): keep PROOF-STATUS currency-check clean scripts/check-proof-status.sh treats every backticked span in a table row or a file section as a file path or as an identifier that file must contain. The previous commit named the two planned Agda modules as paths (they do not exist yet) and backticked status tokens (PROVEN) in the LogtalkMigration row and the P8 section. Name the planned modules in plain text and write the status tokens unquoted there. bash scripts/check-proof-status.sh: 41 files, 77 identifiers, 0 mismatches, the same coverage as on main. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --- verification/PROOF-STATUS.adoc | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 4cb9d5e5..5df865a1 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -220,12 +220,12 @@ entries; the two ledgered non-equalities stated exactly former severity catch-all members explicit (`+catchAllSastLow+`, `+catchAllCiTestsLow+`, `+catchAllUnmaintainedLow+`). Source SHA-256 (at authoring): bbd18e2747c84e2eda7ff5a778a2df7f8960a1ef47b1c253f316b9d97b9902a0. -|Status `+PROVEN+`; correspondence `+AGDA-VERIFIED+`; `+PWG-3+`, no +|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. -Rocq and Lean legs `+OPEN+` (none written), so no `+PWG-2i+`/`+PWG-2ii+`/`+PWG-1+`, +Rocq and Lean legs OPEN (none written), so no PWG-2i/PWG-2ii/PWG-1, reconciliation or runtime-refinement claim. |=== @@ -361,13 +361,15 @@ as hypotheses): [width="100%",cols="28%,14%,42%,16%",options="header",] |=== |Artefact |Language |Claim |Status -|T-RC Agda source (planned `+verification/proofs/agda/ReservoirContraction.agda+`) +|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 `+verification/proofs/agda/PageRankContraction.agda+`) +|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 @@ -497,8 +499,8 @@ rejected ==== 8. Logtalk Migration Correspondence (`+LogtalkMigration.agda+`) -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 +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. From 5522f7bc9b12ea10d8bcb3848402c7a1903ef41e Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:59:11 +0000 Subject: [PATCH 3/8] docs(proofs): state contraction premises strictly; no status for bare declarations Address the Codex review of #1025: - T-RC: the bound holds for 0 <= a <= 1 and rho >= 0, but it is a contraction, and forgetting, only when q = (1 - a) + a*rho < 1, i.e. 0 < a and rho < 1. Hypatia's values are recorded: q = 0.99 (ESN) and 0.97 (LSM). - T-PR: a contraction only when d < 1; with d = 1 the result is non-expansiveness. Hypatia uses d = 0.85. - Reservoir scaling: the largest absolute row sum is at most @reservoir_norm, not always equal to it. Sparsity leaves size-1 reservoirs all zero for most seeds (ESN seeds 1-4, LSM seeds 1-5, checked). Equality is what the tests check for non-degenerate sizes. - GRPC.idr and REST.idr hold declarations and state no proposition, so they no longer read PROVEN; the vocabulary note and the coverage row say so. bash scripts/check-proof-status.sh: 41 files, 77 identifiers, 0 mismatches. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --- docs/proofs/HANDOVER-neural-convergence.adoc | 18 +++++++--- verification/PROOF-STATUS.adoc | 35 ++++++++++++++------ 2 files changed, 38 insertions(+), 15 deletions(-) diff --git a/docs/proofs/HANDOVER-neural-convergence.adoc b/docs/proofs/HANDOVER-neural-convergence.adoc index bc81069b..b7054022 100644 --- a/docs/proofs/HANDOVER-neural-convergence.adoc +++ b/docs/proofs/HANDOVER-neural-convergence.adoc @@ -37,7 +37,7 @@ enter only through hypotheses. Use the *bound* form of the sup norm ==== T-RC — reservoir contraction (ESN and LSM) -Setting: `+0 ≤ a ≤ 1+`; an `+n × n+` matrix `+W+` with +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 @@ -49,7 +49,12 @@ 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. +`+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 @@ -66,7 +71,10 @@ 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 ℓ¹. +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 @@ -79,7 +87,9 @@ ordered ring does not provide; they are out of scope. [cols="2,3,1",options="header"] |=== |Premise |Where |Status -|ESN `+ρ+` = 0.95, LSM `+ρ+` = 0.9 (largest absolute row sum after scaling) +|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+` diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 5df865a1..c5173121 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -63,7 +63,9 @@ 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+`. The two +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. @@ -100,10 +102,13 @@ caps, end-to-end composition |PROVEN type safety |PROVEN |`+src/Hypatia/ABI/GRPC.idr+` |Idris2 |gRPC service type definitions -|PROVEN +|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 -|PROVEN +|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 |PROVEN @@ -341,20 +346,24 @@ 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+`, an `+n × n+` matrix +* *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 approach each other by - the factor `+(1 − a) + a·ρ+` per step. + 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. Existence of a + 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. @@ -377,8 +386,11 @@ verification/proofs/agda/; not yet written) |Reservoir scaling, `+lib/neural/echo_state_network.ex+`, `+lib/neural/liquid_state_machine.ex+` |Elixir |After scaling, the largest -absolute row sum is `+@reservoir_norm+` (ESN 0.95, LSM 0.9), i.e. T-RC's -`+ρ+`: `+test/neural_test.exs+` "reservoir's largest absolute row sum +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+` @@ -558,8 +570,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 From 170439cbbe07271174d842cc9c5775637467e7a0 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:06:13 +0000 Subject: [PATCH 4/8] docs(proofs): call T-PR a contraction, finish the PWG relabel, scope the affirmation Address the second Codex review of #1025: - blitz.a2ml, audit.adoc and gap-analysis.adoc called T-PR a "full PageRank convergence proof". T-PR proves only that two runs approach each other. Convergence to a fixed point needs completeness and is a separate, unplanned theorem; they now say so. - The coverage map still read "Grade 3 / AGDA-VERIFIED" for LogtalkMigration; it now reads PWG-3. - AFFIRMATION now speaks of one open *theorem* obligation, and names the open PROOF-POLICY section 6 toolchain deviation records separately. bash scripts/check-proof-status.sh: document agrees with the tree. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --- .machine_readable/testing/blitz.a2ml | 2 +- AFFIRMATION.adoc | 9 ++++++--- docs/proofs/gap-analysis.adoc | 3 ++- docs/testing/audit.adoc | 6 ++++-- verification/PROOF-STATUS.adoc | 4 ++-- 5 files changed, 15 insertions(+), 9 deletions(-) diff --git a/.machine_readable/testing/blitz.a2ml b/.machine_readable/testing/blitz.a2ml index adec8ef7..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 (T-PR, docs/proofs/HANDOVER-neural-convergence.adoc — Agda, rechecked in Rocq and Lean)", + "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 50bf8216..9626d430 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -33,11 +33,14 @@ 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 and LSM) — two theory theorems, to be + made literally false; see #831.) 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`. + `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/gap-analysis.adoc b/docs/proofs/gap-analysis.adoc index 2e79c0c8..1afdcc07 100644 --- a/docs/proofs/gap-analysis.adoc +++ b/docs/proofs/gap-analysis.adoc @@ -264,7 +264,8 @@ parser-adjacent proofs. *✅ Landed 2026-04-22 via 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+`. The convergence theorem (T-PR) is theory: Agda, +`+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+`.* diff --git a/docs/testing/audit.adoc b/docs/testing/audit.adoc index 1333f7d9..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 (T-PR).* Tracked in -`+docs/proofs/HANDOVER-neural-convergence.adoc+`. +* *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/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index c5173121..3b2efd88 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -582,8 +582,8 @@ the proved properties 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) From 470175a70c6d668fc8e931a9fc99334bc6be3b35 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:06:42 +0000 Subject: [PATCH 5/8] docs(proofs): record the KinGate TLC run as TESTED in needs.adoc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit needs.adoc listed KinGate.tla under "Completed Proofs" as H8 ✅ and said H1-H9 are complete, which contradicts the ledger: a bounded TLC model check is TESTED, not PROVEN (PROOF-POLICY section 4). The section now names tested models, H8 records its bounds, and the priority line separates proved, runtime-asserted and tested obligations. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --- docs/proofs/needs.adoc | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/docs/proofs/needs.adoc b/docs/proofs/needs.adoc index dd2567d5..1d6c84bc 100644 --- a/docs/proofs/needs.adoc +++ b/docs/proofs/needs.adoc @@ -22,7 +22,10 @@ only `+OutcomeLog.agda+` (see `+verification/PROOF-STATUS.adoc+`, 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 H8, which is a bounded TLC +model check: `+TESTED+`, not `+PROVEN+` (PROOF-POLICY §4). [width="100%",cols="24%,30%,46%",options="header",] |=== @@ -50,7 +53,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 ✅ @@ -99,5 +103,6 @@ as `+TESTED+`). === Priority -*MEDIUM* — H1–H9 are complete (H6 as a runtime assertion). The remaining +*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. From 5430d1c2d99def8424abbaef9c84ef3e39ae7708 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:12:54 +0000 Subject: [PATCH 6/8] docs(proofs): record the KinGate section 4 exception; narrow two overclaims Address the third Codex review of #1025: - KinGate.tla now carries the PROOF-POLICY section 4 exception record beside the artefact (obligation H8, tool TLA+/TLC, why not Idris2, and status TESTED with the KinGate.cfg bounds), so "recorded section 4 exception" in needs.adoc is true. Comment lines only; the spec is unchanged. - needs.adoc: H6 is a runtime assertion with an echidnabot audit, not a kernel-checked proof, and is now named as an exception next to H8. - needs.adoc and gap-analysis.adoc no longer credit PageRankInvariants.lean with normalisation or column-stochastic premises. It proves non-negativity of edge weights and weight sums over N only. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --- docs/proofs/gap-analysis.adoc | 3 ++- docs/proofs/needs.adoc | 8 +++++--- verification/proofs/tlaplus/KinGate.tla | 13 +++++++++++++ 3 files changed, 20 insertions(+), 4 deletions(-) diff --git a/docs/proofs/gap-analysis.adoc b/docs/proofs/gap-analysis.adoc index 1afdcc07..a2f102bb 100644 --- a/docs/proofs/gap-analysis.adoc +++ b/docs/proofs/gap-analysis.adoc @@ -263,7 +263,8 @@ 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 +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, diff --git a/docs/proofs/needs.adoc b/docs/proofs/needs.adoc index 1d6c84bc..3a8e42f2 100644 --- a/docs/proofs/needs.adoc +++ b/docs/proofs/needs.adoc @@ -24,8 +24,9 @@ file. === Completed Proofs and Tested Models -Each row is a kernel-checked proof except H8, which is a bounded TLC -model check: `+TESTED+`, not `+PROVEN+` (PROOF-POLICY §4). +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",] |=== @@ -81,7 +82,8 @@ route and the definition of done, in |=== |Component |Proven today |Target theorem |Prover |PageRank (`+lib/neural/graph_of_trust.ex+`; preconditions in -`+PageRankInvariants.lean+`) |non-negativity, normalisation preconditions +`+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) 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 From e8ddae13fdda96a4f70cb223745f845c0ab67dbb Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:19:38 +0000 Subject: [PATCH 7/8] docs(proofs): narrow three PROVEN rows to what is proved; date the amendment Address the fourth Codex review of #1025: - Quarantine.idr: the model has no transition into Permanent (updateState only moves Ok to Soft or Hard and leaves quarantined states unchanged), so the row no longer claims ok/soft/hard/permanent transitions. - ParserTotality.lean: round-trip is checked only on fixed example token lists, not as a general theorem. The PROOF-STATUS and needs.adoc rows say so. - TLC is not pinned: verify-proofs fetches releases/latest and caches it under a fixed key, so "tla2tools 2.19" names only the recorded April run. needs.adoc and the section 6 deviation note say so. - AFFIRMATION: the edited item is marked as a dated 2026-11-09 amendment, so the June affirmed-at timestamp is not read as covering it. bash scripts/check-proof-status.sh: document agrees with the tree. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --- AFFIRMATION.adoc | 4 +++- docs/proofs/needs.adoc | 5 +++-- verification/PROOF-STATUS.adoc | 17 ++++++++++++----- 3 files changed, 18 insertions(+), 8 deletions(-) diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 9626d430..ddc19a1e 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -33,7 +33,9 @@ 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 theorem obligation remains open — + 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 diff --git a/docs/proofs/needs.adoc b/docs/proofs/needs.adoc index 3a8e42f2..d1eec00c 100644 --- a/docs/proofs/needs.adoc +++ b/docs/proofs/needs.adoc @@ -14,7 +14,8 @@ * *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 2.19. The 2026-04-22 retirement of Agda covered +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+` / @@ -67,7 +68,7 @@ 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 diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index 3b2efd88..e5040731 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -147,8 +147,10 @@ now `+FindingFact+`, and the corresponding module is |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 |PROVEN +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 @@ -164,8 +166,9 @@ posterior in (0,1), monotone in successes/failures, zero-observation identity, floor/cap clamp |PROVEN |`+verification/proofs/lean4/ParserTotality.lean+` |Lean 4 |VCL -`+FROM+`-clause parser totality, determinism, round-trip, -malformed-input rejection |PROVEN +`+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). The @@ -424,7 +427,11 @@ 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: +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 From 730833c348b83f5f6e661db9d8a87ed88414d390 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:20:38 +0000 Subject: [PATCH 8/8] docs(proofs): narrow the GraphQL and PipelineState rows to what is proved A self-audit of every PROVEN row against its file, after four Codex rounds kept finding overclaims in rows this PR relabelled. Every other row's listed properties have a matching theorem or definition-level guarantee. Two did not: - GraphQL.idr proves queryReturnsApiResponse and mutationReturnsApiResponse; subscriptions are declared with no proof. - PipelineState.idr makes illegal transitions unconstructible through the ValidTransition GADT (by construction); the terminal/active classification is only defined. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ --- verification/PROOF-STATUS.adoc | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/verification/PROOF-STATUS.adoc b/verification/PROOF-STATUS.adoc index e5040731..a7b8b634 100644 --- a/verification/PROOF-STATUS.adoc +++ b/verification/PROOF-STATUS.adoc @@ -98,8 +98,10 @@ and the wire-contract pin `+connectorCount : length allConnectors = 16+` route totality, dispatch correctness, Bayesian monotonicity, annealing caps, end-to-end composition |PROVEN -|`+src/Hypatia/ABI/GraphQL.idr+` |Idris2 |Query/Mutation/Subscription -type safety |PROVEN +|`+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 |Not a proof: the module type-checks in the ABI package build, but it @@ -113,8 +115,10 @@ applies |`+src/Hypatia/ABI/FFI.idr+` |Idris2 |GADT constructors, `+ffiReturnsApiResponse+` proof |PROVEN -|`+verify/src/PipelineState.idr+` |Idris2 |Pipeline state machine -(ValidTransition GADT), terminal/active classification |PROVEN +|`+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)