diff --git a/README.md b/README.md
index 97b0e1f..4ab5605 100644
--- a/README.md
+++ b/README.md
@@ -12,8 +12,8 @@ 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 | frontier hash-fold + root binding (Lemma 2) | pending |
-| L5 | inclusion/consistency soundness as collision extractors (Theorems 2, 3) | pending |
+| L4 | root binding for inclusion (Lemma 2, Path instance) | **done** (root_binding; boundary = single sha256 axiom) |
+| L5 | inclusion soundness = collision extractor (Theorem 2) **done**; consistency (Theorem 3) pending |
 | L6 | pin-store state machine safety (Proposition 1) | pending |
 
 ## Discipline (identical to the subject corpora)
diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean
index 3e0cd9f..4480d1c 100644
--- a/verification/Proofs/AxiomCheck.lean
+++ b/verification/Proofs/AxiomCheck.lean
@@ -1,6 +1,7 @@
 /- Axiom-cone observation for the audit (Phase 3 of check.sh). -/
 import Proofs.Basic
 import Proofs.Completeness
+import Proofs.Binding
 #print axioms LTLAcc.domsep
 #print axioms LTLAcc.kbelow_pos
 #print axioms LTLAcc.kbelow_lt
@@ -11,3 +12,8 @@ import Proofs.Completeness
 #print axioms LTLAcc.ConsRec
 #print axioms LTLAcc.Path
 #print axioms LTLAcc.incl_complete
+#print axioms LTLAcc.hnode_preimage_inj
+#print axioms LTLAcc.hnode_inj_or_collision
+#print axioms LTLAcc.hleaf_inj_or_collision
+#print axioms LTLAcc.root_binding
+#print axioms LTLAcc.incl_sound
diff --git a/verification/Proofs/AxiomCheck.olean b/verification/Proofs/AxiomCheck.olean
index ad5187d..cc18f98 100644
Binary files a/verification/Proofs/AxiomCheck.olean and b/verification/Proofs/AxiomCheck.olean differ
diff --git a/verification/Proofs/Basic.lean b/verification/Proofs/Basic.lean
index bce2c64..e63ab36 100644
--- a/verification/Proofs/Basic.lean
+++ b/verification/Proofs/Basic.lean
@@ -11,10 +11,22 @@ namespace LTLAcc
 abbrev Bytes := List UInt8
 
 /-- Leaf hash: `H(0x00 ‖ d)` (paper §5.3). -/
-noncomputable def hleaf (d : Bytes) : Bytes := sha256 (0x00 :: d)
+noncomputable def hleaf (d : Bytes) : Hash := sha256 (0x00 :: d)
 
-/-- Node hash: `H(0x01 ‖ x ‖ y)` (paper §5.3). -/
-noncomputable def hnode (x y : Bytes) : Bytes := sha256 (0x01 :: (x ++ y))
+/-- Node hash: `H(0x01 ‖ x ‖ y)` (paper §5.3). Arguments are 32-byte
+    hash values, so the preimage determines the argument pair — the
+    load-bearing width fact of the paper's Lemma 2. -/
+noncomputable def hnode (x y : Hash) : Hash := sha256 (0x01 :: (x.val ++ y.val))
+
+/-- Preimage-level pair injectivity: equal `hnode` PREIMAGES force equal
+    argument pairs, because both components are exactly 32 bytes. -/
+theorem hnode_preimage_inj {x y X Y : Hash}
+    (h : (0x01 : UInt8) :: (x.val ++ y.val) = 0x01 :: (X.val ++ Y.val)) :
+    x = X ∧ y = Y := by
+  injection h with _ happ
+  have hlen : x.val.length = X.val.length := by rw [x.property, X.property]
+  have := List.append_inj happ hlen
+  exact ⟨Subtype.ext this.1, Subtype.ext this.2⟩
 
 /-- **Lemma 1 (Domain separation), preimage form**: no leaf preimage
     equals a node preimage as a byte string — the first byte differs. -/
@@ -74,7 +86,7 @@ theorem kbelow_pow2 (n : Nat) : ∃ j, kbelow n = 2 ^ j := by
 /-- `MTH` (paper §5.3): the RFC 9162 tree head over a leaf-data list.
     `MTH [] = H(ε)`, `MTH [d] = hleaf d`, and for `n ≥ 2` the split at
     `k = kbelow n`. -/
-noncomputable def MTH (D : List Bytes) : Bytes :=
+noncomputable def MTH (D : List Bytes) : Hash :=
   if _h0 : D.length = 0 then sha256 []
   else if _h1 : D.length = 1 then hleaf (D.headD [])
   else
@@ -95,11 +107,9 @@ decreasing_by
 
 /-- `Root` (paper §5.3 / Appendix B): the consumer's root reconstruction.
     `none` = rejection on any length mismatch, exactly as deployed. -/
-noncomputable def Root (v : Bytes) (m n : Nat) (P : List Bytes) : Option Bytes :=
+noncomputable def Root (v : Hash) (m n : Nat) (P : List Hash) : Option Hash :=
   if n = 1 then
-    match P with
-    | [] => some v
-    | _ => none
+    (if P = [] then some v else none)
   else if n = 0 then none
   else
     match P.getLast? with
@@ -125,8 +135,8 @@ decreasing_by
     the reconstructed pair (old root, new root); `none` = shape
     mismatch. The flag `b` records whether the size-`n₀` subtree root is
     carried implicitly (the pinned root `r`) or explicitly in `C`. -/
-noncomputable def ConsRec (n₀ n : Nat) (C : List Bytes) (b : Bool) (r : Bytes) :
-    Option (Bytes × Bytes) :=
+noncomputable def ConsRec (n₀ n : Nat) (C : List Hash) (b : Bool) (r : Hash) :
+    Option (Hash × Hash) :=
   if n₀ = n then
     if b then
       match C with
@@ -159,7 +169,7 @@ decreasing_by
 
 /-- The consumer's acceptance predicate for a consistency proof between
     pinned head `(n₀, r₀)` and offered head `(n₁, r₁)` (paper §5.3). -/
-def acceptCons (n₀ n₁ : Nat) (r₀ r₁ : Bytes) (C : List Bytes) : Prop :=
+def acceptCons (n₀ n₁ : Nat) (r₀ r₁ : Hash) (C : List Hash) : Prop :=
   n₀ = 0 ∨ ConsRec n₀ n₁ C true r₀ = some (r₀, r₁)
 
 end LTLAcc
diff --git a/verification/Proofs/Basic.olean b/verification/Proofs/Basic.olean
index 7422fe1..0bd38bc 100644
Binary files a/verification/Proofs/Basic.olean and b/verification/Proofs/Basic.olean differ
diff --git a/verification/Proofs/Binding.lean b/verification/Proofs/Binding.lean
new file mode 100644
index 0000000..3e0308a
--- /dev/null
+++ b/verification/Proofs/Binding.lean
@@ -0,0 +1,185 @@
+/- L4 (first instance) of the accumulator pyramid: **root binding for the
+   inclusion fold** — the Path instance of the paper's Lemma 2 — and
+   **Theorem 2 (inclusion soundness)** as a constructive statement:
+   an accepting receipt for a wrong leaf EXHIBITS a SHA-256 collision.
+
+   No collision-resistance assumption appears anywhere: `HasCollision`
+   is the conclusion, never a hypothesis. -/
+import Proofs.Completeness
+
+namespace LTLAcc
+
+/-- Two distinct preimages with equal hash — the jackpot. Constructively
+    exhibited by the soundness theorems; believing it cannot be found is
+    the reader's interpretation of SHA-256, exactly as in the paper. -/
+def HasCollision : Prop :=
+  ∃ x y : List UInt8, x ≠ y ∧ sha256 x = sha256 y
+
+/-- Either two hash values have equal preimage pairs, or their equality
+    is itself a collision (the paper's case dichotomy at one node). -/
+theorem hnode_inj_or_collision {x y X Y : Hash}
+    (h : hnode x y = hnode X Y) :
+    (x = X ∧ y = Y) ∨ HasCollision := by
+  by_cases hpre :
+      (0x01 : UInt8) :: (x.val ++ y.val) = 0x01 :: (X.val ++ Y.val)
+  · exact Or.inl (hnode_preimage_inj hpre)
+  · exact Or.inr ⟨_, _, hpre, h⟩
+
+/-- Likewise at a leaf: equal leaf hashes with distinct data collide. -/
+theorem hleaf_inj_or_collision {d e : Bytes}
+    (h : hleaf d = hleaf e) : d = e ∨ HasCollision := by
+  by_cases hde : d = e
+  · exact Or.inl hde
+  · refine Or.inr ⟨0x00 :: d, 0x00 :: e, ?_, h⟩
+    intro hc; injection hc with _ ht; exact hde ht
+
+/-- A non-empty list is its `dropLast` plus its last element
+    (self-contained; no stdlib-name dependence). -/
+theorem eq_dropLast_append_of_getLast? (l : List Hash) (s : Hash)
+    (h : l.getLast? = some s) : l = l.dropLast ++ [s] := by
+  induction l with
+  | nil => simp at h
+  | cons a t ih =>
+      cases t with
+      | nil =>
+          simp at h
+          subst h
+          rfl
+      | cons b u =>
+          have hh : (b :: u).getLast? = some s := by
+            simpa using h
+          have := ih hh
+          calc a :: b :: u = a :: (b :: u) := rfl
+            _ = a :: ((b :: u).dropLast ++ [s]) := by rw [← this]
+            _ = (a :: b :: u).dropLast ++ [s] := by simp
+
+/-- **Root binding** (the Path instance of the paper's Lemma 2): if any
+    reconstruction from `(v, P)` hits the honest root, then either
+    `(v, P)` IS the honest receipt — leaf hash and every consumed
+    sibling — or a collision is exhibited. -/
+theorem root_binding (m : Nat) (D : List Bytes) :
+    ∀ (v : Hash) (P : List Hash), m < D.length →
+    Root v m D.length P = some (MTH D) →
+    (v = hleaf (D.getD m []) ∧ P = Path m D) ∨ HasCollision := by
+  induction m, D using Path.induct with
+  | case1 m D hle =>
+      intro v P hm h
+      have h1 : D.length = 1 := by omega
+      obtain ⟨d, rfl⟩ := exists_singleton_of_length_one D h1
+      have hm0 : m = 0 := by simpa using hm
+      subst hm0
+      have hlen : ([d] : List Bytes).length = 1 := rfl
+      rw [hlen] at h
+      cases P with
+      | nil =>
+          rw [Root_one, MTH_single] at h
+          simp only [Option.some.injEq] at h
+          left
+          refine ⟨?_, by rw [Path]; simp⟩
+          have hg : ([d] : List Bytes).getD 0 [] = d := rfl
+          rw [hg]; exact h
+      | cons p q =>
+          rw [Root_one_cons] at h
+          simp at h
+  | case2 m D hgt k hmk ih =>
+      intro v P hm h
+      have h2 : 2 ≤ D.length := by omega
+      have hkeq : k = kbelow D.length := rfl
+      have hkl : k < D.length := by rw [hkeq]; exact kbelow_lt D.length h2
+      have hmk' : m < kbelow D.length := by rw [← hkeq]; exact hmk
+      have htklen : (D.take k).length = k := by
+        simp [List.length_take]; omega
+      cases hP : P.getLast? with
+      | none =>
+          have hPnil : P = [] := by
+            cases P with
+            | nil => rfl
+            | cons a t => simp at hP
+          subst hPnil
+          rw [Root] at h
+          have hn1 : ¬ D.length = 1 := by omega
+          have hn0 : ¬ D.length = 0 := by omega
+          simp [hn1, hn0] at h
+      | some s =>
+          obtain hsplit := eq_dropLast_append_of_getLast? P s hP
+          rw [hsplit] at h
+          rw [Root_left _ _ _ _ _ h2 hmk', ← hkeq] at h
+          cases hR : Root v m k P.dropLast with
+          | none => rw [hR] at h; simp at h
+          | some x =>
+              rw [hR] at h
+              simp only [Option.map_some, Option.some.injEq] at h
+              rw [MTH_split D h2, ← hkeq] at h
+              rcases hnode_inj_or_collision h with ⟨hx, hs⟩ | hc
+              · have ihm : m < (D.take k).length := by omega
+                have hR' : Root v m (D.take k).length P.dropLast
+                    = some (MTH (D.take k)) := by rw [htklen, hR, hx]
+                rcases ih v P.dropLast ihm hR' with ⟨hv, hPd⟩ | hc
+                · left
+                  refine ⟨?_, ?_⟩
+                  · rw [hv]; exact congrArg hleaf (getD_take D k m hmk)
+                  · have hRHS : Path m D = Path m (D.take k) ++ [MTH (D.drop k)] := by
+                      rw [Path]; simp only [if_neg hgt, ← hkeq, if_pos hmk]
+                    rw [hRHS, hsplit, hPd, hs]
+                · exact Or.inr hc
+              · exact Or.inr hc
+  | case3 m D hgt k hmk ih =>
+      intro v P hm h
+      have h2 : 2 ≤ D.length := by omega
+      have hkeq : k = kbelow D.length := rfl
+      have hkl : k < D.length := by rw [hkeq]; exact kbelow_lt D.length h2
+      have hkp : 0 < k := by rw [hkeq]; exact kbelow_pos D.length
+      have hmk' : ¬ m < kbelow D.length := by rw [← hkeq]; exact hmk
+      have hdplen : (D.drop k).length = D.length - k := by
+        simp [List.length_drop]
+      cases hP : P.getLast? with
+      | none =>
+          have hPnil : P = [] := by
+            cases P with
+            | nil => rfl
+            | cons a t => simp at hP
+          subst hPnil
+          rw [Root] at h
+          have hn1 : ¬ D.length = 1 := by omega
+          have hn0 : ¬ D.length = 0 := by omega
+          simp [hn1, hn0] at h
+      | some s =>
+          obtain hsplit := eq_dropLast_append_of_getLast? P s hP
+          rw [hsplit] at h
+          rw [Root_right _ _ _ _ _ h2 hmk', ← hkeq] at h
+          cases hR : Root v (m - k) (D.length - k) P.dropLast with
+          | none => rw [hR] at h; simp at h
+          | some x =>
+              rw [hR] at h
+              simp only [Option.map_some, Option.some.injEq] at h
+              rw [MTH_split D h2, ← hkeq] at h
+              rcases hnode_inj_or_collision h with ⟨hs, hx⟩ | hc
+              · have ihm : m - k < (D.drop k).length := by omega
+                have hR' : Root v (m - k) (D.drop k).length P.dropLast
+                    = some (MTH (D.drop k)) := by rw [hdplen, hR, hx]
+                rcases ih v P.dropLast ihm hR' with ⟨hv, hPd⟩ | hc
+                · left
+                  have hidx : k + (m - k) = m := by omega
+                  refine ⟨?_, ?_⟩
+                  · rw [hv]
+                    have hh : (D.drop k).getD (m - k) [] = D.getD m [] := by
+                      rw [getD_drop, hidx]
+                    exact congrArg hleaf hh
+                  · have hRHS : Path m D = Path (m - k) (D.drop k) ++ [MTH (D.take k)] := by
+                      rw [Path]; simp only [if_neg hgt, ← hkeq, if_neg hmk]
+                    rw [hRHS, hsplit, hPd, hs]
+                · exact Or.inr hc
+              · exact Or.inr hc
+
+/-- **Theorem 2 (Inclusion soundness: position binding)**, paper §6,
+    constructive form: an accepting receipt whose leaf differs from the
+    honest leaf at position `m` exhibits a SHA-256 collision. -/
+theorem incl_sound (m : Nat) (D : List Bytes) (hm : m < D.length)
+    (d : Bytes) (P : List Hash)
+    (h : Root (hleaf d) m D.length P = some (MTH D)) :
+    d = D.getD m [] ∨ HasCollision := by
+  rcases root_binding m D (hleaf d) P hm h with ⟨hv, _⟩ | hc
+  · exact hleaf_inj_or_collision hv
+  · exact Or.inr hc
+
+end LTLAcc
diff --git a/verification/Proofs/Binding.olean b/verification/Proofs/Binding.olean
new file mode 100644
index 0000000..fc0eade
Binary files /dev/null and b/verification/Proofs/Binding.olean differ
diff --git a/verification/Proofs/Completeness.lean b/verification/Proofs/Completeness.lean
index 24ae35e..9d8ee43 100644
--- a/verification/Proofs/Completeness.lean
+++ b/verification/Proofs/Completeness.lean
@@ -10,7 +10,7 @@ namespace LTLAcc
 
 /-- `Path` (paper §5.3): the operator's inclusion path for index `m`.
     Sibling subtree heads, leaf-to-root order (the paper's `‖ [s]`). -/
-noncomputable def Path (m : Nat) (D : List Bytes) : List Bytes :=
+noncomputable def Path (m : Nat) (D : List Bytes) : List Hash :=
   if D.length ≤ 1 then []
   else
     let k := kbelow D.length
@@ -76,39 +76,37 @@ theorem MTH_split (D : List Bytes) (h : 2 ≤ D.length) :
   have h1 : ¬ D.length = 1 := by omega
   simp only [h0, h1, dite_false]
 
-theorem Root_one (v : Bytes) (m : Nat) : Root v m 1 [] = some v := by
-  rw [Root]; rfl
+theorem Root_one (v : Hash) (m : Nat) : Root v m 1 [] = some v := by
+  rw [Root]; simp
+
+theorem Root_one_cons (v : Hash) (m : Nat) (p : Hash) (q : List Hash) :
+    Root v m 1 (p :: q) = none := by
+  rw [Root]; simp
 
 /-- `Root` at a composite size, left branch (`m < k`). -/
-theorem Root_left (v : Bytes) (m n : Nat) (P : List Bytes) (s : Bytes)
+theorem Root_left (v : Hash) (m n : Nat) (P : List Hash) (s : Hash)
     (hn : 2 ≤ n) (hm : m < kbelow n) :
     Root v m n (P ++ [s]) = (Root v m (kbelow n) P).map (hnode · s) := by
   have h1 : ¬ n = 1 := by omega
   have h0 : ¬ n = 0 := by omega
-  have hne : ¬ (P ++ [s] = []) := by simp
   cases hR : Root v m (kbelow n) P with
   | none =>
       rw [Root]; simp [h0, h1, hm, hR]
-      exact fun hh => absurd hh hne
   | some x =>
       rw [Root]; simp [h0, h1, hm, hR]
-      exact fun hh => absurd hh hne
 
 /-- `Root` at a composite size, right branch (`m ≥ k`). -/
-theorem Root_right (v : Bytes) (m n : Nat) (P : List Bytes) (s : Bytes)
+theorem Root_right (v : Hash) (m n : Nat) (P : List Hash) (s : Hash)
     (hn : 2 ≤ n) (hm : ¬ m < kbelow n) :
     Root v m n (P ++ [s]) =
       (Root v (m - kbelow n) (n - kbelow n) P).map (hnode s ·) := by
   have h1 : ¬ n = 1 := by omega
   have h0 : ¬ n = 0 := by omega
-  have hne : ¬ (P ++ [s] = []) := by simp
   cases hR : Root v (m - kbelow n) (n - kbelow n) P with
   | none =>
       rw [Root]; simp [h0, h1, hm, hR]
-      exact fun hh => absurd hh hne
   | some x =>
       rw [Root]; simp [h0, h1, hm, hR]
-      exact fun hh => absurd hh hne
 
 /-! ### Theorem 1 -/
 
diff --git a/verification/Proofs/Completeness.olean b/verification/Proofs/Completeness.olean
index cb54ae8..d8d93f5 100644
Binary files a/verification/Proofs/Completeness.olean and b/verification/Proofs/Completeness.olean differ
diff --git a/verification/check.sh b/verification/check.sh
index 452c047..18d627a 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -17,7 +17,7 @@ export LEAN_MEM_MB="${LEAN_MEM_MB:-4096}"
 CORES="${LEAN_MAX_CORES:-0-3}"
 
 GEN_MODULES=( LTLAcc/HashExternal )
-PROOFS=( Basic Completeness )
+PROOFS=( Basic Completeness Binding )
 
 # Certificates and their exact expected cones (observed at first green
 # compile, 2026-07-10; any drift in EITHER direction is a failure).
@@ -32,6 +32,11 @@ declare -A CONES=(
   [LTLAcc.ConsRec]="propext, LTLAcc.sha256, Quot.sound"
   [LTLAcc.Path]="propext, LTLAcc.sha256, Quot.sound"
   [LTLAcc.incl_complete]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.hnode_preimage_inj]="propext"
+  [LTLAcc.hnode_inj_or_collision]="propext, LTLAcc.sha256"
+  [LTLAcc.hleaf_inj_or_collision]="LTLAcc.sha256"
+  [LTLAcc.root_binding]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.incl_sound]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
 )
 
 free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'
diff --git a/verification/gen/LTLAcc/HashExternal.lean b/verification/gen/LTLAcc/HashExternal.lean
index 349c344..59ecfe9 100644
--- a/verification/gen/LTLAcc/HashExternal.lean
+++ b/verification/gen/LTLAcc/HashExternal.lean
@@ -1,12 +1,22 @@
 /- The single sanctioned axiom site of this corpus (mirrors the role of
-   gen/ in the *-ed25519-verified repos): SHA-256 as an opaque function.
-   No properties are assumed of it — in particular NOT collision
-   resistance. The soundness theorems downstream are constructive: they
-   EXHIBIT two distinct preimages with equal image. Believing such a
-   pair cannot be found is the reader's interpretation step, exactly as
-   documented in the paper (§6, Remark 1). -/
+   gen/ in the *-ed25519-verified repos): SHA-256 as an opaque function
+   into 32-byte outputs. No properties are assumed of it — in particular
+   NOT collision resistance; the soundness theorems downstream are
+   constructive, they EXHIBIT two distinct preimages with equal image.
+
+   The fixed output WIDTH is part of the function's type, not an
+   assumption about its behavior: it is what makes hnode argument pairs
+   recoverable from preimages (the paper's "65-byte preimages"
+   parenthetical, made explicit). -/
 namespace LTLAcc
 
-axiom sha256 : List UInt8 → List UInt8
+/-- A 32-byte hash value. -/
+def Hash : Type := { l : List UInt8 // l.length = 32 }
+
+instance : Inhabited Hash := ⟨⟨List.replicate 32 0, by simp⟩⟩
+instance : DecidableEq Hash := fun a b =>
+  decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm
+
+axiom sha256 : List UInt8 → Hash
 
 end LTLAcc
diff --git a/verification/gen/LTLAcc/HashExternal.olean b/verification/gen/LTLAcc/HashExternal.olean
index 7377445..3453a43 100644
Binary files a/verification/gen/LTLAcc/HashExternal.olean and b/verification/gen/LTLAcc/HashExternal.olean differ