/machines/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF/submission/README.md · raw

`1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF` never halts

Machine: 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 2 of the 778-machine list).
Class: "Counter Class 4" (spreadsheet Results row 832, no notes or claims). Its twin 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB (row 833) is tm' of Eqv.v TM113, whose tm is our table started in state B, so the same theorem should settle it (proof.md §6.1). This file proves only our string.
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 3.9 s with -native-compiler yes, and coqchk re-checks it in 1.3 s (check_kill.txt).

Mechanism

The tape is a stack of runs of 1s, 0^inf 1^a_1 0 .. 0 1^a_p <A 0 1^c_1 0^g_1 1^c_2 ... A push (R1) takes one 1 from the top run and makes the next run right of the head the new top frame; at the left edge R3 does the same without the payment, and the new frame gains a 1. When the top run is a lone 1 it finishes: R2 merges it into the run below, which moves back to the right side one cell longer.
An epoch starts at 0^inf <A 0 1^3 0^2 W. Its edge frame has value 4, so it can create 3 children; the machine halts only if an epoch needs a 4th. On a word 1^a 0^2 1^b N, the epoch replays the machine's own history one level down, on the marker tail N (lone 1s with even gaps), for a−1 inner epochs.
Each inner epoch costs 2, or 3 when it absorbs a marker. The top level has no markers, so every top epoch costs 2 and the budget never runs out.

How the proof works

TM layer. Three rules on arbitrary sides (tR1, tR3/tR3c, tR2), each one plain es. A big-step frame semantics Inductive Life x R o (4 constructors) is lifted to the TM by one induction (Life_tm). An epoch Ep W c W' is the life of the edge frame.
Epoch rules. U0–U2 and rule S are concrete traces closed by a search tactic. Rule T (replay, ruleT) and rule X (ruleX) compose inner epochs. The translation lemma is Life_shape: a popped frame's outcome depends on its value only through "enough budget".
Absorption law. Marker words are stored as lists of absorption indices (mw P). Orb builds the predicted costs into the orbit, and Inv/Core record where the unabsorbed markers sit, as exact shifted copies (Sh). main proves both by induction on n + #markers (stepU, stepS, stepT_nabs, stepT_abs).
nonhalt. multistep_nonhalt with init (50 steps, solve_init), then progress_nonhalt_cond over nat * list nat with the marker-free orbit as the predicate.

Template and what changed

No solved proof is close. proof.md §7 names CounterClass2v1.v (3,159 lines) as the nearest, but 10 of its 12 transitions differ. - Kept: its top-level shape (multistep_nonhalt + progress_nonhalt_cond with an index type and a predicate), and an inductive big-step relation for nested calls, as its ClosedCall does. - Changed: everything machine-specific is new: the run-model encoding (lside/rside, updt), Life, the epoch rules, the marker-word combinatorics and the invariant. It imports only Individual62 from busycoq (no Longitudinal). The plan's small-step model and stack-simulation relation were dropped in favour of Life (proof.md §7.1).

The file is 876 lines. The informal proof is proof.md; its §7.1 maps every section to lemma names.

Files

1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v (the proof), proof.md (informal proof), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).