/machines/1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB/submission/README.md · raw

`1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB` never halts

Machine: 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 676 of the 778-machine list).
Class: "Counter Class 4" (spreadsheet Results row 833, no notes or claims). It is the trajectory twin of our kill #12 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF (row 832). In busycoq it appears only as tm' of Eqv.v TM113, an equivalence, not a proof.
Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq (commit 0940bb9c). Print Assumptions nonhalt is closed (no axioms). It compiles in 4.2 s with -native-compiler yes, and coqchk re-checks it in 1.3 s (check_kill.txt).

Mechanism

Rename the twin's states A..F to B,C,D,E,F,A. The result is #12 with one transition changed (A0 = 1RA instead of 1RB; in twin names F0 = 1RF), started in #12's state B. It is not #12 up to renaming or mirroring (all 1,440 relabelings checked). F0 is read only at the first step of the left-edge push R3, where it takes a 6-step detour (F0 F0 F1 B1 A1 A0) to the configuration #12 reaches in 2 steps. The tape effect is the same; it costs 4 more steps.
So the run model is #12's. The tape is a stack of runs of 1s, run like a call stack (push R1, edge push R3', pop R2). An epoch on a word W replays the machine's own history one level down, on W's marker tail. Each inner epoch costs 2, or 3 when it absorbs a marker (#12's absorption law).
The difference is the edge. The twin returns to 0^inf <F 0 1^2 0^2 W, where #12 returns to 0^inf <A 0 1^3 0^2 W, so its edge frame has budget 2 instead of 3. The top level has no markers, so every top epoch costs exactly 2: zero slack, but it never runs out.

How the proof works

Rules. tR1, tR3/tR3c (R3', including the detour) and tR2, each one plain es. #12's whole model layer is unchanged: Life/Life_tm, the epoch rules, and main, the absorption law by induction on n + #markers.
Budget 2. The new Ep_tm2 : Ep W 2 W' -> conf [] (2::2::W) -->+ conf [] (2::2::W') carries a cost-2 epoch, proved for #12's value-4 edge frame, over to the twin's value-3 edge frame. It is Life_shape at z = 3, then push0_ok at h = 2, then Life_tm.
nonhalt. init reaches conf [] [2;2;1] in 48 steps (solve_init). Then progress_nonhalt_cond runs with C i := conf [] (2::2::snd i). The exact cost cost [] n = 2, by reflexivity, is what closes the zero-slack step.

Template and what changed

This extends kill #12's .v (876 lines; in #12's own package). The changes: - the tm string; - the head state <{{A}} becomes <{{F}} (9 places: tR1, tR3, tR2, tR3c and conf); - the new Ep_tm2; - init's target, and nonhalt's C and top step; - the comments.

The proof text differs in 4 lines plus the one new lemma, and the file compiled on the first try. It is a direct proof on the holdout string and does not use TM113.eqv. The file is 896 lines and imports only Individual62 from busycoq.

Files

1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v: the proof.
proof.md: the informal delta proof.
parent-proof.md: #12's informal proof, cited as P§n.
check_kill.txt: our verifier's full output.
discord.md: the draft announcement, not posted.