Repository navigation
docs(proofs): align the neural-convergence plan and proof ledger with PROOF-POLICY - #1025
hyperpolymath wants to merge 8 commits into
Conversation
… 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 54 minutes. View limit details
Finishing Touches
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. |
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f283827402
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
… 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5522f7bc9b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 470175a70c
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| 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 |
There was a problem hiding this comment.
The model explicitly transcribes ECHIDNA and Hypatia implementation tables, so it is an engineering property under PROOF-POLICY §§1, 3, and 8.1, not implementation-independent theory. PWG applies only to theory, while an existing engineering proof in another prover retains its checked status until it is next moved to Idris2. Recording PWG-3 and opening Rocq/Lean recheck legs therefore misgrades this artifact; retain its PROVEN evidence without a PWG or theory recheck obligations.
Useful? React with 👍 / 👎.
…claims 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5430d1c2d9
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…endment 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
…oved 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 730833c348
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| 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 |
There was a problem hiding this comment.
When 0 < a ≤ 1 and ρ > 1, the stated modulus is q = 1 + a(ρ − 1) > 1, so this bound permits expansion rather than non-expansiveness. The same incorrect characterization is repeated in verification/PROOF-STATUS.adoc; distinguish the a = 0 or ρ = 1 non-expansive boundary from the ρ > 1 expansive case so the formalization plan does not request a false corollary.
Useful? React with 👍 / 👎.
| 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+`). |
There was a problem hiding this comment.
The new November status conflicts with this document's still-current TL;DR and inventory: lines 8–12 say Agda is retired and only TLA+ is CI-gated, while lines 34–84 list the Lean and Idris proofs as ungated. The inspected .github/workflows/verify-proofs.yml now gates Idris2, Lean, TLA+, and Agda, so readers encounter opposite descriptions of the proof estate in one analysis; update or explicitly supersede the stale opening inventory rather than changing only the final status.
Useful? React with 👍 / 👎.
| |`+verification/proofs/idris2/BatchRollback.idr+` |Idris2 | ||
| |Transactionality (all-or-nothing), Reversibility (snapshot | ||
| restoration), Fault tolerance (failure handling) |COMPLETE | ||
| restoration), Fault tolerance (failure handling) |PROVEN |
There was a problem hiding this comment.
When executeWithFailure is used, it always returns Failed with a partially modified snapshot and never invokes rollback; batchIsTransactional proves only that calling the separately defined rollback function would return the supplied original snapshot. Kernel-checking that theorem therefore does not prove all-or-nothing execution or that failure triggers rollback, so narrow the PROVEN claim to rollback restoration/reversibility or add a theorem that connects a failed execution to an actual rollback.
Useful? React with 👍 / 👎.
| |`+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 |
There was a problem hiding this comment.
For an event sequence containing different timestamps, the checked file has no inductive theorem establishing the advertised bound: processEvents_preserves_invariant explicitly requires every event to satisfy e.timestamp = t, and count_bounded_after_accepts carries the same simultaneous-event premise. The one-step theorem is also conditional on the invariant already holding at the current event's timestamp, so marking unrestricted sequence processing as PROVEN overstates the witness; qualify this row to simultaneous arrivals or add the missing chronological/arbitrary-sequence proof.
Useful? React with 👍 / 👎.
…ce (#1028) ## The bug `build_edges/1` emits one edge per verified success. When the same evidence is recorded twice, the PageRank iteration in `iterate_trust/4` sees parallel edges: - it **divided** a source's trust by the summed weight of *all* of its out-edges, duplicates included; - it **credited** each target with only the *first* matching edge (`Enum.find`). So column sums fell below 1 and trust leaked, and how much leaked depended on how many times the evidence had been logged. Tripling an unchanged outcome log moved a recipe's trust from 0.38 to 0.59 and a bot's from 0.89 to 0.94. I found this while checking the PageRank convergence theorem's premises for #1025. The leak does not break convergence, because the matrix stays column-substochastic, but it makes the scores depend on logging noise. ## The fix - **Rank over the set of edges** (`Enum.uniq` before the adjacency is built), as the Jaccard cross-repo edges already do. Trust then depends on what was observed, not on how often it was logged. `graph.edges` itself is unchanged. - **Credit every edge to a target**, so the columns of the transition matrix sum to 1 even if parallel edges reappear. **This changes production trust scores.** Wherever an outcome log holds repeated (recipe, repo, bot) successes, the scores will move. The alternative would let repeated successes count with their multiplicity. That would also need the Jaccard cross-repo edges reweighted by count; otherwise duplication still shifts mass between edge kinds. I chose set semantics because the cross-repo edges already work that way. Say if you want multiplicity instead. ## Validation - New test, `recording the same evidence k times leaves every trust score unchanged`: - fails on main (`bot-qualification-fixture: once=0.889 thrice=0.939`); - still fails with only the summing change (`0.980` vs `1.0`), because the Jaccard edges ignore multiplicity; - passes with this commit. - `mix test`: 2689 tests, 0 failures, 246 excluded. - `mix format --check-formatted` is clean. --- _Generated by [Claude Code](https://claude.ai/code/session_0165rGu3tsKmJtevmrdMVyfJ)_ Co-authored-by: Claude <noreply@anthropic.com>
Why
The PageRank and ESN convergence proofs were planned in Lean 4 with Mathlib:
HANDOVER-neural-convergence.adoc,needs.adoc,gap-analysis.adocandAFFIRMATION.adocall say so. The handover rewrite in #959 kept that plan. The estate PROOF-POLICY, owner rulings of 2026-10-26 and 2026-11-04, rules it out:agda --safe --without-K --cubical-compatible.PWG-3/2i/2ii/1). §8 replaces the grade ladder in the mathesis brief, whichPROOF-STATUS.adocwas still quoting.This PR fixes the plan and the ledger. It adds no proof, test or runtime behaviour.
What changes
docs/proofs/HANDOVER-neural-convergence.adocis rewritten. It states two theory theorems over an abstract ordered commutative ring. That needs no postulate and no real analysis; the activation and the matrix enter only as hypotheses.Wis at most ρ and the activation is 1-Lipschitz, the leaky update is a sup-norm contraction with modulus(1 − a) + a·ρ. This covers both the ESN and the LSM.c + d·P·xis an ℓ¹ contraction with modulusdwhenPis non-negative and column-substochastic. The old plan assumed a column-stochasticP, butgraph_of_trust.exleaves the column of a dangling node at zero.TESTEDorASSUMED.verification/PROOF-STATUS.adoc:COMPLETEandPARTIALare replaced with §5 tokens. Every formerCOMPLETErow names a file that aVerify Proofsjob kernel-checks and fails hard on.TESTED, as the policy's §4 worked example requires.PROVEN/AGDA-VERIFIED/PWG-3.neural-convergencesection lists T-RC and T-PR asOPENandungraded.OPEN.needs.adocno longer says Agda was retired. OnlyOutcomeLog.agdawas.PROOFS-GAP.mdreferences in Elixir comments and a test moduledoc are repointed.feedback_weightsis never used). The LSM's stale "integrate-and-fire" comment is corrected.Deliberately not in this PR
PageRankInvariants.lean,ESNSpectralScaling.lean) still describe the Mathlib plan in their header comments. They are engineering proofs, and PROOF-POLICY §3 moves them to Idris2 when they are next touched, so they are corrected in that move.verify-proofs.yml: its comments still say "Mathesis Grade 3". I left the workflow untouched.Validation
mix test test/neural_test.exs test/graph_of_trust_convergence_test.exs: 31 tests, 0 failures.mix format --check-formattedis clean on the touched Elixir files.lake buildis clean on main; no Lean file changes here.test/neural_test.exsandtest/graph_of_trust_convergence_test.exs.Generated by Claude Code