diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d88df345..f42388c3 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -39,6 +39,7 @@ jobs:
           python3 scripts/audit_barrier_kernel.py
           python3 scripts/audit_interval_capacity.py
           python3 scripts/audit_floor_excursion.py
+          python3 scripts/audit_five_band_clock.py
 
       - name: Check exact first-descent intervals
         run: |
diff --git a/Collatz.lean b/Collatz.lean
index 7f8e0f63..547b06de 100644
--- a/Collatz.lean
+++ b/Collatz.lean
@@ -2109,3 +2109,4 @@ import Collatz.Exploration.BarrierKernel
 import Collatz.Exploration.IntervalCapacity
 import Collatz.Exploration.TwoStepCapacity
 import Collatz.Exploration.FloorExcursion
+import Collatz.Exploration.FiveBandClock
diff --git a/Collatz/Exploration/FiveBandArithmetic.lean b/Collatz/Exploration/FiveBandArithmetic.lean
new file mode 100644
index 00000000..700df9a4
--- /dev/null
+++ b/Collatz/Exploration/FiveBandArithmetic.lean
@@ -0,0 +1,1023 @@
+import Collatz.Basic
+
+/-! Division-free certificates for the fifty terminal transition prefixes.
+Interval bounds and halving/3x+1 equations are explicit premises. Parity is not needed.
+The rational generator guides the proof; Lean checks every leaf. -/
+namespace Collatz.Exploration.FiveBandArithmetic
+
+set_option maxHeartbeats 2000000
+set_option linter.unusedVariables false
+
+/-- Transition prefix `000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_000
+    (b x0 x1 x2 x3 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h3 : b ≤ x3 ∧ x3 ≤ 5*b)
+    (r0 : 2*x1 = x0)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    : False := by
+  omega
+
+/-- Transition prefix `001000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_001000
+    (b x0 x1 x2 x3 x4 x5 x6 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h6 : b ≤ x6 ∧ x6 ≤ 5*b)
+    (r0 : 2*x1 = x0)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    : False := by
+  omega
+
+/-- Transition prefix `00100100` cannot remain in [b,5b] for b>1. -/
+theorem prefix_00100100
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : 2*x1 = x0)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : 2*x7 = x6)
+    (r7 : 2*x8 = x7)
+    : False := by
+  omega
+
+/-- Transition prefix `00100101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_00100101
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h5 : b ≤ x5 ∧ x5 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : 2*x1 = x0)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : 2*x7 = x6)
+    (r7 : x8 = 3*x7+1)
+    : False := by
+  omega
+
+/-- Transition prefix `0010011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_0010011
+    (b x2 x3 x4 x5 x6 x7 : Nat) (hb : 1 < b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h7 : b ≤ x7 ∧ x7 ≤ 5*b)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : x7 = 3*x6+1)
+    : False := by
+  omega
+
+/-- Transition prefix `00101000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_00101000
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : 2*x1 = x0)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    (r7 : 2*x8 = x7)
+    : False := by
+  omega
+
+/-- Transition prefix `0010100100` cannot remain in [b,5b] for b>1. -/
+theorem prefix_0010100100
+    (b x2 x3 x4 x5 x6 x7 x8 x9 x10 : Nat) (hb : 1 < b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h5 : b ≤ x5 ∧ x5 ≤ 5*b)
+    (h10 : b ≤ x10 ∧ x10 ≤ 5*b)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    (r7 : x8 = 3*x7+1)
+    (r8 : 2*x9 = x8)
+    (r9 : 2*x10 = x9)
+    : False := by
+  omega
+
+/-- Transition prefix `0010100101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_0010100101
+    (b x2 x3 x4 x5 x6 x7 x8 x9 x10 : Nat) (hb : 1 < b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h10 : b ≤ x10 ∧ x10 ≤ 5*b)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    (r7 : x8 = 3*x7+1)
+    (r8 : 2*x9 = x8)
+    (r9 : x10 = 3*x9+1)
+    : False := by
+  omega
+
+/-- Transition prefix `001010011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_001010011
+    (b x1 x2 x3 x4 x5 x6 x7 x8 x9 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h9 : b ≤ x9 ∧ x9 ≤ 5*b)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    (r7 : x8 = 3*x7+1)
+    (r8 : x9 = 3*x8+1)
+    : False := by
+  omega
+
+/-- Transition prefix `0010101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_0010101
+    (b x2 x3 x4 x5 x6 x7 : Nat) (hb : 1 < b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h7 : b ≤ x7 ∧ x7 ≤ 5*b)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    : False := by
+  omega
+
+/-- Transition prefix `001011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_001011
+    (b x1 x2 x3 x4 x5 x6 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h6 : b ≤ x6 ∧ x6 ≤ 5*b)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : x6 = 3*x5+1)
+    : False := by
+  omega
+
+/-- Transition prefix `0011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_0011
+    (b x2 x3 x4 : Nat) (hb : 1 < b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h4 : b ≤ x4 ∧ x4 ≤ 5*b)
+    (r2 : x3 = 3*x2+1)
+    (r3 : x4 = 3*x3+1)
+    : False := by
+  omega
+
+/-- Transition prefix `01000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_01000
+    (b x2 x3 x4 x5 : Nat) (hb : 1 < b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h5 : b ≤ x5 ∧ x5 ≤ 5*b)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : 2*x5 = x4)
+    : False := by
+  omega
+
+/-- Transition prefix `01001000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_01001000
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : 2*x1 = x0)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    (r7 : 2*x8 = x7)
+    : False := by
+  omega
+
+/-- Transition prefix `0100100100` cannot remain in [b,5b] for b>1. -/
+theorem prefix_0100100100
+    (b x2 x3 x4 x5 x6 x7 x8 x9 x10 : Nat) (hb : 1 < b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h10 : b ≤ x10 ∧ x10 ≤ 5*b)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    (r7 : x8 = 3*x7+1)
+    (r8 : 2*x9 = x8)
+    (r9 : 2*x10 = x9)
+    : False := by
+  omega
+
+/-- Transition prefix `0100100101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_0100100101
+    (b x2 x3 x4 x5 x6 x7 x8 x9 x10 : Nat) (hb : 1 < b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h7 : b ≤ x7 ∧ x7 ≤ 5*b)
+    (h10 : b ≤ x10 ∧ x10 ≤ 5*b)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    (r7 : x8 = 3*x7+1)
+    (r8 : 2*x9 = x8)
+    (r9 : x10 = 3*x9+1)
+    : False := by
+  omega
+
+/-- Transition prefix `010010011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_010010011
+    (b x1 x2 x3 x4 x5 x6 x7 x8 x9 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h9 : b ≤ x9 ∧ x9 ≤ 5*b)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    (r7 : x8 = 3*x7+1)
+    (r8 : x9 = 3*x8+1)
+    : False := by
+  omega
+
+/-- Transition prefix `0100101000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_0100101000
+    (b x2 x3 x4 x5 x6 x7 x8 x9 x10 : Nat) (hb : 1 < b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h10 : b ≤ x10 ∧ x10 ≤ 5*b)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : 2*x8 = x7)
+    (r8 : 2*x9 = x8)
+    (r9 : 2*x10 = x9)
+    : False := by
+  omega
+
+/-- Transition prefix `010010100100` cannot remain in [b,5b] for b>1. -/
+theorem prefix_010010100100
+    (b x4 x5 x6 x7 x8 x9 x10 x11 x12 : Nat) (hb : 1 < b)
+    (h4 : b ≤ x4 ∧ x4 ≤ 5*b)
+    (h7 : b ≤ x7 ∧ x7 ≤ 5*b)
+    (h12 : b ≤ x12 ∧ x12 ≤ 5*b)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : 2*x8 = x7)
+    (r8 : 2*x9 = x8)
+    (r9 : x10 = 3*x9+1)
+    (r10 : 2*x11 = x10)
+    (r11 : 2*x12 = x11)
+    : False := by
+  omega
+
+/-- Transition prefix `010010100101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_010010100101
+    (b x4 x5 x6 x7 x8 x9 x10 x11 x12 : Nat) (hb : 1 < b)
+    (h4 : b ≤ x4 ∧ x4 ≤ 5*b)
+    (h12 : b ≤ x12 ∧ x12 ≤ 5*b)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : 2*x8 = x7)
+    (r8 : 2*x9 = x8)
+    (r9 : x10 = 3*x9+1)
+    (r10 : 2*x11 = x10)
+    (r11 : x12 = 3*x11+1)
+    : False := by
+  omega
+
+/-- Transition prefix `01001010011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_01001010011
+    (b x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h11 : b ≤ x11 ∧ x11 ≤ 5*b)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : 2*x8 = x7)
+    (r8 : 2*x9 = x8)
+    (r9 : x10 = 3*x9+1)
+    (r10 : x11 = 3*x10+1)
+    : False := by
+  omega
+
+/-- Transition prefix `010010101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_010010101
+    (b x1 x2 x3 x4 x5 x6 x7 x8 x9 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h9 : b ≤ x9 ∧ x9 ≤ 5*b)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : 2*x8 = x7)
+    (r8 : x9 = 3*x8+1)
+    : False := by
+  omega
+
+/-- Transition prefix `01001011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_01001011
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : 2*x1 = x0)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : x8 = 3*x7+1)
+    : False := by
+  omega
+
+/-- Transition prefix `010011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_010011
+    (b x1 x2 x3 x4 x5 x6 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h6 : b ≤ x6 ∧ x6 ≤ 5*b)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    (r5 : x6 = 3*x5+1)
+    : False := by
+  omega
+
+/-- Transition prefix `0101000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_0101000
+    (b x4 x5 x6 x7 : Nat) (hb : 1 < b)
+    (h4 : b ≤ x4 ∧ x4 ≤ 5*b)
+    (h7 : b ≤ x7 ∧ x7 ≤ 5*b)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    : False := by
+  omega
+
+/-- Transition prefix `010100100` cannot remain in [b,5b] for b>1. -/
+theorem prefix_010100100
+    (b x1 x2 x3 x4 x5 x6 x7 x8 x9 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h4 : b ≤ x4 ∧ x4 ≤ 5*b)
+    (h9 : b ≤ x9 ∧ x9 ≤ 5*b)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : 2*x8 = x7)
+    (r8 : 2*x9 = x8)
+    : False := by
+  omega
+
+/-- Transition prefix `010100101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_010100101
+    (b x1 x2 x3 x4 x5 x6 x7 x8 x9 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h9 : b ≤ x9 ∧ x9 ≤ 5*b)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : 2*x8 = x7)
+    (r8 : x9 = 3*x8+1)
+    : False := by
+  omega
+
+/-- Transition prefix `01010011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_01010011
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : 2*x1 = x0)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : x8 = 3*x7+1)
+    : False := by
+  omega
+
+/-- Transition prefix `010101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_010101
+    (b x1 x2 x3 x4 x5 x6 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h6 : b ≤ x6 ∧ x6 ≤ 5*b)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    : False := by
+  omega
+
+/-- Transition prefix `01011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_01011
+    (b x0 x1 x2 x3 x4 x5 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h5 : b ≤ x5 ∧ x5 ≤ 5*b)
+    (r0 : 2*x1 = x0)
+    (r1 : x2 = 3*x1+1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : x5 = 3*x4+1)
+    : False := by
+  omega
+
+/-- Transition prefix `011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_011
+    (b x1 x2 x3 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h3 : b ≤ x3 ∧ x3 ≤ 5*b)
+    (r1 : x2 = 3*x1+1)
+    (r2 : x3 = 3*x2+1)
+    : False := by
+  omega
+
+/-- Transition prefix `1000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_1000
+    (b x1 x2 x3 x4 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h4 : b ≤ x4 ∧ x4 ≤ 5*b)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : 2*x4 = x3)
+    : False := by
+  omega
+
+/-- Transition prefix `1001000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_1001000
+    (b x1 x2 x3 x4 x5 x6 x7 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h7 : b ≤ x7 ∧ x7 ≤ 5*b)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    (r6 : 2*x7 = x6)
+    : False := by
+  omega
+
+/-- Transition prefix `100100100` cannot remain in [b,5b] for b>1. -/
+theorem prefix_100100100
+    (b x1 x2 x3 x4 x5 x6 x7 x8 x9 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h9 : b ≤ x9 ∧ x9 ≤ 5*b)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : 2*x8 = x7)
+    (r8 : 2*x9 = x8)
+    : False := by
+  omega
+
+/-- Transition prefix `100100101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_100100101
+    (b x1 x2 x3 x4 x5 x6 x7 x8 x9 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h6 : b ≤ x6 ∧ x6 ≤ 5*b)
+    (h9 : b ≤ x9 ∧ x9 ≤ 5*b)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : 2*x8 = x7)
+    (r8 : x9 = 3*x8+1)
+    : False := by
+  omega
+
+/-- Transition prefix `10010011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_10010011
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    (r6 : x7 = 3*x6+1)
+    (r7 : x8 = 3*x7+1)
+    : False := by
+  omega
+
+/-- Transition prefix `100101000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_100101000
+    (b x1 x2 x3 x4 x5 x6 x7 x8 x9 : Nat) (hb : 1 < b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h9 : b ≤ x9 ∧ x9 ≤ 5*b)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : 2*x7 = x6)
+    (r7 : 2*x8 = x7)
+    (r8 : 2*x9 = x8)
+    : False := by
+  omega
+
+/-- Transition prefix `10010100100` cannot remain in [b,5b] for b>1. -/
+theorem prefix_10010100100
+    (b x3 x4 x5 x6 x7 x8 x9 x10 x11 : Nat) (hb : 1 < b)
+    (h3 : b ≤ x3 ∧ x3 ≤ 5*b)
+    (h6 : b ≤ x6 ∧ x6 ≤ 5*b)
+    (h11 : b ≤ x11 ∧ x11 ≤ 5*b)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : 2*x7 = x6)
+    (r7 : 2*x8 = x7)
+    (r8 : x9 = 3*x8+1)
+    (r9 : 2*x10 = x9)
+    (r10 : 2*x11 = x10)
+    : False := by
+  omega
+
+/-- Transition prefix `10010100101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_10010100101
+    (b x3 x4 x5 x6 x7 x8 x9 x10 x11 : Nat) (hb : 1 < b)
+    (h3 : b ≤ x3 ∧ x3 ≤ 5*b)
+    (h11 : b ≤ x11 ∧ x11 ≤ 5*b)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : 2*x7 = x6)
+    (r7 : 2*x8 = x7)
+    (r8 : x9 = 3*x8+1)
+    (r9 : 2*x10 = x9)
+    (r10 : x11 = 3*x10+1)
+    : False := by
+  omega
+
+/-- Transition prefix `1001010011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_1001010011
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h10 : b ≤ x10 ∧ x10 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : 2*x7 = x6)
+    (r7 : 2*x8 = x7)
+    (r8 : x9 = 3*x8+1)
+    (r9 : x10 = 3*x9+1)
+    : False := by
+  omega
+
+/-- Transition prefix `10010101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_10010101
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : 2*x7 = x6)
+    (r7 : x8 = 3*x7+1)
+    : False := by
+  omega
+
+/-- Transition prefix `1001011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_1001011
+    (b x0 x1 x2 x3 x4 x5 x6 x7 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h7 : b ≤ x7 ∧ x7 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : x7 = 3*x6+1)
+    : False := by
+  omega
+
+/-- Transition prefix `10011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_10011
+    (b x0 x1 x2 x3 x4 x5 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h5 : b ≤ x5 ∧ x5 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : 2*x3 = x2)
+    (r3 : x4 = 3*x3+1)
+    (r4 : x5 = 3*x4+1)
+    : False := by
+  omega
+
+/-- Transition prefix `101000` cannot remain in [b,5b] for b>1. -/
+theorem prefix_101000
+    (b x3 x4 x5 x6 : Nat) (hb : 1 < b)
+    (h3 : b ≤ x3 ∧ x3 ≤ 5*b)
+    (h6 : b ≤ x6 ∧ x6 ≤ 5*b)
+    (r3 : 2*x4 = x3)
+    (r4 : 2*x5 = x4)
+    (r5 : 2*x6 = x5)
+    : False := by
+  omega
+
+/-- Transition prefix `10100100` cannot remain in [b,5b] for b>1. -/
+theorem prefix_10100100
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h3 : b ≤ x3 ∧ x3 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : 2*x7 = x6)
+    (r7 : 2*x8 = x7)
+    : False := by
+  omega
+
+/-- Transition prefix `10100101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_10100101
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : 2*x7 = x6)
+    (r7 : x8 = 3*x7+1)
+    : False := by
+  omega
+
+/-- Transition prefix `1010011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_1010011
+    (b x0 x1 x2 x3 x4 x5 x6 x7 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h7 : b ≤ x7 ∧ x7 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : 2*x5 = x4)
+    (r5 : x6 = 3*x5+1)
+    (r6 : x7 = 3*x6+1)
+    : False := by
+  omega
+
+/-- Transition prefix `10101` cannot remain in [b,5b] for b>1. -/
+theorem prefix_10101
+    (b x0 x1 x2 x3 x4 x5 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h5 : b ≤ x5 ∧ x5 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : 2*x4 = x3)
+    (r4 : x5 = 3*x4+1)
+    : False := by
+  omega
+
+/-- Transition prefix `1011` cannot remain in [b,5b] for b>1. -/
+theorem prefix_1011
+    (b x0 x1 x2 x3 x4 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h4 : b ≤ x4 ∧ x4 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : 2*x2 = x1)
+    (r2 : x3 = 3*x2+1)
+    (r3 : x4 = 3*x3+1)
+    : False := by
+  omega
+
+/-- Transition prefix `11` cannot remain in [b,5b] for b>1. -/
+theorem prefix_11
+    (b x0 x1 x2 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (r0 : x1 = 3*x0+1)
+    (r1 : x2 = 3*x1+1)
+    : False := by
+  omega
+
+/-- No thirteen sampled states can satisfy the band and map equations. -/
+theorem impossible_trace
+    (b x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : Nat) (hb : 1 < b)
+    (h0 : b ≤ x0 ∧ x0 ≤ 5*b)
+    (h1 : b ≤ x1 ∧ x1 ≤ 5*b)
+    (h2 : b ≤ x2 ∧ x2 ≤ 5*b)
+    (h3 : b ≤ x3 ∧ x3 ≤ 5*b)
+    (h4 : b ≤ x4 ∧ x4 ≤ 5*b)
+    (h5 : b ≤ x5 ∧ x5 ≤ 5*b)
+    (h6 : b ≤ x6 ∧ x6 ≤ 5*b)
+    (h7 : b ≤ x7 ∧ x7 ≤ 5*b)
+    (h8 : b ≤ x8 ∧ x8 ≤ 5*b)
+    (h9 : b ≤ x9 ∧ x9 ≤ 5*b)
+    (h10 : b ≤ x10 ∧ x10 ≤ 5*b)
+    (h11 : b ≤ x11 ∧ x11 ≤ 5*b)
+    (h12 : b ≤ x12 ∧ x12 ≤ 5*b)
+    (r0 : 2*x1 = x0 ∨ x1 = 3*x0+1)
+    (r1 : 2*x2 = x1 ∨ x2 = 3*x1+1)
+    (r2 : 2*x3 = x2 ∨ x3 = 3*x2+1)
+    (r3 : 2*x4 = x3 ∨ x4 = 3*x3+1)
+    (r4 : 2*x5 = x4 ∨ x5 = 3*x4+1)
+    (r5 : 2*x6 = x5 ∨ x6 = 3*x5+1)
+    (r6 : 2*x7 = x6 ∨ x7 = 3*x6+1)
+    (r7 : 2*x8 = x7 ∨ x8 = 3*x7+1)
+    (r8 : 2*x9 = x8 ∨ x9 = 3*x8+1)
+    (r9 : 2*x10 = x9 ∨ x10 = 3*x9+1)
+    (r10 : 2*x11 = x10 ∨ x11 = 3*x10+1)
+    (r11 : 2*x12 = x11 ∨ x12 = 3*x11+1)
+    : False := by
+  revert r11 r10 r9 r8 r7 r6 r5 r4 r3 r2 r1 r0
+  intro r0
+  rcases r0 with r0 | r0
+  · -- even transition at time 0
+    intro r1
+    rcases r1 with r1 | r1
+    · -- even transition at time 1
+      intro r2
+      rcases r2 with r2 | r2
+      · -- even transition at time 2
+        exact False.elim (prefix_000 b x0 x1 x2 x3 hb h0 h3 r0 r1 r2)
+      · -- odd transition at time 2
+        intro r3
+        rcases r3 with r3 | r3
+        · -- even transition at time 3
+          intro r4
+          rcases r4 with r4 | r4
+          · -- even transition at time 4
+            intro r5
+            rcases r5 with r5 | r5
+            · -- even transition at time 5
+              exact False.elim (prefix_001000 b x0 x1 x2 x3 x4 x5 x6 hb h0 h6 r0 r1 r2 r3 r4 r5)
+            · -- odd transition at time 5
+              intro r6
+              rcases r6 with r6 | r6
+              · -- even transition at time 6
+                intro r7
+                rcases r7 with r7 | r7
+                · -- even transition at time 7
+                  exact False.elim (prefix_00100100 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+                · -- odd transition at time 7
+                  exact False.elim (prefix_00100101 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h5 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+              · -- odd transition at time 6
+                exact False.elim (prefix_0010011 b x2 x3 x4 x5 x6 x7 hb h2 h7 r2 r3 r4 r5 r6)
+          · -- odd transition at time 4
+            intro r5
+            rcases r5 with r5 | r5
+            · -- even transition at time 5
+              intro r6
+              rcases r6 with r6 | r6
+              · -- even transition at time 6
+                intro r7
+                rcases r7 with r7 | r7
+                · -- even transition at time 7
+                  exact False.elim (prefix_00101000 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+                · -- odd transition at time 7
+                  intro r8
+                  rcases r8 with r8 | r8
+                  · -- even transition at time 8
+                    intro r9
+                    rcases r9 with r9 | r9
+                    · -- even transition at time 9
+                      exact False.elim (prefix_0010100100 b x2 x3 x4 x5 x6 x7 x8 x9 x10 hb h2 h5 h10 r2 r3 r4 r5 r6 r7 r8 r9)
+                    · -- odd transition at time 9
+                      exact False.elim (prefix_0010100101 b x2 x3 x4 x5 x6 x7 x8 x9 x10 hb h2 h10 r2 r3 r4 r5 r6 r7 r8 r9)
+                  · -- odd transition at time 8
+                    exact False.elim (prefix_001010011 b x1 x2 x3 x4 x5 x6 x7 x8 x9 hb h1 h9 r1 r2 r3 r4 r5 r6 r7 r8)
+              · -- odd transition at time 6
+                exact False.elim (prefix_0010101 b x2 x3 x4 x5 x6 x7 hb h2 h7 r2 r3 r4 r5 r6)
+            · -- odd transition at time 5
+              exact False.elim (prefix_001011 b x1 x2 x3 x4 x5 x6 hb h1 h6 r1 r2 r3 r4 r5)
+        · -- odd transition at time 3
+          exact False.elim (prefix_0011 b x2 x3 x4 hb h2 h4 r2 r3)
+    · -- odd transition at time 1
+      intro r2
+      rcases r2 with r2 | r2
+      · -- even transition at time 2
+        intro r3
+        rcases r3 with r3 | r3
+        · -- even transition at time 3
+          intro r4
+          rcases r4 with r4 | r4
+          · -- even transition at time 4
+            exact False.elim (prefix_01000 b x2 x3 x4 x5 hb h2 h5 r2 r3 r4)
+          · -- odd transition at time 4
+            intro r5
+            rcases r5 with r5 | r5
+            · -- even transition at time 5
+              intro r6
+              rcases r6 with r6 | r6
+              · -- even transition at time 6
+                intro r7
+                rcases r7 with r7 | r7
+                · -- even transition at time 7
+                  exact False.elim (prefix_01001000 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+                · -- odd transition at time 7
+                  intro r8
+                  rcases r8 with r8 | r8
+                  · -- even transition at time 8
+                    intro r9
+                    rcases r9 with r9 | r9
+                    · -- even transition at time 9
+                      exact False.elim (prefix_0100100100 b x2 x3 x4 x5 x6 x7 x8 x9 x10 hb h2 h10 r2 r3 r4 r5 r6 r7 r8 r9)
+                    · -- odd transition at time 9
+                      exact False.elim (prefix_0100100101 b x2 x3 x4 x5 x6 x7 x8 x9 x10 hb h2 h7 h10 r2 r3 r4 r5 r6 r7 r8 r9)
+                  · -- odd transition at time 8
+                    exact False.elim (prefix_010010011 b x1 x2 x3 x4 x5 x6 x7 x8 x9 hb h1 h9 r1 r2 r3 r4 r5 r6 r7 r8)
+              · -- odd transition at time 6
+                intro r7
+                rcases r7 with r7 | r7
+                · -- even transition at time 7
+                  intro r8
+                  rcases r8 with r8 | r8
+                  · -- even transition at time 8
+                    intro r9
+                    rcases r9 with r9 | r9
+                    · -- even transition at time 9
+                      exact False.elim (prefix_0100101000 b x2 x3 x4 x5 x6 x7 x8 x9 x10 hb h2 h10 r2 r3 r4 r5 r6 r7 r8 r9)
+                    · -- odd transition at time 9
+                      intro r10
+                      rcases r10 with r10 | r10
+                      · -- even transition at time 10
+                        intro r11
+                        rcases r11 with r11 | r11
+                        · -- even transition at time 11
+                          exact False.elim (prefix_010010100100 b x4 x5 x6 x7 x8 x9 x10 x11 x12 hb h4 h7 h12 r4 r5 r6 r7 r8 r9 r10 r11)
+                        · -- odd transition at time 11
+                          exact False.elim (prefix_010010100101 b x4 x5 x6 x7 x8 x9 x10 x11 x12 hb h4 h12 r4 r5 r6 r7 r8 r9 r10 r11)
+                      · -- odd transition at time 10
+                        exact False.elim (prefix_01001010011 b x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 hb h1 h11 r1 r2 r3 r4 r5 r6 r7 r8 r9 r10)
+                  · -- odd transition at time 8
+                    exact False.elim (prefix_010010101 b x1 x2 x3 x4 x5 x6 x7 x8 x9 hb h1 h9 r1 r2 r3 r4 r5 r6 r7 r8)
+                · -- odd transition at time 7
+                  exact False.elim (prefix_01001011 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+            · -- odd transition at time 5
+              exact False.elim (prefix_010011 b x1 x2 x3 x4 x5 x6 hb h1 h6 r1 r2 r3 r4 r5)
+        · -- odd transition at time 3
+          intro r4
+          rcases r4 with r4 | r4
+          · -- even transition at time 4
+            intro r5
+            rcases r5 with r5 | r5
+            · -- even transition at time 5
+              intro r6
+              rcases r6 with r6 | r6
+              · -- even transition at time 6
+                exact False.elim (prefix_0101000 b x4 x5 x6 x7 hb h4 h7 r4 r5 r6)
+              · -- odd transition at time 6
+                intro r7
+                rcases r7 with r7 | r7
+                · -- even transition at time 7
+                  intro r8
+                  rcases r8 with r8 | r8
+                  · -- even transition at time 8
+                    exact False.elim (prefix_010100100 b x1 x2 x3 x4 x5 x6 x7 x8 x9 hb h1 h4 h9 r1 r2 r3 r4 r5 r6 r7 r8)
+                  · -- odd transition at time 8
+                    exact False.elim (prefix_010100101 b x1 x2 x3 x4 x5 x6 x7 x8 x9 hb h1 h9 r1 r2 r3 r4 r5 r6 r7 r8)
+                · -- odd transition at time 7
+                  exact False.elim (prefix_01010011 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+            · -- odd transition at time 5
+              exact False.elim (prefix_010101 b x1 x2 x3 x4 x5 x6 hb h1 h6 r1 r2 r3 r4 r5)
+          · -- odd transition at time 4
+            exact False.elim (prefix_01011 b x0 x1 x2 x3 x4 x5 hb h0 h5 r0 r1 r2 r3 r4)
+      · -- odd transition at time 2
+        exact False.elim (prefix_011 b x1 x2 x3 hb h1 h3 r1 r2)
+  · -- odd transition at time 0
+    intro r1
+    rcases r1 with r1 | r1
+    · -- even transition at time 1
+      intro r2
+      rcases r2 with r2 | r2
+      · -- even transition at time 2
+        intro r3
+        rcases r3 with r3 | r3
+        · -- even transition at time 3
+          exact False.elim (prefix_1000 b x1 x2 x3 x4 hb h1 h4 r1 r2 r3)
+        · -- odd transition at time 3
+          intro r4
+          rcases r4 with r4 | r4
+          · -- even transition at time 4
+            intro r5
+            rcases r5 with r5 | r5
+            · -- even transition at time 5
+              intro r6
+              rcases r6 with r6 | r6
+              · -- even transition at time 6
+                exact False.elim (prefix_1001000 b x1 x2 x3 x4 x5 x6 x7 hb h1 h7 r1 r2 r3 r4 r5 r6)
+              · -- odd transition at time 6
+                intro r7
+                rcases r7 with r7 | r7
+                · -- even transition at time 7
+                  intro r8
+                  rcases r8 with r8 | r8
+                  · -- even transition at time 8
+                    exact False.elim (prefix_100100100 b x1 x2 x3 x4 x5 x6 x7 x8 x9 hb h1 h9 r1 r2 r3 r4 r5 r6 r7 r8)
+                  · -- odd transition at time 8
+                    exact False.elim (prefix_100100101 b x1 x2 x3 x4 x5 x6 x7 x8 x9 hb h1 h6 h9 r1 r2 r3 r4 r5 r6 r7 r8)
+                · -- odd transition at time 7
+                  exact False.elim (prefix_10010011 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+            · -- odd transition at time 5
+              intro r6
+              rcases r6 with r6 | r6
+              · -- even transition at time 6
+                intro r7
+                rcases r7 with r7 | r7
+                · -- even transition at time 7
+                  intro r8
+                  rcases r8 with r8 | r8
+                  · -- even transition at time 8
+                    exact False.elim (prefix_100101000 b x1 x2 x3 x4 x5 x6 x7 x8 x9 hb h1 h9 r1 r2 r3 r4 r5 r6 r7 r8)
+                  · -- odd transition at time 8
+                    intro r9
+                    rcases r9 with r9 | r9
+                    · -- even transition at time 9
+                      intro r10
+                      rcases r10 with r10 | r10
+                      · -- even transition at time 10
+                        exact False.elim (prefix_10010100100 b x3 x4 x5 x6 x7 x8 x9 x10 x11 hb h3 h6 h11 r3 r4 r5 r6 r7 r8 r9 r10)
+                      · -- odd transition at time 10
+                        exact False.elim (prefix_10010100101 b x3 x4 x5 x6 x7 x8 x9 x10 x11 hb h3 h11 r3 r4 r5 r6 r7 r8 r9 r10)
+                    · -- odd transition at time 9
+                      exact False.elim (prefix_1001010011 b x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 hb h0 h10 r0 r1 r2 r3 r4 r5 r6 r7 r8 r9)
+                · -- odd transition at time 7
+                  exact False.elim (prefix_10010101 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+              · -- odd transition at time 6
+                exact False.elim (prefix_1001011 b x0 x1 x2 x3 x4 x5 x6 x7 hb h0 h7 r0 r1 r2 r3 r4 r5 r6)
+          · -- odd transition at time 4
+            exact False.elim (prefix_10011 b x0 x1 x2 x3 x4 x5 hb h0 h5 r0 r1 r2 r3 r4)
+      · -- odd transition at time 2
+        intro r3
+        rcases r3 with r3 | r3
+        · -- even transition at time 3
+          intro r4
+          rcases r4 with r4 | r4
+          · -- even transition at time 4
+            intro r5
+            rcases r5 with r5 | r5
+            · -- even transition at time 5
+              exact False.elim (prefix_101000 b x3 x4 x5 x6 hb h3 h6 r3 r4 r5)
+            · -- odd transition at time 5
+              intro r6
+              rcases r6 with r6 | r6
+              · -- even transition at time 6
+                intro r7
+                rcases r7 with r7 | r7
+                · -- even transition at time 7
+                  exact False.elim (prefix_10100100 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h3 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+                · -- odd transition at time 7
+                  exact False.elim (prefix_10100101 b x0 x1 x2 x3 x4 x5 x6 x7 x8 hb h0 h8 r0 r1 r2 r3 r4 r5 r6 r7)
+              · -- odd transition at time 6
+                exact False.elim (prefix_1010011 b x0 x1 x2 x3 x4 x5 x6 x7 hb h0 h7 r0 r1 r2 r3 r4 r5 r6)
+          · -- odd transition at time 4
+            exact False.elim (prefix_10101 b x0 x1 x2 x3 x4 x5 hb h0 h5 r0 r1 r2 r3 r4)
+        · -- odd transition at time 3
+          exact False.elim (prefix_1011 b x0 x1 x2 x3 x4 hb h0 h4 r0 r1 r2 r3)
+    · -- odd transition at time 1
+      exact False.elim (prefix_11 b x0 x1 x2 hb h0 h2 r0 r1)
+
+end Collatz.Exploration.FiveBandArithmetic
diff --git a/Collatz/Exploration/FiveBandClock.lean b/Collatz/Exploration/FiveBandClock.lean
new file mode 100644
index 00000000..5a8ae7fa
--- /dev/null
+++ b/Collatz/Exploration/FiveBandClock.lean
@@ -0,0 +1,165 @@
+import Collatz.Exploration.FloorExcursion
+import Collatz.Exploration.FiveBandArithmetic
+
+/-! A sharp constant clock for exiting an ordinary Collatz band.
+All statements are finite arithmetic consequences of the actual map.
+The two exit directions are kept explicit. -/
+namespace Collatz.Exploration.FiveBandClock
+open BarrierKernel
+
+/-- Division-free transition equations, with the parity conditions retained. -/
+theorem step_relation {n : Nat} (hn : 0 < n) :
+    (2*step n = n ∧ n%2 = 0) ∨ (step n = 3*n+1 ∧ n%2 = 1) := by
+  have hz : n ≠ 0 := by omega
+  by_cases he : n%2 = 0
+  · left
+    simp only [step, if_neg hz, if_pos he]
+    omega
+  · right
+    exact ⟨by simp [step, hz, he], by omega⟩
+
+/-- Every ordinary orbit exits [b,5b] by time twelve when b>1. -/
+theorem rejection_twelve {b n : Nat} (hb : 1 < b) :
+    intervalCheck b (5*b) 12 n = false := by
+  by_cases ht : intervalCheck b (5*b) 12 n = true
+  · exfalso
+    have hs := (intervalCheck_iff b (5*b) 12 n).mp ht
+    have bounds0 := hs 0 (by decide)
+    have bounds1 := hs 1 (by decide)
+    have bounds2 := hs 2 (by decide)
+    have bounds3 := hs 3 (by decide)
+    have bounds4 := hs 4 (by decide)
+    have bounds5 := hs 5 (by decide)
+    have bounds6 := hs 6 (by decide)
+    have bounds7 := hs 7 (by decide)
+    have bounds8 := hs 8 (by decide)
+    have bounds9 := hs 9 (by decide)
+    have bounds10 := hs 10 (by decide)
+    have bounds11 := hs 11 (by decide)
+    have bounds12 := hs 12 (by decide)
+    have rel (k : Nat) (hk : k ≤ 11) :
+        (2*orbit (k+1) n = orbit k n ∧ (orbit k n)%2 = 0) ∨
+        (orbit (k+1) n = 3*orbit k n+1 ∧ (orbit k n)%2 = 1) := by
+      have hp : 0 < orbit k n := by have := hs k (by omega); omega
+      have h := step_relation hp
+      rw [← orbit_step_commute, ← orbit_succ_steps] at h
+      exact h
+    exact FiveBandArithmetic.impossible_trace b (orbit 0 n) (orbit 1 n) (orbit 2 n) (orbit 3 n) (orbit 4 n) (orbit 5 n) (orbit 6 n) (orbit 7 n) (orbit 8 n) (orbit 9 n) (orbit 10 n) (orbit 11 n) (orbit 12 n) hb
+      bounds0 bounds1 bounds2 bounds3 bounds4 bounds5 bounds6 bounds7 bounds8 bounds9 bounds10 bounds11 bounds12
+      ((rel 0 (by decide)).imp And.left And.left) ((rel 1 (by decide)).imp And.left And.left) ((rel 2 (by decide)).imp And.left And.left) ((rel 3 (by decide)).imp And.left And.left) ((rel 4 (by decide)).imp And.left And.left) ((rel 5 (by decide)).imp And.left And.left) ((rel 6 (by decide)).imp And.left And.left) ((rel 7 (by decide)).imp And.left And.left) ((rel 8 (by decide)).imp And.left And.left) ((rel 9 (by decide)).imp And.left And.left) ((rel 10 (by decide)).imp And.left And.left) ((rel 11 (by decide)).imp And.left And.left)
+  · cases he : intervalCheck b (5*b) 12 n <;> simp_all
+
+/-- The finite clock retains both possible exit directions. -/
+theorem exit_twelve (b n : Nat) (hb : 1 < b) :
+    ∃ k, k ≤ 12 ∧ (orbit k n < b ∨ 5*b < orbit k n) := by
+  by_cases h : ∃ k, k ≤ 12 ∧ (orbit k n < b ∨ 5*b < orbit k n)
+  · exact h
+  · exfalso
+    have hc : intervalCheck b (5*b) 12 n = true := by
+      apply (intervalCheck_iff b (5*b) 12 n).mpr
+      intro k hk
+      by_cases hl : orbit k n < b
+      · exact False.elim (h ⟨k,hk,Or.inl hl⟩)
+      · by_cases hu : 5*b < orbit k n
+        · exact False.elim (h ⟨k,hk,Or.inr hu⟩)
+        · omega
+    rw [rejection_twelve hb] at hc
+    cases hc
+
+/-- Twelve cannot be replaced by eleven in the arbitrary-start band theorem. -/
+theorem clock_sharpness : intervalCheck 40 200 11 114 = true ∧
+    orbit 12 114 = 37 ∧ intervalCheck 40 200 12 114 = false := by decide
+
+/-- Keeping a lower barrier eliminates the downward exit alternative. -/
+theorem high_within_twelve {b n : Nat} (hb : 1 < b) (h : Kernel b n) :
+    ∃ k, k ≤ 12 ∧ 5*b < orbit k n := by
+  obtain ⟨k,hk,hl | hu⟩ := exit_twelve b n hb
+  · have := h k; omega
+  · exact ⟨k,hk,hu⟩
+
+/-- Every future 13-point window contains a high excursion. -/
+theorem high_window {b n : Nat} (hb : 1 < b) (h : Kernel b n) (t : Nat) :
+    ∃ s, t ≤ s ∧ s ≤ t+12 ∧ 5*b < orbit s n := by
+  obtain ⟨k,hk,hv⟩ := high_within_twelve hb (kernel_forward h t)
+  refine ⟨k+t,by omega,by omega,?_⟩
+  rw [orbit_add]
+  exact hv
+
+/-- Explicitly distinct witnesses, one in each disjoint 13-point block.
+This is a conditional lower frequency bound; it does not construct a failed orbit. -/
+theorem disjoint_high_witnesses {b n : Nat} (hb : 1 < b) (h : Kernel b n) :
+    ∃ f : Nat → Nat,
+      (∀ q, 13*q ≤ f q ∧ f q < 13*(q+1) ∧ 5*b < orbit (f q) n) ∧
+      (∀ a c, a < c → f a < f c) := by
+  classical
+  have hw (q : Nat) : ∃ s, 13*q ≤ s ∧ s < 13*(q+1) ∧ 5*b < orbit s n := by
+    obtain ⟨s,hs,ht,hv⟩ := high_window hb h (13*q)
+    exact ⟨s,hs,by omega,hv⟩
+  let f (q : Nat) := Classical.choose (hw q)
+  have hf (q : Nat) : 13*q ≤ f q ∧ f q < 13*(q+1) ∧ 5*b < orbit (f q) n :=
+    Classical.choose_spec (hw q)
+  refine ⟨f,hf,?_⟩
+  intro a c hac
+  have ha := hf a
+  have hc := hf c
+  omega
+
+/-- For any finite block count N there are N distinct high times below 13N. -/
+theorem finite_high_witnesses {b n : Nat} (hb : 1 < b) (h : Kernel b n) (N : Nat) :
+    ∃ f : Fin N → Nat,
+      (∀ q, f q < 13*N ∧ 5*b < orbit (f q) n) ∧
+      (∀ a c, f a = f c → a = c) := by
+  obtain ⟨g,hg,hstrict⟩ := disjoint_high_witnesses hb h
+  refine ⟨fun q => g q.val,?_,?_⟩
+  · intro q
+    change g q.val < 13*N ∧ 5*b < orbit (g q.val) n
+    have hq := hg q.val
+    have hlt := q.isLt
+    exact ⟨by omega,hq.2.2⟩
+  · intro a c he
+    change g a.val = g c.val at he
+    have hv : a.val = c.val := by
+      by_cases hac : a.val < c.val
+      · have := hstrict a.val c.val hac; omega
+      · by_cases hca : c.val < a.val
+        · have := hstrict c.val a.val hca; omega
+        · omega
+    exact Fin.ext hv
+
+/-- A finite observed lower-surviving prefix already supplies distinct witnesses;
+no infinite kernel hypothesis is required for this finite conclusion. -/
+theorem finite_survival_witnesses {b n : Nat} (hb : 1 < b) (N : Nat)
+    (h : Survives b (13*N-1) n) :
+    ∃ f : Fin N → Nat,
+      (∀ q, f q < 13*N ∧ 5*b < orbit (f q) n) ∧
+      (∀ a c, f a = f c → a = c) := by
+  classical
+  have hw (q : Fin N) :
+      ∃ s, 13*q.val ≤ s ∧ s < 13*(q.val+1) ∧ 5*b < orbit s n := by
+    obtain ⟨k,hk,hl | hu⟩ := exit_twelve b (orbit (13*q.val) n) hb
+    · have hq := q.isLt
+      have hlower := h (k+13*q.val) (by omega)
+      rw [orbit_add] at hlower
+      omega
+    · refine ⟨k+13*q.val,by omega,by omega,?_⟩
+      rw [orbit_add]
+      exact hu
+  let f (q : Fin N) := Classical.choose (hw q)
+  have hf (q : Fin N) :
+      13*q.val ≤ f q ∧ f q < 13*(q.val+1) ∧ 5*b < orbit (f q) n :=
+    Classical.choose_spec (hw q)
+  refine ⟨f,?_,?_⟩
+  · intro q
+    have hs := hf q
+    have hq := q.isLt
+    exact ⟨by omega,hs.2.2⟩
+  · intro a c he
+    have ha := hf a
+    have hc := hf c
+    have hv : a.val = c.val := by omega
+    exact Fin.ext hv
+
+/-- The excluded anchor 1 supports the trivial cycle indefinitely. -/
+theorem anchor_one_control : intervalCheck 1 5 100 1 = true := by decide
+
+end Collatz.Exploration.FiveBandClock
diff --git a/README.md b/README.md
index 95aa269f..8e4e14d7 100644
--- a/README.md
+++ b/README.md
@@ -32,7 +32,9 @@ own verification instructions.
   exact window splitting, the greatest invariant barrier kernel, an executable
   interval checker, exact one- and two-step capacities, and smaller verified
   budgets for cycle extraction. A sharp eight-step excursion theorem forces
-  a hypothetical orbit floor to exceed five times its starting value.
+  a hypothetical orbit floor to exceed five times its starting value. Every
+  arbitrary-start orbit exits `[b,5b]` within twelve steps for `b>1`; the
+  clock is sharp and yields conditional high-visit witnesses.
 
 - [First passage through 2,592 steps](Research/PassageAtlas/README.md) —
   a stronger conditional descent theorem, an exact residual condition
diff --git a/Research/BarrierKernel.md b/Research/BarrierKernel.md
index d3397536..ac333c46 100644
--- a/Research/BarrierKernel.md
+++ b/Research/BarrierKernel.md
@@ -209,8 +209,9 @@ Taking an attained minimum of an arbitrary orbit also proves that no
 entire ordinary orbit remains in `[b,5b]` for `b>1`. The exit theorem
 explicitly permits either `C^k(n)<b` or `C^k(n)>5b`; discarding the
 growth alternative would be an invalid step toward a Collatz proof.
-Its statement gives no uniform exit time for arbitrary starts. The
-eight-step bound above is for the start equal to the anchor.
+That attained-minimum argument gives no uniform exit time for arbitrary
+starts. The eight-step bound above is for the start equal to the anchor.
+The separate twelve-step certificate below supplies the uniform clock.
 
 Run `python3 scripts/audit_floor_excursion.py`. The scalar experiment
 checks 199,999 ordinary starts and the exact dichotomy on 25,000
@@ -218,7 +219,7 @@ eight-step survivors. Their first bound-attainment times are 5 (18,750
 starts) and 8 (6,250 starts). It checks 4,099 affine-family samples,
 including very large integers, and 125,745 arbitrary-start band exits.
 The largest exit time observed in the latter finite experiment is 12;
-this is not a universal theorem. The audit inspects all named theorem
+this observation motivated the universal theorem below. The audit inspects all named theorem
 axiom footprints and requires rejection of four false claims.
 
 The trivial cycle shows why `m>1` is necessary. A separate scalar control
@@ -239,3 +240,56 @@ Finite exploration suggests coefficient bounds approaching six in an
 idealized multiplicative model. That model omits the additive correction
 and is not a theorem about actual Collatz orbits. A general transfer
 argument would need to control those corrections and integer realizability.
+
+
+## Sharp twelve-step band clock and high-visit frequency
+
+`FiveBandClock.exit_twelve` strengthens the arbitrary-start band exit:
+for every natural start `n` and integer barrier `b>1`, some `k≤12` satisfies
+
+`C^k(n)<b ∨ 5b<C^k(n)`.
+
+The clock is sharp. At barrier 40 the trajectory from 114 is
+
+`114→57→172→86→43→130→65→196→98→49→148→74→37`.
+
+Times 0 through 11 all lie in `[40,200]`; time 12 exits downward. An
+upper exit alone would be false, even for a positive start in the band.
+
+The arithmetic certificate is stronger than the actual map: it only needs
+thirteen natural states in the band and, at each transition, either
+`2x_(k+1)=x_k` or `x_(k+1)=3x_k+1`. The odd/even guard on the latter
+alternative is unnecessary for this contradiction. The generator uses
+exact rational feasibility of `x_k=a_k*x_0+c_k` to select fifty terminal
+prefixes. Only two or three interval-bound premises are necessary for
+each terminal certificate, keeping the arithmetic proofs small. Each
+prefix is independently proved impossible by Lean, and
+`impossible_trace` combines them by case analysis. Python supplies the
+branch guide, never a trusted axiom or unchecked proof certificate.
+
+If a whole orbit retains a fixed lower barrier `b>1`, each thirteen-point
+window must contain a value greater than `5b`. The file gives explicit
+increasing witnesses in disjoint blocks `[13q,13(q+1))`. Consequently,
+for any `N`, there are `N` distinct high times below `13N`. The same finite
+conclusion already follows from `Survives(b,13N−1,n)`; no assumption about
+the unobserved future is needed. At `N=0`, the conclusion is vacuous.
+
+The existing `Strategy/LocalOrbitCorridor.lean` supplies a related
+three-state exclusion in the narrower accelerated band `[V,2V)`. The
+present certificate concerns the ordinary map, the inclusive ratio-five
+band, and its sharp arbitrary-start clock; it uses no verified-range axiom.
+
+This is a conditional frequency bound at one fixed threshold. It proves
+neither that the kernel is nonempty nor that orbit values are unbounded.
+It does not eliminate growth exits or establish convergence. Literature
+priority and the requested frontier-novel proportion remain unverified.
+
+Run `python3 scripts/audit_five_band_clock.py`. The audit reproduces the
+exact-rational branch generator, builds both Lean files, checks all 61
+named theorem axiom footprints, and requires rejection of four false
+claims. Independent scalar tests cover 627,742 exhaustive ordinary-map
+starts, 60,000 large-integer starts, 20,295 starts under the relaxed
+transition relation, 150,670 lower-surviving windows, and 13,565 distinct
+block witnesses. Controls include the excluded anchor 1, removal of lower
+survival, and the different `3n−1` map. Counts are test evidence; Lean
+proofs establish the universal statements.
diff --git a/scripts/audit_five_band_clock.py b/scripts/audit_five_band_clock.py
new file mode 100644
index 00000000..71b0c56a
--- /dev/null
+++ b/scripts/audit_five_band_clock.py
@@ -0,0 +1,29 @@
+#!/usr/bin/env python3
+"""Audit the universal twelve-step clock and conditional high-visit witnesses."""
+import subprocess
+from audit_barrier_kernel import ROOT, check_axioms, check_false_certificates
+
+MODULE = 'Collatz.Exploration.FiveBandClock'
+
+
+def main():
+    subprocess.run(['python3', str(ROOT / 'scripts/generate_five_band_arithmetic.py')],
+                   cwd=ROOT, check=True)
+    subprocess.run(['lake', 'build', MODULE], cwd=ROOT, check=True)
+    subprocess.run(['python3', str(ROOT / 'scripts/test_five_band_clock.py')],
+                   cwd=ROOT, check=True)
+    count = check_axioms(ROOT / 'Collatz/Exploration/FiveBandClock.lean', MODULE)
+    count += check_axioms(ROOT / 'Collatz/Exploration/FiveBandArithmetic.lean',
+                          'Collatz.Exploration.FiveBandArithmetic')
+    false_claims = [
+        'example : Collatz.Exploration.BarrierKernel.intervalCheck 40 200 11 114 = false := by decide\n',
+        'example : Collatz.Exploration.BarrierKernel.intervalCheck 1 5 12 1 = false := by decide\n',
+        'example : Collatz.orbit 12 114 = 38 := by decide\n',
+        'example : (List.range 13).any (fun k => decide (10 < Collatz.orbit k 2)) = true := by decide\n',
+    ]
+    rejected = check_false_certificates(MODULE, false_claims)
+    print(f'{count} theorem axiom footprints checked; {rejected} false claims rejected')
+
+
+if __name__ == '__main__':
+    main()
diff --git a/scripts/generate_five_band_arithmetic.py b/scripts/generate_five_band_arithmetic.py
new file mode 100644
index 00000000..cde9de6d
--- /dev/null
+++ b/scripts/generate_five_band_arithmetic.py
@@ -0,0 +1,116 @@
+#!/usr/bin/env python3
+"""Reproduce the small transition tree; Lean independently checks every leaf.
+
+Exact rational feasibility only guides which prefixes to stop expanding.
+An erroneous guide produces an unprovable leaf, not an admitted theorem.
+The generator emits explicit natural-number premises, never proof escapes.
+"""
+import argparse
+from fractions import Fraction as F
+from itertools import combinations
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[1]
+SOURCE = ROOT / 'Collatz/Exploration/FiveBandArithmetic.lean'
+
+
+def feasible(states):
+    """Real feasibility for b>=2, with x_k=a_k*x_0+c_k in [b,5b]."""
+    lower = [(1/a, -c/a) for a, c in states]
+    upper = [(5/a, -c/a) for a, c in states]
+    minimum, maximum = F(2), None
+    for a, c in lower:
+        for d, e in upper:
+            coefficient, rhs = a-d, e-c
+            if coefficient > 0:
+                limit = rhs/coefficient
+                maximum = limit if maximum is None else min(maximum, limit)
+            elif coefficient < 0:
+                minimum = max(minimum, rhs/coefficient)
+            elif rhs < 0:
+                return False
+    return maximum is None or minimum <= maximum
+
+
+def certificate():
+    leaves = []
+    cores = {}
+    def walk(word, states):
+        if not feasible(states) or len(word) == 12:
+            leaves.append(word)
+            cores[word] = next(t for size in range(1, len(states)+1)
+                               for t in combinations(range(len(states)), size)
+                               if not feasible([states[i] for i in t]))
+            return
+        a, c = states[-1]
+        walk(word+'0', states+[(a/2, c/2)])
+        walk(word+'1', states+[(3*a, 3*c+1)])
+    walk('', [(F(1), F(0))])
+
+    def relation(k, bit=None):
+        even = f'2*x{k+1} = x{k}'
+        odd = f'x{k+1} = 3*x{k}+1'
+        return even+' ∨ '+odd if bit is None else (even if bit == '0' else odd)
+
+    def statement(name, depth, word=None, core=None):
+        low, high = (0, depth) if core is None else (min(core), max(core))
+        bounds = range(depth+1) if core is None else core
+        out = [f'theorem {name}',
+               '    (b '+' '.join(f'x{i}' for i in range(low, high+1))+' : Nat) (hb : 1 < b)']
+        out += [f'    (h{i} : b ≤ x{i} ∧ x{i} ≤ 5*b)' for i in bounds]
+        out += [f'    (r{i} : {relation(i, None if word is None else word[i])})'
+                for i in range(low, high)]
+        return '\n'.join(out)+'\n    : False := by\n'
+
+    result = ['import Collatz.Basic\n\n',
+              '/-! Division-free certificates for the fifty terminal transition prefixes.\n',
+              'Interval bounds and halving/3x+1 equations are explicit premises. Parity is not needed.\n',
+              'The rational generator guides the proof; Lean checks every leaf. -/\n',
+              'namespace Collatz.Exploration.FiveBandArithmetic\n\n',
+              'set_option maxHeartbeats 2000000\n',
+              'set_option linter.unusedVariables false\n\n']
+    for word in leaves:
+        result += [f'/-- Transition prefix `{word}` cannot remain in [b,5b] for b>1. -/\n',
+                   statement('prefix_'+word, len(word), word, cores[word]), '  omega\n\n']
+    result += ['/-- No thirteen sampled states can satisfy the band and map equations. -/\n',
+               statement('impossible_trace', 12)]
+    lines = ['  revert ' + ' '.join(f'r{i}' for i in range(11, -1, -1))]
+    def emit(word, states, indent):
+        def add(text):
+            lines.append(' '*indent + text)
+        if word in leaves:
+            core = cores[word]
+            low, high = min(core), max(core)
+            arguments = ['b']+[f'x{i}' for i in range(low, high+1)]+['hb']+[
+                f'h{i}' for i in core]+[f'r{i}' for i in range(low, high)]
+            add('exact False.elim (prefix_'+word+' '+' '.join(arguments)+')')
+            return
+        k = len(word)
+        add(f'intro r{k}')
+        add(f'rcases r{k} with r{k} | r{k}')
+        a, c = states[-1]
+        add(f'· -- even transition at time {k}')
+        emit(word+'0', states+[(a/2, c/2)], indent+2)
+        add(f'· -- odd transition at time {k}')
+        emit(word+'1', states+[(3*a, 3*c+1)], indent+2)
+    emit('', [(F(1), F(0))], 2)
+    result += ['\n'.join(lines)+'\n', '\nend Collatz.Exploration.FiveBandArithmetic\n']
+    return ''.join(result), leaves
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--write', action='store_true')
+    args = parser.parse_args()
+    expected, leaves = certificate()
+    if args.write:
+        SOURCE.write_text(expected)
+    else:
+        assert expected == SOURCE.read_text(), 'Transition tree differs: run with --write, then rebuild Lean'
+    assert len(leaves) == 50 and max(map(len, leaves)) == 12
+    assert sum(F(1, 2**len(word)) for word in leaves) == 1
+    print('Exact rational guide: 50 leaves, maximum depth 12; source reproduced')
+
+
+if __name__ == '__main__':
+    main()
diff --git a/scripts/test_five_band_clock.py b/scripts/test_five_band_clock.py
new file mode 100644
index 00000000..67240ac3
--- /dev/null
+++ b/scripts/test_five_band_clock.py
@@ -0,0 +1,82 @@
+#!/usr/bin/env python3
+"""Direct scalar exits, bounded-window frequency, and essential-hypothesis controls."""
+from collections import Counter
+import random
+from test_barrier_kernel import trajectory
+
+
+def exit_time(b, start):
+    n = start
+    for k in range(13):
+        if n < b or 5*b < n:
+            return k
+        n = n//2 if n % 2 == 0 else 3*n+1
+    raise AssertionError((b, start, 'accepted 12-step corridor'))
+
+
+def main():
+    exits = Counter()
+    exhaustive = large = windows = blocks = 0
+    for b in range(2, 501):
+        for n in range(5*b+3):
+            exits[exit_time(b, n)] += 1
+            exhaustive += 1
+    # Independently check the stronger relation: 3n+1 is allowed at even sources.
+    relaxed = 0
+    for b in range(2, 101):
+        for start in range(b, 5*b+1):
+            states = {start}
+            for _ in range(12):
+                next_states = set()
+                for n in states:
+                    options = [3*n+1] + ([n//2] if n % 2 == 0 else [])
+                    next_states.update(m for m in options if b <= m <= 5*b)
+                states = next_states
+            assert not states, (b, start, states)
+            relaxed += 1
+    rng = random.Random(73017)
+    for _ in range(10000):
+        b = rng.randrange(2, 10**120)
+        for n in (0, b, 2*b, 5*b, 5*b+1, rng.randrange(b, 5*b+1)):
+            exits[exit_time(b, n)] += 1
+            large += 1
+    assert max(exits) == 12
+    sharp = trajectory(114, 12)
+    assert sharp == [114, 57, 172, 86, 43, 130, 65, 196, 98, 49, 148, 74, 37]
+    assert all(40 <= n <= 200 for n in sharp[:-1]) and sharp[-1] < 40
+    seeds = list(range(2, 2002)) + [2**90-1, 2**180-1]
+    for seed in seeds:
+        values = trajectory(seed, 511)
+        for b in sorted({2, max(2, seed//5), max(2, seed//2), seed}):
+            end = next((i for i, n in enumerate(values) if n < b), len(values))
+            prefix = values[:end]
+            # Finite lower survival supplies the frequency premise in each window.
+            for t in range(max(0, len(prefix)-12)):
+                assert any(n > 5*b for n in prefix[t:t+13]), (seed, b, t)
+                windows += 1
+            witnesses = []
+            for q in range(len(prefix)//13):
+                s = next(i for i in range(13*q, 13*q+13) if prefix[i] > 5*b)
+                witnesses.append(s)
+                blocks += 1
+            assert all(a < c for a, c in zip(witnesses, witnesses[1:]))
+            assert sum(n > 5*b for n in prefix[:13*len(witnesses)]) >= len(witnesses)
+    # Anchor 1 supports the ordinary trivial cycle; it cannot use the clock theorem.
+    assert all(1 <= n <= 5 for n in trajectory(1, 100))
+    # Keeping only initial positivity/lower survival does not imply a later high visit.
+    assert max(trajectory(2, 12)) <= 10
+    # The changed map 3n-1 defeats both uniform exit and conditional high frequency.
+    n = 5
+    minus = [n]
+    for _ in range(100):
+        n = n//2 if n % 2 == 0 else 3*n-1
+        minus.append(n)
+    assert all(5 <= n <= 25 for n in minus)
+    print(f'{exhaustive} exhaustive and {large} large-integer exit cases; '
+          f'maximum exit {max(exits)}; {relaxed} relaxed-transition starts; '
+          f'{windows} lower-surviving windows; '
+          f'{blocks} distinct block witnesses; sharpness and hypothesis controls passed')
+
+
+if __name__ == '__main__':
+    main()