1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---: never halts

• Machine: 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, viewer https://bbchallenge.org/1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---
• Holdout: on the current BB(6) holdout list (class "Skelet 1-like Class 2").
• Written for: the string itself (no mirror, no renaming). All tapes below are in this machine's orientation. The head works at the left end, and the fixed marker 1001 sits at the right.
• Template: the formal proof of the parent machine 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- (1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v, 694 lines, a separate submission), a binary counter with a re-pairing overflow. Its nearest relative in busycoq is verify/SBCv6.v Module TM21, a loose relative (§6.1). This machine's table is the parent's table mirrored (L ↔ R), with states renamed (A,B,C,D,E,F) ↦ (B,C,D,A,E,F), and it starts in the parent's state D (§0). In the .v, the parent's tape lemmas are mirrored, its rule statements, invariant and closure proof are kept word for word, and the init is new (§6.1).
• Status: fully formalized. 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---.v (671 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c). It imports only Individual62 from busycoq, has one TM_from_str, and compiles in about 12 s (-native-compiler yes). Print Assumptions nonhalt gives "Closed under the global context", and coqchk re-checks the compiled file.
• Where each section lives in the .v: §2.1 S1–S6, T1–T14, Lb, Lf, Rb, Ro; §1 dg, dr, app_ds, R0, K; §2.2 chunkA, LbS, RbS, chunkC, M_spec, Mdrop_spec; §2.3 RoS, Oz, Oout, Ozeq, chunkO, O_spec; §3 Rof, PA, PB, INV, F1, F2, Oz_AB, Oz_CA, decomp, macro_step; §4 init; §5 nonhalt. §6.2 has the full table.

     0    1
A   1RB  0RE
B   1LC  0RE
C   1LD  0LD
D   1RA  0LC
E   1RA  1RF
F   1RA  ---        halting transition: F reads 1 (F is entered only by E1)

Summary. At each return to the left edge the tape is K(d_1 .. d_m; a, b): a block (01)^b 000 (01)^a, then m digits, then the fixed marker 1001. Each digit is a triple (u, β, v) (u copies of 01, a bit β, v copies of 10), and the bits form a binary counter whose least significant digit d_m sits next to the block. - A carry M adds 1 to the counter. Every digit it touches pays one 10. A digit flipped 0→1 gains a 01, and if it has just spent its last 10 it merges ("drops") into the next less significant digit. - On overflow (all bits 1), O re-pairs the halves of every digit, and the counter restarts at 1 with one more digit. - The only way the rules can fail is a carry reaching a bit-0 digit with no 10 left.

The proof derives M, M with a drop, and O from 20 window lemmas (§2). An invariant INV = Common ∧ (A ∨ B ∨ C) on the triples rules out that failure and is closed under the rules (§3). It consists of parities, vbar ≥ 1 and ubar ≥ 2^j bounds, and three classes: a quiet cycle, a top digit about to drop, and a dropped top. The run from blank reaches INV at step 215 (§4). The invariant never looks at the tape, so it is the parent's, word for word.

0. Relation to the parent machine, and the four holdouts with this table

Mirror the parent's table (L ↔ R) and rename its states by π = (A,B,C,D,E,F) ↦ (B,C,D,A,E,F). The result is this string, cell by cell. For a configuration c of the parent, write μc for its reflection (the tape read right to left, head state renamed by π). Then c → c′ under the parent if and only if μc → μc′ under this machine, and c is halted exactly when μc is. The blank tape is its own reflection, so this machine's run is the reflection of the parent table's run from 0^inf D> 0^inf.

The relation is used only to reuse the parent's abstract invariant and its Rocq form (§3, §6), and to give each window lemma the name of its reflection in the parent's proof (§2.1). Every rule below is proved on this machine's own table.

Four holdouts on the current list are relabelings of this table. A search over all 720 state permutations, each with and without mirroring, finds exactly these four.

All four first INV states are in class A. The step and digit values for B, C and D agree with the parent's write-up (§4 there). The wiki's equivalence list for the current holdouts (BB6_holdouts_1590_eqv_778.txt) keeps the four in four separate groups, with this machine as a singleton. So each needs its own proof, with its own TM_from_str. This write-up and its .v cover only this string.

1. Family and notation

K(d_1 .. d_m ; a, b) := 0^inf <C (01)^b 000 (01)^a  d~_m .. d~_2 d~_1  1001 0^inf

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

• Head notation. X> w means the head is in state X on the first cell of w. w <X means it is in state X on the last cell of w. So 0^inf <C (01)^b has the head on the blank cell just left of the block. This is busycoq's {{X}}> / <{{X}}, and the same convention as the parent's write-up.
• d_1 is next to the fixed 1001 and is the most significant bit. d_m is next to the block and is the least significant bit. m ≥ 1, except at step 82 of the init (§4).
• The triple (u, beta, v) means exactly what it means for the parent: u counts the 01s on the marker side, and v counts the 10s on the block side. Only the tape picture is mirrored. So the rules and the invariant, stated on triples, are the parent's.
• 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). Outside INV, M can make (u,0,0), the precursor of the failure mode (§2.4).
• Re-reading (no machine steps). A bit-1 digit with v = 0 is just (01)^u, so it fuses with what lies to its left. If the digit to its left is (u',β',v'), the two read as (u'+u, β', v'). If it is the least significant digit, 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, and 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.3 gives the same definitions in additive form for Rocq, with no subtraction or division.

2. Rules

In busycoq comment-block style:

1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---

K(d_1 .. d_m; a, b) := 0^inf <C (01)^b 000 (01)^a d~_m .. d~_1 1001 0^inf
d~(u,0,v) := (10)^v 00 (01)^u,   d~(u,1,v) := (10)^v (01)^u        (d_m least significant)

start from K((1,1,3); 4, 1)                                   (step 215, §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:

M:  0^inf <C (01)^b 000 (01)^a [(10)^v_j (01)^u_j]_{j=m..j*+1} (10)^v 00 (01)^u X
      --> 0^inf <C (01)^(b+2) 000 (01)^(a+1) [(10)^(v_j-1) 00 (01)^u_j]_{j=m..j*+1} (10)^(v-1) (01)^(u+1) X
O:  0^inf <C (01)^b 000 (01)^a [(10)^v_j (01)^u_j]_{j=m..1} 1001 0^inf
      --> 0^inf <C 01 000 (01)^(b+3) (10)^a (01)^v_m [(10)^u_j 00 (01)^(v_(j-1)-1)]_{j=m..2} (10)^u_1 00 1001 0^inf

Here X is everything right of d_{j*}, and M never reads it. The M and O rules are not taken from simulation. §2.1 lists 20 window lemmas, and §2.2–2.3 derive M and O from them as chains of intermediate configurations. Each step count is the sum along its chain. The same O chain with no digits (m = 0) gives K(; a, b) --> K((1,1,a); b+3, 1) in 89 + 8a + 20b steps (a ≥ 1). It occurs once, inside the initial segment (§4), and the invariant argument does not use it.

2.1 Building blocks

A window lemma w → w' says: 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 on this table. For S1–S6, one block is a finite run, and induction on n gives every n. For example, S5 is (10)^(n+1) 11 <D = (10)^n 1011 <D → (10)^n 11 <D 01 → 11 <D (01)^n 01 (one block, then the IH). Each lemma is the reflection of the parent's lemma of the same name, so the names match the parent's .v (§6.1).

Shift lemmas:

S5 and S6 are the back-bounces. Each block costs 6 steps for a 2-cell advance, because the head doubles back over cells it has just written (S5 moves L L R R L L, S6 moves L R R L L L).

Finite lemmas:

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

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

2.2 Derivation of M

Notation: - X is everything right of d_{j*}. It is never read. - (u*, v*) is d_{j*} = (u*,0,v*). - Y = Π_{i=k..1} (10)^v_i (01)^u_i is the trailing bit-1 digits, written left to right. i = k is d_m, and i = 1 is d_{j*+1}.

                                                                                        steps
    0^inf <C (01)^b 000 (01)^a Y (10)^v* 00 (01)^u* X
 Phase 1: left-edge preamble with a dip into the 000 gap                                4b+10
T1  0^inf 10 E> (01)^b 000 (01)^a Y ..                                                  3
S4  0^inf (10)^(b+1) E> 000 (01)^a Y ..                                                 2b
T2  0^inf (10)^(b+1) <C 001 (01)^a Y ..                                                 5
S1  0^inf <C (01)^(b+1) 0 (01)^(a+1) Y ..                                               2b+2
 Phase 2: one long right sweep, up to the 00 of d_{j*}                                  2a+2b+9+4v*+Σ(2u_i+2v_i)
T1  0^inf 10 E> (01)^(b+1) 0 (01)^(a+1) Y ..                                            3
S4  0^inf (10)^(b+2) E> 0 (01)^(a+1) Y ..                                               2b+2
T3  0^inf (10)^(b+2) 110 E> (01)^a Y ..                                                 3
S4  0^inf (10)^(b+2) 110 (10)^a E> Y (10)^v* 00 (01)^u* X                               2a
Lb  0^inf (10)^(b+2) 110 (10)^a Y' E> (10)^v* 00 (01)^u* X        (i = k down to 1)     Σ(2u_i+2v_i)
                         Y' = Π_{i=k..1} 11 (01)^(v_i−1) (10)^u_i
Lf  0^inf (10)^(b+2) 110 (10)^a Y' 11 <D (10)^(v*−1) (01)^(u*+1) X                      4v*+1
 Phase 3: leftward pass with 2-cell back-bounces, then a plain run to the edge          6a+2b+13+Σ(6u_i+2v_i)
Rb  0^inf (10)^(b+2) 110 (10)^a 11 <D Y'' (10)^(v*−1) (01)^(u*+1) X   (i = 1 up to k)   Σ(6u_i+2v_i)
                         Y'' = Π_{i=k..1} (10)^(v_i−1) 00 (01)^u_i
S5  0^inf (10)^(b+2) 110 11 <D (01)^a Y'' ..                                            6a
T8  0^inf (10)^(b+2) <C 00001 (01)^a Y'' ..                                             9
S1  0^inf <C (01)^(b+2) 000 (01)^(a+1) Y'' (10)^(v*−1) (01)^(u*+1) X                    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 right only as far as the 000 gap, turns (T2) and returns to the edge. - Phase 2 is the only long rightward leg. Its rightmost read is the right 0 of d_{j*}'s 00: T6 reads both cells, then moves left. So M is a side rule, and the tape X right of that 00 is never read. - Phase 3 moves left. It doubles back once per 10 block (S5, on the swept digits' (10)^u_i and on (10)^a). It crosses the (01)^(v−1) blocks and the final (10)^(b+2) with plain sweeps (S2, S1).

When v* = 1, the flipped digit (u*+1,1,0) = (01)^(u*+1) 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=m..1} (10)^v_i (01)^u_i, with all digits bit 1.

                                                                                        steps
    0^inf <C (01)^b 000 (01)^a Y 1001 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)^(b+2) 110 (10)^a Y' E> 1001 0^inf              Y' = Π_{i=m..1} 11 (01)^(v_i−1) (10)^u_i
 Phase 3: turn at the far right
T9  0^inf (10)^(b+2) 110 (10)^a Y' <C 000 1001 0^inf                                    13
 Phase 4: leftward pass
Ro  0^inf (10)^(b+2) 110 (10)^a <C Y''' 000 1001 0^inf      (i = 1 up to m)             Σ(2u_i+6v_i−4)
                         Y''' = Π_{i=m..1} 000 (01)^(v_i−1) 1 (01)^(u_i−1)
 Phase 5: left end                                                                      2a+8b+30
S1  0^inf (10)^(b+2) 110 <C (01)^a Y''' ..                                              2a
T11 0^inf (10)^(b+2) 11 <D 1 (01)^a Y''' ..                                             1
S5  0^inf 11 <D (01)^(b+2) 1 (01)^a Y''' ..                                             6b+12
T12 0^inf 10110 E> (01)^(b+2) 1 (01)^a Y''' ..                                          13
S4  0^inf 10110 (10)^(b+2) E> 1 (01)^a Y''' ..                                          2b+4
 Phase 6: short right sweep over the a block, to the 000 that Ro left before d_m        2a+1
T13 0^inf 10110 (10)^(b+2) 110 E> (01)^(a−1) Y''' ..                                    3
S4  0^inf 10110 (10)^(b+2) 1 (10)^a E> 000 (01)^(v_m−1) ..                              2a−2
 Phase 7: turn in that 000, final run to the edge                                       2a+6b+27
T2  0^inf 1011 (01)^(b+3) (10)^a <C 001 (01)^(v_m−1) ..   (0 (10)^(b+2) 1 = (01)^(b+3))   5
S1  0^inf 1011 (01)^(b+3) <C (01)^a 001 (01)^(v_m−1) ..                                 2a
S6  0^inf 1011 <C 0 (01)^(b+3) 1 (01)^(a−1) 001 (01)^(v_m−1) ..                         6b+18
T14 0^inf <C 0100 0 (01)^(b+3) 1 (01)^(a−1) 001 (01)^(v_m−1) ..                         4

Re-read the final tape with 1 (01)^(n−1) 0 = (10)^n and 01 (01)^(n−1) = (01)^n, splitting each 000 of Y''' as 0 | 00:

0^inf <C 0100 0 (01)^(b+3) 1 (01)^(a−1) 001 (01)^(v_m−1) 1 (01)^(u_m−1) [000 (01)^(v_i−1) 1 (01)^(u_i−1)]_{i=m−1..1} 000 1001 0^inf
  = 0^inf <C 01 000 (01)^(b+3) (10)^a (01)^v_m [(10)^u_(i+1) 00 (01)^(v_i−1)]_{i=m−1..1} (10)^u_1 00 1001 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 first 0 1 of (01)^a, so a ≥ 1. - T9 needs 0^inf on the right. It reads the three blank cells right of 1001 and moves the marker three cells right, so the rightmost cell visited moves 3 cells per overflow.

O has two long rightward legs: phase 2, and the short phase 6.

O at m = 0 (the init, §4). The same chain with no digits works: phase 4 is empty, and phase 6 ends on T9's 000. The final tape is 0^inf <C 01 000 (01)^(b+3) 1 (01)^(a−1) 001 1001 0^inf = 0^inf <C 01 000 (01)^(b+3) (10)^a 01 1001 0^inf = K((1,1,a); b+3, 1). The step count is 89 + 8a + 20b.

2.4 What the rules do, in words

The digits form a binary counter, and each M is one increment. - M flips the trailing 1s to 0 and the last 0 to 1. Every digit it touches pays one 10 from its v, and a digit flipping 0→1 also gains a 01. - When all bits are 1, O swaps the two halves of every digit. Each (01)^u becomes the (10)^u fuel of a new bit-0 digit, and each (10)^v becomes the next digit's (01)^(v−1). The counter restarts at value 1 with one more digit. - When a digit flipping 0→1 has spent its last 10 (v = 1), it drops: its 01s merge into the next digit, and the counter loses that digit.

The only way the rules can fail is the failure mode: a carry reaches a bit-0 digit with v = 0, where Lf's first lemma T4 has no 10 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

The invariant is the parent's (its write-up, §3), unchanged. It is stated on the triples (u, beta, v) and the numbers a, b, and it uses only the rule shapes of §2, which are the parent's. Its Rocq form is the parent's INV and closure lemma, word for word (the closure lemma is named macro_step here), proved against this machine's K and rule lemmas (§6). The argument uses only parities and 2^j bounds. Which digits drop, and when, is irregular, but the invariant never needs to know.

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. Its 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 and 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. §7 lists numerical checks of this on the orbit and on random INV states.

4. Initial segment

0^inf A> 0^inf  --82-->   K(; 3, 1)          = 0^inf <C 01 000 (01)^3 1001 0^inf
                --133-->  K((1,1,3); 4, 1)   = 0^inf <C 01 000 (01)^4 (10)^3 01 1001 0^inf        (step 215)

The 215 steps are a finite run from the blank tape. The second leg is the O chain at m = 0 with a = 3, b = 1 (§2.3; 89 + 24 + 20 = 133), but the proof only needs the 215-step run.

The only K-configurations in steps 0..215 are those at steps 82 and 215. K(; 3, 1) has no digits, so it is not in INV, which is why the init stops at 215.

K((1,1,3); 4, 1) is in class A: - top (1,1,3): bit 1, u_1 = 1; - V = 1, R_tot = R_1 = 0, R1_1 = 0; - ubar_1 = 1 (odd), vbar_1 = 3 ≥ 1 (also the LSB condition); - S = 4 + 0 − 2 = 2 ≥ 1, T = 1 − 1 = 0 ≥ 0 (tight); - a = 4 ≥ 1, b = 1 odd, a + R_tot = 4 even.

The next macro step is O (165 steps), to K((0,0,1), (3,1,4); 4, 1), which is in class B.

In the .v this is init : c0 -->* K [d1 1 3] 4 1, proved by unfold K, R0; cbn; solve_init (all 215 steps at once; the reading of the second leg as O at m = 0 is not used). The parent's init is 483 steps to K [d1 1 2] 8 5.

5. Conclusion

• Init. The run reaches an INV state at step 215 (§4).
• Coverage. Every INV state has a rule (§3.2).
• Progress. Every rule is an exact run of at least 32 steps, composed of the window lemmas of §2.1 (§2.2, §2.3).
• Closure. Every result is again in INV (§3.3).

By the progress theorem (progress_nonhalt_cond with P := INV), the machine never halts.

In the .v this conclusion is nonhalt. The three rules are the lemmas M_spec, Mdrop_spec and O_spec, proved on this table from the window lemmas along the chains of §2.2–2.3 (§6.2).

Why --- (F reading 1) is never used. Formally, every rule is a proved run, so no step of the run is the halting transition. Concretely: F is entered only by E1 (1RF). After the 215-step init, every step of the run lies inside one of the 20 window lemmas. E1 occurs only in T4, T9 and T13, and in each of them the next step is F reading 0 (F0 = 1RA; transition lists in §2.1). The init is a finite run that does not halt either. Nothing is claimed about tapes outside the family, and INV keeps the run inside it.

6. The Rocq formalization

The .v has one TM_from_str (this string). It imports Individual62 and the stdlib ZifyNat, Lia, String, List, Arith. Every lemma is top level (no Section, no Module, no Hypothesis). It does not use busycoq's transport lemmas for mirrored or relabeled machines (flip_halts_iff in Flip.v, perm_nonhalt in Permute.v, both loaded through Individual62): the parent's development is mirrored into this machine's orientation, and the result is proved directly on this table rather than transported from the parent's. The file has two parts and the final theorem: 1. A machine part, from tm to O_spec: window lemmas, digit lemmas, list sweeps, K, the three rule specs and init. 2. An abstract part, from Open Scope nat_scope to macro_step: the derived quantities, INV, F0–F3 and the closure lemma. It mentions the machine only through Kc, M_spec, Mdrop_spec and O_spec. 3. nonhalt.

The .v proves the rules as -->+ runs. The exact step counts of §2 are not part of the formal statement.

6.1 Mapping to the template

The template is the parent's .v (694 lines). Relative to it: - Machine part. The parent's, mirrored by hand with the dictionary below. The three rule-spec statements are the parent's word for word. The accumulators change side: the parent's right-side rw is a left-side accumulator here, and its left-side ro_out is a right-side builder. Beyond the dictionary, the machine part differs from the parent's as follows. - Names: the parent's dl (one digit on the left side) is dr here, and its L0 (the marker side) is R0. - Helpers: the parent's tape lemmas lshift, p01 and p10 are not in the .v. S5's induction step is simpl_tape. follow S5_1. follow IHn. rewrite lpow_shift'. finish., with the framework's lpow_shift' where the parent rewrites with lshift. - S6 instances: Ro uses plain follow S6 (the parent's Ro passes the left context explicitly), and the one explicit S6 instance in chunkO has its arguments mirrored. - O_spec has an unfold R0 before follow T9. - Order: init comes right after K (the parent has it last, after O_spec); chunkA, chunkC, chunkO come after Ozeq (the parent has them before dg); and rot01, rot10 sit together just before the digit lemmas. - Abstract part. The parent's text, byte for byte, except that Lemma step is renamed macro_step, so that it does not shadow the framework's step. - nonhalt. The parent's proof with the base K [d1 1 3] 4 1 in place of K [d1 1 2] 8 5. The tactic lines that close the base are unchanged. init is new (215 steps, against the parent's 483).

Mirror dictionary. busycoq sides are streams listed nearest cell first, so mirroring swaps the two sides and leaves every list literal as it is: - l {{q}}> r ↦ r <{{π q}} l and l <{{q}} r ↦ r {{π q}}> l; - l <* xs ↦ xs *> l, so l <* x <* y ↦ y *> x *> l; - [..] literals, ^^n and 0inf are unchanged; - π = (A,B,C,D,E,F) ↦ (B,C,D,A,E,F); - shift_rule_R ↔ shift_rule_L.

Example: the parent's T3: l <* [0;0;1] <{{E}} r -->* l <{{E}} [0;1;1] *> r becomes T3: l {{E}}> [0;0;1] *> r -->* l <* [0;1;1] {{E}}> r, which is E> 001 → 110 E>.

The interface between the two parts. The abstract part and nonhalt use exactly 13 names from the machine part: tm, dg/d0/d1, K, map0, map1, Oz, Oout, M_spec, Mdrop_spec, O_spec and init. - K appears in the abstract part only in Definition Kc and in nonhalt's change. - The abstract part never unfolds K. All four unfold K lines are in the machine part (init, M_spec, Mdrop_spec, O_spec). - dg, map0, map1, Oz and Oout are plain list functions with no tape in them. They are the parent's, verbatim. - K keeps the parent's signature list dg -> nat -> nat -> Q * tape. Only its body is mirrored.

So the abstract part holds for this machine because the three spec statements are the parent's, word for word:

M_spec     : K (map1 os ++ d0 u (S v) :: rest) a b -->+ K (map0 os ++ d1 (S u) v :: rest) (S a) (S (S b))
Mdrop_spec : K (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) a b -->+ K (map0 os ++ d0 (S u2 + S u) v2 :: rest) (S a) (S (S b))
O_spec     : os <> [] -> K (map1 os) (S a) b -->+ K (Oout os (S a)) (S (S (S b))) 1

Mdrop_spec is M_spec with v = 0, followed by the tape equality [0;1]^^(S u2) *> [0;1]^^(S u) *> .. = [0;1]^^(S u2 + S u) *> .. on the right side (lpow_add), the reflection of the parent's.

Relatives in busycoq. verify/SBCv6.v Module TM21 (line 3702) is a loose relative: LIncs_spec's inner induction is the pattern behind LbS/RbS, and Ov/Ov_spec the list induction behind O_spec. verify/TCv3.v is the loosest relative: the copy-and-modify module style with progress_nonhalt_simple. It has no invariant.

6.2 How the .v file is organized

The family and the init in Rocq:

dr (d0 u v) r := [1;0]^^v *> [0;0] *> [0;1]^^u *> r      dr (d1 u v) r := [1;0]^^v *> [0;1]^^u *> r
app_ds r ds   (LSB-first list, as in the parent)         R0 := [1;0;0;1] *> 0inf
K ds a b      := 0inf <{{C}} [0;1]^^b *> [0;0;0] *> [0;1]^^a *> app_ds R0 ds
init          : c0 -->* K [d1 1 3] 4 1                   (unfold K, R0; cbn; solve_init)

6.3 How the abstract part states §3

• No U_j. R is computed by structural recursion on the LSB-first list: Rof [] = 0, Rof (d0 :: t) = 2·Rof t + 1, Rof (d1 :: t) = 2·Rof t. 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, and AllD P applies it to every digit. So the per-digit data have no subtraction and no division, and the only power of 2 among the per-digit conditions is the bound in PB.
• The classes in this form. PA = canonical, v ≥ R + 1 (vbar ≥ 1), ubar odd, and ubar = 1 for the top digit (A's condition on d_1). PB k = canonical, v + beta odd, ubar ≥ 2^(p+k), and for k = 0 the top is (0,0,1). The global conditions are the additive forms: a + R + 2 ≥ 2^(m+1) (S ≥ 0), b + 3 + 2R ≥ 2^(m+1) (T ≥ 0), with +1 in place of +2 (S ≥ 1) in A and C, and b + 1 + 2R ≥ 2^(m+1) (T ≥ 2) in C.
• 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), preserved digit by digit. That gives ubar′ ≥ ubar/2 with the index one lower, and for a top fall (r = 0) ubar′ = ubar (B → C).
• F3 is two list inductions, Oz_AB and Oz_CA, using Rof (Oz t u) + 1 = 2^(len t + 1).

nonhalt.

Lemma nonhalt: ~halts tm c0.
Proof.
  eapply multistep_nonhalt; [apply init|].
  change (K [d1 1 3] 4 1) with (Kc ([d1 1 3], 4, 1)).
  apply progress_nonhalt_cond with (P := INV).
  - exact macro_step.
  - unfold INV. cbn. repeat split; try lia; try discriminate.
    left. unfold PA, canon, Rd, ub, vof. cbn. repeat split; lia.
Qed.

The base goal is the additive INV of §3 at ([d1 1 3], 4, 1), in class A: - Rof = 0; - a + R + 2 = 6 ≥ 4; - b + 3 + 2R = 4 ≥ 4 (tight, T = 0); - a + R + 1 = 5 ≥ 4; - v_m = 3 ≥ R + 1; - PA (d1 1 3) 0 0: ub = 1.

7. Numerical sanity checks

These are direct simulations of this table and computations in the abstract model of §3, independent of the Rocq proof; the result rests on the .v alone. - Window lemmas. S1–S6 (one block) and T1–T14 are exact runs on their windows and never read outside them. S1–S6 also hold as stated for n ∈ 0..11, 50, 333 and 1000. F is entered only by E1, only in T4, T9 and T13, and reads 0 each time. - M chain (§2.2), link by link. After every lemma application, the whole tape, head and state equal the stated configuration. The end is the M result, the total is the step formula, and the rightmost cell read is the right 0 of d_{j*}'s 00. 37,220 cases: an exhaustive box (4 right contexts, u* ≤ 2, v* ≤ 3, k ≤ 3, u_i, v_i ≤ 2, a ≤ 3 with a = 0 included, b ≤ 2), plus 500 random cases (k ≤ 7, values up to 360). Also 700 random full K-configurations (k = 0..6, 273 of them with a drop): exact tape and step count. - O chain (§2.3), with the same checks and the rightmost cell exactly 3 right of the old 1001. 9,996 cases: a box (m = 0..3 with u_i, v_i ≤ 3, m = 4 with u_i, v_i ≤ 2, a ≤ 3, b ≤ 2; a, b ≤ 4 at m = 0), plus 300 random cases (m ≤ 8, m = 0 included), plus the init leg K(;3,1) → K((1,1,3);4,1). Also 350 random all-ones configurations, m = 1..7. - Init (§4). Blank reaches K(;3,1) at step 82 and K((1,1,3);4,1) at step 215, and there is no other K-configuration in steps 0..215. The next macro step is O (165 steps), to a class-B state. - The real run. Checked by direct simulation to step 999,982,947: at each of the 18,977 macro boundaries from step 215 on, the whole tape, head and state equal the predicted K-configuration, and it is in INV. Rules used in the 18,976 macro steps between them: O 52 times, M with k = 0, 1, 2, 3, 4, 5 trailing ones 9,462, 4,757, 2,377, 1,186, 591, 292 times, k ≥ 6 259 times. Drops: 31 top falls, 11 mid drops. Classes: A 6,759, B 6,096, C 6,122. - The abstract orbit. INV holds for the first 1.2·10^6 macro steps from step 215, which reach machine step ≈ 3.8·10^12, 18 digits and 95 overflows, with 53 top falls, 25 mid drops and no LSB drop. - Inductiveness on random states. 600,000 random INV states of all three classes, not only reachable ones (m up to 10, values near the thresholds and up to 5000), were tested. Each has one macro step, of at least 32 machine steps, with no LSB drop, and it lands in INV. All six transitions A→A, A→B, B→B, B→C, C→A, C→C occur. 2,847 such states, run on the machine for the predicted number of steps, give exactly the abstract successor, merges included. - Exhaustive boxes. All 417,882 INV states with m ≤ 2 in a bounded box step into INV, each one also confirmed on the machine. 5.6 million INV states with m = 3, 4, 5 and values near the INV thresholds also step into INV, covering all six class transitions with top falls and mid drops. - F2 closed forms (R, R1, V, S, T after a drop, and the top-fall case): 20,000 cases, m = 2..12, every j*.

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