diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean
index 59b0fbd..3d27b90 100644
--- a/verification/Proofs/AxiomCheck.lean
+++ b/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
diff --git a/verification/Proofs/AxiomCheck.olean b/verification/Proofs/AxiomCheck.olean
index 245dfde..f2afdfa 100644
Binary files a/verification/Proofs/AxiomCheck.olean and b/verification/Proofs/AxiomCheck.olean differ
diff --git a/verification/Proofs/ProbeRefactor.olean b/verification/Proofs/ProbeRefactor.olean
new file mode 100644
index 0000000..2ad15d2
Binary files /dev/null and b/verification/Proofs/ProbeRefactor.olean differ
diff --git a/verification/Proofs/Refactor.lean b/verification/Proofs/Refactor.lean
new file mode 100644
index 0000000..90bd5a7
--- /dev/null
+++ b/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
diff --git a/verification/Proofs/Refactor.olean b/verification/Proofs/Refactor.olean
new file mode 100644
index 0000000..3dcdd5d
Binary files /dev/null and b/verification/Proofs/Refactor.olean differ
diff --git a/verification/check.sh b/verification/check.sh
index b188c4a..6654bd4 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 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}}'