S5.3 Fable re-audit: machine-verify the ConsRec base refactor (permanent artifact)

Re-derived S5.3 (all done under an Opus switch) from zero. consRecBinding
STATEMENT re-confirmed faithful to paper Thm 3 steps 1-2 (y=MTH D₁ = the
hash-fold condition; some=>collision / none=>x=MTH(D₁.take n₀) = the two
Lemma-2 outcomes); non-vacuous (some-branch is a SPECIFIC-pair IsCollision,
not pigeonhole-provable; none-branch a real equality needing hcons).

FINDING + FIX: Opus changed ConsRec's base definition (list-match →
decidable if) with only 'recompiled clean' as evidence — a definition
that mirrors the deployed verifier. Now machine-checked: consRec_base_
false_eq / consRec_base_true_eq prove the decidable-if base EQUALS the
exact list-match forms it replaced. Kept as PERMANENT cone-audited
theorems (F1 discipline: keep the evidence), not a throwaway probe.

QUEUED for S5.4: extractCons_correct (Theorem 3 endpoint) MUST carry a
permanent non-vacuity witness like extractIncl_nonvacuous/extractMTH_
nonvacuous. S7 must re-confirm the NEW ConsRec base vs Python.

26 certs green. LTL untouched.

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

verification/Proofs/AxiomCheck.lean

@@ -5,6 +5,7 @@ import Proofs.Extract
 import Proofs.Descent
 import Proofs.Consistency
 import Proofs.Binding3
+import Proofs.Refactor
 #print axioms LTLAcc.domsep
 #print axioms LTLAcc.kbelow_pos
 #print axioms LTLAcc.kbelow_lt
@@ -29,3 +30,5 @@ import Proofs.Binding3
 #print axioms LTLAcc.extractConsNode
 #print axioms LTLAcc.take_all
 #print axioms LTLAcc.consRecBinding
+#print axioms LTLAcc.consRec_base_false_eq
+#print axioms LTLAcc.consRec_base_true_eq

verification/Proofs/Refactor.lean

@@ -0,0 +1,27 @@
+/- S5.3 Fable re-audit artifact (permanent, not a throwaway probe): the
+   S5.3 change of ConsRec's base from list-match to decidable `if` must be
+   SEMANTICS-PRESERVING — Opus's only evidence was "the chain recompiled".
+   These two theorems machine-check the equivalence against the exact
+   list-match forms that were replaced, so the refactor's faithfulness is
+   a permanent, cone-audited guarantee. -/
+import Proofs.Basic
+
+namespace LTLAcc
+
+/-- b=false base: decidable-if form = the original `[s]` list-match. -/
+theorem consRec_base_false_eq (C : List Hash) :
+    (if C.length = 1 then some ((C.getLastD default, C.getLastD default) : Hash × Hash) else none)
+    = (match C with | [s] => some (s, s) | _ => none) := by
+  cases C with
+  | nil => rfl
+  | cons a t => cases t with | nil => rfl | cons b u => simp
+
+/-- b=true base: decidable-if form = the original `[]` list-match. -/
+theorem consRec_base_true_eq (C : List Hash) (r : Hash) :
+    (if C = [] then some ((r, r) : Hash × Hash) else none)
+    = (match C with | [] => some (r, r) | _ => none) := by
+  cases C with
+  | nil => rfl
+  | cons a t => rfl
+
+end LTLAcc

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 Extract Descent Consistency Binding3 )
+PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor )
 
 # Certificates and their exact expected cones (observed at first green
 # compile, 2026-07-10; any drift in EITHER direction is a failure).
@@ -46,6 +46,8 @@ declare -A CONES=(
   [LTLAcc.extractConsNode]="propext, LTLAcc.sha256, Quot.sound"
   [LTLAcc.take_all]="propext, Quot.sound"
   [LTLAcc.consRecBinding]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.consRec_base_false_eq]="propext, Quot.sound"
+  [LTLAcc.consRec_base_true_eq]="propext, Quot.sound"
 )
 
 free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'