S3.5 Fable re-audit: permanent non-vacuity witness + honest ledger

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>

README.md

@@ -12,7 +12,7 @@ the same discipline as the four `*-ed25519-verified` subject corpora.
 | L1 | bytes, hleaf/hnode, domain separation (Lemma 1) | **done** (domsep: axiom-free) |
 | L2 | MTH, Root, ConsRec definitions + termination | **done** (cones: propext, LTLAcc.sha256, Quot.sound) |
 | L3 | inclusion completeness (Theorem 1) | **done** (incl_complete: propext, Classical.choice, LTLAcc.sha256, Quot.sound) |
-| L4 | root binding for inclusion (Lemma 2, Path instance) | **done** (root_binding; boundary = single sha256 axiom) |
+| 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 collision extractor extractIncl+correctness (Theorem 2) **done, non-vacuous**; consistency (Theorem 3) pending |
 | L6 | pin-store state machine safety (Proposition 1) | pending |
 

verification/Proofs/AxiomCheck.lean

@@ -16,3 +16,4 @@ import Proofs.Extract
 #print axioms LTLAcc.IsCollision
 #print axioms LTLAcc.extractIncl
 #print axioms LTLAcc.extractIncl_correct
+#print axioms LTLAcc.extractIncl_nonvacuous

verification/Proofs/Extract.lean

@@ -194,4 +194,18 @@ theorem extractIncl_correct (m : Nat) (D : List Bytes) :
                   exact hpair ⟨Subtype.ext hs, Subtype.ext hx⟩
                 · exact hh
 
+/-- **Permanent non-vacuity witness** (re-audit F1): on a NON-forgery
+    input (the offered leaf IS the honest leaf), the extractor's output
+    is provably NOT a collision. Hence `extractIncl_correct`'s conclusion
+    is false for some inputs — it cannot be discharged by pigeonhole or
+    choice, and only the forgery hypotheses make it hold. This theorem
+    guards the corpus against any future drift back into vacuity. -/
+theorem extractIncl_nonvacuous :
+    ¬ IsCollision (extractIncl 0 [([7] : List UInt8)] [7] []).1
+                  (extractIncl 0 [([7] : List UInt8)] [7] []).2 := by
+  rw [extractIncl]
+  simp only [List.length_singleton, if_pos (by omega : (1:Nat) ≤ 1)]
+  intro hcol
+  exact hcol.1 rfl
+
 end LTLAcc

verification/check.sh

@@ -36,6 +36,7 @@ declare -A CONES=(
   [LTLAcc.IsCollision]="LTLAcc.sha256"
   [LTLAcc.extractIncl]="propext, LTLAcc.sha256, Quot.sound"
   [LTLAcc.extractIncl_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.extractIncl_nonvacuous]="propext, LTLAcc.sha256, Quot.sound"
 )
 
 free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'