1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB (W5-4): never halts (informal proof)

• Machine: 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB (740 list, line 525; on every list since 2024-06-14), viewer https://bbchallenge.org/1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB
• Sheet: "Bell eats counter", no claim, no Discord thread. Written for the string itself (no mirror, no renaming). Its only undefined transition is F0.
• Template for the Rocq build: our W4-2 kill machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/...v (from BECv5.v TM1/TM2): one lemma per rule. New here (§9): the level stack, the shift law, the sign law, and the bounded induction of §6 in place of W4-2's progress_nonhalt_cond over an invariant.
• Status: informal proof. Finite claims (low-level rules, initial segment) are exact TM runs. Parametric claims are derived by hand in §3–§6 and each one has a named check in check_proof.py (§10), exhaustive on small cases and random on large ones. Not yet formalized.
• AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

0. Summary

The tape is a bell of 10 pairs with a moving wall 00, followed by a zone that holds a binary counter. The counter's bits sit 3 cells apart, on a lattice anchored at the zone's right end. A zero cell on the lattice is a set bit.

• Round. The head runs from the wall to the zone and back. The wall moves 2 pairs right and the counter is decremented. At value 0 it overflows: it refills to all-set and grows by one bit.
• Bite. When the bell is used up (q ≤ 2 pairs left of the zone), the wall bites the low end of the zone. Most bites end the cycle: the head sweeps back to the left end, and the left part becomes the new bell.
• Nesting. A bite that meets k ≥ 1 low set bits opens k nested levels. Each one is an ordinary cycle run on the rest of the zone, shifted right. Then the outer cycle continues.
• Halting. The only halting configuration is a bite at q = 2 on an all-set zone. It needs an overflow at exactly q = 4.

The proof is an invariant on cycle starts s = (n, w, v) (bell n, zone width w, counter value v):

I = { w >= 3,  d = n - 2^(cap(w)+1) >= 2,  M(s) != 0 (mod 3) }  minus the single state (6, 4, 0)

d >= 2 says the bell is long enough for the counter, and M is a mod-3 quantity that every cycle negates. Inside a cycle, every level other than the first phase of the outer cycle starts in a parity class J that cannot reach the halting overflow.

1. Rule table (busycoq comment-block style)

1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB            (only F0 is undefined)

lattice(w) = { j = w-1-3i : i >= 1, j >= 2 };   bit b of v (b = 0, 1, ...) sits on the b-th smallest lattice cell
enc(w,v)   = 1^w with 0 on the lattice cells of the set bits of v;   L(w) = #lattice(w) = floor(w/3) - 1
cap(w)     = L(w) + [w = 1 mod 3]                    allset(u) = enc(u, 2^L(u) - 1)
R(p,q,Z)   = 0^inf (10)^p 1 C> 0 0 (10)^q Z 0^inf  (p >= 0);   R(-1,q,Z) = 0^inf C> 0 0 (10)^q Z 0^inf  (cycle start)
             (Z never starts with 10: the bell takes every leading 10 pair; Z has no trailing 0)
R_L(p,q,Z) = L 0 0 (10)^p 1 C> 0 0 (10)^q Z 0^inf     (p >= 0, any left context L;  R = R_(0^inf))
R_L(-1,q,Z) = L C> 0 0 (10)^q Z 0^inf                  (only a name for the tape a level pops to)
             no rule is applied to R_L(-1, ..) unless L = 0^inf;  if L = L' 0 0 1 it is the tape R_L'(0, q, Z)

low-level rules (each run reads only the cells shown)
BR   B> 1^k              --> 1^k B>                                    k
S    (01)^k <C           --> <C (01)^k                                 2k       C1 D0
T    (111)^j <C          --> <C (011)^j                                5j       C1 D1 A1 C1 D0
W    C> 00 101010        --> 0101 0011 B>                              10
PS   011 B> (10)^b       --> 0 (10)^b 11 B>                            12b
ZA   00 (10)^a 11 B> 1^f 0  --> C> 0 (01)^(a+1) (011)^j 1              f = 2 mod 3, j = (f+1)/3
                            --> C> 0 (01)^(a+2) 111 (011)^(j-2) 1      f = 1 mod 3, f >= 4, j = (f+2)/3
                            --> C> 0 (01)^a 011111 (011)^(j-1) 1       f = 0 mod 3, f >= 3, j = f/3
PUSH C> 00 1010 (110)^k 111  --> 0101 (001)^k C> 00 101                14+3k   (k >= 0)
B1   00 (10)^p 1 C> 00 10 11 --> C> 00 (10)^(p+3) 1                    2p+15
B0   00 (10)^p 1 C> 00 1^f 0 --> C> 00 (10)^(p+2) 1 (011)^j 1          f = 2 mod 3, j = (f-2)/3
B0c  00 (10)^p 1 C> 00 1^w 0 --> C> 00 (10)^(p+2) 11 allset(w-2)       w = 0 mod 3, w >= 6
     00 (10)^p 1 C> 00 111 00 --> C> 00 (10)^(p+1) 111111              2p+31
Ht   C> 00 101 000       --> 0101 001 F> 0  (F0 undefined)             9

macro rules (Z = enc(w,v), f = position of the first 0 of Z, or w if v = 0; p >= 0 and any left context L;
             the five rounds also hold at p = -1 with L = 0^inf, where they give R(1, ..), §3.2)
R1   R_L(p,q,Z) --> R_L(p+2, q-2, enc(w, v-1))              q >= 3, v >= 1, w = 0,2 mod 3
R2   R_L(p,q,Z) --> R_L(p+2, q-3, enc(w+2, 2v-2))           q >= 3, v >= 1, w = 1 mod 3
O2   R_L(p,q,Z) --> R_L(p+2, q-2, enc(w+1, 2^(L+1)-1))      q >= 3, v = 0,  w = 2 mod 3
O1   R_L(p,q,Z) --> R_L(p+2, q-2, enc(w+1, 2^L-1))          q >= 3, v = 0,  w = 1 mod 3, w >= 4
O0   R_L(p,q,Z) --> R_L(p+2, q-3, enc(w+3, 2^(L+1)-2))      q >= 3, v = 0,  w = 0 mod 3
     (all five = W, PS^(q-3), ZA; 10 + 12(q-3) + f + 1 + 5j + {2(q-2) | 5+2(q-1) | 11+2(q-3)} steps)
B2   R_L(p,2,Z) --> R_L(p+2, 1, Z[2:])  re-parsed           Z starts 111, w >= 6    (PUSH k=0)
                (w = 1, bit 0 set: R_L(p+2, 2, enc(w-4, (v-1)/2)); never occurs, Lemma P)
N    R_L(p,2,(110)^k Y) --> R_L(p+2, G^(k-1)(3, Y[3:]))     k >= 1, Y starts 111, |Y| >= 6
H    R_L(p,2,(110)^k 111) --> halts                         k >= 1  (PUSH k, then Ht: 23+3k steps)
                (also k = 0, Z = 111: PUSH 0, then Ht; never occurs, since a bite zone has width >= 5, P1)
B1   R_L(p,1,Z) --> R_L(-1, p+3, Z[1:])  re-parsed          p >= 0, Z starts 11
B0   R_L(p,0,Z) --> R_L(-1, p+3, enc(w-3, (v-2)/2))         w = 0 mod 3, v >= 1 even
                --> R_L(-1, p+2, enc(w-1, (v-1)/2))         w = 0 mod 3, v odd      (never occurs, Lemma P)
B0c  R_L(p,0,1^w) --> R_L(-1, p+2, enc(w, 2^L-2))           w = 0 mod 3, w >= 6;   1^3 --> R_L(-1,p+1,1^6)
     ending bites (B1, B0, B0c) need the 0 0 left of (10)^p 1 and read nothing left of it

levels:  t = (n,w,v);  F(t) = the cycle start R(-1, F t) reached from R(-1, n, enc(w,v));
         the run from R_L(p0, n, enc(w,v)), p0 >= 0, n >= 3, pops at R_L(-1, F(t) + (p0+1, 0, 0))  (L never read);
         G(t) = F(t) + (1,0,0) = where a level started at R_L(0, n, enc(w,v)) pops
stack:   N = PUSH k, then the innermost level R_L1(0,1,Y[2:]) --B1--> (3, Y[3:]); level i pops into
         level i+1 (R_L(-1, ..) of level i = R_L'(0, ..) of level i+1); level k pops into R(p+2, ..)

invariant:  d(t) = n - 2^(cap(w)+1);  M(t) = n + 2v - 2^(cap+2) (w = 0,2) | n + v - 2^(cap+2) (w = 1)  (mod 3)
   K = { w >= 3, d >= 2 };   I = { t in K : M(t) != 0 } minus (6,4,0)
   J = { w >= 3, n >= 3, n odd if w = 1,2 mod 3 }               (inner phase starts)
   H* = { w = 2: n = 2v+4 } u { w = 1: v = 0, n = 2^(L+1)+4 }    (the phase starts that halt)
   s in I  ->  the cycle from s never halts, and if it ends, F(s) is in I   (M(F s) = -M(s))
start:  c0 -->(327) R(-1, 6, 11111) = (6,5,0),  d = 4, M = 2:  in I

2. Notation and families

• Tape notation. l C> r: state C reads the first cell of r. l <C r: state C reads the last cell of l. Words are written left to right as on the tape.
• Zones. A zone of width w has lattice cells j = w-1-3i (i ≥ 1) with j ≥ 2. Bit b of the value v (b = 0, 1, …, L-1) sits on the b-th smallest lattice cell, so bit 0 is the leftmost one (least significant first). The index i in j = w-1-3i counts from the right and is not the bit index. A set bit is a 0 cell. enc(w, v) is the zone, L(w) the number of bits.
• L(w) = floor(w/3) - 1 for w ≥ 3. The lowest lattice cell is 2, 3 or 4 for w ≡ 0, 1, 2 (mod 3).
• cap(w) = L(w) + [w ≡ 1]. The extra bit for w ≡ 1 is the cell 0 that becomes lattice cell 2 after an R2 round.
• A zone enc(w, v) always starts with 11, so the bell parse is unambiguous. It has no 00.
• f is the first 0 of the zone (the lowest set bit), or f = w when v = 0. Then Z = 1^f 0 r, where for v = 0 the 0 is the first blank cell and r is empty.
• Family. R_L(p, q, Z) (p ≥ 0) as in §1: a left context L, the wall 00 that ends L, the left part (10)^p 1, the wall 00 read by C, the bell (10)^q, the zone Z, then blanks.
• The outer level uses L = 0^inf, written R(p, q, Z).
• A cycle start is R(-1, n, enc(w, v)): no left part, blank left side. It is written as the triple t = (n, w, v).
• R_L(-1, q, Z) = L C> 0 0 (10)^q Z is the tape a level with left context L pops to. Rules are applied at p = -1 only with the blank left side (§3.2). For L = L' 0 0 1 this tape is R_L'(0, q, Z), and that is how an inner pop is read (§3.4).
• Letters. f is always the position of the first 0 of a zone. In §4–§5 the level at which a phase bites is m; it is also the number of overflows before the bite.
• Bites. A rule from q ≥ 3 is a round. A rule from q ≤ 2 is a bite. B1, B0, B0c are ending bites (they end the level, p becomes -1). B2 and N are not.
• Phases. A phase is the run of a level from its phase start (a level start, or the configuration after an N bite) to its next bite. Every phase start has q ≥ 3, except the innermost level of a nested bite, which starts at q = 1 and is a single B1 (§3.4).

3. Rules

3.1 Low-level rules (exact TM runs)

The transitions are A0 = 1RB, A1 = 0RC, B0 = 1LC, B1 = 1RB, C0 = 0RE, C1 = 1LD, D0 = 0LC, D1 = 1LA, E0 = 1RF, E1 = 1RA, F1 = 0RB; F0 is undefined.

Every rule below is a finite run that reads only the cells it shows, so it holds for every context left and right of them. Check LOW runs each one inside random context and verifies that the head never leaves the pattern.

Pair step PS, one pair. 0 1 1 B> 1 0: B1, then B0 writes 1 and C reads the third 1 of 111. T leaves <C 0 1 1 1 with C on the leading 0. C0 E0 F1 B1 B1 then give 0 1 0 1 1 B>. Induction on b.

Zone arrival ZA. Start: 00 (10)^a 11 B> 1^f 0, f ≥ 2. BR runs over 1^f, and B0 writes 1 on the 0. That leaves 00 (10)^a 1^(f+2) <C 1. Then T^j consumes the 1s in threes from the right. What is left depends on f+2 mod 3:

Here 0 (01)^m reads as 00 (10)^(m-1) 1. So in each result C stands on the first 0 of a new wall.

Bites at q = 0. B0 and B0c are the same arrival with the wall itself as the start: C> 00 1^f 0 runs C0 E0 F1 BR^(f-1) B0, then T^j, then the sweep S over the left part.

Ending sweeps. In B1, B0 and B0c the last S runs through the left part (10)^p 1 (= 1 (01)^p read leftwards). Then D reads the second 0 of the 00 left of it, and C stops on the first one. So an ending bite needs those two cells to be 0 and reads nothing further left.

3.2 The round (R1, R2, O0, O1, O2)

For q ≥ 3 and Z = 1^f 0 r, the round is W, then PS^(q-3), then ZA with a = q - 3. Reading the ZA result as a family member gives three cases by f mod 3:

f = 2 (mod 3):          R_L(p, q, 1^f 0 r) --> R_L(p+2, q-2, (110)^((f-2)/3) 111 r)
f = 1 (mod 3), f >= 4:  R_L(p, q, 1^f 0 r) --> R_L(p+2, q-2, 1111 (011)^((f-4)/3) 1 r)
f = 0 (mod 3), f >= 3:  R_L(p, q, 1^f 0 r) --> R_L(p+2, q-3, 11111 (011)^((f-3)/3) 1 r)

Left context. The round reads nothing left of the wall. It turns the wall and the first pair into 0101 (W), so for every L

L C> 0 0 (10)^q Z   -->   L 0101 C> 0 0 (10)^q' Z'

• For p ≥ 0, L is followed by 0 0 (10)^p 1, and (10)^p 1 0101 = (10)^(p+2) 1. So the output is R_L(p+2, q', Z'): the round holds for p ≥ 0 and every L.
• For p = -1, L 0101 = L' 0 0 (10)^1 1 only when L = L' 0. So R_L(-1, q, Z) goes to R_L'(1, q', Z') when L = L' 0, and in particular R(-1, q, Z) goes to R(1, q', Z'). When L ends in 1, the output is one cell short of R_L(1, ..).
• So the round at p = -1 is used only with the blank left side. That is all the proof needs: the only level started at p = -1 is the outer one, and an inner pop R_L(-1, ..) is re-read at once as R_L'(0, ..) with L = L' 0 0 1 (§3.4). Check MAC.round at p = -1 runs the display above with random L.

Counter form. For a zone enc(w, v), the first 0 is at the lowest set bit, and that bit's cell is ≡ w-1 (mod 3). When v = 0, f = w. Rewriting the three outputs:

Rounds with q-2 are 2-rounds; R2 and O0 are 3-rounds. A round never outputs a zone starting with 10, so no reparse is needed.

3.3 Bites

At q = 2, a zone starting 110 has its bit 0 set, so w ≡ 0. Then Z = (110)^k Y, where k is the number of low set bits and Y = Z[3k:]. Y starts with 111 (its first lattice bit is clear), or it is 111 exactly (all bits of Z set). An enc zone of width ≡ 0 that starts with 111 and is not 111 has width ≥ 6.

The zone 111 itself (w = 3, k = 0) halts at q = 2: PUSH 0 leaves R_L(p+2, 1, 1), and Ht follows. It never occurs, because a bite zone has width ≥ 5 (P1). B2 at w = 4 or 5 would need w ≢ 0 at q = 2, which never occurs either (P3).

3.4 Levels, the stack, and the shift law

Levels. A level is a run of the family started at R_L(0, n, Z) (an inner level, any L) or at R(-1, n, Z) (the outer level, blank left side), with n ≥ 3. It applies macro rules until its first ending bite, which leaves it at R_L(-1, n', Z'), the pop.

Shift law. Rounds, B2 and N read nothing left of the wall and add 2 to p. They hold for p ≥ 0 with any L, and the rounds also at p = -1 with the blank left side (§3.2). The ending bites need p ≥ 0. They output q' = p + const, plus a reparse that does not depend on p. Which rule applies depends on (q, Z) only. So:

• (SL1) Let n ≥ 3, and let p0 ≥ 0 with any L, or p0 = -1 with L = 0^inf. The run from R_L(p0, n, Z) applies the same rule sequence as the cycle from R(-1, n, Z). Every p is larger by p0 + 1, and so is the pop's n': the run pops at R_L(-1, F(t) + (p0 + 1, 0, 0)).
• The first rule is a round (n ≥ 3), and after it p ≥ 1. So no rule is ever applied at p = -1 with a nonblank left side.
• (SL2) In particular, a level started at R_L(0, n, Z) pops at R_L(-1, G(t)) with G(t) = F(t) + (1, 0, 0).
• (SL3) The rest of a run after a configuration R_L(p, q, Z) with p ≥ 0 and q ≥ 3 is the run from that configuration. So (SL1) applies to it with p0 = p.

The only TM fact used is that an ending bite reads the two cells left of (10)^p 1 and nothing beyond. For L = 0^inf they are blank. For an inner level they are the 00 of its 001 block (below). Check SH runs the TM from L 0 0 (10)^p0 1 C> 0 0 (10)^n Z with random L and p0, and confirms that it pops at F(t) + (p0 + 1) without visiting L.

The stack (rule N). Take R_L(p, 2, (110)^k Y) with k ≥ 1, Y starting 111, Y ≠ 111.

1. PUSH k gives L 00 (10)^(p+2) 1 (001)^k C> 00 10 Y[2:]. - Write L_i = L 00 (10)^(p+2) 1 (001)^(k-i). Then this is R_{L_1}(0, 1, Y[2:]): level 1, the innermost.
2. Level 1 is one B1 bite (Y[2:] starts 11). It pops at R_{L_1}(-1, 3, Y[3:]). - Y[3:] starts 11, so no reparse.
3. Since L_1 = L_2 0 0 1, the configuration R_{L_1}(-1, q, Z) is the same tape as R_{L_2}(0, q, Z). So each pop is the next level's start. - Level i ≥ 2 starts at R_{L_i}(0, t_i), with t_2 = (3, Y[3:]) and t_(i+1) = G(t_i) by (SL2).
4. Level k pops at R_{L_k}(-1, t_(k+1)), and L_k = L 00 (10)^(p+2) 1. So that tape is R_L(p+2, t_(k+1)). - The outer level continues from there with t_(k+1) = G^(k-1)(3, Y[3:]). For k = 1 this is B2': R_L(p+2, 3, Y[3:]).
5. A nested bite inside a level does the same with that level's own L. Formally the stack is an induction on the length of the computation, since every inner level is a strictly shorter run.

Check NEST runs the TM on random nested bites: the level starts (10)^(p+2) 1 (001)^(k-i+1) C> 00 (10)^(n_i) Z_i occur in order, then the exit. With Y = 111 the innermost level is R(0, 1, 1), and Ht halts: that is H.

Composite form of a cycle with a continuation. Let the first N bite of the outer level from s happen at R(p_c, 2, Z_c), with k low set bits and L_c = L(|Z_c|) bits. Here p_c is in the outer frame, where p = -1 at the cycle start.

F(s) = (p_c + 2) + t_(k+2),     t_2 = (3, Z_c[3k+3:]),  t_(i+1) = G(t_i),     so  d(F s) = p_c + 2 + d(t_(k+2))

By the stack, the outer level resumes at R(p_c + 2, t_(k+1)). By (SL3) the rest pops at F(t_(k+1)) + (p_c + 3) = t_(k+2) + (p_c + 2). Later N bites of the outer level lie inside this last G-step. The cap of t_2 is L_c - k - 1: its zone drops the k+1 low bits.

The same argument for a level started at R_L(0, t), with the first N bite at R_L(p_c, 2, Z_c) and p_c in the level's own frame (p = 0 at the level start), gives

G(t) = (p_c + 2) + t_(k+2)

In the frame of the cycle from t (p = -1 at the start) that bite is at p_c - 1, and the formula reads F(t) = (p_c + 1) + t_(k+2). Check INV (CF-J) tests the own-frame form.

4. Cycle arithmetic

Levels of a phase. Fix a phase start (n, w, v) with w ≡ 0 or 2. Let c = L(w) (= cap(w)) and e = [w ≡ 2].

• Level 0 is the initial zone. R1 rounds decrement v, so the zone becomes all clear at q = E_0 = n - 2v. If E_0 ≥ 3 it overflows: O2 (e = 1) or O0 (e = 0).
• Level i ≥ 1 has a zone with w ≡ 0 and c + i bits. It starts at value 2^(c+i) - 1 (after O2) or 2^(c+i) - 2 (after O0). It reaches 0 at

E_i = E_0 + i - e - (2^(c+i+2) - 2^(c+2))        (i >= 1)

and overflows again (O0) iff E_i ≥ 3. That gives E_(i+1) = E_i + 1 - 2^(c+i+2).

• The phase bites at the first level m with E_m ≤ 2, at some q_b ∈ {0, 1, 2}. So m is also the number of overflows before the bite. Write u for the zone value there; it has c + m bits.
• Level m starts at Q_m = E_(m-1) - 3 for m ≥ 2, and at Q_1 = E_0 - 3 + e for m = 1. Inside level m only 2-rounds (R1) happen, so q_b ≤ Q_m with q_b ≡ Q_m (mod 2).

Position at the bite. Count the decrements of q: n - q_b = 2·(#2-rounds) + 3·(#3-rounds), and the only 3-rounds are the m - e O0 overflows (m ≥ 1). Each round adds 2 to p, so

p_b = n - 1 - q_b - (m - e)        (outer level, p starts at -1)

Reductions for w ≡ 1 (check CH.EQ1, CH.EQ2).

• (EQ1) If v ≥ 1 and n ≥ 4, then F(n, w, v) = F(n-1, w+2, 2v-1). The R2 round from (n, w, v) and the R1 round from (n-1, w+2, 2v-1) both end at R(1, n-3, enc(w+2, 2v-2)). Here cap(w+2) = cap(w), d drops by 1, and M is unchanged.
• (EQ2) If v = 0, then F(n, w, 0) = F(n-2, w+1, 2^L - 1) + (2, 0, 0) (L = L(w)). O1 leads to R(1, n-2, allset(w+1)); apply (SL3). Here cap(w+1) = cap(w) - 1.

5. The invariant

5.1 Definitions

d(t) = n - 2^(cap(w)+1)          M(t) = n + 2v - 2^(cap+2)  (w = 0,2 mod 3);   n + v - 2^(cap+2)  (w = 1)   (mod 3)
K  = { w >= 3, d >= 2 }          I = { t in K : M(t) != 0 } minus (6,4,0)
J  = { w >= 3, n >= 3, n odd when w = 1 or 2 mod 3 }
H* = { w = 2 mod 3, n = 2v + 4 }  u  { w = 1 mod 3, v = 0, n = 2^(L+1) + 4 }
T_c = (2^(c+1)+2, 3c+5, 2^c - 1)        (w = 2 mod 3, d = 2, all set)

A state t is zone-dominated if d(t) ≤ 1, and K-like if d(t) ≥ 2.

H* ∩ K = {T_c : c ≥ 0} ∪ {(6,4,0)}.

• For w ≡ 2: n = 2v + 4 ≥ 2^(c+1) + 2 forces v = 2^c - 1.
• For w ≡ 1: 2^(L+1) + 4 ≥ 2^(L+2) + 2 forces L = 0, so w = 4 and n = 6.

M(T_c) = 0: 2^(c+1) + 2 + 2^(c+1) - 2 - 2^(c+2) = 0. Also H* ∩ J = ∅, because H* has n even and w ≢ 0.

5.2 Lemma P (phase lemma, and coverage)

Take a phase start with q = n ≥ 3 and zone enc(w, v), w ≥ 3, that lies in J or in K. Then:

• (P1) Every zone in the phase is an enc zone, and after the first round its width is ≥ 5.
• The rounds map enc zones to enc zones (§3.2). Widths: R1 keeps w (≥ 6 when v ≥ 1), R2 gives w+2, O2 and O1 give w+1, O0 gives w+3, and 3 → 6, 4 → 5, 5 → 6.
• (P2) Residues and parity.
• w ≡ 1 occurs only at the phase start: R2 leads to ≡ 0, O1 to ≡ 2.
• w ≡ 2 occurs only at the start or right after O1 at the start; R1 keeps it and O2 leads to ≡ 0.
• w ≡ 0 is kept by R1 and O0.
• All rounds before the first 3-round or O2 are 2-rounds, so q keeps the parity of n while w ≢ 0.
• (P3) The bite has w ≡ 0, w ≥ 6, except a B1 at q = 1.
• q = 2 needs w ≡ 0. In J, n is odd while w ≢ 0. In K, level 0 always overflows (E_0 ≥ 4, §5.5), and the w ≡ 1, v = 0 case overflows twice (O1, then O2 at q = n - 2^c ≥ 4).
• q = 0 only right after a 3-round at q = 3, and R2 and O0 leave bit 0 clear. So q = 0 means B0 with bit 0 clear (f ≥ 5), or B0c. The B0 case "bit 0 set" never occurs.
• B0c on 111 never occurs, since a q = 0 zone has width ≥ 6.
• So every configuration has a rule: q ≥ 3 a round; q = 2 B2, N or H; q = 1 B1 (zones start 11, width ≥ 4); q = 0 B0 or B0c.
• (P4) The phase reaches H iff its start is in H*.
• H needs an all-set zone at q = 2. R1 never makes one (v-1 < 2^L - 1). R2 and O0 leave bit 0 clear. O1 makes a w ≡ 2 zone, and q = 2 never meets one (P3).
• So H comes only from O2 at q = 4. O2 acts on a w ≡ 2 level at v = 0: either the start, reaching 0 at q = n - 2v, or the O1 level, reaching 0 at q = n - 2 - 2(2^L - 1) = n - 2^(L+1).
• q = 4 gives exactly H. Conversely, from H the O2 at q = 4 happens and H follows.
• (P5) Ending bites, and pop parity.
• B1 gives n' = p + 3 + r, where the reparse r = 1 only for w ≡ 0 with bit 0 set (then w' = w-3 ≡ 0).
• B2 then B1 gives n' = p + 5 and w' = w - 3 ≡ 0.
• B0 gives n' = p + 3 and w' = w - 3 ≡ 0. B0c gives n' = p + 2 and w' = w ≡ 0.
• So a pop with w' ≡ 1 or 2 has n' = p + 3 ≡ p + 1 (mod 2). Every pop has w' ≥ 3 and n' ≥ p + 2.

Checks ABS.P.* test (P3) and (P5) on every rule application of random K and J cycles. INV.hstar tests (P4) on the exhaustive windows.

5.3 Lemma J (inner phases)

Lemma J. If t ∈ J, the level from t never halts, never reaches a configuration without a rule, and (if it pops) pops into J. The same holds for every phase of the level.

Proof.

• t ∉ H*, so by (P4) its first phase does not reach H, and by (P3) it never reaches a configuration without a rule.
• An inner level has p even: it starts at 0 and adds 2 per round.
• An ending bite then gives n' ≥ p + 2 ≥ 4 (at least one round happened), w' ≥ 3, and n' odd when w' ≡ 1, 2 (P5). So the pop is in J.
• An N bite inside the phase has k ≥ 1 and Y ≠ 111 (no H), so |Y| ≥ 6 and t_2 = (3, Y[3:]) ∈ J.
• Its inner levels are levels from J (by induction on the length of the run, each pops into J if it pops).
• The level resumes at R(p_c + 2, t_(k+1)), a phase start with t_(k+1) ∈ J.
• By (SL3) its pop is t_(k+2) shifted by p_c + 2, which is even. So the pop is in J.

No termination is claimed. A level that never pops is still a run without a halt. □

The induction "on the length of the run" here, and in §5.4 (N) and §5.7, is made exact in §6: Lemmas J, K, Z', Kp and M (for one level) are one bounded statement U(N), proved by strong induction on the number of steps N.

5.4 Lemma M (sign law)

Extend M to every family member, with σ = +1 for w ≡ 1 and σ = -1 otherwise:

Q(p, q, Z) = q - (p+1) + σ v - (-1)^cap(w)    (mod 3)

At p = -1, Q = M, because 2^(cap+2) ≡ (-1)^cap and 2v ≡ -v.

Lemma M. Rounds, B2 and N keep Q. The ending bites negate it. So M(F s) ≡ -M(s).

All congruences are mod 3, with 2^x ≡ (-1)^x, 2 ≡ -1 and v/2 ≡ -v for even v. Write L = L(w).

Rounds (Q' is computed at p+2):

Bites that keep Q (B2, at q = 2, Q' computed at p+2, q' = 1):

Ending bites (Q' computed at p = -1; the claim is Q' ≡ -Q):

N (induction on depth). Let X_i be Q at the start of level i (p = 0). Each level keeps Q until its ending bite, which negates it. The pop (p = -1) has Q = -X_i, and the next level's start has Q one smaller (p+1 goes from 0 to 1). So

X_(i+1) = -X_i - 1,   i.e.   X_(i+1) - 1 = -(X_i - 1)     (mod 3)

Level 1 starts at R(0, 1, Y[2:]), where Y[2:] has w ≡ 1, value v_Y/2 and cap L - k. So X_1 ≡ -v_Y - (-1)^(L-k).

The outer level resumes with Q_out = -X_k - (p+3), and Q_in = 1 - p - v - (-1)^L with v = 2^k - 1 + 2^k v_Y. Substituting X_k = 1 + (-1)^(k-1)(X_1 - 1), both sides equal -p - 1 - (-1)^k(1 + v_Y) - (-1)^L. So Q_out = Q_in. □

5.5 Lemma K, plain cycles

Lemma K. Let s ∈ K, s ∉ {T_c, (6,4,0)}. The cycle from s does not halt, and if it ends, F(s) ∈ K. T_c and (6,4,0) halt (they are in H*).

Halting. The outer first phase halts iff s ∈ H* (P4), i.e. iff s is T_c or (6,4,0). Every later phase starts in J (Lemma J). So the cycle does not halt.

The bound, w ≡ 0 or 2 (c = L(w), e = [w ≡ 2]).

• In K, E_0 = n - 2v ≥ 2^(c+1) + d - 2(2^c - 1) = d + 2 ≥ 4. So level 0 overflows and m ≥ 1.
• In a plain cycle (no N bite) the outer level ends at level m with one of three endings. In each, cap(F s) = c + m - 1 (one bit is dropped), so d' = n' - 2^(c+m):

Here b0 is bit 0 of u. B0c cannot end an outer K cycle: it needs u = 0, so c + m = 1, but q_b = 0 needs m ≥ 2 (next item).

• m = 1. E1 gives d' = d + e + b0 ≥ d ≥ 2. E2 gives d' = d + 1 + e ≥ 3. E0 would need q_b = Q_1 = E_0 - 3 + e = 0 (q = 0 comes only right after a 3-round at q = 3, P3), which is impossible since E_0 ≥ 4.
• m ≥ 2. Level m is reached with Q_m = E_(m-1) - 3 ≥ q_b, so

n = E_0 + 2v >= q_b + 4 - m + e + 2^(c+m+1) - 2^(c+2) + 2v

Substituting into the table gives

d' >= X_m + 2e + 2v + [b0 in E1] + [2 in E2],     X_m = 2^(c+m) - 2^(c+2) - 2m + 6

X_2 = 2. For m ≥ 3, X_m ≥ 4(2^(m-2) - 1) - 2m + 6 = 2^m - 2m + 2 ≥ 4. So d' ≥ 2.

• Equality d' = 2 needs m = 2, e = v = 0 (and b0 = 0 in E1) with Q_2 = q_b. The E1 case is s = (2^(c+2)+3, 3c+3, 0) with F(s) = T_(c+1). This s has M(s) = 0, so it is not in I (its successor halts). The E0 case is s = (2^(c+2)+2, 3c+3, 0) with F(s) = (2^(c+2)+2, 3c+6, 2^(c+1)-2), which is in K and not in H*.

w ≡ 1, v ≥ 1 (cap c = L+1). Use (EQ1) with s~ = (n-1, w+2, 2v-1): w+2 ≡ 0, e = 0, cap c, v~ ≥ 1, d~ = d - 1.

• s and s~ have the same bite: their first rounds (R2 and R1) are not overflows and lead to the same configuration. So m and q_b are the same for both.
• E_0~ = n + 1 - 4v ≥ 2^(c+1) + 3 - 4(2^(c-1) - 1) = 7.
• E1, m = 1: d' = d - 1 + b0, with Q_1 = n - 4v - 2 odd. So n is odd, d is odd, d ≥ 3, and d' ≥ 2.
• E2, m = 1: d' = d~ + 1 = d.
• E0, m = 1: it needs Q_1 = E_0~ - 3 = 0, impossible since E_0~ ≥ 7.
• m ≥ 2: d' ≥ X_m + 2v~ ≥ 4.

w ≡ 1, v = 0. Use (EQ2) with s' = (n-2, w+1, 2^(c-1)-1): w+1 ≡ 2, all set, cap c - 1, d(s') = d + 2^c - 2 ≥ 2. s' = T_(c-1) only when n = 2^c + 4, which with n ≥ 2^(c+1) + 2 means c = 1, s = (6,4,0). Otherwise d(F s) = d(F s') + 2 ≥ 4.

Check CH tests E_0 ≥ d+2, m ≥ 1, the bite zone (w ≡ 0, c+m bits), p_b, the n' and cap' formulas, E0 ⇒ m ≥ 2, and the stated d' bound, on every plain cycle of the window. For w ≡ 1 it tests E_0~ ≥ 7 and the shared bite of s and s~, and E_0' ≥ 4 with m(s) = m(s') + 1 (EQ2, below).

5.6 Lemma A1 (the bell at the first continuation)

A1. If the outer cycle from s ∈ K has an N bite, the first one is at R(p_c, 2, Z_c) with p_c ≥ 2^(L_c) - 3.

Proof. It happens at level m, with q_b = 2 and b0 = 1, so p_c = p_b = n - 3 - m + e and L_c = c + m.

• m = 1: p_c - 2^(c+1) + 3 = d - 1 + e ≥ 1.
• m ≥ 2: the bound on n above (with q_b = 2) gives p_c - 2^(c+m) + 3 ≥ X_m + 2e + 2v ≥ 2.
• w ≡ 1, v ≥ 1 (via s~; the configurations after the first round coincide, so p_c is the same): p_c = n - 4 - m. For m = 1 this is p_c - 2^(c+1) + 3 = d - 2 ≥ 0, tight at d = 2. For m ≥ 2 it is ≥ X_m + 2v~ ≥ 4.
• w ≡ 1, v = 0 (via s', which is in K and is not T_(c-1) unless s = (6,4,0); (6,4,0) has no N bite, it halts): p_c = p_c(s') + 2, with the same L_c. □

5.7 Lemmas Z' and Kp (inner levels), and Lemma K for continuation cycles

Kp. If t ∈ J, d(t) ≥ 2 and the level from t pops, then d(G t) ≥ 3.

Proof. t ∈ K, and t is neither T_c nor (6,4,0): both have even n and w ≢ 0, so they are not in J. Lemma K gives d(F t) ≥ 2, and G = F + 1. □

Z'. If t ∈ J, d(t) ≤ 1 and the level from t pops, then d(G t) ≥ 2 or cap(G t) ≤ cap(t) + 1.

Proof, w ≡ 0 or 2.

• With n ≤ 2^(c+1) + 1: E_1 = E_0 + 1 - e - 2^(c+2) ≤ 2^(c+1) + 2 - 2^(c+2) ≤ 0. So m ≤ 1.
• m = 0, w ≡ 2: n is odd, so q_b = 1 and B1 gives w' = w-1 ≡ 1 with all bits kept: cap' = c + 1.
• m = 0, w ≡ 0: there is no 3-round, so q_b ∈ {1, 2}. B1 or B2+B1 drop bit 0: cap' = c - 1.
• m = 1: E1, E2 or E0 at level 1 give cap' = c. B0c (u = 0, so c = 0) gives cap' = 1 = c + 1.
• An N bite at level m ≤ 1: L_c ≤ c + 1. With p_c in the level's own frame (p = 0 at the level start), the composite form is G t = (p_c + 2) + t_(k+2) (§3.4).
• If some t_i (2 ≤ i ≤ k+2) has d ≥ 2, then by Kp so does t_(k+2), and d(G t) ≥ p_c + 4 ≥ 2.
• Otherwise every t_i is zone-dominated. By Z' on each (shorter) inner level, cap(t_(k+2)) ≤ cap(t_2) + k = L_c - 1 ≤ c.

Proof, w ≡ 1 (n odd).

• v ≥ 1, n ≥ 5: (EQ1) gives t~ = (n-1, w+2, 2v-1) with w ≡ 0, cap c and d - 1 ≤ 0. Apply the w ≡ 0 case.
• v ≥ 1, n = 3: R2 goes to q = 0, then B0 (cap c - 1) or B0c (v = 1, cap c).
• v = 0, n ≥ 5: (EQ2) gives t' = (n-2, w+1, 2^(c-1)-1) ∈ J with cap c - 1. Z' or Kp for t' gives cap(G t) ≤ c, or d(G t) = d(G t') + 2 ≥ 4.
• v = 0, n = 3: O1 goes to q = 1, then B1 gives cap' = c. □

Lemma K, continuation case. Let s ∈ K \ {T_c, (6,4,0)} have an N bite and let its cycle end. By the composite form, d(F s) = p_c + 2 + d(t_(k+2)), with t_2, …, t_(k+2) ∈ J (Lemma J).

• If some t_i has d ≥ 2, Kp carries it to t_(k+2), and d(F s) ≥ p_c + 4 ≥ 4.
• Otherwise every t_i is zone-dominated. cap(t_2) = L_c - k - 1, and Z' gives cap(t_(k+2)) ≤ L_c - 1. With n(t_(k+2)) ≥ 3 and A1:

d(F s) >= (2^(L_c) - 3) + 2 + 3 - 2^(L_c) = 2.

w(F s) = w(t_(k+2)) ≥ 3, so F(s) ∈ K. The data minimum is d(F s) = 5 on continuation cycles.

Induction. Lemmas K (for K), Z' and Kp (for J) refer to runs that pop. Their proofs use the same lemmas for the inner levels of an N bite, and for the rest of the level after it. Each of these is a run that starts later, so it is shorter. §6 states Lemmas J, K, Z', Kp and M (for one level) as one bounded statement U(N) and proves it by strong induction on the number of steps N. The proofs above are its induction step.

5.8 Closure of I

Let s ∈ I. Then:

• s ∉ H: H ∩ K = {T_c, (6,4,0)}, and T_c has M = 0 while (6,4,0) is excluded from I.
• The cycle from s never halts (Lemma K).
• If it ends, F(s) ∈ K (Lemma K), and M(F s) = -M(s) ≠ 0 (Lemma M).
• F(s) ≠ (6,4,0), because (6,4,0) has no predecessor in K. Let m be the number of overflow rounds (O0, O1, O2) of the outer level before its first bite.

(NB) Every cycle from s ∈ K that ends has

n(F s) >= n - m     and     2^(m-1) <= n

• w ≡ 0, 2. By p_b (§4), a plain cycle has n(F s) ≥ p_b + 3 = n + 2 - q_b - m + e. With q_b = 1 (E1, n' = p_b + 3 + b0) this is ≥ n + 1 - m; E2 and E0 give n + 2 - m + e. After an N bite, n(F s) = p_c + 2 + n(t_(k+2)) ≥ p_b + 5 = n + 2 - m + e, since n(t_(k+2)) ≥ 3 (Lemma J). For the second half: m ≥ 1 (§5.5). If m ≥ 2, then level m - 1 overflowed, so E_(m-1) ≥ 3 and

n >= E_0 >= 2^(c+m+1) - 2^(c+2) + 4 - m + e >= 2^(m+1) - m >= 2^m

• w ≡ 1, v ≥ 1. By EQ1, F(s) = F(s~) with n(s~) = n - 1, and s and s~ have the same m (§5.5). The bounds above hold for s~: they use no K-membership, only m ≥ 1 (E_0~ ≥ 7) and that B0c does not end the cycle (it would need c + m = 1, but c ≥ 1). So n(F s) ≥ (n - 1) + 1 - m = n - m and 2^m ≤ n - 1 (or m = 1).
• w ≡ 1, v = 0. By EQ2, F(s) = F(s') + (2, 0, 0) with n(s') = n - 2, and m(s) = m(s') + 1 because O1 counts. s' has w ≡ 2 and E_0' ≥ 4, so m(s') ≥ 1. So n(F s) ≥ (n - 2) + 1 - (m - 1) + 2 = n + 2 - m, and 2^(m-1) ≤ n - 2 (or m - 1 = 1).

So n(F s) = 6 needs n ≤ 6 + m with 2^(m-1) ≤ n, which leaves n ≤ 10.

Check INV runs F on every s ∈ K with n ≤ 12 and w ≤ 30 (K needs c ≤ 2 there): none maps to (6,4,0). Check CH tests each part of NB (the chain bound for m ≥ 2, the plain and continuation n' bounds, and the w ≡ 1 reductions), and INV tests NB itself on every cycle of its windows.

So F(s) ∈ I.

6. Non-halting: induction on the number of steps

The argument is one strong induction on the number of TM steps. Lemma K's bound is used only for cycles that end within the steps considered. So termination of levels is never needed.

Runs. Let t = (n, w, v) with n ≥ 3. Let L be a left side and p0 ≥ 0, or p0 = -1 with L = 0^inf. Write run(L, p0, t) for the TM run from R_L(p0, n, enc(w, v)).

• Its pop is the first ending bite of its own level; ending bites of inner levels do not count. By (SL1) the pop is the tape R_L(-1, F(t) + (p0 + 1, 0, 0)).
• Write K' = K \ ({T_c : c ≥ 0} ∪ {(6,4,0)}).

The statement U(N). For every t ∈ J ∪ K' and every L, p0 as above: in its first N steps, run(L, p0, t) does not halt before its pop. If it pops within N steps, then

(U1)  t in J               ->  G(t) in J                                  (Lemma J)
(U2)  t in K'              ->  F(t) in K                                  (Lemma K)
(U3)  t in J, d(t) <= 1    ->  d(G t) >= 2  or  cap(G t) <= cap(t) + 1    (Lemma Z')
(U4)  M(F t) = -M(t)                                                       (Lemma M)

(U4) is Lemma M for one level: Q starts at M(t) - (p0 + 1) and ends at M(F t) + (p0 + 1), and the level negates it. Kp is a case of (U2). A t ∈ J with d(t) ≥ 2 lies in K', because J contains no T_c and not (6,4,0). So d(G t) = d(F t) + 1 ≥ 3.

U(N) holds for every N. Assume U(N') for all N' < N, and take t, L and p0.

1. First phase. By (SL1) it applies the rules of §3, with p shifted by p0 + 1. By (P1)–(P3) every configuration has a rule. t is not in H, since H ∩ J = ∅ and H* ∩ K = {T_c} ∪ {(6,4,0)}. So by (P4) the phase does not reach H, and every other rule is a finite run that does not halt.
2. A plain end. If the first bite is an ending bite (B1, B0, B0c), or B2 followed by B1, that ending bite is the pop. Then (U1)–(U4) are arithmetic on the first phase: (P5) as in Lemma J, the plain cases of §5.5, the plain cases of Z', and the per-rule tables of Lemma M.
3. An N bite. Otherwise the first bite is an N bite with k low set bits, at R_L(p_c, 2, Z_c). PUSH takes 14 + 3k ≥ 17 steps. Then come, one after the other: - the innermost level, one B1 bite, which leads to t_2 ∈ J; - level i = 2, …, k, which is run(L_i, 0, t_i); - the rest of the level, which is run(L, p_c + 2, t_(k+1)), from the tape where level k pops (SL3).

Each of them starts after at least 17 steps, so U(N') with N' < N applies to it for the steps that are left. - If one of them does not pop within the steps left, the run has neither halted nor popped within N steps. - Otherwise each t_(i+1) is in J, (U1)–(U4) hold for each t_i (i = 2, …, k+1), and the pop of the rest is the pop of the run. (U1)–(U4) then follow from the composite form (§3.4), A1, and the N-bite cases of Lemma J, Lemma K, Z' and Lemma M (the N row of §5.4 uses (U4) for the inner levels). 4. w ≡ 1. The cases of §5.5 and §5.7 for w ≡ 1 go through EQ1 and EQ2. - EQ1 changes only the first round. After it, the run is the same as the run from t~ after its first round, and steps 1–3 apply to it. - After the O1 of EQ2, the run is run(L, p0 + 2, t'), and U(N') applies to it for some N' < N.

Non-halting. Let s ∈ I. For every N, the run from R(-1, s) does not halt within N steps. By strong induction on N:

• By U(N), the cycle from s does not halt before it ends.
• If it ends within N steps, say after N_1 ≥ 1 steps, then F(s) ∈ I (§5.8, from (U2), (U4) and NB). The rest is the run from R(-1, F s) for N - N_1 < N steps. It does not halt, by the induction hypothesis.

By §7, the blank run reaches (6,5,0) ∈ I at step 327. So the machine never halts.

Why F0 is never read. F is entered only by E0. In every low-level rule except Ht, that E0 is followed by F1. Ht is the end of H, and H needs a phase start in H*.

7. Initial segment (exact)

c0 = 0^inf A> 0^inf  -->(4)   R(-1,0,11)   -->(13) R(-1,1,11)   -->(26) R(-1,2,1)    -->(55) R(-1,3,111)
                     -->(116) R(-1,3,111111) -->(175) R(-1,4,111111) -->(244) R(-1,4,11110111)
                     -->(327) R(-1,6,11111) = (6,5,0)

The numbers are absolute step counts at the left records. At (6,5,0): w = 5, cap = 0, d = 6 - 2 = 4, M = 6 - 4 = 2. So it is in I.

The earlier states are outside K: they have w ≤ 2, or d < 2, or n ≤ 2. They are run by direct simulation in init. Check Z confirms the 8 cycle starts and then I along 20,000 abstract cycles.

8. Conclusion

8.1 Non-halting

By §7, the run reaches (6,5,0) ∈ I at step 327. By §6 (strong induction on the number of steps), from a cycle start in I the run does not halt within N steps, for every N: each cycle does not halt before it ends, and each cycle that ends starts the next one in I (§5.8). So the machine never halts.

8.2 Why it is not a cryptid

The rules are counter arithmetic: decrement, refill, and bites that drop 1 to 3 low cells. The nested bites are the same rules on a sub-zone.

The chaotic level-up transients (zones eaten to 5–12 cells, nesting depth up to 24) never need exact tracking. They are inside I: the bound d ≥ 2 and the mod-3 class M ≠ 0 are all the proof uses.

9. Lemma plan for Rocq (template: W4-2)

Formalization route. §6 needs no termination. In busycoq, halts tm c is exists n, halts_in tm c n, and progress_nonhalt' in TM.v is itself a strong induction on n. Three routes:

1. Stack invariant with history. Run progress_nonhalt_cond over a stack invariant on macro boundaries. It must carry a partial derivation of the outer cycle (PartialLev s c), closed into a completed run at the cycle end, because Lemma K at a cycle end uses the whole cycle (A1, the chain t_2, …, t_(k+2)).
2. Termination. Prove that every level from J pops and every cycle from K ends. Then progress_nonhalt_cond runs over cycle starts in I with F directly, as in W4-2. No termination proof is known; the data has every cycle ending (3e7 cycles).
3. Bounded lemmas (recommended). Prove U(N) for every N by strong induction, exactly as in §6. In Rocq form, for all N, t ∈ J ∪ K', l and p0: either ~ halts_in tm (RL l p0 t) k for every k ≤ N (R0 t in place of RL l p0 t for the outer cycle), or the run reaches the pop tape of some t' + (p0 + 1, 0, 0) at a step m ≤ N, with (U1)–(U4) for (t, t'). The second case gives t' directly, so no abstract map F and no uniqueness of the pop are needed. TM.v's preceeds_halt and exceeds_halt split a run at an intermediate configuration. Then ~ halts tm c0 follows by a last strong induction over cycles, as in §6.

Route 3 needs neither termination nor history in an invariant. It is the recommended route.

10. Evidence (python3 -B check_proof.py [--seed S] [--quick | --full] [--only SECTIONS])

Self-contained: its own TM simulator and abstract model, no other scripts. Logs: work/check_proof_seed1.log (default), work/check_proof_quick_seed1.log and work/check_proof_quick_seed2.log (--quick), work/check_proof_full_seed1.log and work/check_proof_full_seed1_INV.log (--full, partial: T to CH and the first INV window, all PASS; the second INV window, the random states and Z did not finish). The number of named checks varies slightly by seed, because MAC.TM and ABS report one line per rule kind that the random sample meets.

Earlier, larger checks of the same lemmas with the stage scripts (notes.md, funded stage): H* on 1.2M states, J/Z'/Kp on 2.4M, 685,028 continuation cycles, Lemma K on 10.4M states of K, 200,000 random states up to w = 75, the closed-rule model against the direct run at all 4,197 cycle starts to 1e11 steps.

11. What is not proved

• Termination of levels and cycles is not proved and not used: §6 is a strong induction on the number of steps. Route 3 of §9 formalizes exactly that.
• The stack (§3.4) is a tape argument plus a TM check. Its formal version is the induction on depth in the Rocq plan.

12. Checkpoint B (Dennis)

Pending (non-blocking).

Review log

• 2026-10-13, informal_proof stage (this file, first version).
• The macro rules from notes.md were derived at tape level for the first time.
  • All five rounds are one lemma: W, PS^(q-3), then the zone arrival ZA in three cases by f mod 3 (the position of the first zero). The table split by w mod 3 is its counter form.
  • The bites B2, B1, B0 and B0c are PUSH/B1/arrival runs from the wall. The nested bite is PUSH k plus the level stack, and H is PUSH k plus the 9-step tail Ht.
• The stack and the shift law now have a tape argument: an ending bite reads exactly two cells left of its left part, 0 0, which for an inner level is its 001 block.
• Lemma K for plain cycles is written in full with the overflow chain E_m, the bite position p_b and the three endings. The w ≡ 1 cases go through the reductions EQ1 and EQ2, with a parity step (d odd) in E1, f = 1.
• Lemmas P, J, M, A1, Z', Kp and the continuation case of K are written out. Z' gets the small cases n = 3 for w ≡ 1, which the funded-stage sketch skipped.
• §6 separates safety from termination. Lemma J and the halting part of Lemma K hold at every configuration. Lemma K's bound is applied only to completed cycles. Termination is not claimed. This changes the Rocq plan (§9, open point).
• check_proof.py is new and self-contained (71–80 named checks, depending on which rule kinds the random sample meets). It found one error in itself and two in draft statements:
  • a halting-tail check that ran one step short;
  • the bound 2^f ≤ n in NB, which fails for w ≡ 1, v = 0 (O1 counts as an overflow); the proof now uses 2^(f-1) ≤ n and checks predecessors of (6,4,0) up to n = 12;
  • the B2 counter form for w ≡ 1 with bit 0 clear, first written as enc(w-2, v); it is enc(w-2, v/2). That case never occurs (Lemma P), so no lemma changed.
• Open: Checkpoint B; a skeptic pass by a second agent; the Rocq build (§9).
• 2026-10-13, skeptic round 1 (verdict: sound; five minor gaps). All five are fixed; no lemma changed.
• The round at p = -1 (§1, §2, §3.2, §3.4, §9). "The round holds for every L and every p ≥ -1" was false for p = -1 with a left context that does not end in 0: L C> 00 (10)^q Z goes to L 0101 C> 00 …, one cell short of R_L(1, ..).
  • Now every non-ending rule is stated for p ≥ 0 with any L. At p = -1 the rounds are stated only for the blank left side (more generally L = L' 0, giving R_L'(1, ..)).
  • R_L(-1, ..) is only the name of a pop tape. (SL1) takes p0 ≥ 0 with any L, or p0 = -1 with the blank left side. The proof never applied a rule at p = -1 to a nonblank left side.
  • The Rocq families (§9) have p : nat, a separate blank cycle start R0, and no rule lemma for a pop tape with an arbitrary left side.
  • New check MAC.round at p = -1: L 0101 C> 00 … for every L (450 runs, 195 with L ending in 1).
• NB (§5.8). The half 2^(m-1) ≤ n is now derived. For m ≥ 2 the overflow chain gives n ≥ E_0 ≥ 2^(c+m+1) - 2^(c+2) + 4 - m + e ≥ 2^m. For w ≡ 1, EQ1 keeps m and lowers n by 1, and EQ2 lowers m by 1 (O1 counts) and n by 2.
  • The other half is sharpened to n(F s) ≥ n - m, so a predecessor of (6,4,0) needs n ≤ 10 (the exhaustive check goes to 12).
  • New CH checks for each part of NB; INV checks the sharper bound.
• Formalization route (§6, §9). §6 is rewritten as one bounded statement U(N), which bundles Lemmas J, K, Z' and M, with Kp as a case. It is proved by strong induction on the number of steps, and non-halting is one more strong induction over cycles.
  • U(N) also carries Lemma M for one level as (U4), because the N row of Lemma M uses it for the inner levels.
  • This is the skeptic's third route. It needs neither termination nor history in an invariant, and §9 now recommends it (busycoq: halts is exists n, halts_in; preceeds_halt, exceeds_halt).
  • The Rocq form is a disjunction (no halt within N steps, or a pop within N steps with (U1)–(U4)), so no abstract map F and no uniqueness of the pop are needed.
• Notation (§1–§5). The bite level is now m, and f is only the first zero of a zone; generic levels are i. Lattice: cells j = w-1-3i, with bit b on the b-th smallest cell.
  • Z' now states its frame: G t = (p_c + 2) + t_(k+2) with p_c in the level's own frame (p = 0 at its start), which is F t + (1,0,0) in the cycle's frame. §3.4 states the own-frame composite form; new check INV CF-J.
• Small omissions. The §1 B2 row has the reparse, w ≥ 6 and the w ≡ 1, bit-0-set case. The zone 111 at q = 2 halts (H with k = 0) and never occurs (P1); the abstract model in check_proof.py now treats it as a gap.
  • §5.5 (w ≡ 1, v ≥ 1): s and s~ share the bite, and the E0 ending at m = 1 is impossible since E_0~ ≥ 7.
  • New ABS check of the bite-zone widths: ≥ 6 at q = 0, 2, ≥ 5 at a phase bite, ≥ 4 for the B1 after B2. The first draft of this check demanded ≥ 5 for every B1 and failed on B2 then B1 (width w - 2 = 4); (P3) already allowed that.
• Validation: check_proof.py default seed 1 81/81 PASS (107 s); quick seeds 1 and 2 80/80; --full seed 1 partial: sections T to CH 74/74 PASS (CH on 1,527,624 states of K, w ≤ 27) and the first INV window (w ≤ 24, n < 2^(cap+4): 610,121 states, 132,766 continuation cycles) PASS; the second INV window (w ≤ 14, n < 2^(cap+11)), the random large states and Z of --full were stopped unfinished after 35 min (the helpers overflow_count and outer_trace step R1 rounds one at a time).