S5 stage 2: extractConsNode extractor defined (consistency, Theorem 3 steps 1-2)

The consistency collision extractor: walks the ConsRec new-root fold in
parallel with the honest size-n tree of D₁ and returns the concrete
colliding node preimage pair at the first level where the fold's hnode
argument pair diverges from the honest node — or none if the fold is
genuine all the way down (binding holds). Both branches verified faithful
to ConsRec's hnode argument order (n₀≤k: y' left / s right; n₀>k: s left
/ y' right). Termination via kbelow bounds.

Deliberate honest checkpoint: the DEFINITION compiles and is cone-audited
[propext, LTLAcc.sha256, Quot.sound]; the binding CORRECTNESS proof — the
single hardest object in the corpus — is stage 3, kept for a fresh
session rather than a rushed long turn. 22 certs green. LTL untouched.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

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)

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

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

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}}'