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

Four 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 three machines are 1RB0LD's machine run from 0^inf B> 0^inf, 0^inf C> 0^inf and 0^inf D> 0^inf (the last one mirrored). These are different orbits of the same macro map. In simulation the 1RB1RF and 1RB0RE runs track 1RB0LD's closely (one far block longer by 2, resp. 1), while the 1RB0RD run is not a shifted copy of it (its base has 3 pairs where 1RB0LD's has 4).

Proof for 1RB0LD_… (Skelet1LikeC2_1RB0LD.v). The tape is a binary down-counter on a list of pairs, K(h; P; T) = 0^inf <A (10)^h 11001 [p_1,q_1,d_1] .. [p_L,q_L,d_L] T 0^inf with [p,q,d] = (10)^p (01)^q s(d), s(1) = 0001, s(0) = 0010. The digits d_j form a binary number, least significant next to the head. Each macro step subtracts 1: it touches the pairs up to the borrow pair (p+1, q−1, digit flipped), and a borrow pair whose q runs out fuses with the next pair. At 0 an End sweep adds a tail (10)^t 1; at the next 0 the overflow re-pairs the blocks as (q_j, p_{j+1}), adds a pair and resets h to 2. Rare double run-outs detour through a second tail (101)^2 (01)^k (X1, X2). - 14 sweep lemmas (each a plain es) and three list inductions (PassesR, PassesL, OvPasses) give the nine macro rules Dec, DecMerge, DecMergeTail, DecMergeEmpty, EndR, EndLast, X2, Ov, X1, each K h P T -->+ K h' P' T'. - Some shapes that no rule covers do halt (for example one with a pass-through pair with q = 1), so the proof rests on a per-step invariant J. Its state is (h, P, T, phase, c4). The ghost phase (8 values) records where the run is in the two-cycle period: an E-cycle containing End, then an L-slot containing EndLast or ending in X1. For every pair, J bounds the projected values p + Rt and q − Rt, where Rt is the number of touches the pair still gets before the next re-pairing. It also fixes parities and bounds pairs 1 and 2 and h. A touch leaves the projected values unchanged, so only merges and re-pairings need arithmetic. - Jstep : forall s, J s -> exists s', Cf s -->+ Cf s' /\ J s'. init reaches the base E-start K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); -) in 78,710 steps (one esx), and J_base checks J there. nonhalt is multistep_nonhalt with init, then progress_nonhalt_cond with P := J. - Relation to SBCv6.v Module TM21 (1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE, a different machine), which is only a loose template. Kept: the configuration as a Fixpoint over the pair list, the overflow as a list re-pairing (ovp/ovpX, like TM21's Ov), and multistep_nonhalt + progress_nonhalt_cond. Changed: the macro step is one decrement rather than TM21's whole-countdown LIncs, because merges happen mid-countdown here, and TM21's LWF (q ≥ 2^len, which rules merges out) is replaced by J. The sweep lemmas are new.

How the other three files reuse it. - Skelet1LikeC2_1RB0RD.v and Skelet1LikeC2_1RB1RF.v are the 1RB0LD file with the state names renamed in the statements of the 14 sweep lemmas, of PassesR, PassesL, OvPasses and of K, plus the new TM string and a new start. Every proof script is unchanged (the es proofs re-close on the renamed table), and so are J, Jstep, J_base and nonhalt. - 1RB0RD: init runs 38,732 steps to K(2; (47,32,0),(40,33,1),(13,34,1); -). This base has 3 pairs, the fewest the invariant allows at an E-start (one clause of J is tight, 48 ≥ 48, as it is at 1RB0LD's base: 96 ≥ 96). - 1RB1RF: init runs 79,114 steps to 1RB0LD's base with far q 26 instead of 24. - Skelet1LikeC2_1RB0RE.v defines 1RB0LD's table as tm3 (a second TM_from_str) and keeps the whole development about it verbatim except for the start. The new start gives nonhalt_D : ~ halts tm3 (D;; tape0): init runs 78,911 steps from D;; tape0 to 1RB0LD's base with far q 25. It uses solve_initD, which is busycoq's solve_init started in D, because esx from a non-c0 start falls back to symbolic es. The mirror and the renaming then use busycoq's own lemmas. perm_twin : Perm (flip tm) tm3 phi is checked entry by entry, and nonhalt applies flip_halts (flip_conf c0 is A;; tape0) and perm_halts (phi A = D) and refutes the result with nonhalt_D.

Checked on this branch (BB6 @ 9cf9e88), Coq 8.20.1: - make, then coqc -Q . BusyCoq -Q ./BigInt BigInt -native-compiler yes on each file: Skelet1LikeC2_1RB0LD.v about 65 s, Skelet1LikeC2_1RB0RD.v about 50 s, Skelet1LikeC2_1RB1RF.v about 65 s, Skelet1LikeC2_1RB0RE.v about 40 s; - Print Assumptions Skelet1LikeC2_<…>.nonhalt for each of the four: Closed under the global context; - coqchk -norec BusyCoq.Skelet1LikeC2_<…> for each of the four: passes.

File names. The older machine-named files in verify/ can't be compiled with -Q . BusyCoq because the module name would start with a digit. So, as with BellEatsCounter_1RB0RF.v, I used descriptive names: the class name plus the first two transitions of each machine. Happy to rename them, or to put the four into one file with a Module per machine if you prefer.

Informal write-ups: one per machine, in the bbchallenge Discord (#bb6).

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 and coqchk. I read through the write-up for 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, but the results rest on the Coq files; extra verification and feedback are very welcome.

🤖 Generated with Claude Code