Nonhalting proofs of four BB(6) holdouts (Skelet 1-like Class 2) that share one transition table: 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- (called the parent below) and the three holdouts that are its table under a state renaming (two 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 the parent run from 0^inf B> 0^inf, 0^inf C> 0^inf and 0^inf D> 0^inf (the last two mirrored). These are different orbits of the same macro map.

In simulation the B-start and C-start runs lock onto the parent's run. After 54 macro steps their states equal the parent's except for one exponent near the top (v_1, u_2 or u_1, depending on the class of the invariant below), larger by 4 (start B) or 3 (start C). From then on the same rule fires at every macro step (checked on the abstract orbits for about 1.2·10^6 macro steps).

The D-start run is a different orbit: 76,245 cells at 10^9 steps, against 77,685 for the parent.

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

The tape is a binary counter on a list of digits d_1 .. d_m, with d_m least significant, followed by a fixed block:

K(d_1 .. d_m; a, b) = 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b B> 0^inf

(u,0,v) = (10)^u 00 (01)^v      bit 0
(u,1,v) = (10)^u (01)^v         bit 1

A carry M adds 1. Every digit it touches pays one 01 from its v, and the digit flipped 0→1 also gains a 10. A flipped digit with no 01 left merges into the next digit (a drop), and the counter loses a digit.

When all bits are 1, the overflow O swaps the halves of every digit:

K((u_1,1,v_1) .. (u_m,1,v_m); a, b)
  --> K((0,0,u_1), (v_1−1,0,u_2), .., (v_{m−1}−1,0,u_m), (v_m,1,a); b+3, 1)

So the counter restarts at 1 with one more digit. The rules fail only if a carry reaches a bit-0 digit with no 01 left.

The rules.

• 20 window lemmas: the shifts S1–S6 (one block by es, then shift_rule_R/shift_rule_L, or induction for S5) and the turns T1–T14 (each a plain es).
• They compose into the digit lemmas Lb, Lf, Rb, Ro.
• List induction over the digits (LbS, RbS, RoS) gives the three rules, each K .. -->+ K ..:
• M_spec;
• Mdrop_spec, M with a drop: M_spec plus a tape equality by lpow_add;
• O_spec.

The invariant. Which digits drop, and when, is irregular, so a cycle has no closed form. The proof rests on a per-step invariant:

INV = Common ∧ (A ∨ B ∨ C)

The classes follow the run:

• A: a cycle with no drops;
• B: the next cycle, while its top digit (0,0,1) is about to fall;
• C: the rest of that cycle.

The clauses are stated through R_j, the number of carries still to come into digit j before the next overflow (Rof, by recursion on the least-significant-first list). They are:

• parities;
• fuel bounds v_j ≥ R_j + 1;
• lower bounds 2^(j−1) resp. 2^j on ubar_j, the value u_j will have at the next overflow.

All of them are in additive form, with no truncating subtraction. Common's v ≥ 1 for every digit is exactly what rules out the failure case.

The closure. Four arithmetic facts F0–F3 give the step lemma:

• F0, prefix bound: Rof_bound;
• F1, touch: F1;
• F2, drop: F2;
• F3, overflow: Oz_AB/Oz_CA.

step : INV s -> exists s', Kc s -->+ Kc s' /\ INV s'
init : c0 -->* K [d1 1 2] 8 5        (* 483 steps by solve_init, to a class-A state *)

A touch leaves ubar and vbar = v − R (the next-overflow values of u and v) unchanged, so only drops and overflows need arithmetic.

Finally, nonhalt is multistep_nonhalt with init, then progress_nonhalt_cond with P := INV.

Relation to verify/SBCv6.v, Module TM21 (1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE). It is a different machine: under the best state renaming, 10 of the 12 transitions differ. The file follows its architecture.

How the other three files reuse it.

verify/Skelet1LikeC2_1RB0RB_1LC0RA.v (start B) is verify/Skelet1LikeC2_1RB0LE_1RC0RC.v with three changes:

• the new TM string;
• the renaming applied to every state name: {{B}}→{{A}} 22 times, {{C}}→{{B}} 18, {{D}}→{{C}} 5, {{E}}→{{D}} 18 (the file names neither A nor F);
• a new start: init runs 732 steps to K [d1 1 10] 8 1 (class A).

Every proof script is unchanged (the es/follow proofs re-close on the renamed table). So are the three rule specs, INV, step and the tactic line that closes the base in nonhalt.

verify/Skelet1LikeC2_1RB0RE_1LC0RE.v (start D, mirrored) is a separate adaptation, proved directly on its own table without busycoq's flip/permute lemmas.

Its machine part (window lemmas, digit lemmas, sweeps and edge chunks) is verify/Skelet1LikeC2_1RB0LE_1RC0RC.v mirrored by hand, with π = A→B, B→C, C→D, D→A:

l {{q}}> r       ↦   r <{{π q}} l
l <* xs          ↦   xs *> l
shift_rule_R     ↔   shift_rule_L
list literals    unchanged

The three rule statements come out word for word. So the abstract part (INV, F0–F3, closure) is the text of verify/Skelet1LikeC2_1RB0LE_1RC0RC.v byte for byte, except that step is renamed macro_step so that it does not shadow the framework's step. New: init, 215 steps to K [d1 1 3] 4 1 (class A).

verify/Skelet1LikeC2_1RB0LD_1RC0RE.v (start C, mirrored) is verify/Skelet1LikeC2_1RB0RE_1LC0RE.v renamed, with the same three kinds of change as above:

• the TM string;
• the renaming A→B, B→C, C→D, D→A on every state name, with no further mirror: {{A}}→{{B}} 5 times, {{C}}→{{D}} 22, {{D}}→{{A}} 18, {{E}} fixed;
• init: 687 steps to K [d1 1 9] 8 1 (class A).

Every proof script, the three rule specs and the abstract part are the text of verify/Skelet1LikeC2_1RB0RE_1LC0RE.v.

Prior work on 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---. The community sheet marks it as done by hipparcos and links his bbchallenge Discord thread (https://discord.com/channels/960643023006490684/1432566675533992019).

Its opening posts analyse this machine (block rules, a stride acceleration, the left-end cycle and hypotheses on the exponents) and leave the proof open. Thanks to hipparcos for that analysis.

The proof here is adapted from the parent's proof, not from the thread. Section 7 of this machine's write-up translates his rules and cycle into its notation and checks his hypotheses against INV. It also answers his question whether a C C0 collision can occur at the right end of the tape: it cannot.

Checked on this branch (BB6 @ 9cf9e88) with Coq 8.20.1. In verify/, make, then for each of the four files:

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

File names. As in PR 15, the names are descriptive: the class name plus the first transitions of each machine. Here it is the first four transitions rather than two, because verify/Skelet1LikeC2_1RB0RE.v and verify/Skelet1LikeC2_1RB0LD.v are already taken by that PR for other machines.

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. The results rest on the Coq files; extra verification and feedback are very welcome.

🤖 Generated with Claude Code

https://claude.ai/code/session_0147LjPGx2SZPASoExt5bz6W