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 <noreply@anthropic.com>
The 'descend' step of the paper's Theorem 3, built extractor-first per
the S3.5 lesson (never a bare '∨ collision'):
- extractMTH (D D'): total function that, given two equal-length leaf
lists sharing a Merkle root, walks the common-shape tree to the first
divergence and returns the concrete colliding preimage pair (a node
pair, or a leaf pair at the bottom).
- extractMTH_correct: |D|=|D'| ∧ D≠D' ∧ MTH D = MTH D' →
IsCollision (extractMTH D D'). Proven by functional induction on
extractMTH; composite case uses MTH_split + append_inj (fixed-width
Hash) to split node preimages or exhibit the node collision.
- extractMTH_nonvacuous: equal lists → output NOT a collision (pinned),
so the conclusion is false for some inputs ⇒ choice-proof.
This also RESTORES, in explicit non-vacuous form, the receipt-uniqueness
content of Lemma 2 deleted in the S3.5 cleanup (re-audit F2): the honest
Merkle fold is injective up to a collision.
18 certs green. Fable statement-audit passed (matches paper Thm 3 step 3
verbatim). LTL untouched (12 leaves, bcd15f9d).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adversarial re-derivation of S3.5 (drill after harness switch). Core
verdict CONFIRMED: extractIncl_correct is faithful and non-vacuous.
Three methodical flaws found and resolved:
- F1: the non-vacuity proof existed only as a deleted probe — evidence
discarded. Now permanent: extractIncl_nonvacuous proves the
extractor's output on a NON-forgery input is NOT a collision, so the
correctness conclusion is false for some inputs and cannot be
discharged by pigeonhole/choice. Guards against future drift back
into vacuity. Cone pinned.
- F2 (queued for S4): deleting root_binding discarded the receipt-
uniqueness content of Lemma 2 (left disjunct: P = Path m D) along
with its vacuous disjunct. To be restored in extractor form during
S4; the S4 consistency walk inlines the same argument regardless.
- F3: README still claimed 'root_binding done' — a deleted theorem
advertised as delivered. Ledger corrected.
15 certs green. LTL untouched.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The S3 Socratic re-audit found incl_sound was kernel-perfect but VACUOUS:
its '... ∨ HasCollision' disjunct (∃ x y, x≠y ∧ sha256 x = sha256 y) is
provable by pigeonhole ALONE (sha256: infinite List UInt8 → finite
32-byte Hash), so the theorem said nothing about forgeries. Even a
data-carrying {p // IsCollision p} disjunct fails (Classical.choice
inhabits it). The only faithful rendering of the paper's 'explicit
algorithm 𝓔' is a NAMED FUNCTION whose correctness is a claim about ITS
OUTPUT.
- extractIncl (m D d P): total function that walks the honest tree and
returns the concrete colliding preimage pair at the first divergence
(a node preimage pair, or the leaf preimage pair at the bottom).
- extractIncl_correct: d ≠ D[m] ∧ accepting-receipt →
IsCollision (extractIncl …).1 (extractIncl …).2. A statement ABOUT the
fixed function's output; pigeonhole cannot discharge it.
ADVERSARIAL CHECK (probe, since removed): proved
¬ IsCollision (extractIncl 0 [[7]] [7] []) — i.e. on a NON-forgery input
the output is provably NOT a collision, so the conclusion is genuinely
false for some inputs ⇒ non-vacuous, choice-proof.
- Removed the vacuous theorems entirely (incl_sound, root_binding,
hnode/hleaf_inj_or_collision, HasCollision def) so no hollow statement
survives in a corpus destined for the log. Kept the real building
blocks (hnode_preimage_inj [propext]; eq_dropLast helper moved to
Completeness; Binding.lean deleted).
extractIncl_correct cone [propext, Classical.choice, LTLAcc.sha256,
Quot.sound]. THE button green (14 certs). Fable statement-audit passed.
LTL untouched (12 leaves, bcd15f9d).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The crux layer — the statement whose HAND proof once carried the frontier
coverage bug is now kernel-checked.
- gen: hash outputs refactored to Hash = {l : List UInt8 // l.length = 32}.
MECHANIZATION FINDING: the paper's pair-coincidence step ('equal hnode
values of distinct argument pairs are a collision') is load-bearing on
FIXED-WIDTH outputs — with unconstrained byte strings x++s = X++Y does
not split. hnode_preimage_inj (cone: propext) makes this explicit via
List.append_inj on equal-length components. Queued as a half-sentence
for the paper's next cycle.
- HasCollision := ∃ x y, x ≠ y ∧ sha256 x = sha256 y — appears ONLY as a
conclusion, never a hypothesis (no collision-resistance assumed).
- hnode_inj_or_collision / hleaf_inj_or_collision: the per-node dichotomy.
- root_binding: any accepting reconstruction from (v,P) to the honest root
either IS the honest receipt (leaf hash AND full path P = Path m D — case
(ii) pinning every consumed sibling) or exhibits a collision. Motive
quantifies (v,P); induction on Path; k-fold discipline.
- incl_sound (Theorem 2, position binding): accepting a wrong leaf at m
yields a collision. Cone [propext, Classical.choice, LTLAcc.sha256,
Quot.sound] — the single hash axiom, pinned in check.sh. ALL GREEN.
Also: Root n=1 branch changed from list-match to decidable 'if P = []'
(well-founded unfolding generated a spurious exhaustiveness obligation);
Root_one_cons added. Fable-5 statement-audit passed. LTL untouched.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adversarial statement-level re-verification of everything S2 shipped,
against paper SS5.3 and the deployed Python verifier: Path recursion,
Root_left/Root_right fold shapes (none exactly where the deployed code
rejects), incl_complete as Theorem 1 verbatim (getD default unreachable
under m < |D|), MTH([]) = H(epsilon) per RFC. All faithful.
One genuine gap found and closed: the kbelow lemmas bounded k but never
established k is a power of two, leaving 'our split point = the RFC
split point' as by-construction folklore. kbelow_pow2 (cone: propext,
Quot.sound) now pins it: 2^j = k < n <= 2k = 2^(j+1) uniquely
determines the RFC 9162 split. THE button green. LTL untouched.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Path (prover-side inclusion path, paper SS5.3) with termination via the
kbelow bounds; self-contained list lemmas (getD_take, getD_drop - no
stdlib-name dependence); equation lemmas MTH_single/MTH_split/Root_one/
Root_left/Root_right (Option.map form; matcher side conditions closed
explicitly); Theorem 1 by functional induction on Path with a k-fold
discipline against the let-bound split point.
incl_complete cone: [propext, Classical.choice, LTLAcc.sha256,
Quot.sound] - pinned exactly in check.sh alongside Path.
THE button green end to end. LTL untouched.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Accumulator pyramid layers 1-2, mechanizing paper SS5.3/SS6 groundwork:
- gen/LTLAcc/HashExternal.lean: the single sanctioned axiom, opaque
sha256 (no properties assumed - the soundness theorems downstream are
constructive collision extractors).
- Proofs/Basic.lean: hleaf/hnode (0x00/0x01 domain stamps); Lemma 1
(domsep) proven AXIOM-FREE; kbelow (largest power of two below n)
with pos/lt/le-two bound lemmas; MTH, Root (Option = rejection),
ConsRec (four cases, b-flag, pinned anchor) - all with kernel-checked
termination via the kbelow bounds.
- check.sh: estate discipline (stub audit, axiom-smuggling gate,
lean-guard compilation, boundary-exact per-certificate cone audit).
All green; observed cones pinned exactly.
Zero contact with the live LTL: no appends, no server, accumulator
frozen at 12 leaves throughout this project.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
