/machines/1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA/submission/README.md · raw

`1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA` never halts

Machine: 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 405 of the 778-machine list) and on the current 740-machine list (line 381). busycoq's verify/ has no proof of it, byte-exact, renamed or mirrored.
Class: "Bell eats counter" (spreadsheet Results row 1022, no notes or claims). Mirrored and renamed, its table is that of 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC (row 1053, "the parent"), 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 17.3 s with -native-compiler yes, and coqchk re-checks it in 71.5 s (check_kill.txt).

Mechanism

The parent's table, from another start. Flip every direction (L↔R) and rename the states A, B, C, D, E, F to E, A, B, F, C, D, and you get the parent's table, all 12 entries. This is the only one of the 720 × 2 maps that does this. The machine starts in A, which is the parent's E, so it runs the parent's table from 0^inf E> 0^inf: a different orbit of the same epoch map.
The parent's counter. In the parent's frame the hub is K(a,b,X) = 0^inf (110)^a 0 (011)^b C> 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 fifth left record, L(16, 0001) at step 1,059, restarts into the hub K(1,17,t1) at step 1,114. That is a base of the parent's orbit invariant (κ = 0, special residue). This orbit never meets the parent's below N = 20,000, so it gets its own finite part: 687 epochs, to N = 17,724, where the invariant of the parent's .v holds.

How the proof works

The parent's whole development is kept for the parent's table as tm30: 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: init7 (1,114 steps from E;; tape0, busycoq's solve_init started in E), fin7 (687 epochs of the model by vm_compute, turned into a TM run by orbit_sound) and inv7 : Inv 10 17724 Y692. With progress_nonhalt_cond they give nonhalt_E : ~ halts tm30 (E;; tape0).
The conjugacy uses busycoq's own lemmas: perm7 : Perm (flip tm) tm30 phi by case analysis, then flip_halts (Flip.v) and perm_halts (Permute.v).

Template and what changed

The file extends the kill for 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC, which is adapted from busycoq's verify/FractalBEC.v, tm10 (it keeps tm10's marker bounce RInc). What changed: tm is this machine, and the parent's table is tm30, with the step notations on it. The parent's init, fin694, inv694, nonhalt_from and nonhalt are replaced by init7, fin7, inv7, nonhalt_from_c (the start made generic), nonhalt_E and the conjugacy (phi, perm7, nonhalt). All other code is the parent's, verbatim. The file has 1,790 lines, every lemma top level, and imports only Individual62 from busycoq. The second TM_from_str literal (tm30) is our checker's only warning.

Files

1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA.v (the proof), proof.md (informal delta proof; §6 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).