1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB: never halts (informal proof, Checkpoint B)

• Machine: 1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB, viewer https://bbchallenge.org/1RB0LF_0RC---_1RD0RA_1LE0RC_0LA0LE_1LE1LB
• Sheet: Results row 918, class "Sync bouncer counter"; no status, notes, links or Discord thread.
• Written for: the string itself (no mirror, no renaming).
• Status: complete at the informal level; formalisation not started.
• Every rule is either (a) a window lemma, checked by one finite run that never reads outside its window, so it holds in every context; (b) a parametric rule with its proof written out as a chain of (a) and earlier rules; or (c) a finite table that is checked exhaustively: the tail table T(f) of §4.2, 16,384 entries.
• What is not written out by hand: the 16,384 entries of T(f) and the four finite facts (T1)–(T4) read off them (§4.2). These are finite computations, re-run by check_proof.py check 5. Lemma RB (§4.3) turns them into TAILFRONT and the closure of L* for every r and every left context. Formalising the table is the hard part of the lemma plan (§9).
• Evidence: check_proof.py (§8), 10 checks.
• AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

     0    1
A   1RB  0LF
B   0RC  ---        halting transition: B reads 1
C   1RD  0RA
D   1LE  0RC
E   0LA  0LE
F   1LE  1LB

0. Overview

The tape right of the head is a binary counter written in three tokens, 00, 01 and Z = 100. A digit is b Z 01 Z^g, where b is 00 (bit 0) or 01 (bit 1) and g is the gap to the next digit. The head bounces off the left end, and every bounce adds 1 to the counter (rule Inc, §2).

At the right end of the counter there is a block of gap-1 digits (the R block) followed by a finite-state "tail" W. When the counter overflows, the carry runs into the tail. The tail answers in one of two ways, decided by a finite table: - S (silent): the counter wraps to 0 and nothing else happens. - N: the whole left part of the tape freezes into a "wall". The machine then spends a long pause eating the wall two increments at a time (§3), rebuilding every gap exactly and possibly inserting new digits.

The proof has four layers: 1. Window lemmas and the parametric counter rules (§2–§3). 2. The overflow: a right sweep, the tail table, a return sweep (lemma RB) whose parity decides N or S, and a parametric rule for the tail's growing end (§4). 3. Four finite facts read off the tail table, which lemma RB turns into TAILFRONT for every R block: the tail's 2-bit front unit cycles 10 → 01 → 11 → 00 → 10, and S can only happen at 11 (§4.5). 4. Linear arithmetic on the counter parameters: an interval invariant at normal-mode overflows that holds whatever the tail chooses at each 11 slot (§5).

1. Notation and families

1.1 Tape notation

• 0^inf u X> v 0^inf: state X reads the first cell of v. u <X v: state X reads the last cell of u.
• Window lemma u <X v → <Y u'v' (or → u'v' Y>): started with the head on the last cell of u (or the first cell of v), the run stays inside the |u|+|v| cells and leaves them on the stated side in state Y. Such a lemma holds in every context.
• Inner record (IR): A reads a 0 that it reached moving left, and the cells from the head on read (001)^p 00 0b10001. All macro rules go from one IR to the next. Note that (001)^p 00 = 00 Z^p.
• Z = 100. A digit is d(b) = 0b10001 = b' Z 01 with b' = 0b. A counter is D_G(v) = d(b_0) Z^(g_1) d(b_1) Z^(g_2) ... d(b_(N-1)), with v = Σ b_i 2^i (LSB leftmost).
• Zn(g) := (010)^(g+1) is a zone: a gap g frozen into the wall.

1.2 The right counter RC and the tail

• At every configuration we use, the counter has this form:
• k ≥ 0 large-gap digits d_0..d_(k-1), with gaps G = (g_1..g_k), every g_i ≥ 7;
• then the gap-2 digit, followed by the gap Z^2;
• then the R block U^q, where U = 01100 = 01 Z and q = 2r + H. In digit terms this is r gap-1 digits 0110001100 plus a half digit H ∈ {0,1}.
• The number of counter digits is N = k + 1 + r + H.
• The tail is W(f, e) := F(f) (0e_1)(0e_2)...(0e_m) 01, where F(f) = 0x0y0z10001 0?0?10001 0?1000?10001 0?0?1000?10001 0?1000?1000?1000?1000?10001 (11 + 9 + 12 + 14 + 27 = 73 cells: 15 bit cells and 58 fixed cells).
• f is the 15 bits at the ? places, read left to right; x, y, z are the first three of them.
• The end unit has m ≥ 0 bits e_1..e_m and the end marker 01.
• The front unit is (y, z).
• L* := the tails with x = 1 and H = y.

1.3 Families

• K_N(a; D; RC) := 0^inf A>(001)^a 00 D RC (normal mode, lead a).
• K_P(Wall; p; D; RC) := 0^inf Wall A>(001)^p 00 D RC (pause mode, inner lead p).
• X(a; G; r, H; f, e) := K_N(a; all bits 1; ...) with the counter of §1.2 and a tail in L*. This is a normal-mode overflow configuration: 0^inf A>(001)^a 00 [0110001 Z^(g_i)]_(i=1..k) 0110001 Z^2 U^(2r+H) W(f, e).
• The invariant set is the configurations X that satisfy INV (§5.3).

2. Window lemmas and the counter

2.1 Window lemmas (check 2: exact output word, exit side and state, step count)

PEN and PFN are 73-cell windows: neither run reads the cell right of P1, so whatever lies there (the end unit) is left unchanged. Check 2 compares the full output word of every row, PEN and PFN included, and also runs PEN/PFN with each 2-cell right context to show it is untouched.

Shift rules, by induction from R4, L1 and L4: C> Z^n → (010)^n C> (3n steps), (010)^n <E → <E Z^n (3n), Z^n <F → <F (001)^n (3n). R2 followed by R4^a is the old shift A> (001)^a 00 → (100)^a 10 C>.

2.2 Rule Inc_L (check 3)

Inc_L. For every left half-tape L, every a ≥ 0 and every counter D_G(v) with v + 1 < 2^N:

L A>(001)^a 00 D_G(v) T → L <F (001)^a 00 D_G(v+1) T, in 6a + 6S_j + 24j + 7 steps.

Here j = the number of trailing 1 bits of v (b_0..b_(j-1) = 1, b_j = 0) and S_j = g_1 + ... + g_j. The head never reads L before the last step, so L is arbitrary. T is arbitrary too, because the run never reads past d_j.

Proof, in order: 1. R2, R4^a. 2. For i = 0..j-1: R3 on d_i, then R4^(g_(i+1)). 3. R5 on d_j. 4. For i = j-1 down to 0: L1^(g_(i+1)), then L2 on the processed d_i. 5. L1^a, then L3.

The step total is 2 + 3a + Σ(7 + 3g) + 3 + Σ(3g + 17) + 3a + 2. In this argument j ranges over 0..N-1, and the proof is by induction on j (the carry depth), like Climb/E_stmt in CounterClass3v2 TM1.

2.3 Rule Inc

Inc. K_N(a; D_G(v); T) → K_N(a+1; D_G(v+1); T) for v + 1 < 2^N, in 6a + 6S_j + 24j + 9 steps.

Proof: Inc_L with L = 0^inf, then END. 0^inf 00 <F → 0^inf <A 01 leaves A reading a 0 that it reached moving left, with 0 01 (001)^a 00 = (001)^(a+1) 00 on its right.

3. Pause rules (check 4: exact whole tape at the next IR, exact steps)

Each pause rule has the shape Inc_L, then (if two increments) B1 and Inc_L again, then a left-end lemma that ends at the next IR. In every rule b_0 = 0 (v even), so the first Inc_L has j = 0 (6p + 7 steps). j and S below belong to the second increment.

D_(g,G)(2u) is the counter with a new LSB digit 0 at gap g in front of the old digits, so its value is 2u.

In ZX/ZXN the second Inc_L ends with F on the last cell of a wall that ends ...010 010 100 100 (ZX) or ...0 100 10100100 (ZXN). In both cases the last 12 cells are 010010100100, and ENDZX (22 steps, L4 twice inside it) turns them into 000100011001. A then reads the 13th cell from the end, which is 0, so this is an IR. That needs h ≥ 3 (ZX) or n ≥ 2 (ZXN). The right side reads 0 000100011001 (001)^p 00 d_0... = 00 0010001 Z^(p+2) d_0..., because 1001 (001)^p 00 = Z^(p+2). ZXP2 ends with BN on the last 6 cells 010010 of (100)^n 10 plus the 00 of the first 001. A then reads the middle cell of block n−1, so n ≥ 2 is needed.

The domains above are wider than what the run needs: Y and the walls are arbitrary words of the stated shape. The check ran them with random walls, random p ≤ 200, gaps ≤ 60 and ≤ 6 digits.

4. The overflow

4.1 Right sweep (OvR)

Start from X(a; G; r, H; f, e), or from the second increment of a P-cycle in pause mode at an overflow slot (wall (100)^n 1 with n ≥ 1, which is (100)^(n-1) 1000 after B1). The carry passes every digit:

R2, R4^a, [R3, R4^(g_i)] for i = 1..k, R3 (gap-2 digit), R4^2, then (R6, R4)^q over the R block.

C now stands on the first cell of F(f), and every token to its left is processed: 00→10, 01→10, Z→010. In particular the gap-2 digit is now 1001010 010010 and each of the q units U = 01100 is now P := 10010.

4.2 The tail table T(f) (check 5)

For each of the 16,384 fixed parts f with x = 1, run the window C> F(f) (73 cells): - For f ≠ 1^15 the head leaves the window on the left, in state σ(f) ∈ {E, F}, without reading the end unit. Counts: y = 0: F (8192); y = 1: E (6581) or F (1610). - For f = 1^15 the head leaves on the right in state C after 73 steps (CF1). This is ENDCARRY, §4.4.

So T(f) is a finite set of window lemmas C> F(f) → <σ(f) F'(f), where F'(f) is the 73-cell output word. They hold for every m, every end-bit setting and every left context.

Four finite facts are read off the table. Check 5 verifies them for all 16,383 f ≠ 1^15: - (T1) If σ(f) = F, then F'(f) begins with 00. - (T2) If y = 0, then σ(f) = F. - (T3) Let F''(f) be F'(f) with its first token replaced by 01 when σ(f) = F, and F''(f) = F'(f) when σ(f) = E. Then F''(f) = F(f') for some f', i.e. the 58 fixed cells of the template are unchanged. - (T4) Call f class S if y = 1 and σ(f) = F, and class N otherwise. Then x' = 1, and y' = 1 − y for class N, y' = y for class S. The front units (y, z) → (y', z') make a TAILFRONT arrow (§4.5) with label e(1−y) for class N and S for class S.

Counts: 00 →N,e1→ 10: 4096; 01 →N,e1→ 11: 4096; 10 →N,e0→ 01: 4096; 11 →N,e0→ 00: 2485; 11 →S→ 10: 1610. With f = 1^15 (ENDCARRY) that makes 16,384.

4.3 Return through the R block (lemma RB), and the boundary

After OvR and T(f) (f ≠ 1^15), the head is on the last cell of P^q in state σ = σ(f), with F'(f) and the untouched end unit on its right. Left of P^q is the processed gap-2 digit 1001010 010010.

Lemma RB. Let σ ∈ {E, F}, q ≥ 0, and let w be any word that starts with 00 if σ = F. Number the units 1..q from the left, and let μ_i be the mode in which unit i is entered: μ_q = σ and μ_i = flip(μ_(i+1)). Let μ := flip(μ_1) = σ flipped q times (μ = σ if q = 0). Then

P^q <σ w → <μ u_1 u_2 ... u_q w*, in Σ_i (5 if μ_i = E, 15 if μ_i = F) steps, where - u_i = t_i 100, with t_1 = 00, and for i ≥ 2, t_i = 01 if μ_(i−1) = F and 00 if μ_(i−1) = E; - w = w with its first token replaced by 01 if q ≥ 1 and σ = F, and w = w otherwise.

Proof, by induction on q. For q = 0 there is nothing to do. For q + 1, the first lemma applied is to the rightmost unit: - σ = E: UE 10010 <E → <F 00100 leaves P^q <F 00100 w. The new right word 00100 w starts with 00, so the induction hypothesis applies with mode F. It gives units 1..q, turns the first token of 00100 into 01 if q ≥ 1 (so t_(q+1) = 01 exactly when μ_q = F, as claimed), and leaves w unchanged (w = w, as claimed for σ = E). - σ = F: w = 00 w' by assumption. UF 10010 <F 00 → <E 00100 01 leaves P^q <E 00100 01 w'. The hypothesis applies with mode E, which has no precondition. It gives units 1..q and does not touch its right word, so u_(q+1) = 00100 (t_(q+1) = 00, matching μ_q = E) and w = 01 w' (matching σ = F).

In both cases the mode flips once more, so the final mode is σ flipped q + 1 times. ∎

So the 00-on-the-right precondition of every UF is carried by the induction: inside the block it is the 00100 just written by UE, and at the right end it is (T1).

The boundary. μ = F gives N and μ = E gives S. - μ = F → N. The two cells right of the head are 00: the token t_1 = 00 of u_1 if q ≥ 1, or the first token of w = F'(f) if q = 0 (then σ = μ = F and (T1) applies). BN 010010 <F 00 → <A 00010001 rewrites the processed Z Z and that token. A then reads the last cell of the processed gap-2 digit 1001010, which is 0, so this is an IR with lead 0. Reading the cells from A: 0 000100 01 ... = 00 | 00100 | 01 .... - BN therefore re-tokenises the processed gap-2 digit. Its first 6 cells 100101 join the wall, its 7th cell and the first cell of BN's output form the lead 00, and the next 5 cells form a new unit u_0 = 00100. - BN also sets t_1 to 01, or the first token of w when q = 0. This is why the R block grows leftward. - From normal mode this is rule NO: X(a; G; r, H; f, e) → 0^inf (100)^a 101001 [Zn(g_i) 1001]_(i=1..k) 01 A> 00 RC'. This is just the processed left part read as a wall: (100)^a 10 [1001010 (010)^(g_i)]_i 100101. - From pause mode (n ≥ 1) it is rule PO: 0^inf (100)^n 1 A>(001)^p 00 D(2^N-2) RC → 0^inf (100)^n Zn(p) 1001 [Zn(g_i) 1001]_i 01 A> 00 RC'. This comes from Inc_L(j = 0), B1, then OvR with left context (100)^(n-1) 1000. - μ = E → S. BS 1001010010010 <E → <E 0010001100100 restores the gap-2 digit with bit 0 and reads nothing to its right. Then [L1^(g_i), L2] for i = k..1, then L1^a and L3 bring F to the cell left of the lead, as in Inc_L. - From normal mode, END gives rule SILENT: X(...) → K_N(a+1; D_G(0); RC') with the gap-2 digit kept. The counter wraps and there is no pause. - From pause mode, END gives rule SILENTP: (100)^n 1 A>(001)^p 00 D(2^N-2) → (100)^(n-1) 1 A>(001)^(p+1) 00 D(0), for n ≥ 1.

The new right counter RC' (the word after the lead 00, minus the gap-2 digit, which is rebuilt by the first ZX after N and kept after S). Write q = 2r + H. From RB, μ_i alternates. - N (μ = F, so μ_1 = E): RC' = u_0 u_1 ... u_q w. The first tokens are 00 at even indices and 01 at odd indices (u_0 = 00100, t_1 set to 01 by BN, and for i ≥ 2, t_i = 01 iff μ_(i−1) = F iff i is odd). The first token of w is 01 if q is even (UF on u_q, or BN when q = 0; here σ = μ_q = F) and is F'(f)'s own first token if q is odd (σ = E). So w = F''(f) of (T3). - The pairs (u_0 u_1), (u_2 u_3), ... are 00100 01100 = 0010001 100 = d(0) Z, R digits with bit 0 at gap 1. - q odd (H = 1): q + 1 units pair up, so r' = (q+1)/2 = r + 1 and H' = 0, and the tail starts at F''(f) with x' = 1 by (T4). - q even (H = 0): u_q = 00100 and the 01 after it form the half digit 0010001, so r' = q/2 = r and H' = 1. That 01 is also x' = 1. - Either way 2r' + H' = q + 1, H' = 1 − H, and the emission is e = (r'+H') − (r+H) = 1 − H. - S* (μ = E, so μ_1 = F): RC' = u_1 ... u_q w, with first tokens 00 at odd i and 01 at even i. - By the class rule below, S needs y = H = 1. So q = 2r + 1 is odd, σ = μ_q = F, and the UF on u_q has set the first token of w to 01. Hence w = F''(f) again. - The pairs (u_1 u_2), ..., (u_(q−2) u_(q−1)) are d(0) Z. - u_q and the 01 after it form the half digit, and that 01 is x' = 1. - So r' = r, H' = 1 = H, and e = 0. - In both cases RC' is U^(2r'+H') W(f', e) except that every R digit has bit 0 (its bit token is 00, not 01). By the next overflow the counter has counted these bits up to 1 again, which is the form X needs. The end unit was never read, so e and m are unchanged.

Class rule. N ⇔ μ = F ⇔ σ(f) flipped 2r + y times is F. By (T2), y = 0 gives σ = F and so N. For y = 1, N ⇔ σ(f) = E. This is exactly the class of (T4) and does not depend on r. Check 6 compares it with full simulation for every f.

L* closure and the front unit. - Class N: x' = 1 and y' = 1 − y = H' (T4). - Class S: x' = 1 and y' = y = H = H' (T4).

So the new tail is in L*, and (y, z) → (y', z') is the TAILFRONT arrow, with emission e = 1 − y for N and e = 0 for S. All of this holds for every r ≥ 0, every a and G, and both normal and pause context, because T(f) is a window lemma and RB, BN and BS are parametric.

4.4 ENDCARRY (f = 1^15; check 7)

After CF1, C reads the end unit (0e_1)...(0e_m) 01. Let j = the number of leading 1s of e, with j := m + 1 when all m bits are 1. In that case the end marker 01 counts as one more 1, R7 writes a new marker on the blank cells, and m grows by 1.

R6^j, R7, then the processed tokens are restored right to left by alternating L3 (E→F, gives 00) and L3F (F→E, gives 01). The rightmost one is restored first, in mode E. So token i of the end unit (1 ≤ i ≤ j) becomes 00 if j − i is even and 01 if j − i is odd. The mode on the last cell of P1 is E for even j and F for odd j. - j even: PEN P1 <E → <E F(100100010001010). Then lemma RB with σ = E and w = F(100100010001010)·(end unit), q = 2r + 1 (H = y = 1), so μ = F and the result is N. The end bits become (10)^(j/2) 1 rest, f' = 100100010001010, H' = 0, e0. - j odd: PFN P1 <F → <F F(010000100100101), which never reads the end unit, so its first token stays 00 (e'_1 = 0). Then RB with σ = F: w = F(010000100100101)·(end unit) starts with 00, as RB needs. q = 2r + 1 is odd, so μ = E and the result is S. The UF on u_q sets the first token to 01, so f' = 110000100100101 and H' = H = 1, e0. The end bits become (01)^((j+1)/2) rest. - Both f' satisfy the conclusions of (T4) for y = 1: 11 →N,e0→ 00 and 11 →S→ 10. So ENDCARRY also closes L* and follows TAILFRONT.

Check 7 covers this for every end unit with m ≤ 10, in normal and in pause context (4,094 overflows), plus 300 random cases with m ≤ 40.

4.5 TAILFRONT and closure of L*

For every tail in L* and every r, a, G, in normal or pause context, the overflow is N or S with exactly the forms above. The new tail is again in L*, with m' = m except in the ENDCARRY growth case. The front unit and the emission follow:

TAILFRONT:   10 -N,e0-> 01 -N,e1-> 11 -N,e0-> 00 -N,e1-> 10,     11 -S,e0-> 10

S occurs only from front unit 11. - Proof: (T1)–(T4) for the 16,383 f ≠ 1^15 (check 5), lemma RB with the boundary analysis (§4.3), and ENDCARRY (§4.4). The only computation is the finite table; every statement over r, a, G and the context is parametric. - Confirmation by full simulation (check 6): one overflow for each of the 16,384 f in four settings: normal context with r = 0 and r = 3, pause context with r = 0 and r = 2. That is 65,536 overflows. Class, 2r' + H', L* closure, the untouched end unit and TAILFRONT all match. Plus 200 random pairs in which PO/SILENTP give the same new RC as NO/SILENT.

5. Macro dynamics and the invariant

5.1 Quantities at a configuration X(a; G; r, H; f, e)

• R := r + H, N = k + 1 + R, M = 2^N;
• Γ := Σ_(i=1..k) (g_i − 1)·2^(i−1);
• c := 2^(k+R) − 2^(k+1) − 2Γ − 4;
• s := a − c, κ := c − M/4.

5.2 One overflow and its pause, in closed form (proof.md rules only)

Slot rule. In a pause the wall is (100)^w 1 and each P100 cycle lowers w by 1 and adds 2 to v. Let the next overflow slot be cyc = (2^N − 2 − v)/2 cycles away. - If cyc ≤ w − 1, the slot is reached with wall (100)^(w−cyc) 1, where w − cyc ≥ 1, and value 2^N − 2. This is a PO slot: PO, or SILENTP, both need n ≥ 1. - If cyc ≥ w + 1, after w cycles the wall is the bare 1 and v + 2 < 2^N, so WX ends the pause. - If cyc = w, the slot would be reached with the bare wall 1. No rule covers this: PO and SILENTP need n ≥ 1, and WX needs v + 2 < 2^N. INV keeps every path away from it (§5.3, check 9c).

After NO with emission e: R' = R + e and M' = 2^e·M. - The first ZX (p = 0) creates the gap-2 digit. The zones are then rebuilt innermost first: for each zone, (g − 2) P010 cycles, then ZX (ZXN for the last one). Every gap is restored exactly. - After ZXN the counter value is v_0 = 2^(k+2) + 4Γ, the wall is (100)^(a−2) 1 and the lead is 0. - The pause then runs P100 cycles (+2 each). The next overflow slot comes after c' = (M' − 2 − v_0)/2 cycles; for e = 0 this is c' = c + 3. - By the slot rule with w = a − 2: if c' ≤ a − 3, the slot is a PO slot with p = c' and wall a − 2 − c' ≥ 1. If c' ≥ a − 1, WX ends the pause and Inc runs to the next normal-mode overflow. c' = a − 2 never occurs under INV.

After PO at inner lead p with emission e: the gap-2 digit and the zones of G are rebuilt as above. Then the zone Zn(p) is rebuilt: (p − 2) P010 cycles, then ZXP1 and ZXP2, which inserts the new gap p − 1. The wall drops by 3 (ZXP1 by 1, ZXP2 by 2). The value is 2(v_G + 2(p−2) + 2) + 2.

The four paths between consecutive normal-mode overflows, starting from front unit f. Each is a composition of the rules above (algebra below, all in terms of M and s):

The algebra: - S: SILENT gives lead a + 1 and counter 0. Then M − 1 Incs reach the next overflow at a + M, with G and R unchanged. - NO e0: p = c + 3, so PO#1 has wall s − 5 and inner lead p = c + 3. - PO#1 (e1): G'' = (c+2) ∪ G, R'' = R + 1, M'' = 4M. Using 2p = M − 2^(k+2) − 4Γ − 2, the value after ZXP2 is v_1 = 2M − 6. The wall is s − 8 and the lead 0. - The next slot comes after (4M − 2 − v_1)/2 = M + 2 cycles. - If M + 2 ≥ (s − 8) + 1, i.e. s ≤ M + 9: WX gives lead s − 7 and value v_1 + 2(s − 7). The next overflow is at a'' = 2M + 12 − s. With the new gaps, c'' = M + 2 (so κ'' = 2) and s'' = M + 10 − s. This is P1. - If M + 2 ≤ (s − 8) − 1, i.e. s ≥ M + 11: PO#2 is reached at p = M + 2 with wall s − M − 10 ≥ 1. Its front unit is 11. - s = M + 10 is the excluded case cyc = w. INV gives s ≤ M − 14 or s ≥ M + 24, so it never occurs. - S at PO#2 (SILENTP): p = M + 3, wall s − M − 11, value 0. The next slot is 2M − 1 ≥ (s − M − 11) + 1 cycles away (s ≤ 3M + 9), so WX gives lead s − 7 and value 2(s − M − 10). Then a'' = 6M + 12 − s and s'' = 5M + 10 − s. This is P1S. - e0 at PO#2: gap M + 1 is inserted, M''' = 8M, value 8M − 18, wall s − M − 13. The next slot is 8 ≤ (s − M − 13) − 1 cycles away (s ≥ M + 22): PO#3 at p = 8 with wall s − M − 21. Its front unit is 00, so the outcome is e1. - PO#3 (e1): gap 7 is inserted, M4 = 32M, value 16M − 18, wall s − M − 24 ≥ 0. The next slot is 8M + 8 ≥ (s − M − 24) + 1 cycles away, so WX follows. Then a'' = 17M + 40 − s, c'' = 8M + 8 (κ = 8) and s'' = 9M + 32 − s. This is P3.

5.3 The invariant

INV at a configuration X: M ≥ 256 (N ≥ 8), κ ∈ {2, 8}, all gaps ≥ 7, tail in L*, and

• f = 11 and 24 ≤ s ≤ M/4 + 2, or
• f = 10 and s ∈ [8, M − 14] ∪ [M + 24, 2M].

Notes on INV: - M ≥ 256 is preserved: M' ∈ {M, 4M, 32M} on every path, and the initial configuration has M = 256. - It is needed: the side conditions below use M ≥ 256 and c = M/4 + κ ≥ 66. Without it, INV as written would also admit N = 5 (k = 0, R = 4, κ = 2) and N = 7 configurations, where the written argument does not apply. (By direct simulation they also close, but the proof does not use them.) - It gives k ≥ 1. From c = M/4 + κ, Γ = 2^(N−3) − 2^k − 2 − κ/2. k = 0 needs Γ = 0, which means N = 5. So under INV there is at least one large-gap digit, and the last zone of every NO rebuild is a ZXN preceded by a ZX.

Which path runs (front unit and s decide; at a 11 slot both choices are covered):

Closure (images of the interval end points; every map has slope ±1; check 9b, exact, N = 8..400):

Side conditions that keep every rule inside its domain. They are linear in s, so the interval end points suffice. Check 9c checks them exactly for N = 8..400, both κ, all three intervals, with the three-way slot rule. Below, M ≥ 256 and c = M/4 + κ ≥ 66: - NO: a = s + c ≥ 74 ≥ 2 (ZXN needs n ≥ 2). - PO#1 slot: w = a − 2 and cyc = c + 3, so cyc ≤ w − 1 ⇔ s ≥ 6. PO#1 has p = c + 3 ≥ 69 and wall s − 5 ≥ 3 (ZXP1 n ≥ 3, ZXP2 n ≥ 2). - After PO#1: w = s − 8 and cyc = M + 2. WX for f = 11 and for f = 10 with s ≤ M − 14, since s ≤ M + 9. PO#2 for s ≥ M + 24, since s ≥ M + 11. - PO#2: p = M + 2 and wall s − M − 10 ≥ 14. - SILENTP at PO#2: wall s − M − 10 ≥ 14 ≥ 1. Afterwards WX, since 2M − 1 ≥ s − M − 10. - PO#3 slot: w = s − M − 13 and cyc = 8 ≤ w − 1. PO#3 has p = 8 and wall s − M − 21 ≥ 3. Afterwards WX, since 8M + 8 ≥ s − M − 23. - New gaps: c + 2 ≥ 68, M + 1 and 7 are all ≥ 7. So every ZX zone has g + 1 ≥ 8 ≥ 3 blocks, and every PO has p ≥ 8, so its zone Zn(p) is rebuilt by p − 2 ≥ 6 P010 cycles, then ZXP1 and ZXP2. - The rebuild never overflows. Let the slack be (2^N − 2 − v)/2, the number of +2 cycles left before the next slot. - A zone of gap g (g − 2 P010 cycles, then a ZX or ZXN that inserts gap g; the first ZX at lead 0 is the case g = 2) needs slack ≥ g − 1 before it. It leaves slack' = 2(slack − g + 2) − 1, since the ZX adds 2 and then doubles the value with one more digit. - The PO zone Zn(p) (p − 2 P010 cycles, ZXP1, then ZXP2, which adds 1 and doubles) needs slack ≥ p before it and leaves slack' = 2(slack − p + 1). - Inverting: slack before = (slack' + 2g − 3)/2 ≥ g − 1 ⇔ slack' ≥ 1, and slack before = slack'/2 + p − 1 ≥ p ⇔ slack' ≥ 2. - At the end of every rebuild the slack is the distance to the next slot: c + 3, M + 2, 8 or 8M + 8, all ≥ 8. Going backwards, every zone had enough slack. So no carry reaches the tail during a rebuild. - S inside a pause happens only at PO#2. PO#1 and PO#3 have front unit 01 or 00. After SILENTP the pause ends with WX before another slot (above).

Evidence for the path table: - Check 10, by direct simulation with no model in between. It builds a configuration in INV from (N, k, κ, G, f, s, tail), runs the real machine to the next normal-mode all-ones inner record, parses it, and requires INV there with exactly one predicted (path, M', s', κ', f'). - N = 8 exhaustive: all G, both κ, every s of all three intervals, 4,599 starts. - Random starts at N = 9..12, including interval end points, f = 1^15 and the tail 110111111111111. That tail becomes 1^15 after e0, e1 (T(f) table), so it forces ENDCARRY at PO#2. - Targeted ENDCARRY-at-PO#2 cases. - Continuous chains of several paths in one simulation. - The real orbit from the blank tape: records at steps 92,299, 1,006,516, 14,514,329 and 114,113,163, joined by paths P1, P1 and S. - Check 9a: compares the closed forms with the event-level model (scripts/deepen3_macro.py, built from the rules of §2–§4 only) on random front-unit sequences. Every transition matches, with no other path. - Check 9d: runs a DFS over all front-unit sequences.

6. Initial segment (check 8)

The first configuration in X ∩ INV is reached by direct simulation from the blank tape in 92,299 steps:

0^inf A>(001)^121 00 0110001 Z^28 0110001 Z^2 (0110001100)^5 01100 W(111111011110101, 010)

So a = 121, G = (28,), r = 5, H = 1, R = 6, N = 8, M = 256. The tail is in L* with m = 3, x = 1, H = y = 1, and the front unit is 11. Further c = 66, s = 55 ∈ [24, 66] and κ = 2.

Earlier all-ones normal-mode records exist (steps 230 … 17,206). Some are X-configurations outside INV, for example step 5,786 with G = () and s = 3. The proof does not use them: the initial segment is the exact 92,299-step run.

7. Conclusion

• Coverage. Every member of the invariant set takes one of the paths S, P1, P1S, P3, whatever the tail chooses at each 11 slot. Each path is a finite composition of rules (Inc, SILENT, NO, PO, SILENTP, P100, WX, P010, ZX, ZXN, ZXP1, ZXP2), each applied inside its domain (§5.3). Each path lands in the invariant set again. So the run never leaves the rule system.
• Progress. Every rule takes at least 2 steps, so each path takes at least 1 step: progress_nonhalt_cond applies with P = INV.
• Halting. The only halting transition is B reading 1, and B is entered only by A0 (1RB) and F1 (1LB). A halt would need the pattern A> 0 1 or a 1 directly left of an F that reads 1.
• Every rule above is an exact composition of window lemmas, finite table entries (T(f)) and parametric chains of them (Inc_L, lemma RB, the ENDCARRY alternation). Each of these runs to its stated end without halting (checks 2, 3, 5).
• So no halting transition is ever executed on the path from the blank tape: the initial segment (check 8) is an exact halt-free run, and after it only rules are used.
• Sanity reading: A0 and F1 fire only inside the window lemmas and the T(f) runs, and in each of these finite runs the following B reads 0 (it never halts). The typical cases are R2 (A0 on the left cell of a 00 token) and B1 (F1 on the 1 of a wall's 01 end, whose left neighbour is 0).

8. Evidence: check_proof.py

Run as python3 -B check_proof.py [--quick]; the log is work/check_proof.full.log. Checks 6, 7 and 10 use 2 worker processes.

The earlier stages also have this evidence, listed in notes.md: - rules 1050/1050 (scripts/deepen_rules.py); - the macro model reproduces the real run exactly to step 555,048,797; - 40,000 overflows of the RC chain; - closure for all bit settings with m ≤ 8 (scripts/deepen3_closure.c).

9. Lemma plan (Rocq)

No family template applies (SBCv2_6x2 tm108 was ruled out in the observe pass). The nearest pattern is CounterClass3v2.v, Module TM1: a hand-written multi-level counter with sweep lemmas, an E_stmt j induction on carry depth (E_all), Climb/Climbs, and Mac_* macro lemmas. Plan:

1. Tape words. Define Z, digits, D_G(v) as a function of a list of (bit, gap), Zn, U, and W(f, e) as list Sym. Prove lpow-style rewriting lemmas, copying lpow_* from TM1.
2. Window lemmas (§2.1): each is one es. The shift rules follow by ind on R4, L1 and L4.
3. Inc_L: induction on the carry depth j over the digit list. The statement is quantified over l (left side) and r, like TM1's E_stmt.
4. Pause rules: short follow chains (Inc_L, B1, Inc_L, END / ENDZX / BN).
5. Overflow, split as in §4: - OvR by follow/ind over digits and units; - T(f): the hard part, 16,383 window lemmas; - lemma RB (§4.3): induction on q with a mode parameter (UE/UF), carrying the 00-on-the-right precondition; - BN/BS; - ENDCARRY by induction on j (L3/L3F alternation).

Options for T(f), cheapest first: - (a) Prove one generic lemma forall f in L*\{1^15}, exists ... by a boolean checker over Fin 2^14 evaluated with vm_compute/native_compute, using a verified step function on lists. A home-made checker must be proved sound against TM.step, so this is a medium-size Rocq development. - (b) Split F(f) into its five units and prove per-unit sweep lemmas over tokens. This would replace the table with about 40 lemmas, but the decomposition has not been worked out. The tail's units are made of the same tokens, and T(f) behaves like a mixed-radix counter with carries, but the per-unit lemmas are not yet derived. - (c) 16k separate es lemmas, generated. Probably too slow. 6. TAILFRONT and closure: the finite facts (T1)–(T4) of §4.2, checked together with T(f) in (5a) or (5b). The rest (class rule, r', H', L* closure, emission) is the symbolic part of §4.3 and needs no computation. 7. Macro arithmetic: a Definition of the invariant on (a, G, R, f, e) as in §5.3, with the path lemmas as Mac_*-style compositions. lia handles the linear parts; powers of 2 enter as M (keep M = 2^N abstract and record only M ≥ 256, M divisible by 4). Never run CTL/NG-style searches inside Rocq. 8. init by solve_init (92,299 steps), then nonhalt via progress_nonhalt_cond, with P = INV plus the family shape.

10. Gaps (what a reviewer should still look at)

• T(f) and (T1)–(T4) are verified by exhaustive computation, not by hand. This is legitimate for a finite fact, but in Rocq it needs (5a) or (5b).
• The R-block return is lemma RB (§4.3), proved by induction on q. The boundary (BN/BS) and the re-parse of RC' are derived symbolically from it. TAILFRONT and L* closure then hold for every r from (T1)–(T4) alone. Check 6 confirms this by full simulation in four settings, two of them in pause context.
• The closed-form path algebra of §5.2 was derived by hand. A reviewer re-derived it independently. Check 10 tests it by direct simulation from INV configurations, N = 8 exhaustively, without the event-level model. Check 9a also compares it with that model.
• No step-count closed form for NO/PO/SILENT/SILENTP: it depends on the T(f) step count. It is not needed: progress only needs ≥ 1 step per rule.

Review log

• 2026-10-10 (informal_proof stage, first version).
• Built from the deepen-round results. New in this stage:
  • the token view and the full window-lemma set (§2.1);
  • Inc_L with a parametric proof;
  • every pause rule as an Inc_L/B1/END chain (ZX/ZXN share the 22-step ENDZX, and ZXP2 uses the overflow's BN);
  • T(f) is a context-free window lemma table: the head never reads the end unit unless f = 1^15. This replaces the round-3 "locality" observation with a proof by finite run;
  • the N/S decision is the parity of the UE/UF alternation over the R block (check 6: class = parity prediction for every f);
  • ENDCARRY decomposed into CF1, the L3/L3F alternation and PEN/PFN;
  • the path closed forms S/P1/P1S/P3 derived by hand (§5.2), including κ' = 2 after P1/P1S and κ' = 8 after P3.
• Corrections to round 3:
  • The first configuration in the invariant set is at step 92,299 (a = 121, r = 5, H = 1), not "the step-36,124 state". The round-3 START is the macro state of the first overflow after step 36,124, and it is the same configuration.
  • The ENDCARRY S case leaves x = 0 after PFN; the UF on the H unit restores x = 1.
• Open: the formalisation route for T(f) (§9 step 5). Checkpoint B not yet reviewed (see the next entry).
• 2026-10-10 (skeptic round 1). Verdict: sound, with 6 gaps, all minor. All six are fixed, and each fix was re-checked. 1. PFN was misstated as P1 <F 00 → <F F(010000100100101) 01.
  • It is the 73-cell window P1 <F → <F F(010000100100101), 123 steps, and it never reads the cell right of P1.
  • The old form would have set e_1 = 1 in the j-odd ENDCARRY case, contradicting §4.4's own result.
  • Fixed in §2.1 and §4.4. §4.4 now also says which end-unit token gets which value.
  • Check 2 now compares the full output word of every window lemma, PEN and PFN included. It runs PEN/PFN on the bare 73-cell window and also with each of the four 2-cell right contexts, which stay unchanged. 2. F(f) is 73 cells, not 75 (§1.2, §4.2, check 5's message). 3. INV now includes M ≥ 256.
  • It is preserved (M' ∈ {M, 4M, 32M}), and the initial configuration has M = 256.
  • §5.3 says why it is needed (the side conditions use c ≥ 66) and that it gives k ≥ 1.
  • Checks 9 and 10 use it. 4. Slot boundaries. §5.2 now has a three-way slot rule: PO iff cyc ≤ w − 1, WX iff cyc ≥ w + 1, and cyc = w (bare wall 1 at the slot) is covered by no rule.
  • After NO: PO iff c' ≤ a − 3, WX iff c' ≥ a − 1.
  • After PO#1: WX iff s ≤ M + 9, PO#2 iff s ≥ M + 11.
  • INV keeps every path off the excluded cases (s ≥ 8, and s ∉ [M − 13, M + 23]).
  • The side conditions in §5.3 are rewritten with the slot rule, and check 9c now tests the three-way rule at every step of every path. 5. Lemma RB is written out (§4.3).
  • It is the UE/UF alternation over P^q, proved by induction on q. The 00-on-the-right precondition is carried by the induction, and the output tokens are given explicitly.
  • The boundary is explicit: BN re-tokenises the processed gap-2 digit into the lead 00 plus a new unit u_0, which is why R grows leftward. BS reads nothing to its right.
  • The re-parse of RC' (r', H', x', emission) is derived symbolically for both classes and both parities of q.
  • TAILFRONT and L* closure for every r now follow from four finite facts (T1)–(T4) of the T(f) table (§4.2). Check 5 verifies these facts for all 16,383 f ≠ 1^15.
  • Check 6 now runs all 16,384 f in four settings (normal context r = 0 and r = 3, pause context r = 0 and r = 2): 65,536 overflows. It also checks 2r' + H' against RB and that the end unit is untouched.
  • Check 7 is now exhaustive for every end unit with m ≤ 10 in both contexts: 4,094 cases, plus 300 random. 6. New check 10: whole paths by plain direct simulation, with no model in between. The C core scripts/check_direct_sim.c is ported from the reviewer's simulator.
  • It builds X ∩ INV from (N, k, κ, G, f, s, tail), runs the real machine to the next normal-mode all-ones inner record, and requires INV there with exactly one predicted (path, M', s', κ', f').
  • Results:
  • N = 8 exhaustive (all G, both κ, every s of the three intervals): 4,599/4,599.
  • Random N = 9..12, including end points, f = 1^15 and the ENDCARRY-at-PO#2 tail 110111111111111: 172/172.
  • Targeted ENDCARRY at PO#2: 72/72. j odd gives P1S, j even gives P3, growth included.
  • 6 continuous chains from N = 8: 6/6.
  • The real orbit: records at 92,299, 1,006,516, 14,514,329 and 114,113,163, joined by paths P1, P1 and S.
• Also tightened (not raised by the reviewer). The rebuild-slack argument in §5.3 now covers the PO zone (ZXP1/ZXP2: slack before = slack'/2 + p − 1) and all four rebuild ends (final slack c + 3, M + 2, 8 or 8M + 8), not only the NO rebuild.
• Re-run. check_proof.py 10/10 PASS (full run 7 min 50 s with 2 workers; work/check_proof.full.log). The previous log is kept as work/check_proof.full.prev.log, and the pre-revision proof.md as work/proof.pre-skeptic1.md.
• Open. Formalisation only: the Rocq route for the T(f) table and (T1)–(T4) (§9 step 5). No fatal or major gap is known. Status: CHECKPOINT_B.