1RB0LC_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---: informal proof (INCOMPLETE: invariant open)

• Machine: 1RB0LC_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, viewer https://bbchallenge.org/1RB0LC_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---
• Sheet: Results and Classifications tabs, class only (Skelet 1-like Class 2); no status, notes, links or Discord thread. Not claimed (notes.md).
• Parent: kill #11 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---. The tables differ only in A1 (twin 0LC, parent 0LE).
• Written for: the string itself (no mirror, no renaming).
• Status: incomplete, STUCK at the invariant (§5). Revised after the skeptic review (Review log at the end).
• Done: the window lemmas (§2); M, O, P (§3.1–3.3); one general macro rule G that covers every transition of the run, the 45 that M/O/P left out included (§3.5); a complete case analysis of the sweep (§3.6); the exact initial segment (§4); the lemma plan (§7).
• §3.6 reduces non-halting to one statement. Every K-configuration either takes a G step, or halts inside the macro step (classes H1, H2), or has left text in one of four classes that no rule covers (U0–U3).
• Missing: a family of configurations, closed under G, that contains a reachable configuration and has no member in H1, H2 or U0–U3. Without it there is no non-halting proof.
• Evidence: check_proof.py (§8), 12 checks, all pass.
• AI assistance: written by Claude (Anthropic) under Dennis's direction.

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

1. Notation and two exact facts

1.1 K-configurations

K(L; a, b) := 0^inf L (10)^a 0^3 (10)^b B> 0^inf          L an arbitrary finite word (the "left text")
digit d = (u, beta, v):   (u,0,v) := (10)^u 00 (01)^v      (u,1,v) := (10)^u (01)^v
K(d_1 .. d_m; a, b) := K(10 01 d_1 .. d_m; a, b)           as in the parent

• a and the (10) run before 0^3 are maximal, so L never ends in 10.
• The parent's family has L = 10 01 d_1 .. d_m. In the twin the left text leaves that shape at step 428 (§4). After that it is a word that ends in digits but starts with irregular text, sometimes at odd parity.
• Window-lemma notation is the parent's: X> means state X on the next cell, <X means state X on the previous cell. A window lemma runs inside its window, so it holds in every tape context.

1.2 Table facts (check 1)

• The only halting transition is F reading 1.
• F is entered only by E1 (1LF).
• In the twin, E is entered only by D1 (0LE). In the parent, A1 also enters E. This is the one change.
• So a halt needs a leftward run D, E, F reading 1, 1, 1: the pattern 111 <D.

1.3 Token machine (check 2)

Pair the cells in the head's parity: the head stands between tokens z = 00, o = 01, a = 10 and X = 11. Every visit of the head to a token starts and ends on a token boundary. So the machine is exactly the following 4-symbol machine, with 5 left-moving states and 2 right-moving states (C' is C entered from the left). Each entry lists the new token, the exit state and the direction. All 28 entries are checked against the cell machine.

left-moving (enters the token on its left)
E:  a->o E   z->X A   o->X D   X->HALT
D:  o->a D   X->a F   a->o C   z->a C' (turns right)
F:  a->o E   z->X A   o->HALT  X->HALT
A:  o->a D   X->o C'  z->o B   a->X B      (the last three turn right)
C:  a->o E   z->X A   o->z B   X->a B      (the last two turn right)
right-moving (enters the token on its right)
B:  o->a B   X->z B   z->o E   a->X A      (the last two turn left)
C': a->o C'  X->z C'  z->a D   o->X D      (the last two turn left)

The blank start is the entry (A, z): cell 0 is the right cell of its token. So the token machine describes the whole run. Halting therefore needs E to meet an X, or F to meet an o or an X, and F comes only from D meeting an X. "Misaligned" left text is not a special case for the machine. It only breaks the digit description. §3.6 states the same hazards in cell terms, at the one place where they can occur.

2. Window lemmas (checks 3, 4)

These are the parent's 20 lemmas (parent proof.md §2.1) under the twin's table, plus four new ones:

C0 = E0 = 1LD. So any window whose first step is E reading 0 has an exact copy entered in C, with the same steps and result. S4c and T2c are two such copies, and §3.5 uses the C-entry copies of T3 and T3j in the same way. The C exits of T3, T5 and T12 therefore differ from the parent only when the next cell read is a 1. F is entered only in T4, T9 and T13, each time reading 0 (check 3).

Composite lemmas: - Lb (twin, u ≥ 2): (10)^u (01)^v <E → <E (01)^u (10)^(v−1) 11, in 2u+2v steps (T4, S3^(v−1), T5, S4c, S4^(u−2)). It has the parent's shape and step count. - Lb1 (new, u = 1 with a 0 on its left): 0 10 (01)^v <E → 0 <C 01 (10)^(v−1) 11, in 2v+2 steps (T4, S3^(v−1), T5). The C that follows reads that 0, so it acts as E. - Lf, Rb, Ro: verbatim. They use no changed lemma. - Lt (new, the bounce on a bit-1 digit with u = 1 whose left neighbour cell is 1): 1 10 (01)^v <E → 01 (10)^(v−1) 000 B>, in 8v+1 steps (T4, S3^(v−1), T5b, S6^(v−1), T10). Check 4 runs it for v = 1..40 and checks the step sum.

3. Macro rules

3.1 M (carry): the parent's M, with a narrower domain

K(L, (u,0,v), (u_j,1,v_j)_{j*<j<=m}; a, b) --> K(L, (u+1,1,v-1), (u_j,0,v_j-1)_j; a+1, b+2)
steps 32 + 8a + 8b + 4v + sum_j (8u_j + 4v_j)
needs v >= 1, a >= 1, and u_j >= 2, v_j >= 1 for every trailing bit-1 digit; L arbitrary

The twin's chain, with X the never-read text left of d_{j*} = (u*,0,v*), Y = Π_i (10)^u_i (01)^v_i the trailing bit-1 digits, and Y' = Π_i (01)^u_i (10)^(v_i−1) 11, Y'' = Π_i (10)^u_i 00 (01)^(v_i−1) as in the parent:

                                                                                        steps
    X (10)^u* 00 (01)^v* Y (10)^a 000 (10)^b B> 0^inf
 Phase 1 (verbatim: T1 S4 T2 S1)                                                         4b+10
    .. Y (10)^(a+1) 0 (10)^(b+1) B> 0^inf
 Phase 2 (changed: T3 exits C, so S4c takes the last 10 of (10)^a)                       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 <C 011 (01)^(b+2)                                                        3
S4c .. Y (10)^(a−1) <E 01 011 (01)^(b+2)                                                 2      needs a >= 1
S4  X (10)^u* 00 (01)^v* Y <E (01)^a 011 (01)^(b+2)                                      2a−2
Lb  X (10)^u* 00 (01)^v* <E Y' (01)^a 011 (01)^(b+2)      (i = k down to 1)              Σ(2u_i+2v_i)   twin Lb, u_i >= 2
Lf  X (10)^(u*+1) (01)^(v*−1) C> 11 Y' (01)^a 011 (01)^(b+2)                             4v*+1
 Phase 3 (verbatim: Rb per digit, S5, T8, S1)                                            6a+2b+13+Σ(6u_i+2v_i)
    X (10)^(u*+1) (01)^(v*−1) Y'' (10)^(a+1) 000 (10)^(b+2) B> 0^inf

The step totals equal the parent's: S4c costs 2, like the S4 block it replaces. a ≥ 1 is needed because of S4c. With a = 0, the C after T3 would read the swept digit's last 1 and bounce. Checked on random K-configs with arbitrary left text (check 5).

3.2 O (overflow at the far left): the parent's O, with a narrower domain

K(d_1..d_m; a, b) → K((0,0,u_1), (v_1−1,0,u_2), .., (v_m,1,a); b+3, 1), in 89 − 4m + 8a + 20b + 4Σu + 8Σv steps. It needs all bits 1, every u_j ≥ 2, v_j ≥ 1, a ≥ 1, and the plain wall 0^inf 10 01. The chain is the parent's §2.3. Two phases change, with Y''' as in the parent:

 Phases 1–2 as in M (§3.1), 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)
 Phase 3: T9 (twin trace, §2)                                                             13
 Phase 4: Ro per digit (verbatim)                                                         Σ(2u_i+6v_i−4)
 Phase 5 (changed: T12 exits C, so S4c takes the last 10 of (10)^(b+2))                   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) <C 01101 0^inf                                            13
S4c .. Y''' (10)^a 1 (10)^(b+1) <E 01 01101                                               2
S4  .. Y''' (10)^a 1 <E (01)^(b+2) 01101                                                  2b+2
 Phases 6–7 (verbatim: T13 S4, then T2 S1 S6 T14)                                         (2a+1)+(2a+6b+27)

Checked in check 5. §3.5 shows that O is one case of a more general overflow O*, and that the wall condition v = 1 is not needed.

3.3 P (partial overflow): new

The leftward sweep meets its first bit-1 digit with u = 1, d_p = (1,1,v_p), and the left text L ends in 1. Then:

K(L, (1,1,v_p), (u_i,1,v_i)_{p<i<=m}; a, b)
  --> L[:-1] 01 (10)^(v_p-1) 00 (01)^u_{p+1} [(10)^(v_i-1) 00 (01)^u_{i+1}]_{p<i<m} (10)^v_m (01)^a (10)^(b+3) 000 10 B> 0^inf
      (k = 1:  L[:-1] 01 (10)^v_p (01)^a (10)^(b+3) 000 10 B> 0^inf)
steps 77 - 4k + 8a + 20b + 4 sum_{i>=p} u_i + 8 sum_{i>=p} v_i          (k = m - p + 1)
needs u_i >= 2 and v_i >= 1 for i > p, v_p >= 1, a >= 1

Read with L' = L[:-1] 01, the result is K(L', (v_p−1,0,u_{p+1}), .., (v_{m−1}−1,0,u_m), (v_m,1,a); b+3, 1). This is the parent's O output on the suffix d_p..d_m without its top digit (0,0,u_p) = (0,0,1).

Derivation as a chain. Check 6 confirms each link on the real machine, as the full tape, head and state after the cumulative step count, on a 405-case box plus 150 random cases. Here Y' = Π_{i>p} (01)^u_i (10)^(v_i−1) 11 and Y''' = Π_{i>p} (10)^(u_i−1) 1 (10)^(v_i−1) 000.

                                                                           cumulative steps
  L 10 (01)^v_p Y (10)^a 000 (10)^b B> 0^inf
phase 1 (T1 S4 T2 S1, as in M)        .. (10)^(a+1) 0 (10)^(b+1) B> 0^inf               4b+10
phase 2 (T1 S4 T3 S4c S4, Lb_i>p)     L 10 (01)^v_p <E Y' (01)^a 011 (01)^(b+2)         + 2a+2b+8 + Σ_{i>p}(2u_i+2v_i)
Lt on d_p (L ends in 1)               L[:-1] 01 (10)^(v_p−1) 000 B> Y' (01)^a 011 (01)^(b+2)   + 8v_p+1
Ro_i>p                                L[:-1] 01 (10)^(v_p−1) 000 Y''' B> (01)^a 011 (01)^(b+2)  + Σ_{i>p}(2u_i+6v_i−4)
phases 5-7 of O (§3.2)                the P result                                       + 6a+14b+58

The total equals the P formula. Compared with O on the suffix, "T9 + Ro on d_p + Lb on d_p" (13 + (6v_p−2) + (2v_p+2) steps) is replaced by Lt (8v_p+1), which is 12 steps cheaper.

What moves. P's leftmost read is the last cell of L, a 1, and Lt rewrites it as 0 1. So L' = L[:-1] 01 is one cell longer than L, and L[:-1] stays where it is on the tape. The right part grows by an odd number of cells: from step 283 to step 428 the text grows from 30 to 37 cells, and the leftmost 1 is at cell −12 at both steps. What flips is the parity of L[:-1] relative to the head and to the digits on its right.

3.4 What M, O and P leave out

To 10^9 there are 22,435 K→K transitions (check 8). M, O and P predict 22,390 of them exactly (M 22,349, P 35, O 6). The other 45 fall outside their domains:

So all 45 are single applications of one rule, with exact domains, outputs and step counts. They are not new local behaviour.

3.5 The general rule G (checks 8, 11)

Let K(L; a, b) with a ≥ 1.

Swept suffix. Read L from the right and peel off maximal digits (10)^u (01)^v (u, v ≥ 1, bit 1): - a digit with u ≥ 2 is swept by Lb, and peeling continues; - a digit with u = 1 and a 0 on its left (a blank counts as 0) is swept by Lb1, and peeling stops, because the cell on its left is 0 and not the end of a digit; - a digit with u = 1 and a 1 on its left is the bounce digit. It is not swept, and the turn is Lt.

What remains is the text X, so L = X d_p .. d_m with d_p .. d_m the swept digits (k = m − p + 1 ≥ 0). X does not end in 10 and does not end in a digit, by maximality.

Phases 1–2. As in M (§3.1). Phase 1 reads only the a/b block. Phase 2 sweeps the a block and then Lb or Lb1 on d_m, .., d_p. The head is then at X <E, or at X <C before a 0 after Lb1, which acts the same (§2).

Turn. On the last cells of X (or on the bounce digit), with X' never read:

Return and right end. - M* (C exit). Rb on d_p, .., d_m, then M's phase 3 tail (S5^a, T8, S1^(b+2)): K(X'·t, d_p..d_m; a, b) --> K(X'·w, (u_i,0,v_i−1)_{i=p..m}; a+1, b+2) steps 31 + 8a + 8b + c + Σ_i (8u_i + 4v_i) c = 4v+1 (Lf), 5 (T3S2), 4v+5 (Jc) (t, w) = (00 (01)^v, 10 (01)^(v−1)) for Lf, (1100, 01) for T3S2, (00 (01)^v 00, 10 (01)^v) for Jc Lf with X' = X'' (10)^u is M: the digit (u,0,v) becomes (u+1,1,v−1). T3S2 turns .. 1 1 00 into .. 0 1. Jc removes a junction (0,0,0) after a bit-0 digit (u,0,v) and flips that digit to (u+1,1,v) without spending a 01. - O* (B exit). Ro on d_p, .., d_m, then O's phases 5–7 (§3.2). Phase 6 sweeps left over (10)^(a−1) and turns (T2) in the 000 that the last Ro left, or that Lt left when there is no swept digit: T2: K(X' 000, d_p..d_m; a, b) --> K(X', (1,1,u_p), (v_p−1,0,u_{p+1}), .., (v_{m−1}−1,0,u_m), (v_m,1,a); b+3, 1) steps 81 − 4k + 8a + 20b + 4 Σ_{i>=p} u_i + 8 Σ_{i>=p} v_i, needs k >= 1 Lt: the P rule of §3.3 (k counts the bounce digit there) On the tape, the T2 result is X' 10 (01)^u_p (10)^(v_p−1) 00 (01)^u_{p+1} .. (10)^v_m (01)^a (10)^(b+3) 000 10 B>. T2 needs k ≥ 1. With k = 0 the turn leaves 100 where phase 6 expects 000 (class U0 below).

Special cases. - M is Lf with every swept digit u ≥ 2. - O is T2 with d_p = the wall digit (1,1,1) (swept by Lb1) and X' = 0^inf. The formula then gives O's output and O's step count. T9 is exactly "Lb1 on 10 01, T2c on the blank, Ro on (1,1,1)": its trace splits as E1 F0 | D0 A1 | C0 D0 A0 B1 C1 | B0 C1 B1 C1. - The far-left wall 10 (01)^v with v ≥ 2 is the same T2 case with d_p = (1,1,v). It gives K((v−1,0,u_1), ..) on a plain 10 01 wall. - P is Lt.

Derivation. Every piece is a composition of the windows of §2. - Phases 1–2 and the two right ends are those of §3.1 and §3.2. They read only the a/b block and the 000 next to it. - Lb, Lb1, Rb and Ro each read one digit. - Each turn reads only the cells in its row.

So G holds in every tape context left of X'. The step counts are the chain sums. Two checks confirm it: - Check 11: 400 random K-configs per turn, with random text left of the turn (X') and an optional Lb1 digit, give the exact tape, head, state and step count. - Check 8: G predicts every one of the 22,435 transitions to 10^9 exactly: Lf 22,353, T3S2 8, Jc 2, T2 37, Lt 35. A scratch run of the same code in this stage did the same for all 67,856 transitions to 10^10: Lf 67,757, T3S2 9, Jc 3, T2 44, Lt 43, with 0 unpredicted and 0 mismatches.

The halting example of §5 is predicted by G up to its last K-config (check 10).

3.6 Case analysis of the sweep (check 12)

The left-moving part of the table is a deterministic automaton. It reads one cell, writes, and moves one cell left; R means it turns right into B:

E: 0 -> 1, D    1 -> 1, F          D: 0 -> 1, A    1 -> 0, E          F: 0 -> 1, D    1 -> HALT
A: 0 -> 1, R    1 -> 0, C          C: 0 -> 1, D    1 -> 0, R          (C0 = E0)

Read right to left, (01)^v takes E to D (T4, S3), and (10)^u takes D to C (u = 1, T5) or to E (u ≥ 2, T5 S4c S4). From C, a 0 continues as from E, and a 1 is the bounce (T5b, i.e. Lt). So after the swept suffix the head is in E at the end of X, or in C before a 0. Since X ends neither in 10 nor in a digit, its ending falls in exactly one class:

(Lt is decided before X, in the swept suffix. The bounce digit is never part of X.)

Statement (relative to an invariant). For every K-configuration K(L; a, b) with a ≥ 1, exactly one of the following holds: - G applies, and its macro step, a composition of non-halting windows, ends in a K-configuration with a' = a+1 or a' = b+3, both ≥ 1; - the macro step halts (H1, H2); - X is in U0–U3.

So the run never halts if every reachable K-configuration is in one of the covered classes (Lf, T2 with k ≥ 1, T3S2, Jc, or Lt). That is the open §5.

Check 12 confirms three things: - the automaton against the table; - the partition on all 21,852 texts X of length ≤ 14 that end neither in 10 nor in a digit (H1 8,191, H2 1,359, Jc 694, Lf 2,744, T2 4,098, T3S2 2,047, U1 1,365, U2 677, U3 677); - the behaviour on 4,300 K-configs built from them: G is exact on Lf/T2/T3S2/Jc/Lt, and H1/H2 halt inside the macro step.

In token terms, H1 is the review's "E meets an X token". H2, U1 and U3 contain its "D meets an X, then F" step. F halts when it then reads a 1: always in H2, and in U3 when the next cell is 1. In the run to 10^10, no K-configuration is in H or U (check 8, and the 10^10 scratch run).

4. Initial segment (check 7)

0^inf A> 0^inf --142--> K((3,1,1); 2, 1) --O, 141--> K((0,0,3),(1,1,2); 4, 1)        (step 283)
               --P, 145--> K(1001000 (2,1,1)(2,1,4); 4, 1)                            (step 428)
               --O* (T2), 181--> K((1,1,2),(0,0,2),(4,1,4); 4, 1)                     (step 609)

• Up to step 283 the twin runs the parent's trajectory (notes.md: the states first differ at step 28, but C0 = E0, so the paths stay together).
• The transition 283→428 is an M-type P: (1,1,2) bounces, with L = 10 01 00 (01)^3 ending in 1. The parent goes on to its INV start at step 483. The twin does not.
• At step 428 the left text is 1001000. The next step is O* with turn T2: X' = 10 01, the turn reads 000, and the swept digits are (2,1,1)(2,1,4). It gives K(10 01, (1,1,2), (0,0,2), (4,1,4); 4, 1) in 81 − 8 + 32 + 20 + 16 + 40 = 181 steps.
• From step 609 on, the run is no longer the parent's.

5. Invariant: OPEN

What a proof still needs (sharper after §3.5–§3.6). A family F of K-configurations such that: 1. F contains the step-609 configuration (or a later one); 2. no member of F has a = 0 or a left text in H1, H2 or U0–U3; 3. G maps F into F.

Then, by induction over macro steps and §3.6, the machine never halts.

Why this is hard: - Shape alone fails (check 10). K((1,0,2); 2, 1) has a plain wall, a ≥ 1 and b odd, and it halts at step 2535. G predicts all 13 of its macro steps. Its last K-config (step 2384) is 1001 1101 0101 0010 1010 1 + (10)^19 000 (10)^13. Its swept suffix ends at X = 10011, which is H1: an all-ones sweep passes the u = 4 digit and E reads 11. In the box m ≤ 2, u, v ∈ 1..3, beta ∈ {0,1}, a, b ∈ 0..3, 807 of 5,472 canonical K-configs halt within 2·10^6 steps. So F has to carry quantitative constraints, as the parent's parities and 2^j bounds did. - X tokens are present in the left text. 5,259 of 22,436 K-configs to 10^9 have an X token in their left text, always with z or o to its right and never an a-run (review count). F must show that no sweep ever reaches one of them in a hazardous state: in E (H1), or in D followed by a 1 (H2, U3). - The parent's INV does not survive. The parent's class-A overflow (top (1,1,v)) is always a P in the twin. P and T2-turns realign the left text, so the family must allow left text at both parities, together with junctions (u,0,0), (0,0,0) and walls 10 (01)^v. - The left text is a hierarchical counter. These leads come from notes.md and from the R4 observation; check_proof.py does not check them: - The left edge barely moves (−69 at 10^9, −81 at 10^10). - The 6-token left prefix takes 113 shapes to 10^10, each reused in long runs with counts near 2^k or 2^k − 1. - R4 1RB0RE_1LC0RD_1LD0LD_1RA0LC_1RA1RF_1RA--- is this table mirrored and renamed. Its observation shows nested "fossil-K" walls whose fuel drops by exactly 1 per level-1 overflow, and walls that dissolve and re-form when the fuel runs out. In head-parity tokens (§1.3), a bit-0 digit (u,0,v) reads o^(u−1) z z a^(v−1), and the K block (10)^a 000 (10)^b reads o^(a−1) z z a^b. So a K block has the token shape of a digit (a,0,b+1). The deep digits look like frozen K blocks of a slower counter, and the T2/T3S2/Jc turns look like the places where a lower level hands a carry to a higher one.

Which turns the run uses, to 10^10: Lf 67,757, Lt 43, T2 44, T3S2 9, Jc 3. Lf is the ordinary carry into a bit-0 digit. The other 99 events are the turns at a junction, a bounce point or the blank, and these are where the invariant has to control the left text.

Suggested route (unchanged in spirit, now with exact rules): 1. Describe a configuration as a list of levels. Each level is a parent-style digit counter, delimited by a junction ((u,0,0), (0,0,0), 000) or by a bounce point (left cell 1 before a u = 1 digit). 2. For one level, lift the parent's F0–F3 arithmetic to G: Lf is the carry; Lt, T2, T3S2 and Jc are the level's overflows. 3. Find the inter-level invariant: what a level's overflow writes into the level above, and why that never produces an H or U ending. A solution here carries over to R4 by mirroring, as #33 did for #11.

Not assessed as a cryptid: no pseudo-random arithmetic has been seen, and the counts are powers of 2. Budget for this stage is used.

6. Halting unreachable, relative to the rules

• Every G step is a composition of the windows of §2, so a G step never halts: halting is F reading 1, and the only F entries in the windows (T4, T9, T13) read 0 (check 3).
• By §3.6, a K-configuration with a ≥ 1 that is in none of H1, H2, U0–U3 takes a G step to another such K-configuration with a' ≥ 1. Whether that one is again outside H and U is exactly §5.
• So non-halting follows from an invariant as in §5, by induction over macro steps. Without §5 there is no proof.

About the coverage check (check 9). The window set contains 1–2-step windows (T11 = B0, S1–S4, S4c, T4, T7, T10). So a full greedy cover mostly says "did not halt", plus a few local bans: A0 is always followed by B1, and C0 D0 is never followed by A1. The review's own DP over the 23 windows also covers 1,024 of 1,342 random 150-step non-halting traces from random tapes. Check 9 shows only that the observed run uses no other local patterns. It is not evidence that unanalysed events are rule-like or safe, and not evidence for non-halting. The earlier sentence "any run that decomposes into these windows does not halt" was true but trivial, because F1 is in no window. The "other" events are now covered by the closed forms of §3.5, not by check 9.

7. Lemma plan: reuse of the parent's .v

The parent's .v is machines/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---.v, 694 lines. - Verbatim (machine part): rot01, lshift, S1_1–S6_1, S1–S6, S5, T1, T2, T4, T6–T11, T13, T14, p01, p10, rot10, fin, Lf, Rb, Ro, chunkC, dg, dl, app_ds, app_ds_app, map0, rw, RbS, ro_out, RoS, Oz, Oout, Ozeq. T9 keeps its statement. Its proof only simulates 13 steps, so it should re-run unchanged on the twin's trace (§2). - Changed statement, same proof idea: - T3, T5, T12 with <{{C}} exits, plus S4c_1 : l <* [0;1] <{{C}} r -->* l <{{E}} [0;1] *> r (es). - Lb for u ≥ 2: [0;1]^^(S (S u)), proof follow T4. follow S3. follow T5. follow S4c_1. follow S4. - map1 becomes map2 := d1 (S (S u)) (S v), and LbS likewise. - chunkA needs [0;1]^^(S a). - chunkO puts S4c_1 before its first S4. - K takes a left side: K' l ds a b := app_ds l ds <* [0;1]^^a <* [0;0;0] <* [0;1]^^b {{B}}> 0inf, with K = K' L0. - M_spec, Mdrop_spec: the same proofs over K' l, since l is never read. - O_spec over map2. It becomes a corollary of G_T2 below. - New: - T5b : l <* [0;1;1] <{{D}} r -->* l <* [0;1;0] {{B}}> r (es; lists nearest cell first). - T3j : l <* [0;0;1;0] <{{E}} r -->* l <{{D}} [1;1;0;1] *> r (es), and the C-entry copies T2c, T3c, T3jc (same scripts: C0 = E0). - Lb1 (T4, S3, T5; exits C before a 0). - Lt v : l <* [1] <* [0;1] <* [1;0]^^(S v) <{{E}} r -->* l <* [1;0] <* [0;1]^^v <* [0;0;0] {{B}}> r (follow T4, S3, T5b, S6, T10). - Turns TT3S2 (T3, S2) and TJc v (T3j, S3, T6, S2, S2). - G_M (one lemma per C-exit turn: Lf, T3S2, Jc) and G_T2, G_Lt (= P_spec), each as phase12; LbS; [Lb1]; turn; RbS/RoS; tail. The O-type tails reuse chunkO and Ozeq (minus its top digit for Lt). - The class split of §3.6 as a lemma on the left list. It covers the G cases only; H and U are what the invariant must exclude. - init : c0 -->* K' ... by solve_init (609 steps, or as far as the family of §5 needs). - Abstract part: none reusable until §5 is solved. The parent's Rof, INV, F0–F3 lemmas are a template for one level only.

8. Evidence (from check_proof.py)

check_proof.py is self-contained: a Python simulator, plus two embedded C helpers (a K-config dumper and a batch halting checker) compiled with gcc into a temp dir. Run 2026-10-10 with the default seed and with --seed 2026 --n 1000 --quick (T2 = 10^8). Both print SUMMARY PASS 12/12 (times in the Review log). Results:

Gaps: §5 (the invariant). Everything in §1–§4 and §6 is derived from finite window runs or checked exactly. §3.5–§3.6 now give closed forms for every transition the run makes, with explicit domains.

Review log

Skeptic review, 2026-10-10. Verdict: not sound, with 1 fatal, 1 major and 3 minor gaps. The reviewer independently re-checked the finished parts with their own code: the 28 token entries; the 23 windows with exact traces; Lt for v = 1..30; M/O/P on 3,000 random configs; the K-configs at 142, 283, 428 and 609; their own C dumper and classifier to 10^9 (M 22,349 / P 35 / O 6 / other 45, 0 mismatches, no halt); the halt of K((1,0,2);2,1) at 2535; and the 807/5,472 box. All held.

Validations re-run after the revision (2026-10-10): check_proof.py default seed SUMMARY PASS 12/12 (79 s); --seed 2026 --n 1000 --quick SUMMARY PASS 12/12 (52 s). Scratch: G on the run to 10^10 (67,856 transitions) with 0 unpredicted and 0 mismatches.