1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF: never halts

• Machine: 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF, viewer https://bbchallenge.org/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF. A BB(6) holdout on every holdout list since June 2024 (line 240 of the 778-machine list, line 224 of the 740-machine list), class "Bell eats counter". Written for the string itself (no mirror, no renaming). Its only undefined transition is E1.
• Template: verify/BECv5.v, Module TM1 (1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB) and Module TM2 (1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LB). They differ from this machine only in F1.
• There, F1 stops the leftward scan at the first 11 it reads. Here F1 = 1LF skips 1s, so the left step is the map phi of §0 on arbitrary words, the counter alternates between two encodings, and an overflow can leave the counter dirty for a while.
• Kept from the template: the right side R n m and the right step on it, the configuration shape w <| R n m, the standard counter (BECv5's LC0 N is std(N) here), and the architecture: one big-step lemma per macro rule, the start by esx, and progress_nonhalt_cond with an invariant.
• New: words in E/O coordinates with phi as an inductive relation, one sweep lemma for phi on them, the packed counter, eleven macro rules in place of TM1's one and TM2's two, and the invariant I with its coverage and closure arithmetic (§8).
• Status: formalized. The accompanying 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v (1,217 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c), importing only Individual62 from busycoq. Print Assumptions nonhalt: Closed under the global context. It compiles in about 66 s with -native-compiler yes, and coqchk re-checks it in about 30 s.
• Where each section lives in the .v (every lemma is top level; §8 has the full table):
• §1: tm (top of the file) and the rule-table comment at the end;
• §2: bt, wd, WS (the word W(e,o)), R, K, pkE/pkO (the packed counter), St;
• §3.1: PA/PF (the left step), TA0–TA2, TF0–TF3, TB, phi_spec, RS, OVe, OVo, OV_even, OV_odd;
• §3.2: bounces, bounces0, OVB;
• §3.3: INC_std(s), Gap(s), F_inc, F_carry, Sweep, INC_pk(s), O3_merge;
• §3.4: std_ov, pk_ov, pk_ov_full, OVoS0, S3_pre, P4_pre, and BS_S0, BS_S1a, BS_S1b, BS_S2, BS_S3a, BS_S3b, BS_P0, BS_P1, BS_P2, BS_P3, BS_P4a, BS_P4b;
• §4: I, I_std, I_pk (4.1); Nfacts, log2_facts, split_v, Cov_S3, Cov_P4 and the case split of step_std/step_pk (4.2); close_diag, close_std, close_pk, C_S1, C_P1, C_P2 (4.3);
• §6: init0; §7.1: step_I, nonhalt.

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. Since TM1 and TM2 differ from this machine only in F1, they run the same 10n+7 steps: this is BECv5's RIncs.

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. From these formulas every overflow time of a direct simulation from the blank tape comes out exactly, to step 9,998,414,763 (§9).

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.

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.
• 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 the .v this is init0 : c0 -->* K 1 0 0 1, by esx, as TM1/TM2 reach their first state.

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 a direct simulation to 1e10 steps, word for word and step for step, and I holds at every clean overflow state of the blank-tape orbit that was computed (§9).

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 start.

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, and no step of the argument relies on statistical behaviour.

7.3 Remark: machine 349 (not formalized here)

• 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--- (a holdout: line 349 of the 740-machine list, line 371 of the 778-machine list; called 349 below), 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). With tm this machine's table, this is busycoq's Perm (flip TM518.tm) tm 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.
• 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).
• What carries over. The mathematics carries over unchanged. The accompanying .v proves only ~halts tm c0 for this machine's own string. A formal proof for 349 would chain TM518.eqv, flip_halts_c0 (Flip.v), perm_nonhalt (Permute.v) with the renaming f, a 73-step start from F, and this file's step_I restated as forall s, I s -> ~halts tm (St s), the pattern busycoq's verify/Skelet15.v uses.

8. Mapping to busycoq

Template: BECv5 TM1/TM2. Same right side R n m, same configuration shape w <| R n m (here K e o n m := WS e o <{{A}} R n m, i.e. K(W(e,o), n, m)), the same right-step run (TM1/TM2's RIncs, here the one lemma RS), the standard counter (LC0 N is WS N 0), and the same top-level shape: big-step lemmas per rule, a start by esx, then multistep_nonhalt and progress_nonhalt_cond. The template's left-side lemmas (LIncs, LIncs', ROv) are stated on its digit lists. Here the left side is an arbitrary word after an overflow, so they are replaced by arithmetic on the pair (e, o): the relations PA/PF and the lemma Sweep.

How the .v is organized. The .v writes l for L-1 (so 2^l ≤ k < 2^(l+1)), true/false for pk/std, and states as St (typ, N, m), with St (false,N,m) = K N 0 0 m and St (true,N,m) = K (pkE N) (pkO N) 0 m.

9. Numerical sanity checks

These are evidence only; the result rests on the .v file alone. Each claim of §3–§6 was also tested numerically: finite claims on every small case, parametric claims on random large ones.

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