1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---: never halts

This machine never halts. It is a binary counter: each time the head returns to the left edge of the tape, the tape spells out the counter's digits. From there the machine either adds 1 to the counter (a carry) or re-pairs the halves of every digit (an overflow).

Its transition table is the table of another machine, called the parent below, with four of its six states renamed. No symbol and no direction changes. So every window lemma, rule and step formula of the parent's proof carries over word for word, and so does the whole invariant argument.

Only the start differs. This machine starts in the state that corresponds to the parent's state D, so from the blank tape it follows a different orbit of the same macro map. The proof is a 687-step initial segment, a check that the parent's invariant holds where that segment ends, and the parent's induction.

Machine, parent and status

• 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, which is attached alongside this one.
• P§n means §n of that write-up.
• Relation to the parent: 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 2dfa4337b76b3b5e7a7bd91a3260395836d1a7672c146a4e2496ee25a2ad8ff6). It has the architecture of busycoq verify/SBCv6.v Module TM21 (a binary counter with a re-pairing overflow).
• What differs: 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).
• What differs in the .v: the TM string, σ applied to every state name, and the initial segment with its base case (§5).
• Status: formalized in the accompanying .v, verify/Skelet1LikeC2_1RB0LD_1RC0RE.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 (the full map is in §5):
• §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.

Notation

The notation is the parent's (P§1). This machine has head state D where the parent has C.

Head position

Head notation as in P§1:

X> w     the head is in state X, on the first cell of w
w <X     the head is in state X, on the last cell of w
<X w     the head is in state X, on the cell just left of w

The family K

At each return to the left edge, the tape is a K:

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)

Each digit is a triple (u, β, v) with bit β. The rules and the invariant are stated on these triples and on a, b.

Other symbols

Summary

This is the parent's binary counter, with head state D where the parent has C. There are two kinds of macro step:

• a carry M adds 1 to the counter;
• an overflow O re-pairs the halves of every digit.

The three-class invariant INV = Common ∧ (A ∨ B ∨ C) of P§3 is closed under M and O.

What carries over

σ 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.

What changes

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 below:

this machine:   K((1,1,9); 8, 1)   (class A)   at step 687
the parent:     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

The renaming is

σ:   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 same table, mirrored

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.

Relabelling

For a configuration c, let σc be c with its head state renamed by σ. The tape and the head position stay the same.

Lemma R (relabelling).

c → c′ under the parent     if and only if     σc → σc′ under this machine
c is halted                 exactly when       σc is halted

The second line holds because 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

c0 = 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

Each row below is an item of the parent's proof, what it becomes for this machine, and why.

Window lemmas

The window lemmas on this table, with their transitions (head notation as in P§1, see Notation):

      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

Digit lemmas

The digit lemmas of P§2.1 read the same with the head states renamed, with the step counts and side conditions of P§2.1:

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)

The rules M and O

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

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.)

The legs

Each leg is an instance of the rules of §1:

step 101 -> 234    O                 133 = 89 − 4 + 16 + 20 + 4 + 8
step 234 -> 326    M_1               92  = 32 + 32 + 8 + 4 + (8 + 8)
step 326 -> 426    M_0 (LSB drop)    100 = 32 + 40 + 24 + 4
step 426 -> 687    O at m = 0        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

The base is K((1,1,9); 8, 1). Its quantities:

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: the top is (1,1,v), every vbar ≥ 1, every ubar is odd, and S ≥ 1.

The base in the .v

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)
  PA (d1 1 9) 0 0, which is:    canonical (1 ≥ 1, 9 ≥ 1)
                                9 ≥ Rd + 1 = 1
                                ub = 1 odd
                                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 the other starts of this table (remark, not used in the proof)

Coupling with 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---

In the shared triple notation, compare this machine's macro orbit with that machine's, which starts from its first INV state K((1,1,2); 8, 5) at step 483 (P§0). The two 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 near the top, larger by 3 here: 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).
• The next O sends u_1 to the new top's v (C → A).

This explains the tapes at 10⁹ steps:

The 6 extra cells here 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 2dfa4337b76b3b5e7a7bd91a3260395836d1a7672c146a4e2496ee25a2ad8ff6) with exactly these changes:

1. TM_from_str "1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---".
2. σ applied to every state name {{X}}, simultaneously (details below).
3. The base: Lemma init, and a change in nonhalt (details below).
4. The header comment, the comments that name a head state, and five section banners (three cite the parent's write-up as P§n; two say the parent's lemmas renamed by sigma).

Change 2: the state renaming

{{A}} -> {{B}}     5 occurrences
{{C}} -> {{D}}    22 occurrences
{{D}} -> {{A}}    18 occurrences
{{E}}             18 occurrences, fixed

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).

Change 3: the base

Lemma init: c0 -->* K [d1 1 9] 8 1.                          (687 steps)

in nonhalt:
  change (K [d1 1 9] 8 1) with (Kc ([d1 1 9], 8, 1)).

init is proved by the parent's unfold K, R0. cbn. solve_init. The base goal is closed by the parent's own tactic line, since every clause is linear arithmetic on constants (§2).

Everything else is the parent's text

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;
• the structure of nonhalt.

The file imports only Individual62 from busycoq, has one TM_from_str, and has no Section, Module or Hypothesis.

Where each section lives

Lemma R in the formal proof

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.
• The cases are 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).
• INV holds at each: class A 7,523, B 6,307, C 5,502.
• The rules used and the drops are listed after this list.
• 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.
• Long run: no halt in 10⁹ steps from blank; the tape then spans 77,691 cells (−77,517..173), 38,839 of them nonzero.

Rules used in the real run, from step 687 to step 999,837,328:

Drops in that run: 30 of the top digit, 12 of a middle digit.

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