1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---: never halts

• Machine: 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, viewer https://bbchallenge.org/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---
• Holdout: on the current BB(6) holdout list (class "Skelet 1-like Class 2").
• Written for: the string itself. There is no mirror or state permutation.
• Template: verify/SBCv6.v, Module TM21 (1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE), a binary counter over a list of digit pairs with a re-pairing overflow. The transition tables are not close: under the best state renaming, 10 of the 12 transitions differ. So the .v follows TM21's architecture, not its lemmas. §6 lists what is kept and what is new.
• Status: fully formalized. The accompanying 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v (694 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c). It compiles in about 9 s, Print Assumptions nonhalt is closed, and coqchk passes.
• Where each section lives in the .v: §2.1 S1–S6, T1–T14, Lb, Lf, Rb, Ro; §2.2 chunkA, LbS, RbS, chunkC, M_spec, Mdrop_spec; §2.3 RoS, chunkO, Oz, Oout, O_spec; §3 INV, PA, PB, Rof; §3.1 Rof_bound, Rof_head0/Rof_head1 (F0), F1, F2, Oz_R, Oz_AB, Oz_CA (F3); §3.2 decomp; §3.3 step; §4 init; §5 nonhalt. §6 has the full table.

Summary. At the right edge the tape is K(d_1 .. d_m; a, b) (§1): a binary counter whose digits are the blocks (10)^u 00 (01)^v (bit 0) and (10)^u (01)^v (bit 1), followed by a block (10)^a 0^3 (10)^b. Two macro rules, each an exact run composed of 20 window lemmas (§2), move the tape from one such configuration to the next: - M (carry) adds 1 to the counter. Every digit it touches pays one 01 from its v, and the digit flipped 0→1 also gains a 10. A flipped digit with no 01 left merges into the next digit (a drop), and the counter loses a digit. - O (overflow), when all bits are 1, swaps the two halves of every digit. The counter restarts at 1 with one more digit.

The rules fail only if a carry reaches a bit-0 digit with no 01 left. The proof is a per-step invariant INV = Common ∧ (A ∨ B ∨ C) (§3) that follows the counter through three phases: a cycle with no drops (A), a cycle whose top digit is about to fall (B), and the rest of that cycle (C). It is stated through R_j, the number of carries still to come into digit j before the next overflow if no digit above it drops. Its clauses are parities, fuel bounds v_j ≥ R_j + 1 and lower bounds 2^j. They exclude the failure case, and four arithmetic facts F0–F3 (§3.1) show that M and O keep INV. Which digits drop when is irregular, but the invariant never needs to know. The run enters INV at step 483 (§4), and progress_nonhalt_cond with P := INV concludes (§5).

1. Family and notation

K(d_1 .. d_m ; a, b) := 0^inf 10 01  d_1 d_2 .. d_m  (10)^a 0^3 (10)^b  B> 0^inf

digit d = (u, beta, v):   (u,0,v) := (10)^u 00 (01)^v        "bit 0"
                          (u,1,v) := (10)^u (01)^v           "bit 1"

• d_1 is next to the fixed leading 10 01. d_m is next to the right-hand block and is the least significant bit. m ≥ 1.
• Canonical form. Every digit has v ≥ 1, and every bit-1 digit has u ≥ 1. Bit-0 digits may have u = 0. INV states are canonical, because Common (§3) requires it, and M and O map INV states to canonical states (§3.3). This does not hold outside INV: M turns a bit-1 digit with v = 1 into (u,0,0), which is not canonical. That digit is the precursor of the failure mode (§2.4).
• Re-reading (no machine steps). A bit-1 digit with v = 0 is just (10)^u, so it fuses with what follows. Followed by (u',β',v'), it becomes (u+u', β', v'). If it is last, it joins the block: a := a + u. We call this a drop of that digit.

Derived quantities. They are used only in the invariant, not in the rules. All are exact integers.

bits beta_1..beta_m, read as a binary number with beta_m least significant:
U_j  = (beta_1 .. beta_j)_2        V = U_m          R_tot = 2^m - 1 - V
R_j  = 2^j - 1 - U_j               carries that will still touch d_j before the next overflow, if no digit above it drops
R1_j = (R_j + 1 - beta_j) / 2      how many of those set d_j to 1   (R_j ≡ 1 + beta_j mod 2)
ubar_j = u_j + R1_j                vbar_j = v_j - R_j               u_j, v_j as they will be at the next overflow
S = a + R_tot - (2^(m+1) - 2)      T = b - (2V - 1)

§6 gives the same definitions in additive form, with no subtraction or division, as the .v states them.

2. Rules

Transition table:

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

The macro rules, in busycoq comment-block style:

1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---

start from K((1,1,2); 8, 5)                                   (step 483, §4)

M  (carry; some bit is 0; j* = index of the LAST bit-0 digit, k = m - j*):
   K(.., (u,0,v), (u_j,1,v_j)_{j*<j<=m}; a, b)
     --> K(.., (u+1,1,v-1), (u_j,0,v_j-1)_{j*<j<=m}; a+1, b+2)
   steps 32 + 8a + 8b + 4v + sum_{j>j*} (8 u_j + 4 v_j)
   needs v >= 1 (u >= 0), u_j >= 1 and v_j >= 1 for j > j*, a >= 0, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, §1)
O  (overflow; all bits 1):
   K((u_1,1,v_1) .. (u_m,1,v_m); a, b)
     --> K((0,0,u_1), (v_1-1,0,u_2), .., (v_{m-1}-1,0,u_m), (v_m,1,a); b+3, 1)
   steps 89 - 4m + 8a + 20b + 4 sum u_j + 8 sum v_j
   needs m >= 1, all u_j, v_j >= 1, a >= 1, b >= 0

On the tape, O's right side is 0^inf 10 01 00 (01)^u_1 [(10)^(v_i-1) 00 (01)^u_(i+1)]_{i<m} (10)^v_m (01)^a (10)^(b+3) 0^3 10 B> 0^inf.

M and O are derived from the 20 window lemmas of §2.1, as chains of intermediate configurations (§2.2, §2.3). Each step count above is the sum along the chain. M needs only a ≥ 0; Common has a ≥ 1 anyway. The .v proves the chains as -->+ statements (M_spec, Mdrop_spec, O_spec), so the step counts are not part of the formal statement.

2.1 Building blocks

Notation. X> means the head is in state X on the next cell, and <X means it is in state X on the previous cell (busycoq's {{X}}> and <{{X}}). A window lemma w → w' means: started on the cells of w, the machine runs the stated number of steps without reading a cell outside w (the last step may move the head onto a neighbouring cell), and leaves w'. Such a lemma holds in every tape context. T1–T14 are exact finite runs (in the .v, each is one es). S1–S6 are proved for one block by a finite run, and induction on n gives every n (in the .v, shift_rule_R/shift_rule_L, and plain induction for S5). For example, C> 11 (01)^(n+1) = C> 11 01 (01)^n → 10 C> 11 (01)^n → 10 (10)^n C> 11.

Shift lemmas:

S5 and S6 are the 2-cell back-bounces: on each block the head steps two cells right, two left and two right again.

Finite lemmas:

Digit lemmas (compositions; u, v of one digit):

In Ro, S6 starts on the last 0 of (10)^u = (10)^(u−1) 1 0. Lb sweeps a bit-1 digit leftward. Lf flips the bit-0 digit. Rb restores a swept digit as bit 0 on the way back in M. Ro does the same in O.

2.2 Derivation of M

Write X for everything left of d_{j*} (it is never read), (u*, v*) for d_{j*} = (u*,0,v*), and Y = Π_{i=1..k} (10)^u_i (01)^v_i for the trailing bit-1 digits (i = 1 is j*+1).

                                                                                        steps
    X (10)^u* 00 (01)^v* Y (10)^a 000 (10)^b B> 0^inf
 Phase 1: right-edge preamble with a dip into the 0^3 gap                               4b+10
T1  .. Y (10)^a 000 (10)^b <E 01                                                        3
S4  .. Y (10)^a 000 <E (01)^(b+1)                                                       2b
T2  .. Y (10)^a 100 B> (01)^(b+1)                                                       5
S1  .. Y (10)^(a+1) 0 (10)^(b+1) B> 0^inf                                               2b+2
 Phase 2: one long left sweep, down to the 00 of d_{j*}                                 2a+2b+9+4v*+Σ(2u_i+2v_i)
T1  .. Y (10)^(a+1) 0 (10)^(b+1) <E 01                                                  3
S4  .. Y (10)^(a+1) 0 <E (01)^(b+2)                                                     2b+2
T3  .. Y (10)^a <E 011 (01)^(b+2)                                                       3
S4  X (10)^u* 00 (01)^v* Y <E (01)^a 011 (01)^(b+2)                                     2a
Lb  X (10)^u* 00 (01)^v* <E Y' (01)^a 011 (01)^(b+2)       (i = k down to 1)            Σ(2u_i+2v_i)
                         Y' = Π_i (01)^u_i (10)^(v_i−1) 11
Lf  X (10)^(u*+1) (01)^(v*−1) C> 11 Y' (01)^a 011 (01)^(b+2)                            4v*+1
 Phase 3: rightward pass with 2-cell back-bounces, then a plain run to the edge         6a+2b+13+Σ(6u_i+2v_i)
Rb  X (10)^(u*+1) (01)^(v*−1) Y'' C> 11 (01)^a 011 (01)^(b+2)   (i = 1 up to k)         Σ(6u_i+2v_i)
                         Y'' = Π_i (10)^u_i 00 (01)^(v_i−1)
S5  .. Y'' (10)^a C> 11 011 (01)^(b+2)                                                  6a
T8  .. Y'' (10)^a 10000 B> (01)^(b+2)                                                   9
S1  X (10)^(u*+1) (01)^(v*−1) Y'' (10)^(a+1) 000 (10)^(b+2) B> 0^inf                    2b+4

The last line is K(.., (u*+1,1,v*−1), (u_i,0,v_i−1)_i; a+1, b+2). The sum is (4b+10) + (2a+2b+9+4v*) + (6a+2b+13) + Σ(8u_i+4v_i) = 32 + 8a + 8b + 4v* + Σ(8u_i+4v_i).

Head path. Phase 1 runs left only to the 0^3 gap, turns (T2) and returns to the edge. Phase 2 is the only long leftward leg. Its leftmost read is the first 0 of d_{j*}'s 00 (T6 reads both cells, then moves right). So M is a side rule: the tape X left of that 00 is never read. Phase 3 moves right. It steps back two cells once per 01 block (S5, on the (01)^u_i blocks and on (01)^a), and it crosses the (10)^(v−1) blocks and the final (01)^(b+2) with plain sweeps (S2, S1). When v* = 1, the flipped digit (u*+1,1,0) drops (§1). When some v_i = 1, the result has (u_i,0,0). That can happen only outside INV (§3.3).

2.3 Derivation of O

Let Y = Π_{i=1..m} (10)^u_i (01)^v_i, with all digits bit 1.

                                                                                        steps
    0^inf 10 01 Y (10)^a 000 (10)^b B> 0^inf
 Phases 1–2 as in M, with Lb on all m digits and no Lf                                  (4b+10)+(2a+2b+8)+Σ(2u_i+2v_i)
    0^inf 10 01 <E Y' (01)^a 011 (01)^(b+2)                Y' = Π_i (01)^u_i (10)^(v_i−1) 11
 Phase 3: turn at the far left
T9  0^inf 10 01 000 B> Y' (01)^a 011 (01)^(b+2)                                         13
 Phase 4: rightward pass
Ro  0^inf 10 01 000 Y''' B> (01)^a 011 (01)^(b+2)          (i = 1 up to m)              Σ(2u_i+6v_i−4)
                         Y''' = Π_i (10)^(u_i−1) 1 (10)^(v_i−1) 000
 Phase 5: right end                                                                     2a+8b+30
S1  .. Y''' (10)^a B> 011 (01)^(b+2)                                                    2a
T11 .. Y''' (10)^a 1 C> 11 (01)^(b+2)                                                   1
S5  .. Y''' (10)^a 1 (10)^(b+2) C> 11 0^inf                                             6b+12
T12 .. Y''' (10)^a 1 (10)^(b+2) <E 01101 0^inf                                          13
S4  .. Y''' (10)^a 1 <E (01)^(b+2) 01101                                                2b+4
 Phase 6: short left sweep over the a block, back to the 000 that Ro left after d_m    2a+1
T13 .. Y''' (10)^(a−1) <E 011 (01)^(b+2) 01101                                          3
S4  .. (10)^(v_m−1) 000 <E (01)^a 1 (01)^(b+2) 01101                                    2a−2
 Phase 7: turn in that 000, final run to the edge                                       2a+6b+27
T2  .. (10)^(v_m−1) 100 B> (01)^a (10)^(b+3) 1101          (1 (01)^(b+2) 0 = (10)^(b+3))  5
S1  .. (10)^(v_m−1) 100 (10)^a B> (10)^(b+3) 1101                                       2a
S6  .. (10)^(v_m−1) 100 (10)^(a−1) 1 (10)^(b+3) 0 B> 1101                               6b+18
T14 .. (10)^(v_m−1) 100 (10)^(a−1) 1 (10)^(b+3) 000 10 B> 0^inf                         4

Re-read the final tape with 0 (10)^(n−1) 1 = (01)^n and (10)^(v_m−1) 10 = (10)^v_m:

0^inf 10 01 000 Π_{i<m}[(10)^(u_i−1) 1 (10)^(v_i−1) 000] (10)^(u_m−1) 1 (10)^(v_m−1) 100 (10)^(a−1) 1 (10)^(b+3) 000 10 B>
  = 0^inf 10 01 00 (01)^u_1 [(10)^(v_i−1) 00 (01)^u_(i+1)]_{i<m} (10)^v_m (01)^a (10)^(b+3) 000 10 B> 0^inf
  = K((0,0,u_1), (v_1−1,0,u_2), .., (v_{m−1}−1,0,u_m), (v_m,1,a); b+3, 1)

The sum is (4b+10) + (2a+2b+8) + 13 + (2a+8b+30) + (2a+1) + (2a+6b+27) + Σ(4u_i+8v_i−4) = 89 − 4m + 8a + 20b + 4Σu_i + 8Σv_i.

The domain: Lb and Ro need u_i, v_i ≥ 1. T13 and the S6 of phase 7 use the last 10 of (10)^a, so a ≥ 1. T9 needs 0^inf on the left. O has two leftward legs: the long phase 2, which T9 ends 3 cells left of the leading 10 01 (so the leftmost cell visited moves 3 cells per overflow), and the short phase 6.

2.4 What the rules do, in words

The digits form a binary counter. Each M is one increment. It flips the trailing 1s to 0 and the last 0 to 1, and every digit it touches pays one 01 from its v. A digit flipping 0→1 also gains a 10. When all bits are 1, O swaps the two halves of every digit: each (10)^u becomes the (01)^u fuel of a new bit-0 digit, and each (01)^v becomes the next digit's (10)^(v-1). The counter restarts at value 1 with one more digit. When a digit flipping 0→1 has spent its last 01 (v = 1), it drops: its 10s merge into the next digit, and the counter loses that digit. The only way the rules can fail is the failure mode: a carry arriving at a bit-0 digit with v = 0, where Lf's first lemma T4 has no 01 to read. That happens if a carry flips a bit-1 digit with v = 1 to 0.

Every macro step is an exact run of at least 32 steps, so every macro step makes progress.

3. Invariant: closure and coverage

INV(D; a, b) := Common ∧ (A ∨ B ∨ C). The three classes are told apart by the top digit d_1.

• Common:
• m ≥ 1, and the tape is canonical (every v_j ≥ 1, every bit-1 u_j ≥ 1);
• a ≥ 1, b odd, a + R_tot even;
• S ≥ 0, T ≥ 0;
• vbar_m ≥ 1 (the LSB never runs out).
• A (quiet cycle):
• d_1 = (0,0,v) with v ≥ 2, or d_1 = (1,1,v);
• for all j, vbar_j ≥ 1 and ubar_j is odd;
• S ≥ 1.
• B (top about to fall):
• d_1 = (0,0,1);
• for all j, v_j + beta_j is odd ("safe parity");
• for j ≥ 2, ubar_j ≥ 2^(j-1).
• C (top has fallen):
• for all j, v_j + beta_j is odd and ubar_j ≥ 2^j;
• S ≥ 1, T ≥ 2.

The run cycles A → B → C → A. A is a cycle with no drops. B is the next cycle, whose top digit (0,0,1) falls at its first touch and is absorbed by the digit below. C is the rest of that cycle. Seen at the overflows, the phases alternate: all u odd (end of A), then all v even (end of C).

3.1 Four arithmetic facts (they follow from the rules alone)

F0 (prefix bound). 0 ≤ U_j ≤ 2^j − 1, so R_j ≥ 0, and R_j ≡ 1 + beta_j (mod 2). If some bit beta_i = 0 with i ≤ j, then U_j ≤ 2^j − 2, so R_j ≥ 1. With the parity: - a bit-0 digit then has R_j odd, so R_j ≥ 1; - a bit-1 digit then has R_j even, so R_j ≥ 2.

In an M step every touched digit j ≥ j* has the bit-0 digit j* in its prefix, so F0 applies to all of them.

F1 (touch). In an M step every digit j ≥ j* is touched. Its prefix value U_j grows by exactly 1, because bits j*..j go from 01..1 to 10..0, so R_j drops by 1. - A 1→0 touch: v−1, R1 unchanged. - A 0→1 touch: u+1, v−1, R1−1.

So ubar_j and vbar_j are unchanged, and v_j + beta_j keeps its parity. Digits j < j* are untouched and unchanged. M also gives a+1, b+2, V+1, R_tot−1, so a + R_tot, S and T are unchanged.

F2 (drop of d_{j}, j < m). Let H = U_{j*−1}. Digits above j* are unchanged. A digit j > j* moves to index j−1. Compare its new R', R1' with the values R°, R1° that F1 alone would give:

R° − R' = 2^(j−j*) · (2^(j*−1) − 1 − H) ≥ 0                 (so vbar only grows)
2·R1'   = R1° + 2^(j−j*−1)            for j ≥ j*+2  ⇒  ubar' ≥ ubar/2 + 2^(j−j*−2)
absorber j = j*+1:  u' = u_{j*+1} + u_{j*} + 1,  R1' = R1_{j*}  ⇒  ubar' = u_{j*+1} + ubar_{j*} + 1 ≥ ubar_{j*} + 1
if j* = 1 (H = 0):  R' = R°, R1' = R1°   (a falling top changes nothing below except the indices)

Here ubar_{j*} is the dropper's value before the step. A drop also changes the global quantities: - V' = H·2^(m−j*), so T grows by 2(H+1)2^(m−j*) ≥ 2; - S grows by 2^(m−1) + (H+1)2^(m−j*) ≥ 2; - R_tot' and R°_tot are both odd, so a + R_tot keeps its parity.

F3 (overflow). At an all-ones state, R = R1 = 0, so ubar = u, vbar = v, V = 2^m − 1 and R_tot = 0. After O there are m+1 digits and V' = 1:

j = 1:        ubar' = 1                    vbar' = u_1 − 1
2 ≤ j ≤ m:    ubar' = v_{j−1} − 1 + 2^(j−1)   vbar' = u_j − (2^j − 1)
j = m+1:      ubar' = v_m + 2^m − 1        vbar' = a − (2^(m+1) − 2)
a' + R_tot' = b + 1 + 2^(m+1)  (even)      T' = 0      S' = b + 3 − 2^(m+1) = T (the T before O)

3.2 Coverage (a rule always applies)

Take an INV state. - Not all bits 1: M applies. It needs v_j ≥ 1 (j ≥ j), u_j ≥ 1 (j > j), a ≥ 0 and b ≥ 0, all in Common. In particular, Common's v_{j*} ≥ 1 is exactly what rules out the failure mode. - All bits 1: O applies (m ≥ 1, all u, v ≥ 1, a ≥ 1).

There is no case split beyond M/O.

3.3 Closure (each case)

M keeps Common. - A digit touched 1→0 has v ≥ 2, so its new v ≥ 1. In A, vbar ≥ 1 gives v ≥ R+1, and F0 gives R ≥ 2, so v ≥ 3. In B/C, v + 1 is odd, so v is even and ≥ 2. - The 0→1 digit either keeps v ≥ 1 or drops. - The LSB never drops. A 0→1 touch of d_m has R_m ≥ 1 (F0), and vbar_m ≥ 1 then gives v_m ≥ 2. So every drop has j* < m, an absorber exists, and m' = m−1 ≥ 1. - The flipped digit gets u+1 ≥ 1. - The rest follows from F1/F2.

A, M step → A. No drop is possible: the 0→1 digit has R ≥ 1 (F0) and vbar ≥ 1, so v ≥ R+1 ≥ 2. F1 keeps every vbar, ubar and S. A top (0,0,v≥2) may become (1,1,v−1) with v−1 ≥ 1. A top (1,1,v) is never touched by M, because the carry stops at the last 0, which lies below it.

B, M step. - j ≥ 2 → B. - Parity is kept by F1. - A non-absorber has ubar' ≥ 2^(j−2) + 2^(j−j*−2) ≥ 2^((j−1)−1). - The absorber has ubar' ≥ ubar_{j*} + 1 ≥ 2^(j*−1). - d_1 is unchanged. - j = 1 → C. The top (0,0,1) flips with v = 1 and falls. - By F2 with H = 0, every other digit keeps its ubar and loses one index, so ubar ≥ 2^(j−1) = 2^(new j). - The new d_1 is the absorber: ubar' = u + ubar_top + 1 = u + 2 ≥ 2. - S grows by 2^m ≥ 2, so S ≥ 1. T grows by 2^m ≥ 4, so T ≥ 2. - B never reaches all-ones (beta_1 = 0), and B has m ≥ 2 (if m = 1, vbar_1 = 0).

C, M step → C. - Parity is kept by F1. - A non-absorber below a drop has ubar' ≥ ubar/2 ≥ 2^(j−1). - The absorber has ubar' ≥ ubar_{j*} + 1 > 2^(j*). This covers j* = 1, a second top fall. - S and T only grow.

A, O step → B. At all-ones the top is (1,1,v), so u_1 = 1 and the new top is (0,0,1). Safe parity: - the top: v = 1, bit 0; - j ≤ m: v = u_j = ubar_j, odd, bit 0; - the LSB: v = a, even because a + R_tot is even with R_tot = 0, bit 1.

Bounds and Common: - ubar' = v_{j−1} − 1 + 2^(j−1) ≥ 2^(j−1), and for the LSB v_m + 2^m − 1 ≥ 2^m. - S' = T ≥ 0. - vbar'_{m+1} = a − 2^(m+1) + 2 ≥ 1, because S ≥ 1 means a ≥ 2^(m+1) − 1. - b' = 1, a' = b+3, and every new v ≥ 1.

C, O step → A. - u_j = ubar_j ≥ 2^j, so the new top is (0,0,u_1) with u_1 ≥ 2. - vbar': u_1 − 1 ≥ 1, u_j − 2^j + 1 ≥ 1, and a − 2^(m+1) + 2 ≥ 1 (from S ≥ 1). - ubar' is odd: 1, v_{j−1} − 1 + 2^(j−1) and v_m + 2^m − 1 are all odd, because every v is even (from v + 1 odd) and j ≥ 2. - S' = T ≥ 2 ≥ 1.

So INV is closed under the macro step, and every INV state has a macro step.

4. Initial segment

0^inf A> 0^inf  --142-->  K((3,1,1); 2, 1)  --O, M, M (141+100+100 steps)-->  K((1,1,2); 8, 5)     (step 483)

The chain is O, then M with j* = 1, then M with j* = 2. The last M is an LSB drop: (1,0,1) flips with v = 1 and joins a (a = 5 + 1 + 2: one 10 from M, two from the dropped digit). K((1,1,2); 8, 5) is in class A: - top (1,1,2); - vbar_1 = 2, ubar_1 = 1; - S = 6, T = 4; - a + R_tot = 8, b = 5.

The earlier K-configs at steps 142, 283 and 383 are not in INV, which is why the initial segment stops at 483. In the .v this is init : c0 -->* K [d1 1 2] 8 5, proved by running all 483 steps at once (solve_init); the O, M, M decomposition above is for orientation only.

Other starts of the same table. Started in B on the blank tape, the same table reaches K((1,1,10); 8, 1) at step 732. Started in C, it reaches K((1,1,9); 8, 1) at step 687. Started in D, it reaches K((1,1,3); 4, 1) at step 215. All three are in class A, so the argument of §3 also covers the three other holdouts with this table: - 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---, started in our B (states renamed A..F → E,A,B,C,D,F, no mirror); - 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---, started in our C (mirrored, states renamed A..F → C,D,A,B,E,F); - 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, started in our D (mirrored, states renamed A..F → B,C,D,A,E,F).

Each is a separate TM_from_str; a formal proof for any of them restates the window lemmas under the renaming or on mirrored tapes, and each has its own .v. The accompanying .v covers only 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.

5. Conclusion

The run reaches an INV state (§4). Every INV state has a rule (§3.2). Every rule is an exact run of at least 32 steps, composed of the window lemmas of §2.1 (§2.2, §2.3), and every result is again in INV (§3.3). By the progress theorem the machine never halts. In the .v this is nonhalt: multistep_nonhalt with init, then progress_nonhalt_cond with P := INV and the closure lemma step : INV s -> exists s', Kc s -->+ Kc s' /\ INV s'.

Why --- (F reading 1) is never used. Every step of the run, after the 483-step initial segment, lies inside one of the 20 window lemmas. F is entered only in T4, T9 and T13, each time by E1, and each time F reads 0 (the transition lists in §2.1). The initial segment is a finite run that does not halt either. We claim nothing about tapes outside the family; INV keeps the run inside it.

6. Mapping to busycoq

The template, TM21

• K is built on the Fixpoint app_ds over a list of digits dg, as TM21's LC0/LC1 over (n, m) pairs, but every digit carries its own bit (d0 u v, d1 u v). The list is least significant digit first. The near block becomes (10)^a 0^3 (10)^b, a fixed right side.
• Overflow. O is a list re-pairing (Oz/Oout), proved by list induction (RoS, Ozeq, O_spec), following TM21's Ov/Ov_spec. T9 runs on 0inf.
• Carry. TM21's LIncs_spec is not a per-carry lemma. It takes an all-C0 list to an all-C1 list over a whole counter cycle (k = 2^len − 1 increments, sideRLs on tm' = flip tm with hLR2^^k). TM21 has no per-carry lemma, so the per-carry M lemma here is new. M_spec is Lb by induction over the list of trailing bit-1 digits (LbS, phase 2), then Lf, then Rb by induction over the same list (RbS, phase 3), with an arbitrary left side X. This follows the pattern of LIncs_spec's inner induction (C0 n (k+m) → C1 (k+n) m, by segRLs_trans and lpow_add). Drops are tape equalities only (lpow_add), with no steps: Mdrop_spec is M_spec followed by one.
• Window lemmas are direct es runs on tm, extended by shift_rule_R/shift_rule_L (S5 by induction), not flip/sideRLs.
• Macro step and invariant. TM21 iterates a whole-cycle BigStep under LWF, which bounds each pair by 2^(length x) ≤ m. Here drops happen at data-dependent times, so a cycle has no closed form, and no such per-pair bound holds, because digits run out and merge. The macro step is therefore one M, one M with a drop, or one O, and the invariant is the per-step INV of §3: digits carry a bit, and INV has three phases with parity conditions and 2^j bounds.
• nonhalt uses multistep_nonhalt + progress_nonhalt_cond with P := INV on macro states (ds, a, b), as TM21 does with LWF.

The .v is 694 lines, about 2.25 times TM21's 308.

INV without truncating subtraction

In nat, v − R, S, T and the division in R1 would truncate silently. Every clause of INV has an additive form: - R_j + U_j + 1 = 2^j; - 2·R1_j + beta_j = R_j + 1 (both sides exact, because R_j ≥ 0 and R_j ≡ 1 + beta_j); - R_tot + V + 1 = 2^m; - vbar_j ≥ 1 ⟺ v_j ≥ R_j + 1; - ubar_j odd ⟺ u_j + R1_j odd; ubar_j ≥ 2^j ⟺ u_j + R1_j ≥ 2^j; - S ≥ 0 ⟺ a + R_tot + 2 ≥ 2^(m+1); S ≥ 1 ⟺ a + R_tot + 1 ≥ 2^(m+1); - T ≥ 0 ⟺ b + 1 ≥ 2V ⟺ b + 3 + 2·R_tot ≥ 2^(m+1); T ≥ 2 ⟺ b + 1 ≥ 2V + 2 ⟺ b + 1 + 2·R_tot ≥ 2^(m+1).

The .v states INV in these forms, with R computed directly and no U_j: - R by recursion. Rof [] = 0, Rof (d0 :: t) = 2·Rof t + 1, Rof (d1 :: t) = 2·Rof t, on the LSB-first list. On the digits d_j .. d_1 it gives R_j (since R_j = 2·R_{j−1} + 1 − beta_j), and on the whole list it gives R_tot. - Per-digit predicates. Every per-digit condition is a predicate P d r p, where r = Rof of the digits above d and p = how many there are (p = j − 1), and AllD P applies it to every digit. Per digit, Rd d r = 2r + 1 − beta = R_j and ub d r = u + r + 1 − beta = ubar_j. So the per-digit data have no subtraction and no division, and the only power of 2 is the bound in PB. - The classes. PA = canonical, v ≥ R + 1 (vbar ≥ 1), ubar odd, and ubar = 1 for the top digit (equivalent to A's condition on d_1, given v ≥ R + 1). PB k = canonical, v + beta odd, ubar ≥ 2^(p+k), and for k = 0 the top is (0,0,1); k = 0 is class B and k = 1 is class C. B's bound is uniform, since the top (0,0,1) has ubar = 1 = 2^0. LSBok is vbar_m ≥ 1. The global clauses are the additive forms above, with S ≥ 1 in A and C and T ≥ 2 in C. - F0 is Rof_bound (R + 1 ≤ 2^len) and Rof_head1/Rof_head0 (the parity of R). - F1 is the lemma F1, generic over any per-digit predicate closed under the two touches (PA_touch0/1, PB_touch0/1), with Rof_M, len_M, LSB_M. - F2 without 2^j. Along the chain of digits below the absorber, the old and new R values satisfy Rel r ro rn := rn + 1 ≤ ro ≤ 2(rn + 1) ∧ (r = 0 → ro = rn + 1), which is preserved digit by digit (ro' = 2ro, rn' = 2rn + 1). That gives ubar' ≥ ubar/2 with the index one lower, and for a top fall (r = 0) ubar' = ubar (B → C). Lemmas: Rel, PB_chain, PB_abs, F2chain, F2, LSB_drop. - F3 is two list inductions, Oz_AB (A → B) and Oz_CA (C → A), using Oz_R: Rof (Oz t u) + 1 = 2^(len t + 1), i.e. after O the m re-paired bit-0 digits above the new LSB have R = 2^m − 1. - The remaining Common facts close by lia after rewriting every power to 2 · 2^m' (pow2S).

How the .v file is organized

It imports Individual62 and the stdlib ZifyNat, Lia, String, List, Arith. Every lemma is top level (no Section, no Module, no Hypothesis).

7. Numerical sanity checks

They are evidence only; the result rests on the .v file alone. The window lemmas, M, O, the initial segment, the run and the other starts are checked by direct simulation of the transition table. The orbit, inductiveness and F1–F3 checks evaluate the macro rules M/O and INV on abstract states (the 2,842-state subset is also run on the machine). - Window lemmas. S1–S6 (one block) and T1–T14 run exactly as stated and never read outside their windows. F is entered only in T4, T9 and T13, and reads 0 each time. - M, link by link (§2.2). After every lemma application, the whole tape, head and state equal the stated intermediate configuration; the end is the M result, the total is the step formula, and the leftmost cell read is the first 0 of d_{j*}'s 00. 37,220 instances: an exhaustive box (4 left contexts, u* ≤ 2, v* ≤ 3, k ≤ 3, u_i, v_i ≤ 2, a ≤ 3 including a = 0, b ≤ 2) plus 500 random ones (k ≤ 7, values up to 360). M is also exact on all 256,000 configurations of a second exhaustive box. - O, link by link (§2.3). The same checks on 9,975 instances: m ≤ 3 with u_i, v_i ≤ 3, m = 4 with u_i, v_i ≤ 2, a ≤ 3, b ≤ 2, plus 300 random ones (m ≤ 8). O's end result is also exact on 66,336 configurations of an exhaustive box and on 20,000 random ones. - Initial segment (§4). From the blank tape: K((3,1,1); 2, 1) at step 142, K((1,1,2); 8, 5) at step 483. - The run. From the blank tape to step 2·10^9, the machine passes 26,396 macro boundaries, and each is the K-configuration that M/O predict. - INV along the orbit. Along the abstract macro orbit from step 483, INV holds for 1.2·10^6 macro steps (to t ≈ 3.7·10^12 by the step formulas, ending with 16 digits (17 at most), with 52 top falls and 26 drops below the top). - INV is inductive. From 750,000 random INV states of all three classes (not only reachable ones; m ≤ 10, values near the thresholds and up to 5000), one macro step is defined, has no LSB drop, and lands in INV; all six transitions A→A, A→B, B→B, B→C, C→A, C→C occur. The same holds for every state in exhaustive boxes up to m = 6 (about 2.5·10^8 states). 2,842 of the random states, run on the machine for the predicted number of steps, give exactly the abstract successor, drops included. - F1–F3. The drop closed forms (F2: R, R1, V, S, T after a drop) hold on 20,000 random cases with m = 2..12 and every j*; F1–F3 hold on all 1,470 cases with m ≤ 9. - Other starts (§4). Started in B, the table reaches K((1,1,10); 8, 1) at step 732; started in C, K((1,1,9); 8, 1) at step 687; started in D, K((1,1,3); 4, 1) at step 215. All three are class A.

Gaps: none.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).