1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---: never halts

This machine never halts. From the blank tape it runs a binary counter: its tape is a row of binary digits, each a run of 10 pairs then a run of 01 pairs (with 00 between them for a digit 0), followed by a block at the right end.

At each return of the head to the right edge, the tape reads as such a counter. A carry adds 1 to the counter. When all digits are 1, an overflow re-pairs the halves of every digit instead.

The machine has the same transition table as another holdout, called the parent below, up to a renaming of the states. Symbols and directions are the same. This machine starts in the state that the parent calls B, so its run is not the parent's run.

The proof reuses the parent's whole argument. Only the start is new: a 732-step run from the blank tape to a configuration where the parent's invariant holds.

Machine and status

• Machine: 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---, viewer https://bbchallenge.org/1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---
• Holdout: on the current BB(6) holdout list (class "Skelet 1-like Class 2"). Not in busycoq.
• Written for: the string itself. The TM_from_str of the .v is this string; no Flip/Permute bridge is used.
• Existing work: there may be existing work on this machine by hipparcos (marked done on the community sheet, not yet in busycoq).
• The sheet's entry for this string links his bbchallenge Discord thread of October 2025: https://discord.com/channels/960643023006490684/1432566675533992019
• Its opening posts analyse this machine (block rules, a stride acceleration, and conjectures on which exponents can reach zero). They say that a proof is not yet in hand.
• The proof below is adapted from the parent's proof (next item), not from that thread. §7 relates the two.
• Parent: this is a delta write-up. It relies on the write-up for 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, called "the parent" below, which is attached alongside this one.
• "P§n" means §n of that write-up.
• This machine is the parent's table with its states renamed by τ = (A,B,C,D,E,F) ↦ (E,A,B,C,D,F), with no mirror. So it runs the parent's table started in the parent's state B (§0).
• Template: the parent's .v (694 lines, sha256 d177c06de5df0ff2e3c2c527bd7fd7454b48bd31f0e207a5ef9dd75b7603b552). It follows the architecture of busycoq verify/SBCv6.v Module TM21 (a binary counter over digit pairs with a re-pairing overflow).
• This machine differs from the parent only in state letters, never in a symbol or a direction: row τ(s) here is the parent's row s with each target t replaced by τ(t).
• The .v differs from the parent's .v in the TM string, τ applied to every state name, and the initial segment with its base case (§5).
• Status: formalized in the accompanying verify/Skelet1LikeC2_1RB0RB_1LC0RA.v (702 lines).
• It proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c).
• It compiles in about 9 s (-native-compiler yes). Print Assumptions nonhalt gives "Closed under the global context" (no axioms), and coqchk re-checks the compiled file.
• Where each section lives in the .v:
  • §0: tm;
  • §1: the window lemmas S1_1–S6_1, S1–S6, T1–T14; the digit lemmas Lb, Lf, Rb, Ro; the family K; the sweeps LbS, RbS, RoS; the rules M_spec, Mdrop_spec, O_spec; the invariant INV and its closure step;
  • §2: init and the base goal in nonhalt;
  • §3: nonhalt.
  • The full map is in §5.

Summary

This is the parent's binary counter, with head state A where the parent has B.

Head notation as in P§2.1: X> puts the head in state X on the next cell, and <X on the previous cell. 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
(10)^u (01)^v           bit 1

As in the parent: - a carry M adds 1 to the counter; - an overflow O re-pairs the halves of every digit; - the three-class invariant INV = Common ∧ (A ∨ B ∨ C) of P§3 is closed under M and O.

τ is a pure renaming of states (Lemma R, §0), so every window lemma, rule, step formula and the whole invariant argument carry over word for word. The invariant is not adjusted.

Only the start differs, because this machine starts in what is the parent's state B. From the blank tape it follows a different orbit of the same macro map:

this machine:  reaches the INV state K((1,1,10); 8, 1)  (class A)  at step 732
the parent:    reaches K((1,1,2); 8, 5)                             at step 483

The proof is that 732-step initial segment, a base-case check, and the parent's induction.

0. The map

The renaming is

τ:  A↦E,  B↦A,  C↦B,  D↦C,  E↦D,  F↦F        (a 5-cycle on A–E)

Row τ(s) of this table is the parent's row s with every target state t replaced by τ(t); symbols and directions are unchanged. For example, the parent's C1 = 0RB becomes 0Rτ(B) = 0RA, which is this machine's B1.

Among all 720 state renamings, each with and without mirroring, τ without mirror is the only map from the parent's table to this one.

Lemma R

Lemma R (relabelling). For a configuration c, let τc be c with its head state renamed by τ; the tape and head position stay the same. Then: - c → c′ under the parent if and only if τc → τc′ under this machine; - c is halted exactly when τc is (F1 is the only undefined cell, and τ fixes F).

So every run c →ⁿ c′ of the parent gives a run τc →ⁿ τc′ here, of the same length, and conversely.

Proof. If the parent has δ(s, x) = (y, d, t), this machine has δ(τs, x) = (y, d, τt) by the table above. ∎

Start, halting cell and the four holdouts

Start. This machine's c0 is

0^inf A> 0^inf  =  τ(0^inf B> 0^inf)

So its run is τ of the parent's table run from 0^inf B> 0^inf. This is not the parent's own run, which starts in A.

Halting cell. Only D1 = 1LF enters F (it is τ of the parent's E1), and F1 is ---. So the machine halts exactly when D reads 1 with a 1 to its left.

The four holdouts with this table. Up to renaming and mirroring, four holdouts share this transition table:

Each has its own .v; this write-up and its .v cover only the string above.

1. What carries over unchanged

The family of P§1, with head state A:

K(d_1..d_m; a, b) := 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf

(u,0,v) = (10)^u 00 (01)^v
(u,1,v) = (10)^u (01)^v

Part by part

The table lists each part of the parent's proof, what it becomes here, and why.

Window and digit lemmas

The window lemmas on this table, with their transitions (head notation as in the Summary, from P§2.1):

      window lemma                 steps  transitions
S1    A>01       -> 10A>             2    A0 B1                 one block of A> (01)^n -> (10)^n A>
S2    B>10       -> 01B>             2    B1 A0                 one block of B> (10)^n -> (01)^n B>
S3    01<C       -> <C10             2    C1 D0                 one block of (01)^n <C -> <C (10)^n
S4    10<D       -> <D01             2    D0 C1                 one block of (10)^n <D -> <D (01)^n
S5    B>1101     -> 10B>11           6    B1 A1 B0 C0 E0 A1     one block of B> 11 (01)^n -> (10)^n B> 11
S6    0A>10      -> 100A>            6    A1 B0 C0 E0 A1 B1     one block of 0 A> (10)^n -> (10)^n 0 A>
T1    A>00       -> <D01             3    A0 B0 C1              (on 0^inf)
T2    000<D      -> 100A>            5    D0 C0 E0 A1 B1
T3    100<D      -> <D011            3    D0 C0 E1
T4    01<D       -> <C11             2    D1 F0
T5    10<C       -> <D01             2    C0 E1
T6    00<C       -> 10B>             3    C0 E0 A1
T7    B>11       -> 00B>             2    B1 A1
T8    B>11011    -> 10000A>          9    B1 A1 B0 C0 E0 A1 B1 A1 B1
T9    0001001<D  -> 1001000A>       13    D1 F0 C0 E1 D0 C0 E0 A1 B1 A0 B1 A1 B1    (0^inf 1001 <D)
T10   A>11       -> 00A>             2    A1 B1
T11   A>0        -> 1B>              1    A0
T12   B>11000    -> <D01101         13    B1 A1 B0 C0 E0 A1 B1 A0 B0 C1 D0 C0 E1    (B> 11 0^inf)
T13   101<D      -> <D011            3    D1 F0 C1
T14   A>1101     -> 0010A>           4    A1 B1 A0 B1

The digit lemmas of P§2.1 read the same with the head states renamed, with the step counts and side conditions of P§2.1:

Lb   (10)^u (01)^v <D            ->  <D (01)^u (10)^(v−1) 11
Lf   (10)^u 00 (01)^v <D         ->  (10)^(u+1) (01)^(v−1) B> 11
Rb   B> 11 (01)^u (10)^(v−1) 11  ->  (10)^u 00 (01)^(v−1) B> 11
Ro   A> (01)^u (10)^(v−1) 11     ->  (10)^(u−1) 1 (10)^(v−1) 000 A>

The rules M and O

The rules in busycoq comment style, for this machine:

1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---     (= tau of 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, tau = EABCDF)

K(d_1 .. d_m; a, b) := 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf
digit (u,0,v) := (10)^u 00 (01)^v,   (u,1,v) := (10)^u (01)^v      (d_m least significant)

start from K((1,1,10); 8, 1)                                  (step 732, section 2)

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_j, v_j >= 1 (j > j*), a, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, P section 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
O at m = 0:  K(; a, b) --> K((1,1,a); b+3, 1)   in 89 + 8a + 20b steps (a >= 1); used only inside the initial segment

We write M_k for an M step with k = m − j* trailing bit-1 digits.

O at m = 0 is the derivation of P§2.3 with no digits (no Lb and no Ro).

The invariant

The invariant, restated from P§3 (derived quantities as in P§1):

INV(d_1..d_m; a, b) := Common /\ (A \/ B \/ C)
Common: m >= 1; 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
A:      d_1 = (0,0,v) with v >= 2, or d_1 = (1,1,v); for all j, vbar_j >= 1 and ubar_j odd; S >= 1
B:      d_1 = (0,0,1); for all j, v_j + beta_j odd; for j >= 2, ubar_j >= 2^(j-1)
C:      for all j, v_j + beta_j odd and ubar_j >= 2^j; S >= 1; T >= 2

2. What changes: initial segment and base (replaces P§4)

A K-configuration is state A on a blank cell with only blanks to its right, with the tape to its left parsing as a K.

Direct simulation of this machine from the blank tape finds them exactly at these steps up to 732. (The parent's table run from 0^inf B> 0^inf gives the same list, as Lemma R says.)

The legs

Each leg is an instance of the rules of §1. Its step count, from the step formulas:

step 122, O:               141 = 89 − 4 + 16 + 20 + 4 + 16
step 263, M_1:             100 = 32 + 32 + 8 + 4 + (16 + 8)
step 363, M_0:             100 = 32 + 40 + 24 + 4
step 463, O at m = 0:      269 = 89 + 80 + 100

The two M legs:

• The M_1 at step 263 flips the top (0,0,1) to (1,1,0), which falls into the next digit: (2,0,1) becomes (3,0,1).
• The M_0 at step 363 flips (3,0,1) to (4,1,0), which joins the block: a = 5 + 1 + 4 = 10.

Two legs use rule cases the invariant argument never needs (the LSB drop, and O at m = 0). That does not matter: the proof uses the 732-step run only as one finite computation, and the table only explains it.

For comparison: - the parent's run has K-configurations at 142, 283 and 383 (not in INV) and reaches its base K((1,1,2); 8, 5) at 483 (P§4); - the mirrored C-start 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- reaches K((1,1,9); 8, 1) at step 687.

INV at the base K((1,1,10); 8, 1)

• top (1,1,10): bit 1, u_1 = 1; m = 1;
• V = 1, R_tot = R_1 = 0, R1_1 = 0;
• ubar_1 = 1 (odd), vbar_1 = 10 ≥ 1 (also the LSB condition);
• S = 8 + 0 − 2 = 6 ≥ 1, T = 1 − 1 = 0 ≥ 0 (tight, as at the parent's base);
• a = 8 ≥ 1, b = 1 odd, a + R_tot = 8 even;
• so Common holds, and class A holds (top (1,1,v), every vbar ≥ 1, every ubar odd, S ≥ 1).

The base in the .v

In the .v, INV is the parent's additive form (P§6). There, R = Rof ds is computed by structural recursion on the least-significant-first digit list, and the clauses carry no subtraction or division.

At ([d1 1 10], 8, 1), with m = 1 and 2^(m+1) = 4, its 12 clauses are:

• ds ≠ [], a = 8 ≥ 1, b mod 2 = 1, (a + R) mod 2 = 0 with R = 0;
• a + R + 2 = 10 ≥ 4 (S ≥ 0), b + 3 + 2R = 4 ≥ 4 (T ≥ 0), LSBok: v_m = 10 ≥ R + 1;
• class A: a + R + 1 = 9 ≥ 4 (S ≥ 1), and PA (d1 1 10) 0 0, which is canonical (1 ≥ 1, 10 ≥ 1), 10 ≥ Rd + 1 = 1, ub = 1 odd, and ub = 1 for the top digit.

Every clause is linear arithmetic on constants, so the parent's own tactic line for its base goal closes this one (§5).

3. The argument (complete)

Theorem. 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- does not halt from the blank tape.

The proof has four steps.

1. Initial segment. The machine runs from c0 to K((1,1,10); 8, 1) in exactly 732 steps without halting. This is a finite exact computation (§2); in Rocq it is init, proved by solve_init.

2. Base. INV([(1,1,10)], 8, 1) holds, in class A (§2).

3. Transfer. P§3.2 (coverage) and P§3.3 (closure): every INV state has a macro step M or O, of at least 32 machine steps, to an INV state. These statements are about the triples and a, b, and the macro steps are rule instances K → K′ of the parent.

By Lemma R, each such instance is a run τK →⁺ τK′ of this machine of the same length, and τK is the K of §1. So coverage and closure hold verbatim for this machine's K-configurations.

4. Conclusion. By induction from the base, the run is an infinite chain of macro steps, each of at least one machine step, so it never halts (progress_nonhalt_cond with P := INV, as in P§5).

No macro step reaches the halting cell: each is an exact computation from one K to the next, composed of window lemmas in which F reads only 0. ∎

The parent's invariant argument (P§3) never refers to the parent's own orbit, so it applies to this orbit unchanged. The parent's orbit statistics (P§7) are evidence there, not premises.

4. How this orbit relates to the other starts of this table (remark, not used in the proof)

In the shared triple notation, three of the four starts of this table run orbits of the same macro map that lock together.

• With the mirrored C-start 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- (base K((1,1,9); 8, 1) at step 687): from macro step 0 on, the two states are equal except for one exponent near the top, larger by 1 here, and the same rule fires at every macro step.
• With the parent (base K((1,1,2); 8, 5) at step 483): from macro step 54 on (step 25,851 here, 25,618 in the parent), the states are equal except for one exponent near the top, larger by 4 here, with the same rule at every macro step.

Where the extra exponent sits:

How it moves: - O sends it from v_1 to digit 2's u (A → B); - the top fall merges it into the new top's u (B → C); - the next O sends it to the new top's v (C → A).

Both couplings were checked on the abstract macro orbits for 1.2·10⁶ macro steps (to t ≈ 3.7·10¹² machine steps, 93 overflows).

This matches the tape widths at 10⁹ steps:

The D-start 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA--- runs a different orbit (76,245 cells at 10⁹ steps).

5. The .v file

The .v is the parent's .v (694 lines, sha256 d177c06de5df0ff2e3c2c527bd7fd7454b48bd31f0e207a5ef9dd75b7603b552) with exactly these changes.

1. TM_from_str "1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---".

2. τ applied to every state name {{X}}, simultaneously: {{B}} -> {{A}} 22 occurrences {{C}} -> {{B}} 18 {{D}} -> {{C}} 5 {{E}} -> {{D}} 18 The parent's file names neither A nor F. This covers the window lemmas, the digit lemmas, the sweeps (LbS, RbS, RoS), the chunks and K.

The es/follow proofs re-close unchanged, because τ maps each transition of the parent's table to a transition of this one (Lemma R).

3. The new initial segment, 732 steps, proved by the parent's unfold K, L0. cbn. solve_init.: Lemma init: c0 -->* K [d1 1 10] 8 1. and in nonhalt: change (K [d1 1 10] 8 1) with (Kc ([d1 1 10], 8, 1)). The base goal is closed by the parent's own tactic line (§2).

4. The header comment, the three chunk comments that name head states, the banner of the invariant part, and the rule block at the end.

What stays the parent's text

Every other line is the parent's text:

• every proof script;
• the statements and proofs of M_spec, Mdrop_spec and O_spec, dg, map0, map1, Oz, Oout, INV, step;
• the structure of nonhalt.

About the file as a whole:

• It imports only Individual62 from busycoq (plus the stdlib ZifyNat, Lia, String, List, Arith).
• It has one TM_from_str, and has no Section, Module or Hypothesis.
• The closure lemma is called step, as in the parent. It shares its short name with the framework's step function, which is harmless because the final statement uses only tm, halts and c0.

Where each part lives

Lemma R is not a premise of the formal proof. Every window lemma, and through them every rule, is proved by es and follow on this machine's own table; Lemma R explains why the parent's scripts close on it.

The step counts are not part of the formal statement (the .v proves -->+ for each rule).

6. Numerical checks

These simulation checks are independent of the .v; the result rests on the .v alone.

• Table: τ without mirror is the only one of the 720 × 2 renamings that maps the parent's table to this one (12 of 12 cells). D1 is the only cell that enters F, and F1 is the only undefined cell.
• Lockstep: from the blank tape, this machine and τ of the parent's table run from 0^inf B> 0^inf agree at every step to 2·10⁷ (state, symbol written, move), with identical tapes at the end.
• Window lemmas: each of the 20 lemmas of §1 runs exactly as stated on this table, never reading outside its window, with τ of the parent's transitions. F is entered only in T4, T9 and T13, and reads 0 each time.
• Rules:
• M on 700 random K-configurations (k = 0..6; 273 with a drop, 257 with u* = 0; a, b ≥ 0) and O on 350 (m = 1..7) give exactly the stated result and step count.
• The leftmost cell read is the first 0 of the flipped 00 (M) and 3 cells left of the leading 1001 (O).
• 2,868 random INV states, run on the machine for one macro step, give exactly the predicted successor.
• Chains: every link of the parent's M and O chains (P§2.2–2.3), renamed by τ, holds on this table (whole tape, head and state) in 47,216 of 47,216 cases:
• M 37,220 and O 9,995 (exhaustive boxes, O including m = 0, plus random cases);
• and the initial leg K(; 10, 5) → K((1,1,10); 8, 1).
• Initial segment: from blank, K-configurations occur exactly at steps 122, 263, 363, 463 and 732, with the legs of §2. The parent's table from 0^inf B> 0^inf gives the same list.
• Real run: all 19,332 macro boundaries from step 732 to step 999,838,005 match the model (whole tape, head and state), and INV holds at each (class A 7,523, B 6,307, C 5,502).
• Rules used: O 53, M_0 9,639, M_1 4,846, M_2 2,422, M_3 1,209, M_4 602, M_5 298, M_6 and above 262.
• Drops: 30 of the top digit, 12 of a middle digit.
• Abstract orbit from the base: INV holds at each of 1.2·10⁶ macro steps (t ≈ 3.7·10¹² machine steps, 16 digits, 93 overflows).
• Random INV states (not only reachable ones):
• 600,000 of 600,000 single macro steps land in INV, each of at least 32 machine steps;
• all six class transitions A→A, A→B, B→B, B→C, C→A, C→C occur;
• the drop closed forms of P§3.1 (F2) hold on 20,000 random cases with m = 2..12 and every j*.
• No halt in 10⁹ steps from blank; the tape then spans 77,693 cells, 38,841 of them nonzero.

7. Relation to hipparcos's analysis

This section translates hipparcos's analysis (the thread in the header) and says what INV decides about it; it is not used in the proof.

Dictionary

His token n is 1 0^n left of the head and 0 1^n right of it. His names translate as follows:

tokens:     X = 1,   C = 2,   C0 = 0,   Cs = 4
R  = 0^inf
L0 = 0^inf 1001
L3 = 0^inf 1001000
>  = A>
b> = B>11
<  = <D

In his order, his 14 block rules are these lemmas of §1:

 1   S1
 2   S5
 3   S4
 4   T9
 5   T2
 6   Lf with v = 1
 7   T1
 8   T12 less its last 3 steps
 9   T3
10   T13
11   T2
12   T8
13   T11
14   Lf with v = 1

In his notation, a K-configuration reads

K(d_1..d_m; a, b) = L0 w_1 C0 … C0 w_m C0 X^(a−1) Cs X^b > R

w = X^(u−1) C X^(v−1)       for bit 1
w = X^(u−1) Cs X^(v−1)      for bit 0

A top (0,0,v) gives L3 X^(v−1) for L0 w_1 (below the top, u ≥ 1 in the run).

His cycle

His cycle is one turn A → B → C → A. His configurations translate as follows:

L0 < r               the far-left turn T9 of an overflow from class C
L3 < f(r)            the class-A carry into the top
L0 C < f²(r)         the overflow from class A
L3 C0 < g(f²(r))     the top fall

Here, for the state K((u_j,1,v_j)_{j≤m}; a, b) of that overflow from class C,

r = Π_j (X^(u_j−1) C X^(v_j−2) C) X^a C X^(b+2) R

So: - passes 1–2 are class A, 3 is B, 4 is C; - his first group is the u_j − 1 and a, his second the v_j − 2 and b + 2; - his collisions Cs C0 < are the other drops.

His rules and hypotheses

Block, stride and collision rules, the cycle, and the exponent table without collisions: true. His 14 rules alone, from L0 b> X^2 R at step 24, reproduce the run to step 10⁹. They miss only C0 C0 < (a halt) and C C0 <.

Collisions only in pass 4: true. INV gives passes 1–2 (class A has no drops) but allows drops in class B.

There the top falls by L3 C0 < and the LSB never drops. Every other digit j starts with v equal to the u_j of the overflow from class A, which is

ubar_j ≥ 2^(j−1) + 1        (F3, F1)

and the digit is touched at most 2^(j−1) − 1 times before the top falls, so it never runs out.

A collision removes one digit, i.e. two exponents.

First group never 0: true at cycle starts, where

u_j − 1 ≥ 2^j − 1   and   a ≥ 2^(m+1) − 1        (class C at all bits 1)

Mid-cycle the j-th one falls by 2^j, to v_j − 2 at the overflow from class A. There INV proves only the weaker bound ≥ −1 (vbar_j ≥ 1).

Second group even: true for each v_j − 2 (v_j + 1 is odd). The X^n R exponent b + 2 is odd at every left-end visit (b odd), as he guessed.

C C0 at the right end: no

C C0 < is D reading the last 1 of a 1001 with a nonzero cell further left. It does not occur in the first 732 steps.

After them, D reads 1 only in T4, T9 (L0 <) and T13 (X C0 <), and T4 meets a 1001 only where Lb starts on a digit (u,1,1).

So C C0 < is Lb on a bit-1 digit with v = 1 (his <D 0111).

The right end is the LSB digit and the block (10)^a 000 (10)^b. The block holds no digit, and INV excludes the LSB:

• A carry sweeps only digits with v ≥ R + 1 ≥ 3 (class A, F0) or v even (B, C).
• An overflow from class C has all v even.
• An overflow from class A has v_m = vbar_m, which is ≥ 1 and even, so v_m ≥ 2.
• It is even because class A starts at the base (vbar = 10) or after an overflow from class C, and class A keeps it. After an overflow from class C, F3 gives the new LSB vbar = a − 2^(m+1) + 2 with a even (a + R_tot even, R_tot = 0).

INV leaves open only a digit (u,1,1) above the LSB at an overflow from class A. That needs u_j = 2^j at the overflow from class C before it (v_j = u_j − 2^j + 1).

Checks

Direct simulation to step 10⁹: - the 14 rules (in random contexts) hold; - both readings hold (19,332 K-configurations, 53 overflows); - the rule-only run holds (38,672 > R moments); - the cycle holds (132 left-end visits); - the table holds (next paragraph); - no C C0 < occurs.

For the table, the tracked exponents are the 289 X^n C exponents at the starts of the 25 complete cycles after step 732: - the 242 not involved in a collision follow his table exactly (each by its place at the start of the cycle); - the 47 caught in a collision follow his collision rule.

On the abstract orbit (1.2·10⁶ macro steps), class B never drops below the top, and every v swept at an overflow from class A is ≥ 4.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).