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

This machine is W4-3, 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA--- (the parent), seen in a mirror (L and R swapped) and with its states renamed. It starts in the parent's state F instead of A. So its run is the mirror image of the parent's transition table run from F.

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,080,059,236 steps. From there the parent's induction runs unchanged. The two runs differ in five deep chain gaps, and nothing in the parent's argument reads their values.

• Machine: 1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD, viewer https://bbchallenge.org/1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD
• Holdout: line 588 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 (Eqv_v2.v, and mirrored in Eqv_v3.v), with nothing proved about halting.
• 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).
• Sibling: W4-3b (line 512) is the same table started in B, without the mirror. Its delta proof has the same layout as this one.
• 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 48b42caf…d1d3, 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 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.

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 cell, and A1 = σ(F)1 is this machine's only undefined cell.

Start. The blank tape is its own mirror image, so 0^inf A> 0^inf is (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 cell. 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 at

steps 48-49 (2 cells, to -6),   219-220 (2 cells, to -11),   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,

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. 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. 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. 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 (in the mirror frame), 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, 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 (explanation, not a premise)

At every record exit from 12 on (the earliest 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. The place i grows by one per record, as the single +4 gap of line 512 does.

• At record exit 28 the first four are block 5's inter, digit and separator gaps, and 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. It still lies in the window, or in the right region (then B is only 26 cells further left).

So the record exits 16 to 25 of this start satisfy (L), (C) and (H), but their windows are not the parent's start-up windows of P Appendix C. (The parent's check_proof.py S7 maps each of them to the next on exact numbers.) Record exit 28 is the first record exit of epoch 2, where (W) is V_r5(1) exactly, and that is the base case used here.

This is an observation (checked at record exits 12 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 five differences 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 : 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. In the gap variables (each block lists t, s, a, lp as (gap - minimum)/4, nearest block first):

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 minimums are t = 4, s = 4, a = 1, lp = 5. So the second block (block 6 of section 2.3) has t = 4 + 4 x 233 = 936 against 4 + 4 x 242 = 972. The third block (block 5 of section 2.3) has

(t, s, a, lp) = (52, 8, 1, 5) against (44, 24, 13, 9) 4. The conjugacy: perm_sib : Perm (flip tm) tmP phi by computation. Then busycoq's flip_halts (Flip.v) and perm_halts (Permute.v) give halts tm c0 -> halts tmP (F;; tape0), and nonhalt_P : ~ halts tmP (F;; 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 48b42cafcdb8bf0653960ac7b4552c8cb99e4afe0f26623d183b8deb9020d1d3 (status line above).

7. Evidence

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

The opening run is computed by scripts/rlsim.py, the run-length simulator of line 512's delta stage (copied unchanged). It is independent of the parent's defect model and of the Coq simulator. It runs this machine's own table with every L and R swapped, and S2 checks it cell by cell against direct simulation of the unmirrored string.