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

`1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---` never halts

Machine: 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---, a BB(6) holdout on the current list; not in busycoq.
Class: "Skelet 1-like Class 2" (community sheet). It is the table of 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- ("the parent", proved in verify/Skelet1LikeC2_1RB0LE_1RC0RC.v) with the states renamed A->E, B->A, C->B, D->C, E->D (F fixed), no mirror, so it runs the parent's table started in the parent's state B.
Existing work: There may be existing work on this machine by hipparcos (marked done on the community sheet, not yet in busycoq).
The sheet links his October 2025 Discord thread (https://discord.com/channels/960643023006490684/1432566675533992019).
Its opening posts analyse this machine (block rules, a stride acceleration, conjectures) and leave the proof open.
This proof is adapted from the parent's proof, not from that thread.
Result: Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq (commit 0940bb9c). Print Assumptions nonhalt is closed (no axioms). It compiles in 10.4 s with -native-compiler yes, and coqchk re-checks it in 2.0 s (check_kill.txt).

Mechanism

Same counter as the parent. At each return to the right edge the tape is K = 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf, with digits (10)^u 00 (01)^v (bit 0) or (10)^u (01)^v (bit 1); d_m is the least significant bit.
Carry and overflow. Each carry M adds 1: every digit it touches pays one 01, a digit flipped 0->1 gains a 10, and a flipped digit with no 01 left merges into the next one. On overflow (all bits 1), O re-pairs the halves of every digit, and the counter restarts with one more digit.
Different orbit, same macro map. The rules are the parent's with head state A instead of B. Only the start differs: from blank the machine reaches K((1,1,10); 8, 1) at step 732 (class A of the invariant), where the parent reaches K((1,1,2); 8, 5) at step 483.

How the proof works

Rules. 20 window lemmas S1-S6, T1-T14 (es, then shift_rule_L/R or induction) compose into the digit lemmas Lb/Lf/Rb/Ro, the sweeps LbS/RbS/RoS and the rule specs M_spec, Mdrop_spec (carry with a merge) and O_spec.
Invariant. The parent's three-phase INV = Common /\ (A \/ B \/ C) (no merges / top digit about to merge / merged), with parities and lower bounds, rules out the one failure case (a carry reaching a bit-0 digit with no 01 left). step shows that every INV state takes M or O to an INV state.
nonhalt. multistep_nonhalt with init (c0 reaches K [d1 1 10] 8 1 in 732 steps, solve_init), then progress_nonhalt_cond with P := INV.

Template and what changed

It extends the parent's .v, verify/Skelet1LikeC2_1RB0LE_1RC0RC.v (694 lines), which follows the architecture of busycoq SBCv6.v Module TM21 (carries plus a re-pairing overflow). The changes are those of proof.md §5: - the TM string; - the renaming on every state name: {{B}}->{{A}} (22), {{C}}->{{B}} (18), {{D}}->{{C}} (5), {{E}}->{{D}} (18); - init (732 steps to K [d1 1 10] 8 1, against the parent's 483 to K [d1 1 2] 8 5) and the base in nonhalt, closed by the parent's own tactic line; - the header and the comments.

Every proof script, the three rule specs and the invariant part are the parent's text; no tactic was changed. The file is 702 lines, imports only Individual62 from busycoq, and has one TM_from_str. It is a direct proof on the holdout string, with no Flip/Permute bridge.

Files

1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---.v (the proof; upstream verify/Skelet1LikeC2_1RB0RB_1LC0RA.v), proof.md (informal delta proof), parent-proof.md (the parent's informal proof, cited as P§n), check_kill.txt (our verifier's full output: compile against pinned busycoq, theorem statement, forbidden tokens, Print Assumptions, coqchk), discord.md (draft announcement, not posted).