From 30cf6563ff2f0032c107d4fca9ab10fc8ee9348d Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 17:15:08 +0200 Subject: [PATCH] S4 Fable re-audit: correct a false ledger claim (F2 was NOT resolved) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adversarial re-derivation of S4. The mathematics HOLDS: extractMTH_correct is faithful to paper Theorem 3 step 3 (hypotheses, recursion, node/leaf collision cases all re-verified), sub-call length/difference obligations sound, non-vacuity witness valid. The defect was in the CLAIM: S4's commit/README stated extractMTH 'restores the receipt-uniqueness content of Lemma 2'. Wrong instance. Lemma 2 has three instantiations; the deleted root_binding was the PATH instance (uniqueness of accepting receipts (v,P) for Root, quantifying over adversarial paths); extractMTH is the WHOLE-TREE instance (MTH injective on equal-length leaf lists). Nothing in the corpus currently states path-uniqueness. Ledger corrected: whole-tree instance done; path instance honestly listed as deleted-and-not-restored (optional — not needed for Theorem 3 assembly). No Lean changes; 18 certs remain green. LTL untouched. Co-Authored-By: Claude Fable 5 --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 84e2363..7a32906 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,8 @@ the same discipline as the four `*-ed25519-verified` subject corpora. | L3 | inclusion completeness (Theorem 1) | **done** (incl_complete: propext, Classical.choice, LTLAcc.sha256, Quot.sound) | | L4 | frontier binding content (Lemma 2) | **inlined in the extractor walk** (extractIncl); standalone receipt-uniqueness theorem queued for S4 restoration in extractor form | | L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 2) **done, non-vacuous** | -| L6a | descent extractor `extractMTH` (Theorem 3 step 3; restored receipt-uniqueness of Lemma 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) | pending (S5) | | L6 | pin-store state machine safety (Proposition 1) | pending |