diff --git a/README.md b/README.md
index d49c0f5..366d7f0 100644
--- a/README.md
+++ b/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 |
 
diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean
index d918dc2..fcb364e 100644
--- a/verification/Proofs/AxiomCheck.lean
+++ b/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
diff --git a/verification/Proofs/Extract.lean b/verification/Proofs/Extract.lean
index a9e017d..abbf289 100644
--- a/verification/Proofs/Extract.lean
+++ b/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
diff --git a/verification/Proofs/Extract.olean b/verification/Proofs/Extract.olean
index 92e2711..7ffd33c 100644
Binary files a/verification/Proofs/Extract.olean and b/verification/Proofs/Extract.olean differ
diff --git a/verification/check.sh b/verification/check.sh
index f6b8540..30eda8d 100755
--- a/verification/check.sh
+++ b/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}}'