1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---: never halts

• Machine: 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, viewer https://bbchallenge.org/1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---
• Holdout lists: line 34 of data/holdouts/2026-10-07_778.txt, byte for byte, and present in all 26 snapshot files in data/holdouts/ (2024-06-14 to 2026-10-07). Sheet: the Results tab gives the class "Skelet 1-like Class 2" and the note "Machine with the most common transitions". The Level 0 tab says "Fun fact: machine with the most common transitions". There is no status, link or "done by" entry, so no Discord thread is linked. Not on the data/discord/ lists. Unclaimed (ground rule 7, notes.md; check 10).
• Written for: the string itself (no mirror, no renaming). All tapes below are in this machine's orientation. The head works at the left end, and the fixed marker 1001 sits at the right.
• Parent: our kill #11 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- (KILLED_NONHALT, check_kill PASS). This machine runs #11's table, mirrored, started in #11's state D (§0). The rules here are derived afresh, on this table, from window lemmas checked on this table. The invariant argument (§3) is #11's word for word, because it never looks at the tape.
• Status: informal proof, revised after the skeptic review (Review log at the end). Stage informal_proof; Checkpoint B pending (non-blocking). Not a kill: only tools/check_kill.sh PASS counts. Evidence: check_proof.py, 14 checks, ALL PASS (§7). The mirror dictionary of the lemma plan (§6) is confirmed in Rocq on the window lemmas, digit lemmas, K and init (rocq/plan_check.v, 1.2 s). #11's abstract part, verbatim, compiles against this machine's tm, K and init with the three rule specs as hypotheses (rocq/abstract_check.v, 8.9 s, §6). So the Rocq work left is exactly M_spec, Mdrop_spec and O_spec on this table.
• AI assistance: written by Claude (Anthropic) under Dennis's direction.

     0    1
A   1RB  0RE
B   1LC  0RE
C   1LD  0LD
D   1RA  0LC
E   1RA  1RF
F   1RA  ---        halting transition: F reads 1 (F is entered only by E1)

0. Relation to kill #11, and the four holdouts with this table

Mirror #11's table (L ↔ R) and rename its states by π = (A,B,C,D,E,F) ↦ (B,C,D,A,E,F). The result is this string, cell by cell (check 10). For a configuration c of #11, write μc for its reflection (the tape read right to left, head state renamed by π). Then c → c′ under #11 if and only if μc → μc′ under this machine, and c is halted exactly when μc is. The blank tape is its own reflection, so this machine's run is the reflection of #11's table run from 0^inf D> 0^inf.

We use the relation only to cross-check the window lemmas (check 11: each one is the reflection of #11's lemma of the same name) and to reuse #11's abstract invariant and its Rocq form (§3, §6). Every rule below is proved on this machine's own table.

Four holdouts on the 778 list are relabelings of this table. Check 10 searched all 720 state permutations, each with and without mirroring.

All four first INV states are in class A. The step and digit values for B, C and D agree with #11's proof.md §4. data/holdouts/2026-10-07_eqv_1590.txt keeps the four in four separate groups, with this machine as a singleton (check 10). So each needs its own proof, with its own TM_from_str.

1. Family and notation

K(d_1 .. d_m ; a, b) := 0^inf <C (01)^b 000 (01)^a  d~_m .. d~_2 d~_1  1001 0^inf

digit d = (u, beta, v):   d~(u,0,v) := (10)^v 00 (01)^u        "bit 0"
                          d~(u,1,v) := (10)^v (01)^u           "bit 1"

• Head notation. X> w means the head is in state X on the first cell of w. w <X means it is in state X on the last cell of w. So 0^inf <C (01)^b has the head on the blank cell just left of the block. This is busycoq's {{X}}> / <{{X}}, and the same convention as #11's proof.md.
• d_1 is next to the fixed 1001 and is the most significant bit. d_m is next to the block and is the least significant bit. m ≥ 1, except at step 82 of the init (§4).
• The triple (u, beta, v) means exactly what it means in #11: u counts the 01s on the marker side, and v counts the 10s on the block side. Only the tape picture is mirrored. So the rules and the invariant, stated on triples, are #11's.
• Canonical form. Every digit has v ≥ 1, and every bit-1 digit has u ≥ 1. Bit-0 digits may have u = 0. INV states are canonical, because Common (§3) requires it, and M and O map INV states to canonical states (§3.3). Outside INV, M can make (u,0,0), the precursor of the failure mode (§2.4).
• Re-reading (no machine steps). A bit-1 digit with v = 0 is just (01)^u, so it fuses with what lies to its left. If the digit to its left is (u',β',v'), the two read as (u'+u, β', v'). If it is the least significant digit, it joins the block: a := a + u. We call this a drop of that digit.

Derived quantities. They are used only in the invariant, not in the rules, and all are exact integers.

bits beta_1..beta_m, read as a binary number with beta_m least significant:
U_j  = (beta_1 .. beta_j)_2        V = U_m          R_tot = 2^m - 1 - V
R_j  = 2^j - 1 - U_j               carries that will still touch d_j before the next overflow, if no digit above it drops
R1_j = (R_j + 1 - beta_j) / 2      how many of those set d_j to 1   (R_j ≡ 1 + beta_j mod 2)
ubar_j = u_j + R1_j                vbar_j = v_j - R_j               u_j, v_j as they will be at the next overflow
S = a + R_tot - (2^(m+1) - 2)      T = b - (2V - 1)

§6 gives the same definitions in additive form for Rocq, with no subtraction or division.

2. Rules

In busycoq comment-block style:

1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---

K(d_1 .. d_m; a, b) := 0^inf <C (01)^b 000 (01)^a d~_m .. d~_1 1001 0^inf
d~(u,0,v) := (10)^v 00 (01)^u,   d~(u,1,v) := (10)^v (01)^u        (d_m least significant)

start from K((1,1,3); 4, 1)                                   (step 215, §4)

M  (carry; some bit is 0; j* = index of the LAST bit-0 digit, k = m - j*):
   K(.., (u,0,v), (u_j,1,v_j)_{j*<j<=m}; a, b)
     --> K(.., (u+1,1,v-1), (u_j,0,v_j-1)_{j*<j<=m}; a+1, b+2)
   steps 32 + 8a + 8b + 4v + sum_{j>j*} (8 u_j + 4 v_j)
   needs v >= 1 (u >= 0), u_j >= 1 and v_j >= 1 for j > j*, a >= 0, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, §1)
O  (overflow; all bits 1):
   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)
   steps 89 - 4m + 8a + 20b + 4 sum u_j + 8 sum v_j
   needs m >= 1, all u_j, v_j >= 1, a >= 1, b >= 0

On the tape:

M:  0^inf <C (01)^b 000 (01)^a [(10)^v_j (01)^u_j]_{j=m..j*+1} (10)^v 00 (01)^u X
      --> 0^inf <C (01)^(b+2) 000 (01)^(a+1) [(10)^(v_j-1) 00 (01)^u_j]_{j=m..j*+1} (10)^(v-1) (01)^(u+1) X
O:  0^inf <C (01)^b 000 (01)^a [(10)^v_j (01)^u_j]_{j=m..1} 1001 0^inf
      --> 0^inf <C 01 000 (01)^(b+3) (10)^a (01)^v_m [(10)^u_j 00 (01)^(v_(j-1)-1)]_{j=m..2} (10)^u_1 00 1001 0^inf

Here X is everything right of d_{j*}, and M never reads it. The M and O rules are not taken from simulation. §2.1 lists 20 window lemmas, and §2.2–2.3 derive M and O from them as chains of intermediate configurations. Each step count is the sum along its chain. The same O chain with no digits (m = 0) gives K(; a, b) --> K((1,1,a); b+3, 1) in 89 + 8a + 20b steps (a ≥ 1). It occurs once, inside the initial segment (§4), and the invariant argument does not use it.

2.1 Building blocks

A window lemma w → w' says: started on the cells of w, the machine runs the stated number of steps without reading a cell outside w (the last step may move the head onto a neighbouring cell) and leaves w'. Such a lemma holds in every tape context. All 20 lemmas below are checked by exact finite runs on this table (check 11). For T1–T14 that check is the proof. For S1–S6 it checks one block, and induction on n gives every n. For example, S5 is (10)^(n+1) 11 <D = (10)^n 1011 <D → (10)^n 11 <D 01 → 11 <D (01)^n 01 (one block, then the IH). Check 1 also runs S1–S6 directly for n up to 1000. Each lemma is the reflection of #11's lemma of the same name (check 11). The names are kept so that §6's port is a name-for-name map.

Shift lemmas:

S5 and S6 are the back-bounces. Each block costs 6 steps for a 2-cell advance, because the head doubles back over cells it has just written (S5 moves L L R R L L, S6 moves L R R L L L).

Finite lemmas:

Digit lemmas (compositions; u, v of one digit):

In Ro, S6 starts on the first 0 of (01)^u = 0 1 (01)^(u−1). - Lb sweeps a bit-1 digit rightward. - Lf flips the bit-0 digit. - Rb restores a swept digit as bit 0 on M's way back. - Ro does the same in O.

2.2 Derivation of M

Notation: - X is everything right of d_{j*}. It is never read. - (u*, v*) is d_{j*} = (u*,0,v*). - Y = Π_{i=k..1} (10)^v_i (01)^u_i is the trailing bit-1 digits, written left to right. i = k is d_m, and i = 1 is d_{j*+1}.

                                                                                        steps
    0^inf <C (01)^b 000 (01)^a Y (10)^v* 00 (01)^u* X
 Phase 1: left-edge preamble with a dip into the 000 gap                                4b+10
T1  0^inf 10 E> (01)^b 000 (01)^a Y ..                                                  3
S4  0^inf (10)^(b+1) E> 000 (01)^a Y ..                                                 2b
T2  0^inf (10)^(b+1) <C 001 (01)^a Y ..                                                 5
S1  0^inf <C (01)^(b+1) 0 (01)^(a+1) Y ..                                               2b+2
 Phase 2: one long right sweep, up to the 00 of d_{j*}                                  2a+2b+9+4v*+Σ(2u_i+2v_i)
T1  0^inf 10 E> (01)^(b+1) 0 (01)^(a+1) Y ..                                            3
S4  0^inf (10)^(b+2) E> 0 (01)^(a+1) Y ..                                               2b+2
T3  0^inf (10)^(b+2) 110 E> (01)^a Y ..                                                 3
S4  0^inf (10)^(b+2) 110 (10)^a E> Y (10)^v* 00 (01)^u* X                               2a
Lb  0^inf (10)^(b+2) 110 (10)^a Y' E> (10)^v* 00 (01)^u* X        (i = k down to 1)     Σ(2u_i+2v_i)
                         Y' = Π_{i=k..1} 11 (01)^(v_i−1) (10)^u_i
Lf  0^inf (10)^(b+2) 110 (10)^a Y' 11 <D (10)^(v*−1) (01)^(u*+1) X                      4v*+1
 Phase 3: leftward pass with 2-cell back-bounces, then a plain run to the edge          6a+2b+13+Σ(6u_i+2v_i)
Rb  0^inf (10)^(b+2) 110 (10)^a 11 <D Y'' (10)^(v*−1) (01)^(u*+1) X   (i = 1 up to k)   Σ(6u_i+2v_i)
                         Y'' = Π_{i=k..1} (10)^(v_i−1) 00 (01)^u_i
S5  0^inf (10)^(b+2) 110 11 <D (01)^a Y'' ..                                            6a
T8  0^inf (10)^(b+2) <C 00001 (01)^a Y'' ..                                             9
S1  0^inf <C (01)^(b+2) 000 (01)^(a+1) Y'' (10)^(v*−1) (01)^(u*+1) X                    2b+4

The last line is K(.., (u*+1,1,v*−1), (u_i,0,v_i−1)_i; a+1, b+2). The sum is (4b+10) + (2a+2b+9+4v*) + (6a+2b+13) + Σ(8u_i+4v_i) = 32 + 8a + 8b + 4v* + Σ(8u_i+4v_i).

Head path. - Phase 1 runs right only as far as the 000 gap, turns (T2) and returns to the edge. - Phase 2 is the only long rightward leg. Its rightmost read is the right 0 of d_{j*}'s 00: T6 reads both cells, then moves left. So M is a side rule, and the tape X right of that 00 is never read (checks 2 and 12 confirm the rightmost cell exactly). - Phase 3 moves left. It doubles back once per 10 block (S5, on the swept digits' (10)^u_i and on (10)^a). It crosses the (01)^(v−1) blocks and the final (10)^(b+2) with plain sweeps (S2, S1).

When v* = 1, the flipped digit (u*+1,1,0) = (01)^(u*+1) drops (§1). When some v_i = 1, the result has (u_i,0,0). That can happen only outside INV (§3.3).

2.3 Derivation of O

Let Y = Π_{i=m..1} (10)^v_i (01)^u_i, with all digits bit 1.

                                                                                        steps
    0^inf <C (01)^b 000 (01)^a Y 1001 0^inf
 Phases 1–2 as in M, with Lb on all m digits and no Lf                                  (4b+10)+(2a+2b+8)+Σ(2u_i+2v_i)
    0^inf (10)^(b+2) 110 (10)^a Y' E> 1001 0^inf              Y' = Π_{i=m..1} 11 (01)^(v_i−1) (10)^u_i
 Phase 3: turn at the far right
T9  0^inf (10)^(b+2) 110 (10)^a Y' <C 000 1001 0^inf                                    13
 Phase 4: leftward pass
Ro  0^inf (10)^(b+2) 110 (10)^a <C Y''' 000 1001 0^inf      (i = 1 up to m)             Σ(2u_i+6v_i−4)
                         Y''' = Π_{i=m..1} 000 (01)^(v_i−1) 1 (01)^(u_i−1)
 Phase 5: left end                                                                      2a+8b+30
S1  0^inf (10)^(b+2) 110 <C (01)^a Y''' ..                                              2a
T11 0^inf (10)^(b+2) 11 <D 1 (01)^a Y''' ..                                             1
S5  0^inf 11 <D (01)^(b+2) 1 (01)^a Y''' ..                                             6b+12
T12 0^inf 10110 E> (01)^(b+2) 1 (01)^a Y''' ..                                          13
S4  0^inf 10110 (10)^(b+2) E> 1 (01)^a Y''' ..                                          2b+4
 Phase 6: short right sweep over the a block, to the 000 that Ro left before d_m        2a+1
T13 0^inf 10110 (10)^(b+2) 110 E> (01)^(a−1) Y''' ..                                    3
S4  0^inf 10110 (10)^(b+2) 1 (10)^a E> 000 (01)^(v_m−1) ..                              2a−2
 Phase 7: turn in that 000, final run to the edge                                       2a+6b+27
T2  0^inf 1011 (01)^(b+3) (10)^a <C 001 (01)^(v_m−1) ..   (0 (10)^(b+2) 1 = (01)^(b+3))   5
S1  0^inf 1011 (01)^(b+3) <C (01)^a 001 (01)^(v_m−1) ..                                 2a
S6  0^inf 1011 <C 0 (01)^(b+3) 1 (01)^(a−1) 001 (01)^(v_m−1) ..                         6b+18
T14 0^inf <C 0100 0 (01)^(b+3) 1 (01)^(a−1) 001 (01)^(v_m−1) ..                         4

Re-read the final tape with 1 (01)^(n−1) 0 = (10)^n and 01 (01)^(n−1) = (01)^n, splitting each 000 of Y''' as 0 | 00:

0^inf <C 0100 0 (01)^(b+3) 1 (01)^(a−1) 001 (01)^(v_m−1) 1 (01)^(u_m−1) [000 (01)^(v_i−1) 1 (01)^(u_i−1)]_{i=m−1..1} 000 1001 0^inf
  = 0^inf <C 01 000 (01)^(b+3) (10)^a (01)^v_m [(10)^u_(i+1) 00 (01)^(v_i−1)]_{i=m−1..1} (10)^u_1 00 1001 0^inf
  = 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)

The sum is (4b+10) + (2a+2b+8) + 13 + (2a+8b+30) + (2a+1) + (2a+6b+27) + Σ(4u_i+8v_i−4) = 89 − 4m + 8a + 20b + 4Σu_i + 8Σv_i.

The domain: - Lb and Ro need u_i, v_i ≥ 1. - T13 and the S6 of phase 7 use the first 0 1 of (01)^a, so a ≥ 1. - T9 needs 0^inf on the right. It reads the three blank cells right of 1001 and moves the marker three cells right, so the rightmost cell visited moves 3 cells per overflow (checks 3 and 13).

O has two long rightward legs: phase 2, and the short phase 6.

O at m = 0 (the init, §4). The same chain with no digits works: phase 4 is empty, and phase 6 ends on T9's 000. The final tape is 0^inf <C 01 000 (01)^(b+3) 1 (01)^(a−1) 001 1001 0^inf = 0^inf <C 01 000 (01)^(b+3) (10)^a 01 1001 0^inf = K((1,1,a); b+3, 1). The step count is 89 + 8a + 20b (check 13, box and random cases with m = 0).

2.4 What the rules do, in words

The digits form a binary counter, and each M is one increment. - M flips the trailing 1s to 0 and the last 0 to 1. Every digit it touches pays one 10 from its v, and a digit flipping 0→1 also gains a 01. - When all bits are 1, O swaps the two halves of every digit. Each (01)^u becomes the (10)^u fuel of a new bit-0 digit, and each (10)^v becomes the next digit's (01)^(v−1). The counter restarts at value 1 with one more digit. - When a digit flipping 0→1 has spent its last 10 (v = 1), it drops: its 01s merge into the next digit, and the counter loses that digit.

The only way the rules can fail is the failure mode: a carry reaches a bit-0 digit with v = 0, where Lf's first lemma T4 has no 10 to read. That happens if a carry flips a bit-1 digit with v = 1 to 0. Every macro step is an exact run of at least 32 steps, so every macro step makes progress.

3. Invariant: closure and coverage

This section is #11's proof.md §3, unchanged. It is stated on the triples (u, beta, v) and the numbers a, b, and it uses only the rule shapes of §2, which are the same as #11's. The Rocq form of this section (#11's .v, INV and step) has been checked by Rocq for #11. It has also been checked verbatim against this machine's K, with the three rule specs as hypotheses (rocq/abstract_check.v, §6).

INV(D; a, b) := Common ∧ (A ∨ B ∨ C). The three classes are told apart by the top digit d_1.

• Common:
• m ≥ 1, and the tape is canonical (every v_j ≥ 1, every bit-1 u_j ≥ 1);
• a ≥ 1, b odd, a + R_tot even;
• S ≥ 0, T ≥ 0;
• vbar_m ≥ 1 (the LSB never runs out).
• A (quiet cycle):
• d_1 = (0,0,v) with v ≥ 2, or d_1 = (1,1,v);
• for all j, vbar_j ≥ 1 and ubar_j is odd;
• S ≥ 1.
• B (top about to fall):
• d_1 = (0,0,1);
• for all j, v_j + beta_j is odd ("safe parity");
• for j ≥ 2, ubar_j ≥ 2^(j-1).
• C (top has fallen):
• for all j, v_j + beta_j is odd and ubar_j ≥ 2^j;
• S ≥ 1, T ≥ 2.

The run cycles A → B → C → A. - A is a cycle with no drops. - B is the next cycle. Its top digit (0,0,1) falls at its first touch and is absorbed by the digit below. - C is the rest of that cycle.

Seen at the overflows, the phases alternate: all u odd (end of A), then all v even (end of C).

3.1 Four arithmetic facts (they follow from the rules alone)

F0 (prefix bound). 0 ≤ U_j ≤ 2^j − 1, so R_j ≥ 0, and R_j ≡ 1 + beta_j (mod 2). If some bit beta_i = 0 with i ≤ j, then U_j ≤ 2^j − 2, so R_j ≥ 1. With the parity: - a bit-0 digit then has R_j odd, so R_j ≥ 1; - a bit-1 digit then has R_j even, so R_j ≥ 2.

In an M step every touched digit j ≥ j* has the bit-0 digit j* in its prefix, so F0 applies to all of them.

F1 (touch). In an M step every digit j ≥ j* is touched. Its prefix value U_j grows by exactly 1, because bits j*..j go from 01..1 to 10..0, so R_j drops by 1. - A 1→0 touch: v−1, R1 unchanged. - A 0→1 touch: u+1, v−1, R1−1.

So ubar_j and vbar_j are unchanged, and v_j + beta_j keeps its parity. Digits j < j* are untouched and unchanged. M also gives a+1, b+2, V+1 and R_tot−1, so a + R_tot, S and T are unchanged.

F2 (drop of d_{j}, j < m). Let H = U_{j*−1}. Digits above j* are unchanged. A digit j > j* moves to index j−1. Compare its new R', R1' with the values R°, R1° that F1 alone would give:

R° − R' = 2^(j−j*) · (2^(j*−1) − 1 − H) ≥ 0                 (so vbar only grows)
2·R1'   = R1° + 2^(j−j*−1)            for j ≥ j*+2  ⇒  ubar' ≥ ubar/2 + 2^(j−j*−2)
absorber j = j*+1:  u' = u_{j*+1} + u_{j*} + 1,  R1' = R1_{j*}  ⇒  ubar' = u_{j*+1} + ubar_{j*} + 1 ≥ ubar_{j*} + 1
if j* = 1 (H = 0):  R' = R°, R1' = R1°   (a falling top changes nothing below except the indices)

Here ubar_{j*} is the dropper's value before the step. A drop also changes the global quantities: - V' = H·2^(m−j*), so T grows by 2(H+1)2^(m−j*) ≥ 2; - S grows by 2^(m−1) + (H+1)2^(m−j*) ≥ 2; - R_tot' and R°_tot are both odd, so a + R_tot keeps its parity.

F3 (overflow). At an all-ones state, R = R1 = 0, so ubar = u, vbar = v, V = 2^m − 1 and R_tot = 0. After O there are m+1 digits and V' = 1:

j = 1:        ubar' = 1                    vbar' = u_1 − 1
2 ≤ j ≤ m:    ubar' = v_{j−1} − 1 + 2^(j−1)   vbar' = u_j − (2^j − 1)
j = m+1:      ubar' = v_m + 2^m − 1        vbar' = a − (2^(m+1) − 2)
a' + R_tot' = b + 1 + 2^(m+1)  (even)      T' = 0      S' = b + 3 − 2^(m+1) = T (the T before O)

3.2 Coverage (a rule always applies)

Take an INV state. - Not all bits 1: M applies. It needs v_j ≥ 1 (j ≥ j), u_j ≥ 1 (j > j), a ≥ 0 and b ≥ 0, all in Common. In particular, Common's v_{j*} ≥ 1 is exactly what rules out the failure mode. - All bits 1: O applies (m ≥ 1, all u, v ≥ 1, a ≥ 1).

There is no case split beyond M/O.

3.3 Closure (each case)

M keeps Common. - A digit touched 1→0 has v ≥ 2, so its new v ≥ 1. In A, vbar ≥ 1 gives v ≥ R+1, and F0 gives R ≥ 2, so v ≥ 3. In B/C, v + 1 is odd, so v is even and ≥ 2. - The 0→1 digit either keeps v ≥ 1 or drops. - The LSB never drops. A 0→1 touch of d_m has R_m ≥ 1 (F0), and vbar_m ≥ 1 then gives v_m ≥ 2. So every drop has j* < m, an absorber exists, and m' = m−1 ≥ 1. - The flipped digit gets u+1 ≥ 1. - The rest follows from F1/F2.

A, M step → A. No drop is possible: the 0→1 digit has R ≥ 1 (F0) and vbar ≥ 1, so v ≥ R+1 ≥ 2. F1 keeps every vbar, ubar and S. A top (0,0,v≥2) may become (1,1,v−1) with v−1 ≥ 1. A top (1,1,v) is never touched by M, because the carry stops at the last 0, which lies below it.

B, M step. - j ≥ 2 → B. - Parity is kept by F1. - A non-absorber has ubar' ≥ 2^(j−2) + 2^(j−j*−2) ≥ 2^((j−1)−1). - The absorber has ubar' ≥ ubar_{j*} + 1 ≥ 2^(j*−1). - d_1 is unchanged. - j = 1 → C. The top (0,0,1) flips with v = 1 and falls. - By F2 with H = 0, every other digit keeps its ubar and loses one index, so ubar ≥ 2^(j−1) = 2^(new j). - The new d_1 is the absorber: ubar' = u + ubar_top + 1 = u + 2 ≥ 2. - S grows by 2^m ≥ 2, so S ≥ 1. T grows by 2^m ≥ 4, so T ≥ 2. - B never reaches all-ones (beta_1 = 0), and B has m ≥ 2 (if m = 1, vbar_1 = 0).

C, M step → C. - Parity is kept by F1. - A non-absorber below a drop has ubar' ≥ ubar/2 ≥ 2^(j−1). - The absorber has ubar' ≥ ubar_{j*} + 1 > 2^(j*). This covers j* = 1, a second top fall. - S and T only grow.

A, O step → B. At all-ones the top is (1,1,v), so u_1 = 1 and the new top is (0,0,1). Safe parity: - the top: v = 1, bit 0; - j ≤ m: v = u_j = ubar_j, odd, bit 0; - the LSB: v = a, even because a + R_tot is even with R_tot = 0, bit 1.

Bounds and Common: - ubar' = v_{j−1} − 1 + 2^(j−1) ≥ 2^(j−1), and for the LSB v_m + 2^m − 1 ≥ 2^m. - S' = T ≥ 0. - vbar'_{m+1} = a − 2^(m+1) + 2 ≥ 1, because S ≥ 1 means a ≥ 2^(m+1) − 1. - b' = 1, a' = b+3, and every new v ≥ 1.

C, O step → A. - u_j = ubar_j ≥ 2^j, so the new top is (0,0,u_1) with u_1 ≥ 2. - vbar': u_1 − 1 ≥ 1, u_j − 2^j + 1 ≥ 1, and a − 2^(m+1) + 2 ≥ 1 (from S ≥ 1). - ubar' is odd: 1, v_{j−1} − 1 + 2^(j−1) and v_m + 2^m − 1 are all odd, because every v is even (from v + 1 odd) and j ≥ 2. - S' = T ≥ 2 ≥ 1.

So INV is closed under the macro step, and every INV state has a macro step. Checks 6–9 test this on this machine's orbit and on random INV states (§7).

4. Initial segment

0^inf A> 0^inf  --82-->   K(; 3, 1)          = 0^inf <C 01 000 (01)^3 1001 0^inf
                --133-->  K((1,1,3); 4, 1)   = 0^inf <C 01 000 (01)^4 (10)^3 01 1001 0^inf        (step 215)

The 215 steps are a finite run from the blank tape (check 4). The second leg is the O chain at m = 0 with a = 3, b = 1 (§2.3; 89 + 24 + 20 = 133), but the proof only needs the 215-step run.

The only K-configurations in steps 0..215 are those at steps 82 and 215 (check 4). K(; 3, 1) has no digits, so it is not in INV, which is why the init stops at 215.

K((1,1,3); 4, 1) is in class A: - top (1,1,3): bit 1, u_1 = 1; - V = 1, R_tot = R_1 = 0, R1_1 = 0; - ubar_1 = 1 (odd), vbar_1 = 3 ≥ 1 (also the LSB condition); - S = 4 + 0 − 2 = 2 ≥ 1, T = 1 − 1 = 0 ≥ 0 (tight); - a = 4 ≥ 1, b = 1 odd, a + R_tot = 4 even.

The next macro step is O (165 steps), to K((0,0,1), (3,1,4); 4, 1), which is in class B (check 4).

In Rocq this is init: c0 -->* K [d1 1 3] 4 1 by solve_init. It already compiles in rocq/plan_check.v. Compare #11's 483-step init to K [d1 1 2] 8 5.

5. Conclusion

• Init. The run reaches an INV state at step 215 (§4).
• Coverage. Every INV state has a rule (§3.2).
• Progress. Every rule is an exact run of at least 32 steps, composed of the window lemmas of §2.1 (§2.2, §2.3).
• Closure. Every result is again in INV (§3.3).

By the progress theorem (progress_nonhalt_cond with P := INV), the machine never halts.

In Rocq, this conclusion is already checked conditionally: rocq/abstract_check.v proves M_spec → Mdrop_spec → O_spec → ~ halts tm c0 for this string (§6). The informal derivations of §2.2–2.3 discharge the three premises.

Why --- (F reading 1) is never used. F is entered only by E1 (1RF). After the 215-step init, every step of the run lies inside one of the 20 window lemmas. E1 occurs only in T4, T9 and T13, and in each of them the next step is F reading 0 (F0 = 1RA; transition lists in §2.1, check 11). The init is a finite run that does not halt either. Nothing is claimed about tapes outside the family, and INV keeps the run inside it.

6. Lemma plan (Rocq)

Route (a), recommended: a scripted mirror of #11's .v. The result is one file with one TM_from_str (this string), so check_kill has nothing to warn about. #11's .v (692 lines) has two parts: 1. A machine part, lines 1–267: window lemmas, digit lemmas, list sweeps, K, the three rule specs and init. 2. An abstract part, from Open Scope nat_scope to step. It mentions the machine only through Kc, M_spec, Mdrop_spec and O_spec.

The interface between the two parts. Check 14 (a text check of #11's .v) gives the exact list. The abstract part and nonhalt use these 13 machine-part names and no others: tm, dg/d0/d1, K, map0, map1, Oz, Oout, M_spec, Mdrop_spec, O_spec and init. - K appears in the abstract part only in Definition Kc and in nonhalt's change. - The abstract part never unfolds K. All four unfold K lines are in the machine part. - dg, map0, map1, Oz and Oout are plain list functions with no tape in them. They are copied verbatim. - K keeps its signature list dg -> nat -> nat -> Q * tape. Only its body is mirrored.

So the port needs those definitions and the three spec statements word for word, and nothing else from #11's machine part.

Rocq-checked conditional (rocq/abstract_check.v, 2026-10-10). scripts/make_abstract_check.py builds this file mechanically: - rocq/plan_check.v in full: this machine's tm, the window and digit lemmas, dg, dr, app_ds, R0, K and the proved init; - #11's map1, map0, Oz and Oout, verbatim; - a Section whose only hypotheses are #11's statements of M_spec, Mdrop_spec and O_spec, verbatim, about this machine's K; - #11's abstract part, verbatim; - #11's nonhalt, with only the base changed to K [d1 1 3] 4 1.

It compiles with Coq 8.20.1 in 8.9 s, exit 0. After End Abstract, Check nonhalt prints (M_spec stmt) -> (Mdrop_spec stmt) -> (O_spec stmt) -> ~ halts tm c0 for this machine's string. Print Assumptions nonhalt gives "Closed under the global context". The record is rocq/abstract_check.out, and check 14 ties it to the file's sha256. Rocq has therefore checked these, with no hand argument left in between: - INV, closure (step) and coverage; - the base case at ([d1 1 3], 4, 1), closed by #11's own tactic line; - the init.

Only the three spec lemmas remain unproved. This file is a scratch check, not the kill file: its Hypothesis lines would fail check_kill by design.

The plan:

• Mirror dictionary for the machine part. busycoq sides are streams listed nearest cell first, so mirroring swaps the two sides and leaves every list literal as it is:
• l {{q}}> r ↦ r <{{π q}} l and l <{{q}} r ↦ r {{π q}}> l;
• l <* xs ↦ xs *> l, so l <* x <* y ↦ y *> x *> l;
• [..] literals, ^^n and 0inf are unchanged;
• π = (A,B,C,D,E,F) ↦ (B,C,D,A,E,F);
• shift_rule_R ↔ shift_rule_L.

Example: #11's T3: l <* [0;0;1] <{{E}} r -->* l <{{E}} [0;1;1] *> r becomes T3: l {{E}}> [0;0;1] *> r -->* l <* [0;1;1] {{E}}> r, which is E> 001 → 110 E>. - Already compiled (rocq/plan_check.v, Coq 8.20.1, 1.2 s, no admits): - S1–S6, with S1, S2 and S6 by shift_rule_L, S3 and S4 by shift_rule_R, and S5 by induction; - T1–T14 by es; - Lb, Lf, Rb, Ro by follow chains and #11's finisher fin (simpl_tape plus the rot01/rot10 stream identities); - the family and init: dr (d0 u v) r := [1;0]^^v *> [0;0] *> [0;1]^^u *> r dr (d1 u v) r := [1;0]^^v *> [0;1]^^u *> r app_ds r ds (LSB-first list, as #11) R0 := [1;0;0;1] *> 0inf K ds a b := 0inf <{{C}} [0;1]^^b *> [0;0;0] *> [0;1]^^a *> app_ds R0 ds init : c0 -->* K [d1 1 3] 4 1 (unfold K, R0; cbn; solve_init) - Still to port, name for name: - the list sweeps LbS, RbS, RoS: rw becomes a left-side builder lw ((u,v)::t) l = lw t (l <* [1;1] <* [1;0]^^v <* [0;1]^^(S u)), the shape of the compiled Lb's right-hand side, and ro_out becomes a right-side builder; - chunkA, chunkC, chunkO: §2.2 phases 1–2a, phase 3's tail and §2.3 phases 5–7; - Ozeq; - M_spec, Mdrop_spec, O_spec. They must keep #11's statements exactly (same dg, map0, map1, Oz, Oout, K signature), so the abstract part compiles unchanged. Check 14 compares the three lines below with #11's .v, whitespace-normalized: M_spec : K (map1 os ++ d0 u (S v) :: rest) a b -->+ K (map0 os ++ d1 (S u) v :: rest) (S a) (S (S b)) Mdrop_spec : K (map1 (os ++ [(u2,v2)]) ++ d0 u 1 :: rest) a b -->+ K (map0 os ++ d0 (S u2 + S u) v2 :: rest) (S a) (S (S b)) O_spec : os <> [] -> K (map1 os) (S a) b -->+ K (Oout os (S a)) (S (S (S b))) 1 Mdrop_spec's tape equality becomes [0;1]^^(S u2) *> [0;1]^^(S u) *> .. = [0;1]^^(S u2 + S u) *> .. on the right side (lpow_add), the reflection of #11's. - Abstract part, verbatim: bof, vof, Rof, Rd, ub, AllD, canon, PA, PB, LSBok, INV, Kc, F1/F2/F3 as F1, F2chain, F2, Oz_AB, Oz_CA, and step : INV s -> exists s', Kc s -->+ Kc s' /\ INV s'. Already compiled against this machine's K, with the specs as hypotheses (rocq/abstract_check.v, above). - nonhalt: #11's proof with K [d1 1 3] 4 1 and Kc ([d1 1 3], 4, 1), also already compiled in rocq/abstract_check.v: Lemma nonhalt: ~halts tm c0. Proof. eapply multistep_nonhalt; [apply init|]. change (K [d1 1 3] 4 1) with (Kc ([d1 1 3], 4, 1)). apply progress_nonhalt_cond with (P := INV); [exact step | (* base: class A *)]. The base goal is the additive INV of §3 at ([d1 1 3], 4, 1), closed by cbn; repeat split; lia: - Rof = 0; - a + R + 2 = 6 ≥ 4; - b + 3 + 2R = 4 ≥ 4 (tight, T = 0); - a + R + 1 = 5 ≥ 4; - v_m = 3 ≥ R + 1; - PA (d1 1 3) 0 0: ub = 1. - Expected size: about 700 lines, compiling in about 9 s like #11. It is Individual62 only, with no new axioms.

Route (b), the alternative: transport. Keep #11's development for tm11, prove an init from 0^inf D> 0^inf under tm11 (215 steps to the mirror of K [d1 1 3] 4 1), and transfer the result with Flip.v (flip_halts_iff) and Permute.v (perm_nonhalt). It needs a second TM_from_str (check_kill warns) and both modules instantiated in the Individual62 context. It saves no proof work over (a), since the init is new either way.

Templates. - Our kill #11 is the direct parent: the whole file, with the machine part mirrored. - Kill #3 is the same top-level pattern (multistep_nonhalt + progress_nonhalt_cond with a per-macro-step invariant). - vendor/busycoq/verify/SBCv6.v Module TM21 (line 3702) is a loose relative. LIncs_spec's inner induction is the pattern behind LbS/RbS, and Ov/Ov_spec the list induction behind O_spec. - TCv3.v is the loosest relative: the copy-and-modify module style with progress_nonhalt_simple. It has no invariant.

The C-start and D-start rows of §0 would follow the same plan, with the inits 732 and 687.

7. Evidence (from check_proof.py)

check_proof.py is self-contained: its own simulator on this table, its own K-configurations in this orientation, the abstract model and INV, the lemma table, and the chains in this orientation. #11's string and lemma windows appear only as data, for the cross-checks. Check 14 reads #11's .v as text. It was run with the default seed (check_proof.out) and again with --seed 2026 --tm-steps 1e9 --orbit 1.2e6 --induct 6e5 (check_proof_long.out). Both runs, after the review revision: ALL PASS, 14 checks (2026-10-10).

The observe stage reached the same 1e9 closure independently (scripts/closure_1e9.json, tools/sim.py with #11's model in #11's coordinates): 18,976 macro steps. Check 5 counts the K at step 215 as well, so it reports 18,977.

Gaps. - Open, for the formal stage. M_spec, Mdrop_spec and O_spec are not yet proved in Rocq on this table. Neither are their supports: LbS, RbS, RoS, chunkA, chunkC, chunkO and Ozeq. - They are derived informally from 20 window lemmas, each proved by a finite run (§2.2, §2.3, check 11). The word identities and step sums of the chains are written out, and checks 12–13 confirm every link on the real machine. - The window and digit lemmas they are built from already compile (rocq/plan_check.v). - What remains is bookkeeping: the list inductions and the lpow rewriting. - Everything else in the Rocq argument is checked conditionally on exactly these three statements: rocq/abstract_check.v proves M_spec → Mdrop_spec → O_spec → ~ halts tm c0 for this string (§6, check 14). That covers INV, closure, coverage, the base case and the init. - So the claim that #11's step and nonhalt carry over unchanged is now a compiled fact, given the three specs. They must be proved with #11's statements word for word (check 14 (b), (d)). - Status stays informal_proof until tools/check_kill.sh PASSes on the single-tm kill file. - §3 is a hand proof that uses only F0–F3 and the rule shapes. - Checks 7 and 9 test it on random states. #11's skeptic review re-derived it on exhaustive boxes, and this file's review did so on its own (Review log). - Its Rocq form (step) is checked for #11, and against this machine's K with the specs as hypotheses (rocq/abstract_check.v). - The cryptid protocol does not apply. The argument is parities and 2^j bounds, with no pseudo-random arithmetic. Which digits drop when is irregular, but the invariant never needs to know. - Skeptic review done (2026-10-10): sound, 2 minor gaps, both resolved (Review log). The reviewer checked the proof independently with its own C simulator and model, written only from this text: - init; - #11's Rocq INV against §3 on 300k states; - exhaustive INV boxes (m ≤ 2 absolute, 417,882 states, all run on the machine; threshold-relative boxes to m ≤ 5, 5.6M states), covering all six class transitions; - 21k random large states on the machine, plus 14.7M orbit steps; - the real run to 2·10^8; - an 88% failure-detection control; - the plan_check.v recompile; - the §0 relabeling search.

It found 0 failures. Dennis's Checkpoint B notes (pending, non-blocking) go into this file before any submission.

8. Open items for Dennis

• Checkpoint A asked: port #11 by scripted mirror (route a), or transport with Flip/Permute (route b)? This file recommends (a), and rocq/plan_check.v shows the dictionary works.
• Duplicate work (ground rule 7). This machine (start A) is unclaimed. hipparcos's Level-1 entry is the C-start row of §0, a different holdout. The draft Discord question in observe.json (discord_check) is still unsent.
• The D-start row of §0 (1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---) is this table under a state renaming, with no mirror. A kill of this machine would carry over by renaming states and replacing the init (687 steps). Nobody has claimed it in the sheet or the Discord lists we hold. That was not re-checked here.

Review log

Skeptic review, 2026-10-10. Verdict: sound, with 2 minor gaps and no fatal or major one. No mathematical defect was found. Both gaps are resolved below; neither was rejected.

Validations re-run after the revision (2026-10-10). - check_proof.py, default seed: ALL PASS, 14 checks, 16 s (check_proof.out). - check_proof.py --seed 2026 --tm-steps 1e9 --orbit 1.2e6 --induct 6e5: ALL PASS, 14 checks, 90 s (check_proof_long.out). This includes the real-machine closure at all 18,977/18,977 macro boundaries to step 999,982,947, a 1.2·10^6-step INV orbit, 600,000/600,000 random-INV induction, and check 14 at 16/16. - rocq/plan_check.v: recompiled, 1.19 s, exit 0 (rocq/plan_check.out). - rocq/abstract_check.v: compiled, 8.9 s, exit 0, closed (rocq/abstract_check.out).

Outcome. No fatal or major gap remains, so the status is CHECKPOINT_B (stage informal_proof), and formalization by route (a) may start. The next step is to port LbS, RbS, RoS, chunkA, chunkC, chunkO, Ozeq and the three specs, with their statements fixed by check 14. Then replace the section hypotheses of abstract_check.v with those lemmas, giving one file with one tm, and run tools/check_kill.sh.