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

`1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---` never halts

Machine: 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---, a BB(6) holdout on the current holdout list, class "Skelet 1-like Class 2".
The same table started in B (1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---) and in F, mirrored (1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD), gives two more holdouts. This file proves only the string above; the other two have their own files.
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 steps. So the result rests on coqc's kernel check at Qed, with the VM and native compiler trusted.

Mechanism

Between two blank ends the tape is alternating except at defects (two equal neighbours). A sweep complements the cells it crosses, so the defect pattern changes only when the head meets a defect. Sweeps run through fixed 4-cycles of states, and at a defect the head passes, turns or wiggles depending only on the defect's position mod 4 against the head's phase. Halting needs two adjacent defects met in one particular phase.
The defects are a base-3 counter: a left word that counts to 81, a chain of K digit blocks (eight states each) that the head increments once per visit, and a right region of old blocks plus two blocks X, Y that grow and are eaten in step with the chain.
Every 81 x 3^K visits the left word overflows, the chain regroups one defect later, and the right region moves to the next of six classes. After six classes K grows by 2 and the scale u becomes 9u. The long blocks are affine in u, so each grows by a factor close to 9 but not exactly 9: 74844u - 36 becomes 673596u - 36.

How the proof works

Simulator. A symbolic run-length simulator of tm, with run lengths as linear forms, sound for every valuation and every content of abstract tape sides (sstep_spec, reach_spec). Every finite run below is one computation.
Chain. The 17 single-block runs the proof uses: 11 symbolic computations (m = 3) with every gap a variable, and 6 runs of block 1 with concrete lengths; the visit (Lemmas C, C') by list induction (vis_spec); Lemma T, the visits of a whole interval for every K (interval).
Left word. Its 81 episodes, the last one the left record (lw_ep).
Right region. A verified executor runs the six interval programs with 4-cycle jumps, gaps linear in t with u = 9^(e-2) = 1 + 8t (exec_spec, jump_lemma, int_r5 .. int_r4). The X/Y lengths cancel the u-terms exactly.
Induction. Lemma S per class (S_r5 .. S_r4), invariant Inv and inv_step. nonhalt = multistep_nonhalt with init28 (blank tape to record exit 28, about 2.63e12 steps, in 38 pieces) and base28, then progress_nonhalt_cond with Inv.

Template and what changed

The outer shape is verify/SBCv6.v, Module TM21: configurations over a digit-block list, one invariant, a closure lemma, multistep_nonhalt + progress_nonhalt_cond. The computed, proved-correct step is the idea of verify/Sk1like_TC_v1.v. - Changed: TM21's hand-composed window lemmas are replaced by the verified simulator. The digit list is a chain of eight-state blocks with an exit phase. The right region needs an executor with 4-cycle jumps, and one macro step is a whole record interval (81 x 3^K visits) with six invariant classes and u -> 9u per period.

The file is 2,584 lines. The accompanying write-up is the informal proof; its first table maps each section to lemma names.

Files

1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---.v: the proof, upstream verify/Skelet1LikeC2_1RB0RF_1RC0RB.v.
The informal write-up, the full output of the automated checks (statement, forbidden tokens, compile, Print Assumptions, coqchk), and the Discord message.