Nonhalting proofs of three BB(6) holdouts (Skelet 1-like Class 2) that share one transition table: 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA--- (called the parent below) and the two holdouts that are its table under a state renaming (one of them also mirrored), each with a different start state.

With PR 15, PR 16 and a separate PR for 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB (which halts), this covers 12 of the 14 Skelet 1-like Class 2 holdouts on the current list.

Three files, each with a top-level Lemma nonhalt: ~halts tm c0. for its own string. Each imports only Individual62 from busycoq.

In each case this is the only one of the 720 renamings, with or without the mirror, that fits. So the other two machines are the parent run from 0^inf B> 0^inf and 0^inf F> 0^inf (the second mirrored). These are different orbits of the same macro map. In both files phi is the inverse map, from the machine's states to the parent's.

In simulation both runs stay close to the parent's. Each reaches record exit 28 (below) about 2.63·10^12 steps in, with exactly the parent's window there. Its configuration there differs from the parent's only in deep chain gaps: one gap for the B start (a digit gap of 17 instead of 13), five gaps in two blocks for the F start.

Proof for the parent (verify/Skelet1LikeC2_1RB0RF_1RC0RB.v).

Between two blank ends the tape is alternating (…0101…) with a few exceptions, and the head sweeps across it. A sweep runs through a fixed 4-cycle of states and complements every cell it crosses:

moving right: B0 C1 A0 B1   (1RC 0RA 1RB 0RB)
moving left : D1 D0 E1 C0   (0LD 1LE 0LC 1LD)

This keeps the defects (edges between two equal cells) in place, so the defect pattern changes only when the head meets a defect. There the head passes, turns or wiggles, depending on the defect's position mod 4 against the head's phase; a turn or wiggle can also cancel two defects, which happens inside some right-region episodes and is covered by the same rules. The only halt (F reading 1, entered only by A1 = 0RF) is a rightward wiggle at a defect e with e + 1 also a defect.

The defects form a base-3 counter in three regions:

• a left word of 10 defects, which counts to 81 and then moves 3 cells left (a left record);
• a chain of K digit blocks (each a digit defect and its separators), a ternary number that the head increments once per visit from the right;
• a right region of old blocks ("fossils") and two growing blocks X and Y next to the right end.

Every 81·3^K visits the left word overflows, the chain is regrouped one defect later, and the right region moves to the next of six classes r5, r0, …, r4. After six classes K is larger by 2 and the scale u below becomes 9u. The long gaps are affine in u, so they grow by a factor close to 9 but not exactly 9 (for example 74844u − 36 becomes 673596u − 36).

The invariant. At a record exit (just after a left record) of class r and epoch e, let K = K0(r) + 2e and u = 9^(e−2). The invariant C_r(e) fixes:

• the left word;
• the chain: K blocks, all in state U0 (digit value 0), each gap with the residue mod 4 and the minimum of its role, and otherwise free;
• a window: the last few chain gaps and the whole right region, exactly, as affine functions of u.

Lemma S maps C_r(e) to C_(r+1)(e), and C_r4(e) to C_r5(e+1), for e ≥ 2. X and Y stay in step with the counter by an exact cancellation of the u-terms (section 5.4 of the write-up).

The Coq proof.

• A symbolic run-length simulator of tm, whose run lengths are linear forms c + v_1 x_1 + … + v_n x_n over N. It is sound for every value of the x_i and every content of abstract tape sides (sstep_spec, reach_spec).
• A successful run is free of halts and never reads the abstract sides. A gap of residue c is a run of length c + 4x, so one computation covers every x.
• The 17 single-block runs that the proof uses: 11 for the three-separator blocks, with every gap symbolic, and 6 for the first block, whose digit gap is always 1, with concrete lengths. Then the chain visit by induction on the block list (visit3_spec, cb_spec, vis_spec).
• The visits of a whole record interval as a computation on block labels, for every chain length (interval, interval_tm).
• The left word: all 81 episodes in one computation, the last one being the left record (lw_all, lw_ep).
• The right region: a verified executor for interval programs with 4-cycle jumps, by induction on the cycle count (exec_spec, jump_lemma), and the six interval programs with u = 1 + 8t, checked by vm_compute (int_r5 .. int_r4).
• The record visit, the regrouping (regroup, a tape equality by list induction) and the six record-exit episodes. They compose into Lemma S per class (S_r5 .. S_r4) and the closure:

inv_step : Inv s -> exists s', cfgI s -->+ cfgI s' /\ Inv s'
init28   : c0 -->* ev_cfg [] (fun _ => const S0) cfg28
           (* record exit 28: 2,629,088,227,408 machine steps,
              18,571,896 simulator steps in 38 native_compute pieces *)

base28 runs the record-exit episode into the state of inv28 : Inv (C5, 2, 0%N, nus28) (class r5, epoch 2).

Finally, nonhalt is multistep_nonhalt with this base case, then progress_nonhalt_cond with Inv.

Templates. The outer shape follows verify/SBCv6.v, Module TM21: a configuration built from a list of digit blocks, one invariant with a closure lemma, and multistep_nonhalt + progress_nonhalt_cond. The simulator follows the idea of verify/Sk1like_TC_v1.v: a step function that is computed, proved correct once, and run by evaluation. New here: one macro step is a whole record interval (81·3^K visits), the invariant has six classes, and the right region needs the jump executor.

How the other two files reuse it.

Both are verify/Skelet1LikeC2_1RB0RF_1RC0RB.v with three changes:

• Two tables. tm is the machine's own string, and tmP is the parent's table. The step notations are for tmP, so the parent's library (the simulator and its soundness, the block, chain, left-word and right-region lemmas, Lemma S, Inv and inv_step) is kept word for word, stated for tmP.
• A new base case. init28 runs tmP from the new start to that run's record exit 28, again in 38 native_compute pieces, with that run's chain (L28, nus28). inv28 and base28 are the parent's text, and the parent's closing proof gives nonhalt_P : ~ halts tmP (B;; tape0), resp. (F;; tape0).
• The conjugacy, with busycoq's own lemmas. A Perm lemma, checked entry by entry, and perm_halts (verify/Permute.v) turn halts tm c0 into a halt of tmP from the new start. The mirrored file applies flip_halts (verify/Flip.v) first.

The invariant asks of the deep gaps only their residue mod 4 and minimum, so no new induction is needed.

Checked on this branch (BB6 @ d026880) with Coq 8.20.1. The framework .vo files were built with make at 9cf9e88 and reused: d026880 differs from 9cf9e88 only by the eight Skelet1LikeC2 files of PR 15 and PR 16, so the framework is the same. Then, in verify/, for each of the three files:

coqc -Q . BusyCoq -Q ./BigInt BigInt -native-compiler yes Skelet1LikeC2_<…>.v
Print Assumptions Skelet1LikeC2_<…>.nonhalt.
timeout 600 coqchk -Q . BusyCoq -Q ./BigInt BigInt -norec BusyCoq.Skelet1LikeC2_<…>

coqchk warns Native compiler is disabled, falling back to VM conversion test. After 600 s it was on ck_15 of the 38 base-case pieces ck_0 .. ck_37, in all three files. So these results rest on coqc's kernel check at Qed, with the VM and the native compiler in the trusted base. The times were measured on a lightly loaded machine.

File names. As in PR 15 and PR 16, the names are the class name plus the first transitions of each machine. It is four transitions, as in PR 16, because two-transition prefixes such as 1RB0RA_ are shared by many holdouts.

A module name cannot contain -, so in 1RB---_1LC0LA_… the undefined A1 is written 1RZ, the usual spelling of a halting transition (Z = halt state): verify/Skelet1LikeC2_1RB1RZ_1LC0LA.v. The exact string is in the file header and in TM_from_str.

Happy to rename them, or to put the three into one file with a Module per machine if you prefer.

Informal write-ups: one per machine, in the bbchallenge Discord (#bb6). The write-ups for the B and F starts build on the parent's.

AI disclosure: the informal proofs and the Coq formalizations were produced with Claude Code (Opus 5.5) and checked by compiling against unmodified busycoq, with Print Assumptions (coqchk does not finish within 600 s, see above). The results rest on the Coq files; extra verification and feedback are very welcome.

🤖 Generated with Claude Code