1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD: never halts

This machine is a known machine in disguise. Swap left and right, rename its states, and its table becomes the table of 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---, called the parent below. Only the start differs: this machine runs the parent's table from the parent's state F instead of A.

The parent never halts. Its tape carries a base-3 counter made of defects (places where two neighbouring cells are equal), and its proof is an induction over the moments just after a left record ("record exits").

The invariant of that induction fixes the left end, the right end and the last few chain gaps exactly. The rest of the chain only needs gaps of the right residue and size.

From the blank tape this machine reaches such a record exit after 2,629,080,059,236 steps. There it differs from the parent's own run only in five deep chain gaps. From that moment on, the parent's induction applies unchanged.

Machine and status

• Machine: 1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD, viewer https://bbchallenge.org/1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD
• Holdout: on the current BB(6) holdout list, class "Skelet 1-like Class 2". busycoq has no proof of it, as written, renamed or mirrored.
• Parent: 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---, proved non-halting in Coq. Its write-up is attached alongside. Below, P§n means section n of that write-up.
• Status: fully formalized. The accompanying verify/Skelet1LikeC2_1RB1RZ_1LC0LA.v (2,622 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9).
• It compiles in about a minute with -native-compiler yes.
• Print Assumptions nonhalt is closed (no axioms).
• coqchk does not finish within a 600 s cap. The base case is 38 native_compute steps, as in the parent, so the result rests on coqc's kernel check at Qed, with the VM and the native compiler in the trusted base.

Template

The parent's file, verify/Skelet1LikeC2_1RB0RF_1RC0RB.v, takes its outer shape from verify/SBCv6.v, Module TM21, and its verified run-length simulator follows the idea of verify/Sk1like_TC_v1.v. The file for this machine is the parent's file with three changes:

• Two tables. tm is this machine and tmP is the parent's table. The parent's simulator and invariant library is kept verbatim, stated for tmP: the simulator and its soundness, the chain and region lemmas, Lemma S, Inv and inv_step. The base-case pieces and the initial and final theorems are this file's own (section 6).
• A new base case. The parent's table is run from F;; tape0 instead of c0, up to record exit 28. The chain there is this run's.
• A conjugacy. busycoq's flip_halts (verify/Flip.v) and perm_halts (verify/Permute.v) turn a halt of tm into a halt of tmP from F. The permutation lemma perm_phi : Perm (flip tm) tmP phi is checked by case analysis.

No new induction is needed.

Where each section lives in the .v

Summary

The proof has four steps.

1. Relation (section 1). The run of this machine from the blank tape is the mirror image of the parent's table run from 0^inf F> 0^inf, step for step, with the states renamed.

2. Opening run (section 2). That run reaches the parent's record exit 28 after 2,629,080,059,236 steps, without halting.

3. Base (section 3). The configuration there satisfies the parent's invariant C_r5(2). It differs from the parent's own record exit 28 only in five deep chain gaps, which the invariant leaves free.

4. Induction (section 4). The parent's Lemma S carries the invariant forward forever, so the machine never halts.

Section 5 explains why the two runs are so close; the proof does not use it. Section 6 maps the argument to the .v, and section 7 lists the numerical checks.

1. The relation

1.1 Mirror and renaming

Write σ for the map from the parent's states to this machine's states, and φ for its inverse:

sigma:             A -> B,  B -> C,  C -> D,  D -> E,  E -> F,  F -> A
phi = sigma^-1:    A -> F,  B -> A,  C -> B,  D -> C,  E -> D,  F -> E

Row σ(q) of this table is the parent's row q, with every target state t replaced by σ(t) and every direction reversed. The symbols written are unchanged.

For example, the parent's C1 = 0RA becomes 0Lσ(A) = 0LB, which is this machine's D1. Among all 720 renamings, with and without the mirror, this is the only map from the parent's table to this one.

1.2 The run is a mirror image

For a configuration c of the parent's table, let c* be its mirror image with the head state renamed by σ:

cell x of c*      =  cell -x of c
head cell of c*   =  -(head cell of c)
state of c*       =  σ(state of c)

Lemma R (mirror and relabelling). c → c′ in the parent's table exactly when c → c′ here. And c is halted exactly when c* is.

Proof. Both tables read the same symbol in corresponding states. Where the parent writes w, moves d and goes to t, this machine writes w, moves -d and goes to σ(t). The halting part holds because F1 is the parent's only undefined entry, and A1 = σ(F)1 is this machine's only undefined entry. ∎

Start. The blank tape is its own mirror image, so the start of this machine is the mirror image of the parent's table started in F:

0^inf A> 0^inf   =   ( 0^inf F> 0^inf )*

So the run of this machine is the mirror image of the parent's table run from F, step for step.

Halting entry. Here only B1 = 0LA enters A, and the machine halts only when A then reads 1. B1 is the mirror image of the parent's A1 = 0RF under σ. So a halt here is the mirror image of a halt of the parent's table.

1.3 The mirror frame

From here on, positions are given in the mirror frame: cell x below is cell -x of this machine's own tape. Left and right are the parent's, and states are written in the parent's names.

At a record exit the head is in the parent's state B, which is this machine's C. On this machine's own tape it moves left there (C1 = 0LC).

2. The opening run

2.1 Records

The parent numbers its records by the moves of λ, the leftmost cell that has held 1 so far (P§3.1). In the mirror frame, λ is minus the rightmost cell of this machine's tape that has held 1. A left record is a move of λ by 3 cells in 3 consecutive steps.

On this start λ is set to 0 at step 1 and moves 1 cell at step 2. After that it moves by 1 or 2 cells only here:

steps   48-49    2 cells, to -6
steps  219-220   2 cells, to -11
step   6360      1 cell,  to -15

Every other move is by 3 cells in 3 consecutive steps. The first seventeen such moves begin at steps

9, 56, 329, 7891, 10906, 20681, 76882, 422401, 621182,
1179635, 4613856, 6881197, 12196818, 43554645, 65364494, 114281959, 397794936

The parent's start-up has five small moves (steps 1, 6-7, 838-839, 7820 and 17531-17532). This start has one more 3-cell move in its start-up. So record n of this start is its (n + 1)-th 3-cell move, as P§9 says, and record 16 is the move at steps 397,794,936-938.

2.2 Record exits

P§3.3 defines the record exit of record n operationally. It is the first configuration after left record n in which

• the head is in state B reading 1, moving right, and
• exactly 10 + 4K - 2 edges in (lo, h - 1] are defects in the pre-sweep frame.

Here h is the head cell and lo = λ - 1. The number K is K0(r) + 2e, for the class r = (n - 11) mod 6 and the epoch e = (n - 16) div 6 of record n.

On this start the record exits 16 to 28 are at these steps. Head cells are in the mirror frame; on this machine's own tape the head cell is the negative.

None of these runs halts. The proof needs only the last line: the run from the blank tape to record exit 28 is one finite computation.

2.3 Record exit 28

At step 2,629,080,059,236 the configuration is, in the mirror frame:

lo = -94,    A = lo + 34 = -60,    B = 111,833,    hi = 2,961,776
head on cell B - 1 = 111,832, in state B (this machine's C), reading 1, moving right

On this machine's own tape the head is on cell -111,832, in state C, reading 1, moving left.

The left word is the ten defects

A - 32, -27, -26, -21, -20, -15, -14, -9, -8, -4

The chain has K = 7 blocks in state U0. Block 1 has m = 1, the others m = 3 (P§3.2). Where a gap differs from the parent's record exit 28, the parent's value follows in parentheses.

Block 1's digit is at A + 2 and its separator at A + 3. The last separator of block 7 is at B - 2 = 111,831.

The right region, read from B, is

B  -224493-  x1  -673559-  x2  -7-  x3  -9841-  x4  -1942040-  x5  -3-  hi

Against the parent's record exit 28 (the example of P§3.4):

• the left word, K, blocks 1-4 and 7, and the whole right region are the same;
• block 5 has gaps 5, 1, 8, 52 here and 9, 13, 24, 44 in the parent;
• block 6's last separator gap is 936 here and 972 in the parent;
• so the chain is 60 cells shorter here: A is 2 cells further left (-60 against -58), and B is 62 cells further left (111,833 against 111,895);
• this run takes 8,168,172 fewer steps.

3. The invariant holds at record exit 28

Record 28 has class r5 and epoch e = 2. So u = 9^(e-2) = 1 and K = K0(r5) + 2e = 3 + 4 = 7. The four parts of C_r5(2) in P§3.3 are checked in turn.

(L) Left word. lo = A - 34, and the defects left of A are exactly the ten of 2.3. Also λ = lo + 1 = -93 is the leftmost cell that has ever held 1 (in the mirror frame), so this lo is the lo of P§3.1.

(C) Chain. The defects in [A, B] are 4K - 2 = 26 defects forming K = 7 blocks in U0. Block 1 is (A+2; A+3), and the last separator is at B - 2. Every gap has the residue and at least the smallest value of its role:

digit gaps      1, 1, 1, 1, 1, 37, 8277                              all 1 mod 4, all >= 1
separator gaps  4, 4, 4, 4, 4, 4, 8, 52, 36, 936, 24912, 74808       all 0 mod 4, all >= 4
inter gaps      5, 5, 5, 5, 37, 2737                                 all 1 mod 4, all >= 5

Consecutive bases then differ by 2 mod 4, as (C) requires.

(W) Window. J(r5) = 3. The last three chain gaps and the right region are V_r5(1) of P§3.4:

chain window:  8316u - 39,  24948u - 36,  74844u - 36                       = 8277, 24912, 74808
right region:  224532u - 39,  673596u - 37,  7,  (19683u - 1)/2,  1942056u - 16,  3
            =  224493,  673559,  7,  9841,  1942040,  3

(H) Head. The head is on cell B - 1 in state B, the cell holds 1, and state B moves right.

So record exit 28 is in C_r5(2). Its deep chain (blocks 1 to 6 and the inter gap of block 7) differs from the parent's in five gaps, all in blocks 5 and 6. (C) asks of the deep chain only residues and minimums, and those hold.

4. The argument

Theorem. 1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD does not halt from the blank tape.

1. Opening run. By Lemma R, the run of this machine is the mirror image of the parent's table run from 0^inf F> 0^inf. That run reaches record exit 28 after 2,629,080,059,236 steps without halting (section 2).
2. Base. Record exit 28 is in C_r5(2) (section 3).
3. Induction. Lemma S (P§6) is the step:

C_r(e) -->+ C_(r+1)(e) for e >= 2, without halting C_r4(e) -->+ C_r5(e + 1)

Its only hypothesis is the invariant (P§7 for the halting part). The deep chain enters only through the residues and minimums of (C). 4. The deep chain is free. The parent's formal proof states Lemma S this way. Its invariant Inv lists the chain as gap variables, and the deep part of that list is arbitrary (P§10.3). 5. Conclusion. So the parent's table, run from F, passes through infinitely many record exits and never halts. By Lemma R this machine does the same, in the mirror and with its states renamed. ∎

Nothing in the parent's argument after its base case depends on the parent's own orbit. Its base case (P§8) and its twelve concrete steps 16 → 28 are not used here: the configuration at record exit 28 is reached directly.

5. Why the runs agree so closely

This section is an explanation, not a premise of the proof.

At every record exit from 12 to 28 (the ones checked), the two runs' gap lists (lo → each defect → hi) have the same length. They differ in exactly five entries, always by the same amounts:

place      i      i+1     i+2     i+3     i+7
change    -4     -12     -16      +8     -36          (this run minus the parent's; -60 in all)

At every record the new left digit joins the chain, so the parse moves one defect along. So the place i grows by one per record.

• At record exit 28 the first four are block 5's inter, digit and separator gaps. The fifth is block 6's last separator gap (section 2.3).
• From record exit 26 on, all five are deep chain gaps. The window and the right region are then the parent's, and B is 62 cells further left.
• At record exits 16 to 25 the first four are already deep. The fifth is a start-up gap of 969 to 973 cells in the parent (36 fewer here), the first fossil of P§3.4.

At record exits 16 to 25 that fifth gap still lies in the window, or in the right region (then B is only 26 cells further left). So these record exits satisfy (L), (C) and (H), but their windows are not the parent's start-up windows of P Appendix C.

Record exit 28 is the first record exit of epoch 2, where (W) is V_r5(1) exactly. That is why it is the base case here. The start-ups differ before record exit 12: λ moves at different steps (2.1), and the five differences first appear somewhere before it.

6. The formalization

The .v proves Lemma nonhalt : ~ halts tm c0. along the lines of section 4. It is the parent's .v with the following changes, and nothing else.

1. Two tables. tm is this machine and tmP is the parent. The library part of the parent's file is kept word for word, with tm renamed tmP. That part holds the simulator and its soundness, the chain and region lemmas, Lemma S, Inv and inv_step.

2. The base case. init28 : F;; tape0 -->* cfg28 for tmP, in 38 native_compute pieces of at most 500,000 simulator steps (18,571,554 in all). cfg28 is the record exit 28 of section 2.3, in the mirror frame (the parent's orientation).

3. The chain. L28 and nus28 are those of this run. inv28, base28 and the record-exit episode are the parent's text.

4. The conjugacy. perm_phi : Perm (flip tm) tmP phi holds by computation. Then busycoq's flip_halts and perm_halts give

halts tm c0 -> halts tmP (F;; tape0)

and nonhalt_P : ~ halts tmP (F;; tape0) closes it.

6.1 The gap variables

In nus28 each m = 3 block lists four gap variables, nearest block first. They are the gaps t, s (the separator gaps, last one first), a (the digit gap) and lp (the inter gap before the digit), each as (gap - minimum) / 4:

t = 4 + 4 x0,    s = 4 + 4 x1,    a = 1 + 4 x2,    lp = 5 + 4 x3

For this start and for the parent:

this start:  [18701; 6227; 2069; 683] [233; 8; 9; 8] [12; 1; 0; 0] [0; 0; 0; 0]^3
parent:      [18701; 6227; 2069; 683] [242; 8; 9; 8] [10; 5; 3; 1] [0; 0; 0; 0]^3

The first list is block 7 of section 2.3, the window block, and it is the same in both. The second list is block 6:

t  =  4 + 4 x 233  =  936        against      4 + 4 x 242  =  972

The third list is block 5:

(t, s, a, lp)  =  (52, 8, 1, 5)      against      (44, 24, 13, 9)

The last three lists are blocks 4, 3 and 2, all at the minimum gaps.

7. Numerical checks

They are evidence only; the result rests on the .v file alone.

• Relation. σ with the mirror is the only map among the 720 renamings, with and without the mirror. From the blank tape this machine and the parent's table from F run as mirror images, step for step, for 2 x 10^6 steps, and their tapes are mirror images after 10^9 steps.
• Opening run. The tables of section 2 come from a run-length simulator independent of the parent's defect model and of the Coq simulator. It agrees with direct simulation of this machine, cell by cell, at 7 step counts up to 10^8, and at record exit 16.
• Invariant. (L), (C) and (H) hold at every record exit 16 to 28 of this run, and record exit 28 is in C_r5(2).
• The five gaps. The pattern of section 5 holds at every record exit 12 to 28.
• The .v data. cfg28 is the simulated tape at record exit 28, cell by cell, and L28 and nus28 decode to the chain of section 2.3.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic); corrections from an independent audit by GPT-6 Astra (OpenAI).