diff --git a/README.md b/README.md
index f808711..7c9a182 100644
--- a/README.md
+++ b/README.md
@@ -16,7 +16,7 @@ the same discipline as the four `*-ed25519-verified` subject corpora.
 | L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 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) | in progress (S5): stage-1 arithmetic/list infrastructure done (kbelow_prefix_eq, take surgery); binding + assembly next |
+| L6b | ConsRec binding + Theorem 3 assembly (extractCons) | in progress (S5): stage-1 arithmetic/list infrastructure done (kbelow_prefix_eq, take surgery); stage-1 infra + extractConsNode extractor DEFINED; binding proof (steps 1-2) + extractCons assembly = stage 3 |
 | 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 202c3fa..6fd10d5 100644
--- a/verification/Proofs/AxiomCheck.lean
+++ b/verification/Proofs/AxiomCheck.lean
@@ -25,3 +25,4 @@ import Proofs.Consistency
 #print axioms LTLAcc.kbelow_prefix_eq
 #print axioms LTLAcc.take_take_le
 #print axioms LTLAcc.take_drop_prefix
+#print axioms LTLAcc.extractConsNode
diff --git a/verification/Proofs/Consistency.lean b/verification/Proofs/Consistency.lean
index c91af52..43c3026 100644
--- a/verification/Proofs/Consistency.lean
+++ b/verification/Proofs/Consistency.lean
@@ -64,4 +64,43 @@ theorem take_drop_prefix (l : List Bytes) (k n₀ : Nat) :
     (l.take n₀).drop k = (l.drop k).take (n₀ - k) := by
   rw [List.drop_take]
 
+/-! ### the consistency collision extractor (paper Theorem 3, steps 1-2) -/
+
+/-- Walk the `ConsRec` fold in parallel with the honest size-`n` tree of
+    `D₁`. At each level the new-root component builds `hnode` of a left and
+    a right value; compare that argument pair against the honest node
+    `hnode (MTH (D₁.take k)) (MTH (D₁.drop k))`. Return `some` concrete
+    colliding preimage pair at the first mismatch (steps 1-2 of Theorem 3),
+    or `none` if the fold is genuine all the way down — in which case the
+    binding `x = MTH (D₁.take n₀)` holds (proven in stage 3). -/
+noncomputable def extractConsNode (n₀ n : Nat) (C : List Hash) (b : Bool)
+    (r : Hash) (D₁ : List Bytes) : Option (List UInt8 × List UInt8) :=
+  if n₀ = n then none
+  else if n₀ > n ∨ n₀ = 0 ∨ n ≤ 1 then none
+  else
+    match C.getLast? with
+    | none => none
+    | some s =>
+        let k := kbelow n
+        if n₀ ≤ k then
+          let y' := ((ConsRec n₀ k C.dropLast b r).map Prod.snd).getD default
+          if y' = MTH (D₁.take k) ∧ s = MTH (D₁.drop k) then
+            extractConsNode n₀ k C.dropLast b r (D₁.take k)
+          else
+            some (0x01 :: (y'.val ++ s.val),
+                  0x01 :: ((MTH (D₁.take k)).val ++ (MTH (D₁.drop k)).val))
+        else
+          let y' := ((ConsRec (n₀ - k) (n - k) C.dropLast false r).map Prod.snd).getD default
+          if s = MTH (D₁.take k) ∧ y' = MTH (D₁.drop k) then
+            extractConsNode (n₀ - k) (n - k) C.dropLast false r (D₁.drop k)
+          else
+            some (0x01 :: (s.val ++ y'.val),
+                  0x01 :: ((MTH (D₁.take k)).val ++ (MTH (D₁.drop k)).val))
+termination_by n
+decreasing_by
+  · have h2 : 2 ≤ n := by omega
+    exact kbelow_lt n h2
+  · have := kbelow_pos n
+    omega
+
 end LTLAcc
diff --git a/verification/Proofs/Consistency.olean b/verification/Proofs/Consistency.olean
index 50cc899..c8ff9c7 100644
Binary files a/verification/Proofs/Consistency.olean and b/verification/Proofs/Consistency.olean differ
diff --git a/verification/check.sh b/verification/check.sh
index d09cb4a..20cbe0d 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -43,6 +43,7 @@ declare -A CONES=(
   [LTLAcc.kbelow_prefix_eq]="propext, Quot.sound"
   [LTLAcc.take_take_le]="propext, Quot.sound"
   [LTLAcc.take_drop_prefix]="propext, Classical.choice, Quot.sound"
+  [LTLAcc.extractConsNode]="propext, LTLAcc.sha256, Quot.sound"
 )
 
 free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'