/machines/1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC/submission/README.md · raw

`1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC` never halts

Machine: 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC, a BB(6) holdout. It is on every holdout list from 2024-06-14 through 2026-10-07 (line 748 of the 778-machine list) and on the current 740-machine list (line 710). busycoq's verify/ has no proof of it, under any renaming or mirror.
Class: "Bell eats counter" (spreadsheet Results row 1053, no notes or claims).
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 15.5 s with -native-compiler yes, and coqchk re-checks it in 67.7 s (check_kill.txt).

Mechanism

A marker bounce feeding a counter. The hub is 0^inf (110)^a 0 (011)^b C> X 0^inf. Each bounce moves the 0 marker one block to the right, adds 1 to the counter word X and spends one 011 of the budget b. X is binary, LSB first: 3-cell blocks d01 (001)^e separated by 000, ending in a 4-stage tail.
Partial eats leave a residue. At b = 1 the low block is eaten. An a-block (d = 0) gives new budget. A b-block (or a bare tail) sweeps (110)^a into a left record, and the next epoch restarts with budget N = k + 1 and a residue that is not a clean counter.
Recursive digestion. The first bounces of an epoch digest the residue. At a b-block one bounce runs a whole sub-epoch on the rest of the word, and the next level runs nested inside the block it leaves. The machine can only halt at an eat that comes before the digestion ends.

How the proof works

Every finite run is one es lemma, with symbolic exponents and any left context. Words have a syntax with an encoding into tapes. The local pass LP and the epoch map Phi are mutually inductive relations (the nested sub-epoch is an LP constructor whose premise is a Phi), and sound turns every derivation into a TM run.
The digestion fits in the budget (the write-up's Lemma D). One potential over counter positions bounds the positions a digestion creates. A weighted one, with future positions prepaid, bounds the digestion's cost and the merged block exponents. An invariant on epochs (block count, two weighted exponent masses, the residue's prefix, a lower bound on N) is closed for N ≥ 17,705.
nonhalt: init (solve_init to K(1,8,010001)), then 691 epochs of a computable fuel model, proved sound, by vm_compute to N = 17,713, where the invariant holds; then progress_nonhalt_cond with the invariant.

Template and what changed

Adapted from busycoq's verify/FractalBEC.v, tm10 (1LB0LF_1LC1LF_1RD1LB_---0RE_1RA0RE_0LA0RC). Mirrored, tm10 differs from this machine only in C1 (1RB there, 0RE here). - Kept: tm10's marker bounce RInc, mirrored, as the region pass RP0/RP1; es for every finite run; multistep_nonhalt from an exact start. - Changed: tm10's counter (LInc, 2-cell digits) and its whole-counter eat (Ov) do not occur here, and neither does its induction on the epoch number with progress_nonhalt_simple. Everything above the bounce is new: the word syntax, LP/Phi with the nested sub-epoch, counter words and their potentials, the epoch invariant with progress_nonhalt_cond, and the fuel model for the finite part.

The file has 1,726 lines, every lemma top level, and imports only Individual62 from busycoq.

Files

1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v (the proof), proof.md (informal proof; §8 maps it to the .v), check_kill.txt (our verifier's full output), discord.md (draft announcement, not posted).