1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---: never halts (delta proof from W4-3)

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

The parent's proof is an induction over record exits. Its invariant C_r(e) fixes the left word, a window of the chain and the right region exactly. The deep part of the chain is free, apart from residues and minimums.

This start reaches a record exit in C_r5(2) after 2,629,088,387,088 steps. From there the parent's induction runs unchanged. The two runs differ in one deep chain gap, 4 cells longer here, and nothing in the parent's argument reads that gap's value.

• Machine: 1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---, viewer https://bbchallenge.org/1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---
• Holdout: line 512 of the 740 list, byte for byte, exactly once. Sheet (Results tab): class "Skelet 1-like Class 2", no status, notes, sources or "Done By". busycoq has no completed proof of it; it occurs only as an equivalence endpoint.
• Parent: W4-3 (line 341), KILLED_NONHALT, check_kill PASS (sha256 7bda36dc…3f4c). Below, P§n is section n of the parent's write-up (submission/proof.md of the parent; sections 1-8 have the same numbers in its internal proof.md).
• Adjusted invariant: none. Only the base case changes.
• Evidence: check_proof.py, SUMMARY PASS (section 7).
• Status: the informal delta is complete and validated (Checkpoint B).
• The formal delta of section 6 is the .v in this directory, written by the formalization stage.
• It has a check_kill PASS: sha256 ef701290…2296, 2,621 lines, compile 72 s, 0 assumptions, coqchk timeout at 600 s (policy A).
• That run is the formalization stage's (rocq/check_kill.log); it has not been re-run independently here.
• AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

1. The renaming

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

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

Row σ(q) of this table is the parent's row q, with every target state t replaced by σ(t). Symbols and directions are unchanged, so there is no mirror.

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

Lemma R (relabelling). For a configuration c of the parent's table, let σc be c with its head state renamed by σ; the tape and the head cell stay the same. Then c → c′ in the parent's table exactly when σc → σc′ here. And c is halted exactly when σc is, since F1 is the only undefined cell of both tables and σ fixes F.

Start. This machine starts from 0^inf A> 0^inf, which is σ of 0^inf B> 0^inf. So its run is σ of the parent's table run from state B, step for step.

Halting cell. Here only E1 = 0RF enters F, and the machine halts only when F then reads 1. E1 is σ of the parent's A1 = 0RF, which occurs only in the wiggle of P§2.2. So a halt here is σ of the parent's halt: a rightward d = 1 event at a defect e with e + 1 also a defect.

From here on, configurations are written in the parent's state names. In particular the head state at a record exit is the parent's B, which is this machine's A.

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). A left record is a move of λ by 3 cells in 3 consecutive steps.

On this start, λ moves by 1 or 2 cells only during the start-up, at steps

1, 4-5, 18-19, 930-931, 7984, 17719-17720

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

34, 75, 1042, 1265, 29525, 91614, 443229, 648082,
1213303, 4665524, 6953169, 12290878, 43671313, 65535690, 114514475, 398094148

So record n is the n-th 3-cell move, exactly as in the parent (whose small moves are at steps 1, 6-7, 838-839, 7820 and 17531-17532). The third start of this table, line 588, has one extra 3-cell move in its start-up; this one has none.

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,

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

On this start the record exits 16 to 28 are at these steps. Cells are numbered from the start cell 0.

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,088,387,088 the configuration is:

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

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, with these gaps (block 1 has m = 1, the others m = 3):

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,895.

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, every chain gap except one, and the whole right region are the same;
• the digit gap of block 5 is 17 here and 13 in the parent;
• A is 2 cells further left here (-60 against -58), so B is 2 cells further right (111,897 against 111,895);
• this run takes 159,680 more 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. Take the four parts of C_r5(2) in P§3.3 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, so this lo is the parent's lo.

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

digit gaps      1, 1, 1, 1, 17, 37, 8277                      all 1 mod 4, all >= 1
separator gaps  4, 4, 4, 4, 4, 4, 24, 44, 36, 972, 24912, 74808   all 0 mod 4, all >= 4
inter gaps      5, 5, 5, 9, 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 one gap. (C) asks of the deep chain only residues and minimums, and those hold.

4. The argument

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

1. Opening run. By Lemma R, the run of this machine is σ of the parent's table run from 0^inf B> 0^inf. That run reaches record exit 28 after 2,629,088,387,088 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 B, passes through infinitely many record exits and never halts. By Lemma R this machine does the same, 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 (explanation, not a premise)

The record exits 16 to 27 of this start are in C_r(e) too, with exactly the parent's start-up windows (the values of the parent's Appendix C). In fact, at every record exit from 12 on (the earliest checked) the two runs differ in only one gap, 4 cells longer here.

At every record the new left digit joins the chain, so the parse moves one defect along. The extra 4 cells stay in one physical gap, whose index in the chain grows by one per record:

• at record exit 12 it is the 10th gap from lo, among the first defects of the tape (records 12 to 15 are not yet in the invariant's form, which starts at record 16);
• at record exit 16 it is the digit gap of block 2 (K = 3);
• at record exit 28 it is the digit gap of block 5 (K = 7).

Its role cycles digit → separator → separator → inter → digit. The regrouping offsets of P§6.2 change it in the same way in both runs, so the difference stays exactly 4.

Over an epoch K grows by 2, so the chain gains 8 gaps, while the gap moves 6 places. It falls further behind the right end of the chain and stays in the deep part, where only residues and minimums matter. This is an observation (checked at record exits 16 to 28, and to 33 with --full); the induction in section 4 does not need it.

The start-ups differ before that: λ moves at different steps (2.1), and the extra 4 cells first appear somewhere before record exit 12.

6. Formalization delta

The .v in this directory proves Lemma nonhalt : ~ halts tm c0. along these lines. It is the parent's file 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 copied byte for byte, 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 : B;; tape0 -->* cfg28 for tmP, in 38 native_compute pieces of at most 500,000 simulator steps (18,571,902 in all). cfg28 is the record exit 28 of section 2.3. 3. L28 and nus28 are those of this run. inv28, base28 and the record-exit episode are the parent's text. In the 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

The third block is block 5 of section 2.3, whose digit gap a = 1 + 4 x 4 = 17 against 1 + 4 x 3 = 13. 4. The conjugacy: perm_sib : Perm tm tmP phi by computation, and busycoq's perm_halts (Permute.v), give halts tm c0 -> halts tmP (B;; tape0). Then nonhalt_P : ~ halts tmP (B;; tape0) closes it.

check_proof.py S5 checks that cfg28, L28 and nus28 of the .v are the tape of the independent run of section 2 at record exit 28, and that the rest of the file is the parent's text. Whether it compiles is check_kill's verdict: PASS on sha256 ef701290f44d323062af1f5a08583de0158bdb2ba450fbd0c10ad7217e042296 (status line above).

7. Evidence

nice -n 10 python3 -B check_proof.py (default about 1 min; --full about 4 min). Output in check_proof.out and check_proof_full.out.

The opening run is computed by scripts/rlsim.py, a run-length simulator written for this stage. It is independent of the parent's defect model and of the Coq simulator, and it runs this machine's own table, not the renamed one.