docs(proofs): record Stage 1.1; add optimisation ledger + build-with-proofs discipline; truth-fix TOPOLOGY#48
Merged
Conversation
…proofs discipline; truth-fix TOPOLOGY PROOFS.adoc: - Mark Stage 1.1 (buildGetLeaf) DONE; add buildGetLeaf + Util.VectLemmas to the proven surface; flip the powerTwoSucc transport WATCH-FOR -> RESOLVED. - Split remaining Stage 1 into 1.2 root-fold law / 1.3 IO<->pure bridge / 1.4 D2. - Surface the Repair-is-a-stub precondition + recommended pure-model decision (Stage 3). - Add three sections: the IO<->pure bridge (estate-wide spine), the build-with-proofs discipline, and the optimisation ledger (against the proven backdrop). - Reconcile module count: 19 core modules (+ separate src/abi tree). TOPOLOGY.md: - Regrade the dashboard onto the honest proof axis: Merkle 70%, Repair 20% (stub), ECHIDNA 10% (stubbed), crypto-not-yet-linked 20%. Replaces the inflated 80-100% bars that contradicted the ledger. - Point to docs/PROOFS.adoc as authoritative; clarify bars track proof completeness. https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
hyperpolymath
marked this pull request as ready for review
June 17, 2026 23:10
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Documentation-only update closing out the Stage 1.1 milestone and re-anchoring the repo's status claims to the proof ledger. No
.idrchanges — the proven surface is unchanged from205df0a(Stage 1.1, verified green onmain).docs/PROOFS.adoc(authoritative ledger)buildGetLeaf) DONE; addbuildGetLeaf+Ochrance.Util.VectLemmas(×5) to the proven surface.powerTwoSucctransport WATCH-FOR → RESOLVED (discharged via theindexReplace/finToNatReplace/splitAtConcattransport-cancellation lemmas — no builder reshape).CollisionResistant.src/abitree; was "24").TOPOLOGY.md(dashboard truth-fix)The dashboard claimed
Merkle 100%,A2ML 100%,Zig FFI 100%,ECHIDNA 60% refining, overall~80%— contradicting the ledger (crypto not yet linked; ECHIDNA entirely stubbed; Repair a stub). Regraded onto the honest proof axis: Merkle 70%, Repair 20% (stub), ECHIDNA 10% (stubbed), crypto-linked 20%, overall ~40%; points toPROOFS.adocas authoritative.Why
Keeps the repo's outward claims from outstripping the proofs, and records — for the next working window — exactly which code is safe to optimise (anything under a proof) and which must be proven first.
🤖 Generated with Claude Code
https://claude.ai/code/session_011z2t8zAxfcCNLJzU7YdpBQ
Generated by Claude Code