1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---: never halts

• Machine: 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, viewer https://bbchallenge.org/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---
• Sheet: Results tab, class only; no status, notes or links; no Discord thread for this string. The same table appears in two other holdouts (see notes.md). 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- is this table started in our B. It is on the Level 1 tab (hipparcos, thread 1432566675533992019), so the duplicate-work question is still open. 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- is the mirror, started in our C. §4 gives their inits.
• Written for: the string itself (no mirror, no renaming).
• Status: informal proof, revised after the skeptic review (Review log at the end). Checkpoint B pending, non-blocking. Evidence: check_proof.py (§7).
• AI assistance: written by Claude (Anthropic) under Dennis's direction.

     0    1
A   1RB  0LE
B   1RC  0RC
C   1LD  0RB
D   1LA  0LE
E   1LD  1LF
F   1LD  ---        halting transition: F reads 1

1. Family and notation

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

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

• d_1 is next to the fixed leading 10 01. d_m is next to the right-hand block and is the least significant bit. m ≥ 1.
• 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). This does not hold outside INV: M turns a bit-1 digit with v = 1 into (u,0,0), which is not canonical. That digit is the precursor of the failure mode (§2.4).
• Re-reading (no machine steps). A bit-1 digit with v = 0 is just (10)^u, so it fuses with what follows. Followed by (u',β',v'), it becomes (u+u', β', v'). If it is last, 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. 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, with no subtraction or division, for Rocq.

2. Rules

In busycoq comment-block style:

1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---

start from K((1,1,2); 8, 5)                                   (step 483, §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, O's right side is 0^inf 10 01 00 (01)^u_1 [(10)^(v_i-1) 00 (01)^u_(i+1)]_{i<m} (10)^v_m (01)^a (10)^(b+3) 0^3 10 B> 0^inf.

M and O are not taken from simulation. §2.1 lists 20 window lemmas, and §2.2 and §2.3 derive M and O from them as chains of intermediate configurations. Each step count above is the sum along the chain. (M's domain is a ≥ 0; the earlier a ≥ 1 was more than the derivation needs. Common has a ≥ 1 anyway.)

2.1 Building blocks

Notation. X> means the head is in state X on the next cell, and <X means it is in state X on the previous cell (busycoq's {{X}}> and <{{X}}). A window lemma w → w' means: 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 (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, C> 11 (01)^(n+1) = C> 11 01 (01)^n → 10 C> 11 (01)^n → 10 (10)^n C> 11.

Shift lemmas:

S1 and S3 are the old R1 and R2. S5 and S6 are the 2-cell back-bounces: on each block the head steps two cells right, two left and two right again.

Finite lemmas:

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

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

2.2 Derivation of M

Write X for everything left of d_{j*} (it is never read), (u*, v*) for d_{j*} = (u*,0,v*), and Y = Π_{i=1..k} (10)^u_i (01)^v_i for the trailing bit-1 digits (i = 1 is j*+1).

                                                                                        steps
    X (10)^u* 00 (01)^v* Y (10)^a 000 (10)^b B> 0^inf
 Phase 1: right-edge preamble with a dip into the 0^3 gap                               4b+10
T1  .. Y (10)^a 000 (10)^b <E 01                                                        3
S4  .. Y (10)^a 000 <E (01)^(b+1)                                                       2b
T2  .. Y (10)^a 100 B> (01)^(b+1)                                                       5
S1  .. Y (10)^(a+1) 0 (10)^(b+1) B> 0^inf                                               2b+2
 Phase 2: one long left sweep, down to the 00 of d_{j*}                                 2a+2b+9+4v*+Σ(2u_i+2v_i)
T1  .. Y (10)^(a+1) 0 (10)^(b+1) <E 01                                                  3
S4  .. Y (10)^(a+1) 0 <E (01)^(b+2)                                                     2b+2
T3  .. Y (10)^a <E 011 (01)^(b+2)                                                       3
S4  X (10)^u* 00 (01)^v* Y <E (01)^a 011 (01)^(b+2)                                     2a
Lb  X (10)^u* 00 (01)^v* <E Y' (01)^a 011 (01)^(b+2)       (i = k down to 1)            Σ(2u_i+2v_i)
                         Y' = Π_i (01)^u_i (10)^(v_i−1) 11
Lf  X (10)^(u*+1) (01)^(v*−1) C> 11 Y' (01)^a 011 (01)^(b+2)                            4v*+1
 Phase 3: rightward pass with 2-cell back-bounces, then a plain run to the edge         6a+2b+13+Σ(6u_i+2v_i)
Rb  X (10)^(u*+1) (01)^(v*−1) Y'' C> 11 (01)^a 011 (01)^(b+2)   (i = 1 up to k)         Σ(6u_i+2v_i)
                         Y'' = Π_i (10)^u_i 00 (01)^(v_i−1)
S5  .. Y'' (10)^a C> 11 011 (01)^(b+2)                                                  6a
T8  .. Y'' (10)^a 10000 B> (01)^(b+2)                                                   9
S1  X (10)^(u*+1) (01)^(v*−1) Y'' (10)^(a+1) 000 (10)^(b+2) B> 0^inf                    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 left only to the 0^3 gap, turns (T2) and returns to the edge. Phase 2 is the only long leftward leg. Its leftmost read is the first 0 of d_{j*}'s 00 (T6 reads both cells, then moves right). So M is a side rule: the tape X left of that 00 is never read. Phase 3 moves right. It steps back two cells once per 01 block (S5, on the (01)^u_i blocks and on (01)^a), and it crosses the (10)^(v−1) blocks and the final (01)^(b+2) with plain sweeps (S2, S1). When v* = 1, the flipped digit (u*+1,1,0) 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=1..m} (10)^u_i (01)^v_i, with all digits bit 1.

                                                                                        steps
    0^inf 10 01 Y (10)^a 000 (10)^b B> 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 01 <E Y' (01)^a 011 (01)^(b+2)                Y' = Π_i (01)^u_i (10)^(v_i−1) 11
 Phase 3: turn at the far left
T9  0^inf 10 01 000 B> Y' (01)^a 011 (01)^(b+2)                                         13
 Phase 4: rightward pass
Ro  0^inf 10 01 000 Y''' B> (01)^a 011 (01)^(b+2)          (i = 1 up to m)              Σ(2u_i+6v_i−4)
                         Y''' = Π_i (10)^(u_i−1) 1 (10)^(v_i−1) 000
 Phase 5: right end                                                                     2a+8b+30
S1  .. Y''' (10)^a B> 011 (01)^(b+2)                                                    2a
T11 .. Y''' (10)^a 1 C> 11 (01)^(b+2)                                                   1
S5  .. Y''' (10)^a 1 (10)^(b+2) C> 11 0^inf                                             6b+12
T12 .. Y''' (10)^a 1 (10)^(b+2) <E 01101 0^inf                                          13
S4  .. Y''' (10)^a 1 <E (01)^(b+2) 01101                                                2b+4
 Phase 6: short left sweep over the a block, back to the 000 that Ro left after d_m    2a+1
T13 .. Y''' (10)^(a−1) <E 011 (01)^(b+2) 01101                                          3
S4  .. (10)^(v_m−1) 000 <E (01)^a 1 (01)^(b+2) 01101                                    2a−2
 Phase 7: turn in that 000, final run to the edge                                       2a+6b+27
T2  .. (10)^(v_m−1) 100 B> (01)^a (10)^(b+3) 1101          (1 (01)^(b+2) 0 = (10)^(b+3))  5
S1  .. (10)^(v_m−1) 100 (10)^a B> (10)^(b+3) 1101                                       2a
S6  .. (10)^(v_m−1) 100 (10)^(a−1) 1 (10)^(b+3) 0 B> 1101                               6b+18
T14 .. (10)^(v_m−1) 100 (10)^(a−1) 1 (10)^(b+3) 000 10 B> 0^inf                         4

Re-read the final tape with 0 (10)^(n−1) 1 = (01)^n and (10)^(v_m−1) 10 = (10)^v_m:

0^inf 10 01 000 Π_{i<m}[(10)^(u_i−1) 1 (10)^(v_i−1) 000] (10)^(u_m−1) 1 (10)^(v_m−1) 100 (10)^(a−1) 1 (10)^(b+3) 000 10 B>
  = 0^inf 10 01 00 (01)^u_1 [(10)^(v_i−1) 00 (01)^u_(i+1)]_{i<m} (10)^v_m (01)^a (10)^(b+3) 000 10 B> 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 last 10 of (10)^a, so a ≥ 1. T9 needs 0^inf on the left. O has two long leftward legs: phase 2, which T9 ends 3 cells left of the leading 10 01 (so the leftmost cell visited moves 3 cells per overflow), and the short phase 6.

2.4 What the rules do, in words

The digits form a binary counter. Each M is one increment. It flips the trailing 1s to 0 and the last 0 to 1, and every digit it touches pays one 01 from its v. A digit flipping 0→1 also gains a 10. When all bits are 1, O swaps the two halves of every digit: each (10)^u becomes the (01)^u fuel of a new bit-0 digit, and each (01)^v becomes the next digit's (10)^(v-1). The counter restarts at value 1 with one more digit. When a digit flipping 0→1 has spent its last 01 (v = 1), it drops: its 10s merge into the next digit, and the counter loses that digit. The only way the rules can fail is the failure mode: a carry arriving at a bit-0 digit with v = 0, where Lf's first lemma T4 has no 01 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

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, whose 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, 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.

4. Initial segment

0^inf A> 0^inf  --142-->  K((3,1,1); 2, 1)  --O,M1,M0 (141+100+100 steps)-->  K((1,1,2); 8, 5)     (step 483)

The chain is O, then M with j* = 1, then M with j* = 2. The last M is an LSB drop: (1,0,1) flips with v = 1 and joins a (a = 5 + 1 + 2: one 10 from M, two from the dropped digit). K((1,1,2); 8, 5) is in class A: - top (1,1,2); - vbar_1 = 2, ubar_1 = 1; - S = 6, T = 4; - a + R_tot = 8, b = 5.

The earlier K-configs at steps 142, 283 and 383 are not in INV, which is why the init stops at 483. Checked by direct simulation from the blank tape (check 4). In Rocq, the 483 steps are one solve_init/es run.

Twins, for later. The same table started in B on the blank tape reaches K((1,1,10); 8, 1) at step 732. Started in C, it reaches K((1,1,9); 8, 1) at step 687. Both are class A (check 10), so the same argument covers both other holdouts. Each twin is a separate TM_from_str, though, so the formal work is three .v files, or one file plus an equivalence lemma: - the B-start twin needs every lemma re-proved under the renamed states (A..F → E,A,B,C,D,F); - the C-start twin is the mirror, so its lemmas run on mirrored tapes.

The B-start twin is hipparcos's Level-1 entry (ground rule 7). Resolve the duplicate-work question before formalizing it.

5. Conclusion

The run reaches an INV state (§4). Every INV state has a rule (§3.2). Every rule is an exact run of at least 32 steps, composed of the window lemmas of §2.1 (§2.2, §2.3), and every result is again in INV (§3.3). By the progress theorem the machine never halts.

Why --- (F reading 1) is never used. Every step of the run, after the 483-step init, lies inside one of the 20 window lemmas. F is entered only in T4, T9 and T13, each time by E1, and each time F reads 0 (the transition lists in §2.1; check 11). The init run is a finite simulation that does not halt either. We claim nothing about tapes outside the family; INV keeps the run inside it.

6. Mapping to busycoq, and what is new

• K is a Fixpoint over a list of (u, bit, v) triples, as LC0/LC1 in SBCv6.v TM21, but with a per-digit bit. The near block becomes (10)^a 0^3 (10)^b, a fixed right side.
• The Rocq sub-lemmas are §2.1's table.
• S1–S6 by induction on n from a one-block es run.
• T1–T14 by es.
• Lb, Lf, Rb, Ro by composing those.
• M: Lb by induction over the list of trailing bit-1 digits (phase 2), Lf, then Rb by induction over the same list (phase 3), with an arbitrary left side X.
• O: the same list inductions with Lb and Ro, and T9 on 0inf.
• Drops are tape equalities only (lpow_add), with no steps.

The head path these lemmas describe: - M: a dip into the 0^3 gap, one long left sweep to d_{j*}'s 00, a rightward pass with 2-cell back-bounces on the 01 blocks, and a plain run to the edge. - O: the same, except that the long sweep ends with a far-left turn (T9), and it has a second, short left leg over the a block.

The "4 right-edge records per M" in notes.md counts new right-edge maxima, not excursions. - Closest template. TM21's LIncs_spec is not a per-carry lemma. It takes an all-C0 list to an all-C1 list over a whole counter cycle (k = 2^len − 1 increments, sideRLs on tm' = flip tm with hLR2^^k). TM21 has no per-carry lemma to adapt, so the per-carry M lemma is new work. The closest pattern is LIncs_spec's inner induction (C0 n (k+m) → C1 (k+n) m, by segRLs_trans and lpow_add). O follows the list induction of TM21's Ov/Ov_spec. - init: c0 -->* K((1,1,2);8,5) by es/solve_init (483 steps). - nonhalt by multistep_nonhalt + progress_nonhalt_cond with P := INV on macro states. Unlike TM21, do not use a whole-cycle BigStep: drops happen at data-dependent times, so the cycle has no closed form, but the per-step invariant is simple. - INV without truncating subtraction. In nat, v − R, S, T and the division in R1 would truncate silently and could make INV vacuous. State everything additively, or work in Z: - R_j + U_j + 1 = 2^j; - 2·R1_j + beta_j = R_j + 1 (both sides exact, because R_j ≥ 0 and R_j ≡ 1 + beta_j); - R_tot + V + 1 = 2^m; - vbar_j ≥ 1 ⟺ v_j ≥ R_j + 1; - ubar_j odd ⟺ Nat.Odd (u_j + R1_j); ubar_j ≥ 2^j ⟺ u_j + R1_j ≥ 2^j; - S ≥ 0 ⟺ a + R_tot + 2 ≥ 2^(m+1); S ≥ 1 ⟺ a + R_tot + 1 ≥ 2^(m+1); - T ≥ 0 ⟺ b + 1 ≥ 2V; T ≥ 2 ⟺ b + 1 ≥ 2V + 2. - New compared with TM21: - digits carry a bit; - digits run out and merge (TM21's LWF: 2^len ≤ m fails here); - the invariant has three phases with parity conditions and 2^j bounds, through the prefix values U_j.

The Rocq work is mostly the arithmetic of F0–F3. Define U_j as a fold over the bit list, and prove F0 and F2 as standalone lemmas about 2^j, because lia will not do them unaided.

7. Evidence (from check_proof.py)

check_proof.py is self-contained: its own simulator, abstract model, INV, lemma table and chains. It was run with the default seed and again with --seed 2026 --induct 6e5 --orbit 1.2e6. Everything passed (2026-10-10, 19 s and 35 s):

Independent re-check (skeptic review, 2026-10-10, own simulator and model, r11/ in the skeptic's scratchpad): - M exhaustive on 256,000 configs, O on 66,336, and 20,000 random O configs, all exact; - the real machine against the macro model at all 26,396 macro boundaries to t = 2·10^9; - F1–F3 exhaustive (1,470 identities, m ≤ 9); - INV closed under one macro step on exhaustive boxes up to m = 6 (about 250M states); - mutation tests: a weakened INV is caught.

Gaps. - M and O are now derived (§2.2, §2.3) from 20 window lemmas. Each window lemma is proved by a finite run (check 11). The chains' word identities and step sums are written out above, and checks 12–13 confirm every link on the real machine. What remains is bookkeeping, which Rocq settles: the list inductions and the lpow rewriting. - §3 is a hand proof that uses only F0–F3 and the rule shapes. Checks 7 and 9 test it on random states, and the skeptic re-derived it by hand and checked it on exhaustive boxes. Rocq will be the real check. - 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.

Review log

Skeptic review, 2026-10-10. Verdict: sound, with 1 major and 6 minor gaps. All are resolved below; none was rejected.