/machines/1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---/submission/README.md · raw

`1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---` never halts

Machine: 1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---, a BB(6) holdout on the current holdout list, class "Skelet 1-like Class 2". busycoq's verify/ has no completed proof of it, byte-exact, renamed or mirrored.
Parent: Rename the states A, B, C, D, E, F to B, C, D, E, A, F, and its table becomes that of 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA--- ("the parent"), 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.
Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9). Print Assumptions nonhalt is closed (no axioms). It compiles in about a minute with -native-compiler yes.
coqchk does not finish within a 600 s cap (the base case is 38 native_compute pieces, as in the parent), so the result rests on coqc's kernel check at Qed, with the VM and native compiler trusted.

Mechanism

The parent's proof is an invariant at the start of each record interval: a left word, a chain of digit blocks all in state U0, and a window (the last chain block and the right region) given exactly as affine functions of u = 9^(e-2). The deep chain gaps are free, apart from residue and minimum, which the encoding builds in.
From 0^inf B> 0^inf the parent's table reaches its record exit 28 after 18,571,902 steps of the parent's run-length simulator. There the window is the parent's own, and only the deep chain differs: its block 5 (the third chain block from the head) has digit gap 17 instead of 13.
So this run enters the parent's invariant at class r5, e = 2, t = 0, and the parent's closure lemma carries it forever.

How the proof works

The parent's simulator and invariant library is kept for the parent's table as tmP: the simulator and its soundness, the block, chain, left-word and right-region lemmas, Lemma S per class, Inv and inv_step.
New: init28 (from B;; tape0 to record exit 28 in 38 native_compute pieces ck_0 .. ck_37), this run's chain L28 and gap variables nus28, and nonhalt_P : ~ halts tmP (B;; tape0).
The conjugacy uses busycoq's own lemmas: perm_phi : Perm tm tmP phi by case analysis, then perm_halts (verify/Permute.v).

Template and what changed

The file is the parent's file, verify/Skelet1LikeC2_1RB0RF_1RC0RB.v, with these changes: tm is this machine and the parent's table is tmP (the step notations are on tmP); the base case (cfg28, b28_i, ck_i, init28) and L28 / nus28 are this run's; nonhalt_P, phi, perm_phi and nonhalt are new. All other code is the parent's, verbatim. The parent's file follows verify/SBCv6.v, Module TM21 (shape) and verify/Sk1like_TC_v1.v (the verified simulator idea). This file has 2,622 lines and imports only Individual62 from busycoq. Apart from the usual native-compiler and coqchk-timeout notes, the second TM_from_str literal (tmP) is the only warning of the automated checks.

Files

1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---.v: the proof, upstream verify/Skelet1LikeC2_1RB0RA_1LC0RE.v.
The informal write-up (a delta proof), the parent's write-up, the full output of the automated checks (statement, forbidden tokens, compile, Print Assumptions, coqchk), and the Discord message.