1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (W4-2): never halts (informal proof)

• Machine: 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (740 list, line 224; on every list since 2024-06-14), viewer https://bbchallenge.org/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF
• Sheet: "Bell eats counter", no claim, no Discord thread. Written for the string itself (no mirror, no renaming). Its only undefined transition is E1.
• Template: verify/BECv5.v, Module TM1 (...1LA0RB) and Module TM2 (...1LA1LB). They differ from this machine only in F1. The right side R n m, the right step RIncs, the standard counter LC0 with its increments, and the standard overflow ROv carry over word for word (§8).
• Machine 349 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- is the tm' of Eqv_v3 TM518. That module's tm is this table mirrored (L↔R) and renamed F→A, A→B, B→C, C→D, D→E, E→F, then started in its A, which is this table's F. The same mathematics covers 349 (§7.3). Its Rocq proof needs a short reduction (flip, then renaming, then TM518.eqv) on top of this machine's lemmas (§8).
• Status: informal proof, complete. Finite claims (low-level rules, initial segment) are executed exactly. Parametric claims are derived by hand in §3–§4, and check_proof.py checks each one, exhaustively on small cases and on random large ones (§9). 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 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf. The left part w is a word read as two interleaved binary numbers (even cells E, odd cells O). The right part is BECv5's R n m. - Bounce. Each bounce applies one map phi to w and moves one 10 from the n-block to the m-block. - Overflow. At n = 0 the right side eats the low end of w (an overflow), and n is refilled from what it ate. - Counter. Most of the time w is a binary counter, alternating between two encodings: standard std and packed pk. - Halting. The machine can halt (and meets the one branch with no rule) only if an overflow finds the lowest 1 of phi(w) on an odd cell and the two cells above it are not 00. That can only happen while w is still dirty after the previous overflow.

The proof is an invariant I on the clean overflow states (typ, N, m). It consists of linear bounds on N in terms of m, chosen by the parities of N and m. Under I, every cycle is one of eleven macro rules (§3.4). None of them meets a halting overflow, and each maps I into itself (§4).

1. Rule table (busycoq comment-block style)

1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF          (only E1 is undefined)

words: w = ... c2 c1 c0 (offset 0 = the cell A reads); W(e,o): bit d of e at offset 2d, bit d of o at offset 2d+1
std(N) = W(N,0);   pk(N) = W(N-2^(P+1), 2^P) for 2^(P+1) <= N < 2^(P+2)
K(w,n,m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf   (= BECv5's  w <| R n m);   S(typ,N,m) = K(typ(N),0,m)
phi(w): last cell 0 -> 1;  else (e,e+1) := lowest pair of adjacent 0 cells: cell e+1 := 1, cells 0..e := 0

R1  K(w,n,m) --> K(phi(w), n-1, m+1)       n >= 1                                    steps L(w) + 10n+7
R2  K(w,0,m) --> K(x, m+1+u, 0)            phi(w) = x 1 0^(2u)                       steps L(w) + 2u+8
R3  K(w,0,m) --> K(x', 0, m+u+2)           phi(w) = x' 0 0 1 0^(2u+1)  (x'00 may be 0^inf)   L(w) + 2u+15
R4  K(w,0,m) --> halt (E1)                 phi(w) = x 1 1 0^(2u+1)
R5  K(w,0,m) --> nested scan, no rule      phi(w) = x 1 0 1 0^(2u+1)
    L(w) = 1 if c0 = 0, else 2e+3 with (e,e+1) as in phi

N+1 = (2k+1) 2^i,  b = m+1+i,  L = bitlen(k),  r = k - 2^(L-1),  tz = number of trailing 0 bits
S0  S(std,N,m) --> S(std, b, b)                k = 0
S1  S(std,N,m) --> S(pk, 2k+b, b)              k >= 1, and k = 2^(L-1) or 2k+b >= 2^(L+1)
S2  S(std,N,m) --> S(std, b+L+3, b+L+3)        k not a power of 2, 2k+b+1 = 2^(L+1)
S3  S(std,N,m) --> S(std, D+n, n)              k not a power of 2, k < 3*2^(L-2), 3*2^(L-1) < 2k+b+1 < 2^(L+1)
P0  S(pk,N,m)  --> S(std, b+1, b+1)            k = 0
P1  S(pk,N,m)  --> S(std, k+b, b)              k >= 1, k = 2^(L-1)
P2  S(pk,N,m)  --> S(std, 2r+b, b)             r >= 1, 2r+b >= 2^L
P3  S(pk,N,m)  --> S(std, b+L+1, b+L+1)        r >= 1, 2r+b+1 = 2^L
P4  S(pk,N,m)  --> S(pk, D+n, n)               1 <= r < 2^(L-2), 2^(L-1) < 2r+b+1 < 2^L
    S3/P4: v = 2k+b+1-3*2^(L-1) (S3) or 2r+b+1-2^(L-1) (P4); u = tz(v), h = L-2-u, g = v >> (u+1), n = b+1+u;
           D = 3*2^h if g = 0 (S3a/P4a);  D = 2^(h+1)+2g if g >= 1 and n >= 2^(h+1)-2g (S3b/P4b)
    each rule runs to the FIRST overflow state K(w',0,m') with w' clean and N' >= 1;  S2 and P0 pass through
    K(0^inf,0,M) = S(std,0,M) on the way (M = b+L+2 / b; not in I), and leave it by S0

invariant I(typ,N,m):   1 <= m <= N (pk: N >= 2), and
  N = m (mod 2):   std: 2N <= 3m+6 (N even), N <= 2m+3 (N odd);   pk: N <= 2m+3 (N even), 2N <= 5m+6 (N odd)
  N != m (mod 2):  N <= m+3
I(s) -> exactly one of S0..S3, P0..P4 applies to s, and I holds at its result

start: c0 -->(32) K(1,0,1) = S(std,1,1), which satisfies I

2. Notation and families

• Words. A word w is the finite nonzero part of the tape left of the head, plus the cell under it. It is written highest cell first and read as a number: bit d is the cell at offset d, offset 0 = the cell A reads. Even offsets are E-cells, odd offsets O-cells.
• W(e, o) is the word with bit d of e on E-cell 2d and bit d of o on O-cell 2d+1. Every word is W(e,o) for exactly one pair. Hi·W_h(c, o) means the high word Hi shifted up by 2h cells, above a low part of 2h cells holding c, o < 2^h.
• Counters.
• Standard: std(N) = W(N, 0). Its digits are 00 = 0 and 01 = 1, and this is BECv5's LC0 N = BinInc <[0;1] N.
• Packed: pk(N) = W(N - 2^(P+1), 2^P), for N ≥ 2 with 2^(P+1) ≤ N < 2^(P+2). The top two bits share one digit pair 1t, and the rest are std digits. For example, pk(6) = W(2, 2) = 1100 and pk(7) = 1101.
• The words std(N) and pk(N) are clean. Every other word is dirty.
• Configurations.
• K(w, n, m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf, for n, m ≥ 0. This is BECv5's w <| R n m with R n m = [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^m *> const 0.
• A clean overflow state S(typ, N, m) = K(typ(N), 0, m) is written (typ, N, m).
• Parameters of a state (typ, N, m):
• i = the number of trailing 1 bits of N, and k = N >> (i+1), so N + 1 = (2k+1)·2^i;
• b = m + 1 + i, L = bitlen(k), and for pk with k ≥ 1, r = k - 2^(L-1);
• tz(x) = the number of trailing 0 bits of x.

3. Rules

3.1 Low-level rules (finite runs and shift rules)

Notation: l <S r = state S reading the last cell of l; l S> r = state S reading the first cell of r. X is any right context, and Y = (10)^(m+2) 0^inf.

Left step L (= phi). For every word l and every right side r: - L0. l 0 <A r --> l 1 B> r (A0, 1 step). - L1. l 0 0 z <A r --> l 1 0^(|z|+1) B> r, in 2|z|+3 steps. Here z begins and ends with 1 and has no factor 00; l 0 0 may be 0^inf. - Proof. Every cell of z is read moving left, in state A or F. - A 1 is read by A1 = 1LF or F1 = 1LF, so the next state is F. - Every 0 of z has a 1 to its right, so F reads it. F0 = 1LA writes 1, and A then reads a 1 (no 00 in z), so the scan continues. - After |z| steps F reads the lower 0 of the pair: F0 writes 1. A reads the upper 0: A0 = 1RB writes 1. B1 = 0RB then clears the |z|+1 ones back to the boundary. - Every word with last cell 1 is l 0 0 z for exactly one such z. So L0/L1 compute phi. The runs use only A0, A1, F0, F1 and B1, and they never read right of the boundary.

Right step RS (n ≥ 1), l B> R n m --> l <A R (n-1) (m+1) in 10n+7 steps, for every l. Write R n m = 1 1 0 (10)^n 0 X with X = (10)^m 0^inf.

RS never moves left of the boundary cell. It reads F only as F0 (never F1), and E only once, on a 0 that B wrote earlier in the same step. This is exactly BECv5's RIncs: TM1 and TM2 run the same 10n+7 steps (check RS).

Overflow OV (n = 0). Let f = phi(w) = x 1 0^q, the result of the left step. - OV0. f B> 1 1 0 0 X --> f <C 1 0 1 0 X in 7 steps (B1 B1 B0 C0 D0 C0 D0). So the head is at f <C Y. - CD. 0 0 <C --> <C 1 0 (C0 D0), applied to the 0s of f. - OVe (q = 2u). x 1 0^(2u) <C Y --> x 1 <C (10)^u Y, then C1 gives x <A 1 (10)^(u+m+2) 0^inf = K(x, m+1+u, 0). Total q+8 steps after the left step. - OVo (q = 2u+1). x 1 0 0^(2u) <C Y --> x 1 0 <C (10)^u Y, then C0 and D1 give x <E 0 0 (10)^u Y (q+8 steps so far). Then E reads the last cell of x: - x ends in 1: E1, halt (step q+9). - x = x' 0 0 (or x = 0^inf): E0 A0 B0 C0 D0 C1 gives x' <A 1 1 0 0 (10)^(u+m+2) 0^inf = K(x', 0, m+u+2). Total q+14 steps. - x ends in 10: E0, then A1 enters an F-scan inside x. This case has no rule and is never reached.

3.2 Level-1 rules

• R1 = L then RS: K(w,n,m) --> K(phi(w), n-1, m+1) for n ≥ 1. Iterated: K(w,n,m) -->* K(phi^n(w), 0, m+n).
• R2 / R3 / R4 / R5 = L then OV, with the cases of §1.
• The step counts are those of the comment block. Check Z recomputes every overflow time of the direct run to step 9,998,414,763 from these formulas, exactly.

3.3 phi in E/O coordinates

Lemma SW. Let Hi be any word, h ≥ 1, 1 ≤ o < 2^h, P = tz(o), 0 ≤ c < 2^(P+1), and w = Hi·W_h(c, o). - (i) If c < 2^(P+1) - 1, then phi(w) = Hi·W_h(c+1, o). - (ii) If c = 2^(P+1) - 1 and o' := o + 2^P < 2^h, then phi(w) = Hi·W_h(0, o'). - Its lowest 1 is the O-cell 2g+1, g = tz(o'): a landing. - The two cells above it (offsets 2g+3, 2g+2) are (bit g+1 of o, 0) if g+1 < h, and the two lowest cells of Hi if g = h-1. - (iii) If c = 2^(P+1) - 1 and o + 2^P = 2^h, then phi(w) = phi(Hi·1)·0^(2h-1), where Hi·1 is Hi with one cell 1 appended below it.

Proof. The low part below offset 2P+1 has E-cells = the bits of c and O-cells = 0. No E-bit of c lies above P. - (i) Let d ≤ P be the lowest 0 bit of c. - If d = 0, the last cell is 0 and becomes 1. - If d ≥ 1, the cells 0..2d-2 alternate (E = 1, O = 0). So every pair of adjacent cells below 2d-1 contains a 1. - Cells 2d-1 (an O-cell below 2P+1, so 0) and 2d (bit d of c, 0) form the lowest 00 pair. phi sets cell 2d and clears 0..2d-1, which gives c+1. - (ii) and (iii) The counter is full: all E-cells ≤ 2P are 1. Let s ≥ 1 be the length of the run of 1 bits of o starting at bit P. - The O-cells 2P+1, …, 2P+2s-1 are 1, and the E-cells between them are 0 (bits of c above P). - So every pair of adjacent cells up to offset 2P+2s-1 contains a 1. - Case P+s < h. Cells 2P+2s (E, bit P+s of c, 0) and 2P+2s+1 (O, bit P+s of o, 0) are the lowest 00 pair. phi sets the O-cell 2(P+s)+1 and clears everything below, which gives o + 2^P with c = 0. The two cells above the landing are the E-cell 2g+2, which is 0, and the O-cell 2g+3, which is bit g+1 of o. When g = h-1 these two cells are the lowest two cells of Hi. - Case P+s = h. Cell 2h-1 is 1 and nothing below it is a 00 pair. So the lowest 00 pair of w is the lowest 00 pair of Hi·1, whose cell 0 is that 1. phi on w and phi on Hi·1 set the same cell, and w's cells 0..2h-2 are cleared. ∎

Sweep corollary. Under the hypotheses of SW, call T = 2o + c the T-count. Each phi adds 1 to T as long as T < 2^(h+1): (i) adds 1 to c, and (ii) changes (o, 2^(P+1)-1) to (o+2^P, 0). - The O-values met are the barriers o_0 = o < o_1 < … < 2^h, with o_(t+1) = o_t + 2^tz(o_t). Equivalently they are (o >> g << g) + 2^g for the 0 bits g of o with tz(o) < g < h, followed by 2^h. - For T+j < 2^(h+1), phi^j(w) = Hi·W_h(T+j-2o_t, o_t), where o_t is the largest barrier with 2·o_t ≤ T+j. - The landings are exactly T+j = 2·o_t (t ≥ 1), and at T+j = 2^(h+1) the word is phi(Hi·1)·0^(2h-1) (SW iii).

Increments. - INC-std: phi(std(N)) = std(N+1). With no O-bits, the proof of SW(i) applies to every digit. - INC-pk: phi(pk(N)) = pk(N+1) for N ≥ 2. This is SW with Hi = 0^inf, h = P+1, o = 2^P. Case (i) adds 1. Case (iii) occurs at N = 2^(P+2)-1 and gives phi('1')·0^(2P+1) = 100·0^(2P+1) = W(0, 2^(P+1)) = pk(2^(P+2)).

Orbit lemmas. Each comes from the sweep corollary with the high word shown. The constant words are phi(1) = 100, phi(11) = 1000, phi(1011) = 100000 and phi(111) = 10000.

In O3, the barrier 3·2^(L-2) is (k >> (L-2) << (L-2)) + 2^(L-2), for the 0 bit L-2, which lies above tz(k) because k is not a power of 2. The next barrier is 2^L. O4 is the same with r and the 0 bit L-2 of r.

3.4 Macro rules

Overflow words of clean counters. Let N+1 = (2k+1)2^i. - std. phi(std(N)) = std(N+1) has its lowest 1 at E-cell 2i. The cells above it are the bits of k, now on O-cells. So q = 2i and x = W(0, k). - pk, k = 0 (N = 2^i - 1, i ≥ 2). phi(pk(N)) = W(0, 2^(i-1)): q = 2i-1 and x = 0^inf, so R3 applies, with m + (q+3)/2 = b. - pk, k ≥ 1. phi(pk(N)) = pk(N+1) = W(N+1-2^(P+1), 2^P) has its lowest 1 at E-cell 2i (i ≤ P). The E-bits above it move to O-cells, and the top O-cell 2P+1 moves to E-cell 2(P-i). So q = 2i and x = W(2^(L-1), r) with L = P-i+1. For r = 0 this is std(k).

Then R2 gives K(x, b, 0), and R1^b gives K(phi^b(x), 0, b). If that word is not clean, the next overflow sees phi^(b+1)(x).

In S3 and P4, the E-bits of phi^(b+1)(x) above offset 2u move to O-cells and become g = v >> (u+1) < 2^h. The O-cells 2L-3 and 2L-1 (S3), or the O-cell 2L-3 and the E-cell 2L-2 (P4), move to E-cells 2h and 2h+2 (S3), or to E-cell 2h and O-cell 2h+1 (P4).

Where a macro rule ends. Each macro rule runs from S(typ, N, m) to the first overflow state K(w', 0, m') whose word w' is clean with N' ≥ 1. That state is the result column. The other overflow states met on the way are of two kinds. - Dirty: phi^b(x) in S2, S3, P3 and P4. - In S2 and S3 its O-part is a barrier o with 2^(L-1) < o < 2^L, so o is neither 0 nor a power of 2. - In P3 and P4 it has the E-bit L-1 (from Hi = 1) above an O-part 0 < o < 2^(L-1), which a pk word cannot have. - Empty: K(0^inf, 0, M) = S(std, 0, M), met only in S2 (M = b+L+2, after R3 with x empty) and P0 (M = b), once each. - It violates I0 (N = 0 < M), so it is never the end of a macro rule and never a state of the induction. - The step out of it is exactly S0 at (std, 0, M): R2 with q = 0 gives K(0^inf, M+1, 0), then R1^(M+1) gives (std, M+1, M+1). S0 has no hypothesis on m. - So S2 = (run to (std,0,M)) followed by S0, and the same holds for P0.

Check B confirms this: the abstract trace on every small state, the direct TM run (which passes exactly the overflow states of the abstract trace), one empty state with the stated M in S2 and P0 only, and S0 from it.

The overflows inside a macro rule. Each one is of one of these kinds: - a clean counter (q even, or q odd with x = 0^inf, the all-ones pk); - O3's top word 1 0^(2L+1) (R3 with x = 0^inf); - std(2^L) in P3 (q even); - a final-gap word with v ≥ 1 (q = 2u even); - K(0^inf, 0, M) (q = 0).

So R4 and R5 never occur inside a macro rule. The landings of the gen-2 orbits O5/O6 (the last possible one, at T = 2^h, has 01 or 11 above it) all come before j0 ≤ n. They happen during bounces, where R1 applies to any word, so they do no harm.

4. Invariant, coverage, closure

4.1 The invariant

For a clean state (typ, N, m): - I0: 1 ≤ m ≤ N (pk: N ≥ 2). - Class P (N ≡ m mod 2). With D = N - m (even), the bounds are:

• Class X (N ≢ m mod 2): N ≤ m+3, i.e. D ≤ 3 (D odd, so D ∈ {1, 3}).

In class P, N even ⇔ m even ⇔ i = 0. The weakest bound in every class is 2N ≤ 5m+6. The strongest P bound is 2D ≤ m+6, so D even with 2D ≤ m'+6 satisfies all four P bounds at once.

4.2 Lemma S (coverage): if I(s), exactly one macro rule applies to s

The preconditions are mutually exclusive by construction (k = 0 / k a power of 2 / k not, and the position of T). It remains to show that a state with I never falls outside them: it is never dirty outside the final gap, and the gen-2 merge comes in time.

std, k not a power of 2 (so k ≥ 3, L ≥ 2, k ≥ 2^(L-1)+1). T = 2k+b+1. T > 2^(L+1) gives S1 and T = 2^(L+1) gives S2. Suppose T < 2^(L+1); then b < 2^(L+1) - 1 - 2k ≤ 2^L - 3. - i ≥ 1 is impossible: N+1 = (2k+1)2^i ≥ 2(2^L+3), so N ≥ 2^(L+1)+5, and I gives N ≤ 2m+3 (std, N odd, either class). So m ≥ 2^L+1 and b ≥ m+2 > 2^L - 3. - i = 0 in class X is impossible: N = 2k ≤ m+3 gives b = m+1 ≥ 2k-2, so T ≥ 4k-1 > 2^(L+1). - i = 0 in class P (m even): 4k ≤ 3m+6, so 3T = 6k+3m+6 ≥ 10k. - T ≤ 2^(L+1)-1 gives k < 0.6·2^L < 3·2^(L-2), so bit L-2 of k is 0. - T ≥ 10k/3 > 3·2^(L-1). - So S3's range holds. - T = 2k+m+2 is even, so v is even and u ≥ 1. - 3m ≥ 4k-6 ≥ 2^(L+1)-2 gives n = m+2+u > 2^(L-1) ≥ 2^(h+1) ≥ j0, so in case g ≥ 1 the S3b condition holds.

pk, k not a power of 2 (r ≥ 1, L ≥ 2). T = 2r+b+1. T > 2^L gives P2 and T = 2^L gives P3. Suppose T < 2^L, so b ≤ 2^L - 4. Also N+1 = (2k+1)2^i with 2k+1 ≥ 2^L+3. - i ≥ 2 is impossible: N ≥ 4·2^L + 11, and the weakest bound 2N ≤ 5m+6 gives m > 2^L, so b > 2^L. - Class X is impossible. - i = 1: N ≥ 2^(L+1)+5 and N ≤ m+3 give m > 2^L, so b > 2^L. - i = 0: N = 2k ≤ m+3 gives T ≥ 2r+2k-1 = 2^L+4r-1 > 2^L. - i = 0, class P (m, N even): N ≤ 2m+3 means 2k ≤ 2m+2, so m ≥ k-1. - Then T = 2r+m+2 ≥ 3r + 2^(L-1) + 1 > 2^(L-1). - T < 2^L gives 3r < 2^(L-1), so r < 2^(L-2), and L ≥ 3 follows. - T is even, so u ≥ 1. - n = m+2+u ≥ k+1 > 2^(L-1) ≥ j0. - i = 1, class P (m odd, N = 4k+1): 2N ≤ 5m+6 gives 5m ≥ 8k-4. Then 5T = 10r+5m+15 ≥ 18r + 4·2^L + 11. - T < 2^L gives 18r < 2^L - 11, so r < 2^(L-2). - T ≥ (4·2^L+11)/5 > 2^(L-1). - T = 2r+m+3 is even, so u ≥ 1. - n = m+3+u ≥ (8k-4)/5 + 3 > 2^(L-1) ≥ j0.

So under I the dirty cases are exactly: std with i = 0 in class P (S3), and pk with i ≤ 1 in class P (P4). Each is in its final gap (past every landing of its gen-1 orbit) with u ≥ 1, and its gen-2 orbit merges before the next overflow.

4.3 Lemma C (closure): if I(s) and s → s' by a macro rule, then I(s')

Each result has the form N' = m' + D with D ≥ 0 and m' ≥ 1, so I0 holds (for pk, N' ≥ 2). It remains to bound D.

• S0, S2, P0, P3: D = 0.
• S1: D = 2k, class P, m' = b, and the result is pk. We need D ≤ b+3 (b even) or 2D ≤ 3b+6 (b odd).
• i = 0, class P (b odd): 4k ≤ 3m+6 = 3b+3.
• i = 0, class X (b even): 2k = N ≤ m+3 = b+2.
• i ≥ 1: N+1 ≥ 2(2k+1) gives 2k ≤ (N-1)/2 ≤ m+1 < b (I: N ≤ 2m+3 for std with N odd). Both bounds hold.
• P1: D = k = 2^(L-1), m' = b, and the result is std.
• k = 1: class X with D = 1.
• k ≥ 2: class P. We need 2k ≤ b+6 (b even) or k ≤ b+3 (b odd).
  • i = 0, class P: k ≤ m+1 and b = m+1 is odd.
  • i = 0, class X: 2k ≤ m+3 and b = m+1 is even.
  • i ≥ 1, class P (m odd, so b = m+1+i ≡ i mod 2), using 2N ≤ 5m+6:
  • i odd: k ≤ (N-1)/4 ≤ (5m+4)/8 ≤ b+3;
  • i even ≥ 2: 2k ≤ (N-3)/4 ≤ 5m/8 ≤ b+6.
  • i ≥ 1, class X: 2k ≤ (N-1)/2 ≤ (m+2)/2.
• P2: D = 2r < k (since r < 2^(L-1) ≤ k-r), class P, m' = b, and the result is std. We need 4r ≤ b+6 (b even) or 2r ≤ b+3 (b odd).
• i = 0, class P (b odd): 2r < k ≤ m+1 = b.
• i = 0, class X (b even): 4r < 2k ≤ m+3 = b+2.
• i odd, class P (b odd): 2r < k ≤ (5m+4)/8.
• i even ≥ 2, class P (b even): 4r < 2k ≤ 5m/8.
• i ≥ 1, class X: 4r < 2k ≤ (m+2)/2.
• S3, P4: D = 3·2^h (g = 0) or 2^(h+1)+2g ≤ 2^(h+2)-2 (g ≥ 1), so D < 2^(h+2) = 2^(L-u). Here m' = n > 2^(L-1) (Lemma S) and n ≡ u (mod 2): n = m+2+u with m even, or n = m+3+u with m odd.
• h = 0: then g = 0 and D = 3, class X.
• h ≥ 1: D is even, class P.
  • u odd (n odd): D < 2^(L-1) < n, which gives D ≤ n+3 and 2D ≤ 3n+6.
  • u even ≥ 2 (n even): D < 2^(L-2), so 2D < 2^(L-1) < n, which gives 2D ≤ n+6 and D ≤ n+3.

5. Progress and halting

• Progress. Every macro rule contains at least one overflow and at least one bounce, so it takes at least 9 steps. Also m' ≥ m+1 in every rule (check INV.progress).
• Halting. The only undefined transition is E1. E is entered only by D1, in two places:
• in RS, where E reads a cell that B has just written 0;
• in OVo, where E reads the last cell of x.
• Inside the macro rules, OVo occurs only with x = 0^inf (the resets in S2 and P0), where E reads 0. The left step L never enters E. So under I, E1 is never executed.

6. Initial segment (exact)

c0 = 0^inf A> 0^inf (the head reading 0) runs 32 steps:

(std, 1, 1) satisfies I: 1 ≤ 1 ≤ 1, class P, N odd, and N ≤ 2m+3 = 5. In Rocq this is init: c0 -->* S (std,1,1) by esx, as TM1/TM2 do with S (6,6).

From there the macro rules give (std,1,1) →S0 (std,3,3) →S0 (std,6,6) →S1 (pk,13,7) →P2 (std,11,9) →S1 (pk,14,12) → … The orbit of all overflow configurations given by R1–R3 (including the dirty and empty-x ones) equals the 1,003 overflow configurations of the stored direct C run to 1e10 steps, word for word and step for step (check Z). The clean subsequence equals the macro-rule orbit, and 40 fresh direct-TM macro steps chained from (std,1,1) agree. Along the blank-tape orbit, I holds for the 500,000 cycles checked by default (2,000,000 with --full). Earlier stages checked 17,000,000 cycles.

7. Conclusion

7.1 Non-halting

• The run reaches S(std,1,1), and I holds there (§6).
• If I(s), exactly one macro rule takes s →+ s' (Lemma S, §3.4), and I(s') holds (Lemma C).
• Every macro rule is a finite chain of the exact rules L, RS and OV, and none of them executes E1 (§5).

The induction runs over the clean overflow states with N ≥ 1 that satisfy I. The step from s to s' is one whole macro rule, which ends at the first clean overflow state with N ≥ 1 after s (§3.4, "Where a macro rule ends"). The state (std, 0, M) that S2 and P0 pass through is outside I, and the induction never stops there. By induction the machine runs forever. In busycoq terms this is progress_nonhalt_cond with P := I on states (typ, N, m), after multistep_nonhalt with the 32-step init.

7.2 Why it is not a cryptid

The branch taken in each cycle depends on bit patterns of N (i, k, the gap position of T), which look pseudo-random. But I is closed under every branch. Lemma C uses only linear bounds and two parity facts: N ≡ m in class P, and T even at the dirty overflows. Halting is excluded by inequalities, not by residues. Ground rule 6 does not apply.

7.3 Machine 349

• What Eqv_v3 says. In verify/Eqv_v3.v, Module TM518 has tm = 1RB1RA_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---, tm' = 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (349, on the 740 list), and eqv: halts tm c0 <-> halts tm' c0.
• TM518 tm is this table mirrored and renamed. Swap L and R in every transition, and rename this table's states F→A, A→B, B→C, C→D, D→E, E→F. The result is TM518 tm, character for character. Its start state A is this table's F.
• So flip tm (directions swapped back) is this table with renamed states. Its state q behaves like this table's state f(q), where f = (A↦F, B↦A, C↦B, D↦C, E↦D, F↦E). This is busycoq's Perm (flip tm) W42 f.
• The run of TM518 tm from the blank tape is the mirror image of this table's run from 0^inf F> 0^inf: the same cells, the head at minus the position, and the state renamed.
• Check F verifies the string identity, the Perm transition by transition, the Eqv_v3 strings, and a lockstep run of both machines (200,000 steps by default, 1,000,000 with --full).
• The run from F.
• From 0^inf F> 0^inf (F reading 0), the transitions F0 A0 B1 B0 C0 D0 C0 D1 E0 A0 B0 C0 D0 C1 reach K(0^inf, 0, 1) in 14 steps.
• K(0^inf, 0, 1) is the clean state (std, 0, 1). As in S2 and P0, it is outside I (N < m), and S0 (no precondition on m) takes it to (std, 2, 2) at step 73. That state satisfies I.
• Then (std,2,2) →S1 (pk,5,3) →P1 (std,6,5) → …, and the induction of §7.1 applies from (std,2,2) (check F).
• What carries over, and what does not. The mathematics carries over unchanged. The Rocq proof does not carry over by itself: nonhalt for this machine is about c0, which starts in A, while 349 needs this table started in F and seen through a mirror and a renaming. §8 gives the reduction. It reuses this machine's lemmas and adds only an initial segment of 73 steps from F.

8. Lemma plan for Rocq (template: BECv5 TM1/TM2)

Shared shape, as in TM1/TM2: - Notation "l <| r" := (l <{{A}} [] *> r) and "l |> r" := (l <* [] {{B}}> r); - R n m; hL := (A,[]), hR := (B,[]); tm' := flip tm; - the state S '(t,a,b) := word t a <| R 0 b; - BigStep lemmas, init by esx, and nonhalt by multistep_nonhalt + progress_nonhalt_cond.

Risks. - The general OV and SW lemmas need care with <[...] list orientation (rocq-notes: left lists read reversed). - 349: the TM518 module of Eqv_v3 runs solve_eqv with a CTL/NG certificate. Copying it may cost compile time or memory; time it alone before you rely on it. Fallback: Require a compiled Eqv_v3. - The arithmetic of Lemma S/C has many cases. Split it into one lemma per rule, each with lia after stating the rule's bounds in terms of 2^L, 2^h, k, r and m. - No CTL/NG parameter searches are involved. The NG parameters of TM518.eqv are given in Eqv_v3.

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

Every claim above has a named check. The results are in work/check_proof_seed1.log (default), work/check_proof_seed2.log (default, seed 2) and work/check_proof_full_seed1.log (--full).

10. Checkpoint B (Dennis)

Pending (non-blocking).

Review log

• 2026-10-11, funded stage hunt. First draft: rules, the closed-form step B (17 cases), the invariant I, Lemma S, Lemma C and a check list. That draft is kept as work/proof_draft_hunt_2026-10-11.md. Its checks were exhaustive to m = 1300 and on 5.2M random states. The hunt's checks caught two errors before the draft: a wrong closed form (pk gen-1 R reset, outside I) and a wrong lemma ("pk odd is never dirty"; pk i = 1 is).
• 2026-10-11, informal_proof stage (this revision).
• Rewritten as a complete proof.
  • The full rule table is in comment-block form (§1).
  • The low-level rules are exact TM runs with step counts: L0/L1 with a proof, RS as an 8-row chain, OV with all branches (§3.1).
  • The landing claims are now one general lemma, SW, with a proof, a sweep corollary and four orbit lemmas O3–O6 (§3.3). They replace the stated-not-derived "gen 1 / gen 2 landing lemmas" of the draft.
  • The 17-case step B is cut to the 11 macro rules that can occur under I, each with an exact precondition, including the gen-2 merge condition (§3.4). Gen-1 N/H/R landings and gen-2 "merge at overflow" are not rules. Lemma S shows they never occur under I.
• Lemma S and Lemma C were redone in terms of the rules. Every inequality step is a separate check.
• check_proof.py is new and self-contained, with its own simulator and none of the hunt scripts. It found four bugs in itself and none in the proof:
  • two off-by-one padding comparisons;
  • an O4 check that ran on r = 0;
  • an all-ones reset check that expected i+2 for i+1 (the proof text had i+1 right).

• A self-review pass over this text, done before the final check runs, fixed four slips:

  • §6 listed the start-F orbit as the blank-tape orbit; it now reads (std,1,1) → (std,3,3) → (std,6,6) → (pk,13,7) → …;
  • Lemma C, P1: the parity was given as b ≡ i+1; it is b ≡ i (m odd), and the case split was already right;
  • S1 now states k ≥ 1;
  • the RS remark on E: E reads a 0 that B wrote, not one that D1 wrote.

  None of these changes a rule or a bound that the checks test. - Corrections to earlier notes: - 349's (std,2,2) is reached at step 73, not 63 as a first count here said; - the direct-run file has 1,003 overflow rows (notes said 1,002). - Open: Checkpoint B; a skeptic pass by a second agent; formalization (§8). - 2026-10-11, skeptic round 1 (verdict: sound; two minor gaps), with this revision. - Gap 1: 349 is a mirror, not just a different start. - The text said Eqv_v3 TM518 tm is "this table started in F". In fact it is this table mirrored (L↔R), renamed F→A, A→B, …, E→F, and started in its A. That is confirmed from the strings, and check F now runs the two machines in lockstep. - Fixed in the header, §0, §7.3 and §8. §8 now has a 349 row. The skeptic proposed mirroring every side lemma; that is kept as the fallback. The main route follows Skelet15.v: TM518.eqv, then flip_halts_c0, then perm_nonhalt with the renaming, then 73 steps from F by execute, then an exported nonhalt_I. A risk line covers the cost of TM518's solve_eqv. - New checks: F.TM518_eq_mirror_rename_of_table, F.Eqv_v3_TM518_strings_and_eqv, F.349_and_table_on_740_list, F.Perm_flip_TM518_to_table, F.TM518_lockstep_mirror_of_startF. - Gap 2: where a macro step ends. - Added "Where a macro rule ends" (§3.4), a line in the §1 block, the induction statement in §7.1, and the BigStep note in §8. Each rule ends at the first clean overflow state with N ≥ 1. (std,0,M) is an intermediate state of S2 and P0 only; it lies outside I and S0 leaves it. - The checks already stopped there (the abstract executor and the direct runner skip the empty word), so no rule or bound changed. - New checks: B.end_first_clean_N>=1_{abstract,TM}, B.overflow_states_TM_eq_abstract, B.empty_state_only_in_S2_P0_{abstract,TM}, B.S2_P0_pass_(std,0,M)once{abstract,TM}, B.S2_P0_(std,0,M)not_I_then_S0{abstract,TM}. - Teeth. The new F checks fail when this table is started in A instead of F, or when the renaming swaps two states (a scratch mutation run). - Results. 147/147 PASS with seed 1 --full (39 s; lockstep 1,000,000 steps; 25,656 abstract and 330 direct-TM endpoint checks), seed 1 default, and seed 2 default. - Re-check. Both gaps were re-read against the revised text and are closed. No fatal or major gap was raised. Status: CHECKPOINT_B. - Open. Checkpoint B (Dennis); formalization (§8), including a solo timing of TM518's solve_eqv for 349.