/machines/1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---/submission/proof.md · raw

1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE--- never halts

This machine is the machine 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA--- (the parent) under a renaming of its states. It starts in the parent's state B instead of A. So it runs the parent's table, only from a different start.

The parent's proof is an invariant at record exits. It holds for every tape of a given shape, whatever the deep chain gaps are. This start reaches a tape of that shape, so the parent's induction finishes the proof.

1. The renaming

Write phi for the state map from this machine to the parent:

phi:  A -> B,  B -> C,  C -> D,  D -> E,  E -> A,  F -> F

Row q of this machine becomes the parent's row phi(q) when every destination state in it is renamed by phi. Entry for entry (12/12), for every state q and symbol s:

this machine:  q reading s       ->  write w, move d, go to q'
the parent:    phi(q) reading s  ->  write w, move d, go to phi(q')

For example, A0 = 1RB here, and the parent's B0 = 1RC, with phi(B) = C. There is no mirror: the directions agree. The undefined entry F1 is the parent's undefined F1.

So this machine halts from the blank tape exactly when the parent halts from

0^inf B> 0^inf

2. The parent's invariant

The parent's write-up is attached alongside. Its section 3.3 defines an invariant C_r(e) at every record exit. It has three parts:

the left word W_1;
a chain of K digit blocks, all in state U0, whose gaps have fixed residues mod 4 and fixed minimums;
a window: the last few chain gaps and the right region, given exactly as affine functions of u = 9^(e-2).

The deep chain gaps (those outside the window) are free, apart from residue and minimum. The record lemma maps C_r(e) to C_(r+1)(e) (and C_r4(e) to C_r5(e+1)) for every e >= 2. Its proof never looks at the values of the deep gaps.

The parent's formal proof, verify/Skelet1LikeC2_1RB0RF_1RC0RB.v, states this directly (its write-up, section 10.3). Its invariant Inv lists the chain as gap variables, and the deep part of that list is arbitrary.

3. The base case for this start

Run the parent's table from 0^inf B> 0^inf. After 18,571,902 steps of the parent's run-length simulator (it crosses a whole alternating stretch in one step), the tape is a record exit of class r5 with e = 2 (u = 1).

Compared with the parent's own record exit 28:

the right region is identical;
the window block of the chain is identical;
the deep chain differs in one place: block 5 (the third from the head) has digit gap 1 + 4 * 4 = 17 instead of 1 + 4 * 3 = 13.

In gap variables (each block lists t, s, a, lp as (gap - minimum) / 4, nearest block first):

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

So the tape satisfies C_r5(2), and the parent's induction applies from there on.

4. Conclusion

From the blank tape this machine follows the parent's run from B. That run reaches C_r5(2) without halting.

The invariant is a statement about record exits, not about every step. From each record exit in the invariant, the parent's record lemma (its Lemma S) gives a finite run of at least one step, without a halt, to the next record exit, which is again in the invariant.

These runs follow one another forever, so the run never halts. In the formal proof this is inv_step together with busycoq's progress_nonhalt_cond.

Checks

The formal proof, verify/Skelet1LikeC2_1RB0RA_1LC0RE.v, is the parent's formal proof with a new base case. The base case is 38 pieces of the simulator, each one a computation checked by the proof assistant. The renaming is checked entry by entry.

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