/machines/1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD/submission/README.md · raw

`1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD` never halts

Machine: 1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD, a BB(6) holdout on the current holdout list, class "Skelet 1-like Class 2". Viewer: https://bbchallenge.org/1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD
Parent: mirrored (L <-> R) and renamed (A..F -> F, A, B, C, D, E), its table is that of 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---, all 12 entries. It starts in A, the parent's F, so it runs the parent's table from 0^inf F> 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

In the parent's orientation (this tape is its mirror image), the tape alternates between two blank ends except at defects (two equal neighbours). The defects are a base-3 counter: a left word that counts to 81, a chain of K digit blocks bumped once per visit, and a right region of fossils plus two blocks X, Y that grow in step with the chain.
Every 81 x 3^K visits the left word overflows (a record), the chain regroups and the right region moves to the next of six classes. After six classes K is 2 larger and the scale u becomes 9u. The long gaps are affine in u, so each grows by a factor close to 9 but not exactly 9.
From F the parent's table reaches the parent's record exit 28 with the parent's exact window (last chain block and right region). Only five deep chain gaps differ, and the chain is 60 cells shorter.

How the proof works

The parent's invariant at record exits fixes the left word, the window and the right region. The deep chain gaps are free apart from residue and minimum, which the gap-variable encoding builds in.
New base case: init28 runs F;; tape0 to record exit 28 (about 2.63e12 machine steps, 18,571,554 simulator steps in 38 pieces). The parent's base28 and inv28 then hold for this run's nus28, and the parent's inv_step gives nonhalt_P.
Conjugacy: perm_phi : Perm (flip tm) tmP phi by case analysis, then busycoq's flip_halts (verify/Flip.v) and perm_halts (verify/Permute.v). No new induction.

Template and what changed

The template is the parent's file, verify/Skelet1LikeC2_1RB0RF_1RC0RB.v, whose outer shape is verify/SBCv6.v, Module TM21, with the verified-simulator idea of verify/Sk1like_TC_v1.v. Its simulator and invariant library is kept verbatim, stated for its table renamed tmP. New here: the base case (cfg28, b28_i, ck_i, init28), this run's L28 / nus28, and nonhalt_P, phi, perm_phi, nonhalt. The file has 2,622 lines and imports only Individual62 from busycoq. The only warning of the automated checks beyond the usual native-compiler and coqchk notes is the second TM_from_str literal (tmP).

Files

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