/machines/1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB/submission/README.md · raw

`1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB` never halts

Machine: 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB, a BB(6) holdout. It is on every holdout list since June 2024 (line 626 of the 778-machine list) and on the current 740-machine list (line 590). busycoq's verify/ has no proof of it, byte-exact, renamed or mirrored.
Class: "Bell eats counter" (spreadsheet Results row 1046, no notes or claims). Its table is that of 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC (row 1053, "the parent") with the states renamed, and this proof extends the kill for that machine.
Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c). Print Assumptions nonhalt is closed (no axioms). It compiles in 14.3 s with -native-compiler yes, and coqchk re-checks it in 63.5 s (check_kill.txt).

Mechanism

The parent's table, from another start. Rename the parent's states A, B, C, D, E, F to E, A, B, C, D, F (no mirror) and you get this table, all 12 entries. The machine starts in A, which is the parent's B, so it runs the parent's table from 0^inf B> 0^inf: a different orbit of the same epoch map.
The parent's counter. The hub is K(a,b,X) = 0^inf (110)^a 0 (011)^b B> X 0^inf. Each bounce moves the marker one block and adds 1 to the counter word X. At b = 1 the low digit is eaten and leaves a residue, which the next epoch digests recursively; one bounce can run a whole sub-epoch.
Only the start and the finite part are new. The blank tape reaches the hub K(1,3,t1) at step 55. The parent's epoch invariant first holds 691 model epochs later, at N = 17,712. This orbit first meets the parent's at epoch 795 (N = 20,922, past the threshold), so it gets its own finite part.

How the proof works

The parent's whole development is reused: every finite run as one es, the mutually inductive local pass and epoch map LP/Phi with sound, the computable fuel model, the potentials, the epoch invariant Inv and inv_step.
New: init (55 steps, solve_init), fin691 (691 epochs of the model by vm_compute, turned into a TM run by orbit_sound) and inv691 : Inv 11 17712 Y691. With progress_nonhalt_cond they give nonhalt.

Template and what changed

The file is the kill for 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC with σ applied, and that kill is adapted from busycoq's verify/FractalBEC.v, tm10 (it keeps tm10's marker bounce RInc). What changed: the TM string; σ (A→E, C→B, E→D) on the 59 state tokens, all in statements (the Section 1 runs, LPspec, Phispec, K, Rst); init (K 3 t1 for K 8 t2); the finite part (fin691/inv691 for fin694/inv694); and the nonhalt call. Every other proof script is the parent's. One TM literal, no bridge lemma. The file has 1,755 lines, every lemma top level, and imports only Individual62 from busycoq.

Files

1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v (the proof), proof.md (informal proof; §8 maps it to the .v), parent-proof.md (the parent's write-up, cited there as "parent §n"), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).