From 8cdea8ff7e8e2bc532a980fb34770833511cc52a Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 18:24:23 +0200 Subject: [PATCH] S5 stage-2 Fable re-audit: flag load-bearing invariant, correct 'verified' overclaim MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Re-derived the planned stage-3 binding against the extractConsNode definition. Definition is SOUND (candidate/ConsRec hnode alignment re-confirmed: n₀≤k hnode y s ↔ 0x01::y'++s; n₀>k hnode s y ↔ 0x01::s++y'). FINDING (protects stage 3): extractConsNode's candidate is a genuine collision ONLY under y_current = MTH(D₁_current) — sha256(LHS) = hnode y' s = y_current, sha256(RHS) = MTH D₁_current, equal iff the value-equality invariant holds. The stage-3 binding statement MUST thread through the recursion (Lemma 2's top-down equality). Planned statement already carries it; note now flags it as load-bearing so it can't be dropped. LEDGER: cfde9b2 claimed the extractor 'verified faithful' — that overclaimed kernel-verification; it is inspection-only until consRecBinding is proven. README corrected to say so. No Lean change (definition sound). 22 certs green. LTL untouched. Co-Authored-By: Claude Fable 5 --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 7c9a182..8772c51 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,7 @@ the same discipline as the four `*-ed25519-verified` subject corpora. | L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 2) **done, non-vacuous** | | L6a | descent extractor `extractMTH` (Theorem 3 step 3 = Lemma 2, WHOLE-TREE instance) **done, non-vacuous** | | — | Lemma 2, PATH instance (receipt-uniqueness of `Root`): deleted with the vacuous `root_binding` in S3.5 and **not yet restored**; optional, not needed for Theorem 3 | -| L6b | ConsRec binding + Theorem 3 assembly (extractCons) | in progress (S5): stage-1 arithmetic/list infrastructure done (kbelow_prefix_eq, take surgery); stage-1 infra + extractConsNode extractor DEFINED; binding proof (steps 1-2) + extractCons assembly = stage 3 | +| L6b | ConsRec binding + Theorem 3 assembly (extractCons) | in progress (S5): stage-1 arithmetic/list infrastructure done (kbelow_prefix_eq, take surgery); stage-1 infra + extractConsNode extractor DEFINED (faithful to ConsRec by inspection — NOT yet machine-checked); binding proof + extractCons assembly = stage 3 | | L6 | pin-store state machine safety (Proposition 1) | pending | ## Discipline (identical to the subject corpora)