1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---: never halts

• Machine: 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---, viewer https://bbchallenge.org/1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---
• Holdout: on the current BB(6) holdout list.
• Written for: the string itself. The TM_from_str of the .v is this string; no Flip/Permute bridge is used.
• Parent: this is a delta write-up. It relies on the write-up for 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, called "the parent" below. "P§n" means §n of that write-up. This machine is the parent's table with its states renamed by σ = (A,B,C,D,E,F) ↦ (B,C,D,A,E,F), with no mirror. So it runs the parent's table started in the parent's state D (§0).
• Template: the .v for the parent (671 lines, sha256 37cb180280f0896396a28bb32a548a6bfdd22d0b47b2f526230ed2208dbb2053), which has the architecture of busycoq verify/SBCv6.v Module TM21 (a binary counter with a re-pairing overflow). This machine differs from the parent only in state letters, never in a symbol or direction: row σ(s) here is the parent's row s with each target t replaced by σ(t). The .v differs from the parent's .v in the TM string, σ applied to every state name, and the initial segment with its base case (§5).
• Status: formalized in the accompanying 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---.v (673 lines). It 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 (no axioms), and coqchk passes.
• Where each section lives in the .v: §0 tm; §1 the window lemmas S1_1–S6_1, S1–S6, T1–T14, the digit lemmas Lb, Lf, Rb, Ro, the family K, the sweeps LbS, RbS, RoS, the rules M_spec, Mdrop_spec, O_spec, the invariant INV and its closure macro_step; §2 init and the base goal in nonhalt; §3 nonhalt. The full map is in §5.

Summary. This is the parent's binary counter, with head state D where the parent has C. At each return to the left edge the tape is K = 0^inf <D (01)^b 000 (01)^a d~_m .. d~_1 1001 0^inf. A carry M adds 1 to the counter, an overflow O re-pairs the halves of every digit, and the three-class invariant INV = Common ∧ (A ∨ B ∨ C) of P§3 is closed under M and O. σ is a pure renaming of states (Lemma R, §0). So every window lemma, rule, step formula and the whole invariant argument carry over word for word. The invariant is not adjusted. Only the start differs, because this machine starts in what is the parent's state D: from the blank tape it follows a different orbit of the same macro map and reaches the INV state K((1,1,9); 8, 1) (class A) at step 687, where the parent reaches K((1,1,3); 4, 1) at step 215. The proof is that 687-step initial segment, a base-case check, and the parent's induction.

0. The map

σ: A↦B, B↦C, C↦D, D↦A, E↦E, F↦F (a 4-cycle on A–D). Row σ(s) of this table is the parent's row s with every target state t replaced by σ(t); symbols and directions are unchanged. For example, the parent's D1 = 0LC becomes 0Lσ(C) = 0LD, which is this machine's A1. Among all 720 state renamings, each with and without mirroring, σ without mirror is the only map from the parent's table to this one. The parent's table is in turn the table of 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- mirrored and renamed by (A,B,C,D,E,F) ↦ (B,C,D,A,E,F) (P§0). So this machine is also that table mirrored, with states renamed by the composite (A,B,C,D,E,F) ↦ (C,D,A,B,E,F), and started in its state C. P§0 lists the four holdouts with this table and their start states; this machine is the D row.

Lemma R (relabelling). For a configuration c, let σc be c with its head state renamed by σ; the tape and head position stay the same. Then c → c′ under the parent if and only if σc → σc′ under this machine, and c is halted exactly when σc is (F1 is the only undefined cell, and σ fixes F). So every run c →ⁿ c′ of the parent gives a run σc →ⁿ σc′ here, of the same length, and conversely.

Proof. If the parent has δ(s, x) = (y, d, t), this machine has δ(σs, x) = (y, d, σt) by the table above. ∎

Start. This machine's c0 is 0^inf A> 0^inf = σ(0^inf D> 0^inf). So its run is σ of the parent's table run from 0^inf D> 0^inf. This is not the parent's own run, which starts in A.

Halting cell. Only E1 = 1RF enters F, and F1 is ---, exactly as in the parent (σ fixes E and F). So the machine halts exactly when E reads 1 with a 1 to its right.

1. What carries over unchanged

Head notation as in P§1: X> w puts the head in state X on the first cell of w, and w <X on the last cell of w (so <X w is on the cell just left of w). The window lemmas on this table, with their transitions:

      window lemma                 steps  transitions
S1    10<D       -> <D01             2    D0 A1                 one block of (10)^n <D -> <D (01)^n
S2    01<A       -> <A10             2    A1 D0                 one block of (01)^n <A -> <A (10)^n
S3    B>10       -> 01B>             2    B1 E0                 one block of B> (10)^n -> (01)^n B>
S4    E>01       -> 10E>             2    E0 B1                 one block of E> (01)^n -> (10)^n E>
S5    1011<A     -> 11<A01           6    A1 D1 A0 B0 C0 D1     one block of (10)^n 11 <A -> 11 <A (01)^n
S6    01<D0      -> <D001            6    D1 A0 B0 C0 D1 A1     one block of (01)^n <D 0 -> <D 0 (01)^n
T1    00<D       -> 10E>             3    D0 A0 B1              (on 0^inf)
T2    E>000      -> <D001            5    E0 B0 C0 D1 A1
T3    E>001      -> 110E>            3    E0 B0 C1
T4    E>10       -> 11B>             2    E1 F0
T5    B>01       -> 10E>             2    B0 C1
T6    B>00       -> <A01             3    B0 C0 D1
T7    11<A       -> <A00             2    A1 D1
T8    11011<A    -> <D00001          9    A1 D1 A0 B0 C0 D1 A1 D1 A1
T9    E>1001000  -> <D0001001       13    E1 F0 B0 C1 E0 B0 C0 D1 A1 D0 A1 D1 A1    (E> 1001 0^inf)
T10   11<D       -> <D00             2    D1 A1
T11   0<D        -> <A1              1    D0
T12   00011<A    -> 10110E>         13    A1 D1 A0 B0 C0 D1 A1 D0 A0 B1 E0 B0 C1    (0^inf 11 <A)
T13   E>101      -> 110E>            3    E1 F0 B1
T14   1011<D     -> <D0100           4    D1 A1 D0 A1

The digit lemmas of P§2.1 read the same with the head states renamed: Lb E> (10)^v (01)^u → 11 (01)^(v−1) (10)^u E>, Lf E> (10)^v 00 (01)^u → 11 <A (10)^(v−1) (01)^(u+1), Rb 11 (01)^(v−1) (10)^u 11 <A → 11 <A (10)^(v−1) 00 (01)^u, Ro 11 (01)^(v−1) (10)^u <D → <D 000 (01)^(v−1) 1 (01)^(u−1), with the step counts and side conditions of P§2.1.

The rules in busycoq comment style, for this machine:

1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---     (= sigma of 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, sigma = BCDAEF)

K(d_1 .. d_m; a, b) := 0^inf <D (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,9); 8, 1)                                   (step 687, section 2)

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_j, v_j >= 1 (j > j*), a, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, P section 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
O at m = 0:  K(; a, b) --> K((1,1,a); b+3, 1)   in 89 + 8a + 20b steps (a >= 1); used only inside the initial segment

We write M_k for an M step with k = m − j* trailing bit-1 digits.

The invariant, restated from P§3 (derived quantities as in P§1):

INV(d_1..d_m; a, b) := Common /\ (A \/ B \/ C)
Common: m >= 1; 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
A:      d_1 = (0,0,v) with v >= 2, or d_1 = (1,1,v); for all j, vbar_j >= 1 and ubar_j odd; S >= 1
B:      d_1 = (0,0,1); for all j, v_j + beta_j odd; for j >= 2, ubar_j >= 2^(j-1)
C:      for all j, v_j + beta_j odd and ubar_j >= 2^j; S >= 1; T >= 2

2. What changes: initial segment and base (replaces P§4)

A K-configuration is state D on a blank cell with only blanks to its left, with the tape to its right parsing as a K. Direct simulation of this machine from the blank tape finds them exactly at these steps up to 687. (The parent's table run from 0^inf D> 0^inf gives the same list, as Lemma R says.)

Each leg is an instance of the rules of §1: 133 = 89 − 4 + 16 + 20 + 4 + 8; 92 = 32 + 32 + 8 + 4 + (8 + 8); 100 = 32 + 40 + 24 + 4; 261 = 89 + 72 + 100. Two legs use rule cases the invariant argument never needs (the LSB drop, and O at m = 0). That does not matter: the proof uses the 687-step run only as one finite computation, and the table only explains it.

For comparison, the parent's run has K-configurations at 82 (K(; 3, 1)) and 215 (K((1,1,3); 4, 1)) (P§4); P§0 lists the first INV K-configuration for all four start states of this table.

INV at the base K((1,1,9); 8, 1): - top (1,1,9): bit 1, u_1 = 1; m = 1; - V = 1, R_tot = R_1 = 0, R1_1 = 0; - ubar_1 = 1 (odd), vbar_1 = 9 ≥ 1 (also the LSB condition); - S = 8 + 0 − 2 = 6 ≥ 1, T = 1 − 1 = 0 ≥ 0 (tight, as at the parent's base); - a = 8 ≥ 1, b = 1 odd, a + R_tot = 8 even; - so Common holds, and class A holds (top (1,1,v), every vbar ≥ 1, every ubar odd, S ≥ 1).

In the .v, INV is the parent's additive form: R = Rof ds is computed by structural recursion on the least-significant-first digit list, and the clauses carry no subtraction or division. At ([d1 1 9], 8, 1), with m = 1 and 2^(m+1) = 4, its 12 clauses are: - ds ≠ [], a = 8 ≥ 1, b mod 2 = 1, (a + R) mod 2 = 0 with R = 0; - a + R + 2 = 10 ≥ 4 (S ≥ 0), b + 3 + 2R = 4 ≥ 4 (T ≥ 0), LSBok: v_m = 9 ≥ R + 1; - class A: a + R + 1 = 9 ≥ 4 (S ≥ 1), and PA (d1 1 9) 0 0, which is canonical (1 ≥ 1, 9 ≥ 1), 9 ≥ Rd + 1 = 1, ub = 1 odd, and ub = 1 for the top digit.

Compared with the parent's base K((1,1,3); 4, 1), only v_1 (9 against 3) and a (8 against 4) differ. Every clause that reads them is a lower bound, except the parity of a + R, which is even in both.

3. The argument (complete)

Theorem. 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- does not halt from the blank tape.

1. Initial segment. The machine runs from c0 to K((1,1,9); 8, 1) in exactly 687 steps without halting. This is a finite exact computation (§2); in Rocq it is init, proved by solve_init.
2. Base. INV([(1,1,9)], 8, 1) holds, in class A (§2).
3. Transfer. P§3.2 (coverage) and P§3.3 (closure): every INV state has a macro step M or O, of at least 32 machine steps, to an INV state. These statements are about the triples and a, b, and the macro steps are rule instances K → K′ of the parent. By Lemma R, each such instance is a run σK →⁺ σK′ of this machine of the same length, and σK is the K of §1. So coverage and closure hold verbatim for this machine's K-configurations.
4. Conclusion. By induction from the base, the run is an infinite chain of macro steps, each of at least one machine step, so it never halts (progress_nonhalt_cond with P := INV, as in P§5). No macro step reaches the halting cell: each is an exact computation from one K to the next, composed of window lemmas in which F reads only 0. ∎

The parent's invariant argument (P§3) never refers to the parent's own orbit, so it applies to this orbit unchanged.

4. How this orbit relates to its siblings (remark, not used in the proof)

Coupling with 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---. In the shared triple notation, this machine's macro orbit and that machine's (from its first INV state K((1,1,2); 8, 5) at step 483, P§0) reach a fixed offset after 54 macro steps (step 25,718 here, 25,618 there). Observed facts, checked on the two abstract macro orbits for 1,199,946 further macro steps (to t ≈ 3.7·10¹² machine steps, 93 overflows): - from then on, at every macro step, the two states are equal except for one exponent, larger by 3 here, on the top digit: v_1 in class A, u_2 in class B (where the top is (0,0,1)), u_1 in class C; - the same rule fires at every macro step.

Where the +3 travels: O sends the top's v_1 to digit 2's u (class A → B, new top (0,0,1)), the top fall merges digit 2's u into the new top's u (B → C), and the next O sends u_1 to the new top's v (C → A). This explains the tapes at 10⁹ steps: 77,691 cells and 38,839 nonzero here, against 77,685 and 38,836 for that machine. The 6 extra cells are the three extra 10/01 blocks.

The parent's own run is a different orbit, with no such coupling (76,245 cells and 38,119 nonzero at 10⁹ steps).

5. The .v file

The .v is the parent's .v (671 lines, sha256 37cb180280f0896396a28bb32a548a6bfdd22d0b47b2f526230ed2208dbb2053) with exactly these changes: 1. TM_from_str "1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---". 2. σ applied to every state name {{X}}, simultaneously: {{A}} → {{B}} (5 occurrences), {{C}} → {{D}} (22), {{D}} → {{A}} (18). {{E}} (18 occurrences) is fixed, and the parent's file names neither B nor F. This covers the window lemmas, the digit lemmas, the sweeps (LbS, RbS, RoS), the chunks and K. The es/follow proofs re-close unchanged, because σ maps each transition of the parent's table to a transition of this one (Lemma R). 3. Lemma init: c0 -->* K [d1 1 9] 8 1. (687 steps, proved by the parent's unfold K, R0. cbn. solve_init.), and in nonhalt, change (K [d1 1 9] 8 1) with (Kc ([d1 1 9], 8, 1)). The base goal is closed by the parent's own tactic line, since every clause is linear arithmetic on constants (§2). 4. The header comment and the comments that name a head state.

Every other line is the parent's text: every proof script, the statements and proofs of M_spec, Mdrop_spec and O_spec, dg, map0, map1, Oz, Oout, INV, macro_step, and the structure of nonhalt. The file imports only Individual62 from busycoq, has one TM_from_str, and has no Section, Module or Hypothesis.

Lemma R is not a premise of the formal proof. Every window lemma, and through them every rule, is proved by es and follow on this machine's own table; Lemma R explains why the parent's scripts close on it. The step counts are not part of the formal statement (the .v proves -->+ for each rule).

6. Numerical checks

These simulation checks are independent of the .v; the result rests on the .v alone. - Lockstep: from the blank tape, this machine and σ of the parent's table run from 0^inf D> 0^inf agree at every step to 2·10⁷ (state, symbol written, move), with identical tapes at the end. - Window lemmas: each of the 20 lemmas of §1 runs exactly as stated on this table, never reading outside its window, with σ of the parent's transitions. F is entered only in T4, T9 and T13, and reads 0 each time. - Rules: M on 700 random K-configurations (k = 0..6; 273 with a drop, 257 with u* = 0; a, b ≥ 0) and O on 350 (m = 1..7) give exactly the stated result and step count. The rightmost cell read is the right 0 of the flipped 00 (M) and 3 cells right of the old 1001 (O). - Chains: every link of the M and O chains of P§2.2–2.3, renamed by σ, holds on this table (whole tape, head and state) in 47,216 of 47,216 cases (exhaustive boxes plus random cases, and the initial leg K(; 9, 5) → K((1,1,9); 8, 1)). - Initial segment: from blank, K-configurations occur exactly at steps 101, 234, 326, 426 and 687, with the legs of §2. - Real run: all 19,332 macro boundaries from step 687 to step 999,837,328 match the model (whole tape, head and state), and INV holds at each (class A 7,523, B 6,307, C 5,502). Rules used: O 53, M_0 9,639, M_1 4,846, M_2 2,422, M_3 1,209, M_4 602, M_5 298, M_6 and above 262; drops: 30 of the top digit, 12 of a middle digit. - Abstract orbit from the base: INV holds at each of 1.2·10⁶ macro steps (t ≈ 3.7·10¹² machine steps, 16 digits, 93 overflows). - Random INV states (not only reachable ones): 600,000 of 600,000 single macro steps land in INV, each of at least 32 machine steps; all six class transitions A→A, A→B, B→B, B→C, C→A, C→C occur. - No halt in 10⁹ steps from blank; the tape then spans 77,691 cells (−77,517..173), 38,839 of them nonzero.

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