Next: four holdouts, one table up to renaming (Skelet 1-like Class 2), four start states:

`1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---` (row 1278): <FILE_LINK_1RB0LD>
`1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---` (row 1288, from B): <FILE_LINK_1RB0RD>
`1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---` (row 1280, from C): <FILE_LINK_1RB1RF>
`1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---` (row 1289, mirrored, from D): <FILE_LINK_1RB0RE>
PR: <PR_LINK>
Informal write-ups: attached

1RB0LD is a binary down-counter on pairs `(10)^p (01)^q s(d)`: a decrement touches pairs up to the borrow, a pair whose q runs out fuses with the next, and overflow re-pairs the blocks. Nine macro rules and an invariant J (a ghost phase plus per-pair bounds on p + Rt and q - Rt, Rt = touches left before re-pairing; touches leave these fixed) go into `progress_nonhalt_cond`.

1RB0RD and 1RB1RF: 1RB0LD's file with the states renamed (same proof scripts) and a new `init`. 1RB0RE: proves 1RB0LD never halts from `0^inf D> 0^inf`, then uses busycoq's `flip_halts` and `perm_halts`.

All four: top-level `nonhalt: ~halts tm c0`, `Print Assumptions` closed, coqchk passes.

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.