1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (W5-1): never halts (informal proof)

• Machine: 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- (740 list, line 349; on every list since 2024-06-14), viewer https://bbchallenge.org/1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---
• Sheet: "Bell eats counter", class only (results.csv row 1038), no claim, no Discord thread. Its only undefined transition is F1.
• Written for: the table TP = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC, started in its state F. 349 is TP mirrored (L↔R) and renamed, and 349 from the blank tape is TP from 0^inf F> 0^inf seen in a mirror (Lemma M, §3.1). Mirroring and renaming do not change halting (busycoq flip_halts, perm_halts).
• Template: our kill W4-2 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (check_kill PASS 2026-10-11; machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/proof.md and .v). TP is W4-2's table with one cell changed: F1 = 1RC instead of 1LF.
• Not used: Eqv_v3.v Module TM518 pairs 349 with W4-2's mirror (eqv), but Eqv_v3.v imports BBinf, which reports/targeting.md rules out. This proof does not go through it.
• Status: informal proof, complete. The machine-level claims (one-digit lemmas, detour, right step, overflow, initial segment) are exact finite runs or shift rules. The arithmetic layer is W4-2's, word for word, and is written out in full here (§3.5–§4). check_proof.py checks every claim, exhaustively on small cases and on random large ones (§9). Not yet formalized as a kill. The whole lemma plan of §8 compiles as one plan-check file, and Print Assumptions nonhalt reports it closed under the global context (§8). That compile is not a check_kill run.
• AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

0. Summary

349 runs W4-2's counter in a mirror, started in W4-2's state F. One transition differs, and it only changes how long one kind of step takes.

• Conjugacy (Lemma M). 349 is TP mirrored and renamed by f = (A↦F, B↦A, C↦B, D↦C, E↦D, F↦E). So 349 never halts if TP never halts from 0^inf F> 0^inf.
• Detour (Lemma E). In TP, F1 = 1RC is followed by C1 = 1LA and A1 = 1LF whenever F has a 1 on its right. These three steps leave the tape, head and state exactly as W4-2's single F1 = 1LF does. TP enters F only by A1, which writes that 1, so the condition always holds.
• Rules. TP's left step therefore computes W4-2's map phi, with 2 extra steps per F1. The right step and the overflow never read F1, so they are W4-2's runs. Hence W4-2's level-1 rules R1–R5 hold on TP with new step counts, and everything above them carries over: the macro rules S0–S3 and P0–P4, the invariant I, Lemma S and Lemma C are statements about phi and integers.
• Start. From F the run reaches the clean state (std, 2, 2) at step 73, which satisfies I.

1. Rule table (busycoq comment-block style)

1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---        (349; only F1 is undefined)
  = TP mirrored (L<->R) and renamed by f: A->F, B->A, C->B, D->C, E->D, F->E   (349 state q behaves as TP state f q)
TP = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC   (W4-2 = ..._1LA1LF: only F1 differs; only E1 undefined)
349 from 0^inf A> 0^inf  =  mirror of TP from 0^inf F> 0^inf   (flip_halts + perm_halts)

TP below.  words: w = ... w_2 w_1 w_0, w_d = the cell at offset d (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;   S(typ,N,m) = K(typ(N),0,m)
   in 349's orientation: K'(w,n,m) = 0^inf (01)^m 0 (01)^(1+n) 1 B> w~ 0^inf   (w~ = w from offset 0, left to right)
phi(w): w_0 = 0 -> w_0 := 1;  else (e,e+1) := lowest pair of adjacent 0 cells: w_(e+1) := 1, w_0..w_e := 0

E   l 1 <F 1 r  -->(3)  l <F 1 1 r        F1 C1 A1  (W4-2: l 1 <F r -->(1) l <F 1 r);  TP enters F only by A1 (1LF)
L   0^inf w <A r  -->  0^inf phi(w) B> r     steps L_TP(w) = 1 if w_0 = 0, else 2e+3+2*p11(w)
    p11(w) = #{d : 1 <= d <= e-1, w_(d-1) = w_d = 1}  (one detour per adjacent 11 pair below the 00 pair)

R1  K(w,n,m) --> K(phi(w), n-1, m+1)       n >= 1                                    steps L_TP(w) + 10n+7
R2  K(w,0,m) --> K(x, m+1+u, 0)            phi(w) = x 1 0^(2u)                       steps L_TP(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_TP(w) + 2u+15
R4  K(w,0,m) --> halt (E1; 349: F1)        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)

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: 349 from c0 = 0^inf A> 0^inf -->(14) K'(0^inf,0,1) = S(std,0,1) -->(59, S0) S(std,2,2) at step 73, in I
       (TP: F;; tape0 -->(73) K(std 2,0,2); the first F1 is TP's 122nd transition)

2. Notation and families

This is W4-2's notation, repeated so this file can be read alone.

• Configurations in general. l <S r is state S reading the last cell of l; l S> r is state S reading the first cell of r. Cells are written left to right.
• 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, and offset 0 is 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. In Rocq this is WS e o.
• Hi·W_h(c, o) is 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).
• Packed: pk(N) = W(N - 2^(P+1), 2^P) for N ≥ 2 with 2^(P+1) ≤ N < 2^(P+2). For example pk(6) = 1100, pk(7) = 1101.
• std(N) and pk(N) are clean words; every other word is dirty.
• Configurations (TP). K(w, n, m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf for n, m ≥ 0. The right part is R n m of the .v. A clean overflow state S(typ, N, m) = K(typ(N), 0, m) is written (typ, N, m).
• The same configuration in 349. Mirror the tape and rename the state (TP's A is 349's B):

K'(w, n, m) = 0^inf (01)^m 0 (01)^(1+n) 1 B> w~ 0^inf

Here w~ is w written from offset 0 to the right. Every rule below holds for K' on 349 with the same step counts (check D). - Parameters of (typ, N, m): i = the number of trailing 1 bits of N, 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) is the number of trailing 0 bits of x.

3. Rules

3.1 Lemma M: 349 is TP in a mirror

Lemma M. Swap L and R in every transition of TP, and rename TP's states by f⁻¹ (F→A, A→B, B→C, C→D, D→E, E→F). The result is 349, character for character.

• So flip tm349 (349 with its directions swapped back) at state q is TP at state f(q), for every state and symbol, halting cells included. This is busycoq's Perm (flip tm349) TP f (Permute.v): tm (q,s) = None → tm' (f q, s) = None, and tm (q,s) = Some (s',d,q') → tm' (f q, s) = Some (s',d,f q').
• Consequence. flip_halts (Flip.v) gives halts tm349 c0 → halts (flip tm349) (A;; tape0), because the blank tape is its own mirror. Then perm_halts gives halts TP (f A;; tape0) = halts TP (F;; tape0).
• So it suffices to show that TP never halts from 0^inf F> 0^inf.

349's undefined cell F1 is TP's E1. Check T verifies the string identity and both Perm clauses cell by cell. Check Z runs 349 from blank and TP from F in lockstep (state renamed, head at minus the position, every cell mirrored) for 10^6 steps (--full: 5·10^6).

For comparison, Eqv_v3's TM518 tm is W4-2 mirrored and renamed by the same f, and 349 differs from it only in A1 (349: 1LD; TM518 tm: 1RA). That one cell is exactly TP's F1.

3.2 The left step on TP

Lemma E (detour). For every left side l and right side r, on TP:

l 1 <F 1 r   -->(3)   l <F 1 1 r          transitions F1 (1RC), C1 (1LA), A1 (1LF)

• Proof. F reads the 1 and F1 writes 1 and moves right, so C reads the cell right of F, which is 1. C1 writes 1 and moves left, so A reads F's cell, now 1. A1 writes 1 and moves left, so F reads the last cell of l.
• W4-2's F1 = 1LF does the same in one step: l 1 <F r --> l <F 1 r, and with r = 1 r' that is the right-hand side above.
• Why the 1 is always there. The only transition into F is A1 = 1LF (check T). It writes 1 and moves left, so right after F is entered the cell on its right is 1. F leaves F at once (F0 = 1LA, F1 = 1RC). So in every run, every time F reads a cell, the cell on its right holds 1, except for the very first read of a run started in F.
• 349's form, mirrored: x 1 A> 1 y --(A1 D1 B1)--> x 1 1 A> y.

The eight one-digit lemmas. These are the .v's TA0–TB. Here l and r are arbitrary, cells are written left to right, and a is 0 or 1.

• TA2 needs no side condition: E's 1 on the right is the cell A1 has just written.
• TF2' and TF3' need 1 as the first cell of the right side. Without it they are false on TP. For example, W4-2's TF2 with l = 1, r = 0 0^inf never reaches its right-hand side within 40 steps on TP (check TL).
• In W4-2's .v these are TF2 l r: [1;0] *> l <{{F}} r -->+ l <{{A}} [1;1] *> r and TF3. The restated versions put [1] *> r on the right of both sides.

The left step (phi_spec). The .v reads phi digit pair by digit pair through two relations, PA e o e' o' (A at an E-cell) and PF e o e' o' (F at an E-cell). Their constructors PA0–PA2 and PF0–PF3 are chosen by the parities of e and o. Read as functions they are PA(w) = phi(w) and PF(w) = phi(2w+1) >> 1 (check PS).

Lemma L. On TP, for all e, o and every right side r: - (PA) if PA e o e' o', then WS e o <A r -->+ WS e' o' B> r; - (PF) if PF e o e' o', then WS e o <F 1 r -->+ WS e' o' B> 1 r.

Proof. Mutual induction on the derivation, exactly as W4-2's phi_spec. Each case first rewrites the lowest digit pair, then:

• The PF hypothesis is only ever applied to a right side that starts with 1, which is what the restated (PF) clause demands.
• TF2' and TF3' are only used in PF cases, whose goal has 1 r on the right by the restated clause.
• The PA clause is unchanged. It is the only part the rest of the proof uses (PA_spec := proj1 phi_spec). ∎

Left step L. For every word w and every right side r, 0^inf w <A r --> 0^inf phi(w) B> r on TP. - L0 (w_0 = 0). A0 = 1RB writes 1 and moves right: l 0 <A r --> l 1 B> r in 1 step. - L1 (w_0 = 1). Let (e, e+1) be the lowest pair of adjacent 0 cells (the 0s above w count), so e ≥ 1. The cells at offsets 0..e-1 contain no 00, and w_(e-1) = 1, since otherwise (e-1, e) would be a lower pair.

Proof of L1. The head moves left through offsets 0, 1, …, e+1, reading each cell once (apart from the detours). We show by induction on d: when offset d (1 ≤ d ≤ e+1) is read, every cell at offsets 0..d-1 is now 1, and the state is F if w_(d-1) = 1 and A if w_(d-1) = 0.

• d = 1: A reads w_0 = 1. A1 = 1LF writes 1 and moves left, so F reads offset 1.
• F reads a 1 at offset d (1 ≤ d ≤ e-1). The cell on its right, offset d-1, is 1 by the induction hypothesis, so Lemma E applies: three steps (F1 C1 A1) later, offset d is 1 and F reads offset d+1.
• F reads a 0 at offset d ≤ e-1. F0 = 1LA writes 1, and A reads offset d+1. That cell is 1: d+1 ≤ e-1 (d+1 = e would make (d, e) a lower 00 pair), and w_d = 0 has no 0 next to it below offset e. A1 = 1LF writes 1, and F reads offset d+2.
• So A only ever reads a 1 inside offsets 1..e-1, and the claim holds up to d = e.
• At d = e, F reads the 0 (w_(e-1) = 1). F0 = 1LA writes 1, and A reads offset e+1, which is 0. A0 = 1RB writes 1 and moves right.
• B now meets the e+1 ones at offsets e, …, 0. B1 = 0RB clears each and moves right, ending at B> r.

The result has 1 at offset e+1 and 0 at offsets 0..e, which is phi(w). ∎

• Step count. W4-2's run of L1 takes e reads below offset e, then F0, A0 and e+1 B1 steps: 2e+3. On TP every F-read of a 1 costs 3 steps instead of 1. F reads offset d with value 1 exactly when w_(d-1) = w_d = 1 (1 ≤ d ≤ e-1). So L_TP(w) = 2e + 3 + 2·p11(w), where p11(w) counts the adjacent 11 pairs among offsets 0..e-1.
• Locality. The scan never reads right of offset 0: a detour from F at offset d ≥ 1 reads offset d-1 ≥ 0. The transitions used are A0, A1, F0, F1, C1 and B1.

Check LS runs every word up to 14 cells and 3,000 random words up to 90 cells. It confirms the result, the step count, the untouched right side, and that every F1 is followed by C1 reading 1 and then A1.

3.3 Right step and overflow on TP

These runs are W4-2's, cell for cell, because they never read F1 and TP differs from W4-2 only in F1.

• 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. The run is the chain below (W4-2's, every transition the same on TP).

RS never moves left of the boundary cell. It reads F only as F0 (in the shift 01 <A --> <A 11) and never reads F1. It reads E once, on a 0 that B wrote earlier in the same step, so it never executes E1. Check RS verifies every row of the chain on TP. - Overflow OV (n = 0). Let f = phi(w) = x 1 0^q, X = (10)^m 0^inf and Y = (10)^(m+2) 0^inf. - OV0: f B> 1 1 0 0 X --> f <C 1 0 1 0 X, 7 steps (B1 B1 B0 C0 D0 C0 D0). - CD: 0 0 <C --> <C 1 0 (C0 D0), applied to the 0s of f. - OVe (q = 2u): then C1 gives x <A 1 (10)^(u+m+2) 0^inf = K(x, m+1+u, 0), q+8 steps after the left step. - OVo (q = 2u+1): C0 and D1 give x <E 0 0 (10)^u Y, q+8 steps. Then E reads the last cell of x: - x ends in 1: E1, halt (TP E1 = 349 F1); - x = x' 0 0 or 0^inf: E0 A0 B0 C0 D0 C1 give K(x', 0, m+u+2), q+14 steps in all; - x ends in 10: E0, then A1 enters an F-scan inside x (no rule; never reached). - None of these enters F except the last, nested case. Check OV runs W4-2's OV checks on TP: every f up to 13 cells with m ≤ 3, plus 2,000 random cases. - In .v form these are RS, OVe and OVo of W4-2's file, unchanged (check V).

3.4 Level-1 rules

R1 = L then RS; R2–R5 = L then OV, with the cases of §1. The step counts are W4-2's with L replaced by L_TP.

Iterated: K(w, n, m) -->* K(phi^n(w), 0, m+n). Checks K (TP, every word up to 11 cells) and D (349 in K' form, every word up to 10 cells plus 2,000 random) run each case with its exact step count.

3.5 phi in E/O coordinates

These lemmas concern only the map phi, which is the same for TP and W4-2. The proofs below are W4-2's. In W4-2's .v they are lemmas about the relations PA/PAs (Gap, Gaps, F_inc, F_carry, Sweep, INC_std, INC_pk, the orbit lemmas inside BS_*), and none of them mentions the machine.

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.

Check M re-runs W4-2's checks of all of these: SW exhaustively for h ≤ 5 and every high word up to 6 cells, plus 30,000 random cases; O3–O6 exhaustively for small parameters and at random up to 60 bits.

3.6 Macro rules

Each macro rule is a finite chain of R1–R3 from a clean state S(typ, N, m) to the first later overflow state K(w', 0, m') whose word w' is clean with N' ≥ 1. The variables are those of §2, and for S3/P4 also v, u, h, g, n, D of §1.

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

Check M checks the overflow words for every N < 8,192, plus 5,000 random N.

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.

Check B compares each closed form with an abstract execution of R1–R4 (every clean state with m ≤ 90, N ≤ 3m+8, plus 2,000 constructed large states per rule) and with direct runs of both TP and 349 (30 per rule). The two direct runs agree with each other in step count and in every overflow state met. Check B also confirms where each rule ends: one empty state with the stated M, in S2 and P0 only, left by S0.

4. Invariant, coverage, closure

The induction runs over clean overflow states (typ, N, m) with N ≥ 1. §4 uses only the closed forms of §3.6, so it is the same as for W4-2, and the arguments below are W4-2's. In W4-2's .v it is I, Cov_S3, Cov_P4, C_S1, C_P1, C_P2, step_std, step_pk and step_I, none of which executes the machine (check V).

4.1 The invariant

• I0: 1 ≤ m ≤ N (pk: N ≥ 2).
• Class P (N ≡ m mod 2), with D = N - m:

• Class X (N ≢ m mod 2): N ≤ m+3.

In class P, N even ⇔ m even ⇔ i = 0. The weakest bound in every class is 2N ≤ 5m+6.

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.

Check M re-runs W4-2's INV checks under this seed: every state with I and m ≤ 700 (251,124 states; --full: m ≤ 1300, 856,374 states), plus 300,000 random boundary states up to m ≈ 2^60, with every inequality step of Lemma S and Lemma C as its own check.

5. Progress and halting

• Progress. Every macro rule contains an overflow and at least one bounce, so it takes at least 9 steps. Also m' ≥ m+1 in every rule (checks M and B).
• Halting. TP's only undefined transition is E1 (349: F1). 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 (in S2 and P0), where E reads 0.
• The left step never enters E: its transitions are A0, A1, F0, F1, C1 and B1, and a detour goes F1, C1, A1 and never through D.
• So under I, E1 is never executed.

6. Initial segment (exact)

349 starts in A on the blank tape, which is TP's F. The first 14 steps, in both alphabets:

349:  A0 B0 C1 C0 D0 E0 D0 E1 F0 B0 C0 D0 E0 D1
TP:   F0 A0 B1 B0 C0 D0 C0 D1 E0 A0 B0 C0 D0 C1

The rest is TP's run, cut into the rules of §3.2–§3.4:

• Steps 15–73 are the macro rule S0 at (std, 0, 1): k = 0, i = 0, b = 2, result (std, 2, 2). S0 has no hypothesis on m, so it applies although (std, 0, 1) is outside I.
• (std, 2, 2) satisfies I: 1 ≤ 2 ≤ 2, class P with N even, and 2N = 4 ≤ 3m+6 = 12.
• No F1 is read in these 73 steps. The first detour starts at transition 122 (after 121 steps), in 349's letters A1 D1 B1. So these 73 steps are also W4-2's run from F, since the two tables differ only in F1.
• In .v form: F;; tape0 -->* K 2 0 0 2, where K 2 0 0 2 = WS 2 0 <{{A}} R 0 2 = St (false, 2, 2). Fallback: 14 steps to K 0 0 0 1, then BS_S0 with i = 0, m = 1 (K (2^0-1) 0 0 1 -->+ K 2 0 0 2).

From there the macro rules give

(std,2,2) @73 -S1-> (pk,5,3) @174 -P1-> (std,6,5) @395 -S1-> (pk,12,6) @686 -P2-> (std,11,7) @1,055
  -S1-> (pk,12,10) @1,742 -P2-> (std,15,11) @2,535 -S0-> (std,16,16) @4,116 -S1-> (pk,33,17) @5,855 -> ...

with the step number of each overflow state after @. Check Z runs 349 directly from blank: its overflow configurations (all of them, clean, dirty and empty) equal the R1–R3 orbit from K(0^inf, 0, 1) at step 14, with the exact step number of each from the formulas of §3.4. That is 182 configurations to step 59,775,614 by default (--full: 306 to step 299,701,194). The clean ones equal the macro orbit from (std, 2, 2).

7. Conclusion

7.1 Non-halting

• 349 never halts from blank if TP never halts from 0^inf F> 0^inf (Lemma M).
• TP reaches S(std, 2, 2) at step 73, and I holds there (§6).
• If I(s), exactly one macro rule takes s →+ s' (Lemma S), and I(s') holds (Lemma C).
• Every macro rule is a finite chain of the exact rules of §3.2–§3.4, and none of them executes E1 (§5).

By induction TP runs forever from F. In busycoq terms: progress_nonhalt_cond with P := I on states (typ, N, m), after multistep_nonhalt with the 73-step start from F; then flip_halts and perm_halts for 349.

7.2 Why it is not a cryptid

The branch taken in each cycle depends on bit patterns of N, 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. The detour changes step counts only, never a branch. Ground rule 6 does not apply.

7.3 A remark: the run is W4-2's run, stretched

By §3.2 (Lemma E and "why the 1 is always there"), TP's run from F is W4-2's run from F with every F1 replaced by the three steps F1 C1 A1, and nothing else changed. Check Z confirms this in lockstep for 3·10^6 W4-2 steps (--full: 3·10^7 steps, 479 detours, TP steps = W4-2 steps + 2·479). The proof above does not use this remark: it re-proves the machine-level lemmas on TP directly, which is also what the .v does.

8. Lemma plan for Rocq (template: W4-2's .v, 1,217 lines)

W4-2's .v uses the machine in exactly twelve lemmas, the ones proved by execution: TA0, TA1, TA2, TF0, TF1, TF2, TF3, TB, RS, OVe, OVo and init0. Everything else is arithmetic over the PA/PF relations, or a composition of PA_spec, RS, OVe and OVo. Check V confirms this on the file itself: these are the only lemmas whose proofs contain an execution tactic, and tm occurs only in the two notations -->* and -->+. So the new file is W4-2's with these changes:

That is about 45 changed or added lines of code, plus comments. The file then has one top-level Definition tm (349's string), as check_kill requires.

The whole plan compiles. rocq/plan_check_full.v (written by rocq/mk_plan_check_full.py) is items 2–8 in one file: - the head of rocq/plan_check_phi.v up to PA_spec (items 2, 4, 5); - then W4-2's .v from PA_spec on, word for word, except that init0 is replaced by initF (item 6) and W4-2's nonhalt and closing comment by nonhalt_F, tm, f349, perm_349 and nonhalt (items 7, 8); - and a final Print Assumptions nonhalt.

It compiles against the pinned busycoq in vendor/ (coqc 8.20.1, -native-compiler no) in 65.5 s, and Print Assumptions nonhalt prints Closed under the global context (work/plan_check_full.log). The round-1 skeptic built the same file independently (byte-identical) and got the same result in 67 s. This is a plan check, not a check_kill run, so it is not a kill.

The reduction adds no assumptions. flip_halts and perm_halts do not use flip_involutive, the one lemma of Flip.v that uses functional extensionality. The closed Print Assumptions above confirms this.

Left for the kill file. Item 1 (the plan check still carries W4-2's header comment, which names W4-2's machine), item 9 (W4-2's closing comment block is dropped, and §1 of this file goes in its place), removing the trailing Print Assumptions line, naming the file after 349's string, and tools/check_kill.sh.

Risks. - Unification in phi_spec (resolved). After TA2, TF1 or TF3 the right side is [1;1] *> r (or [1;1] *> [1] *> r), and the hypothesis expects [1] *> ?r. The two are convertible, and apply accepts them once the instance is explicit: apply (H ([1] *> r)), apply (H ([1] *> [1] *> r)), apply (TB _ ([1] *> r)). rocq/plan_check_phi.v is W4-2's .v up to PA_spec with items 2, 4 and 5 applied; it compiles in 1.2 s. Its negative control rocq/plan_check_phi_neg_TF2.v (W4-2's unrestated TF2 on TP) fails at es, as §3.2 says it must. - Start from F (resolved). esx takes its fast path only from c0. solve_initF (#24's route, rocq-notes) proves initF in the plan check, with the proof of item 6. - Names. W4-2's file defines tm and nonhalt; both are renamed (items 2 and 7), so the new tm and nonhalt are the only ones.

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

The script imports W4-2's check_proof.py as a library for phi, the closed forms, I, the abstract executor and W4-2's arithmetic checks, and re-runs those under its own seed. Everything about TP and 349 is new. Results: work/check_proof_seed1.log and work/check_proof_seed2.log (default, 219/219 PASS, 44 s each) and work/check_proof_full_seed1.log (--full, 219/219 PASS, 77 s).

10. Checkpoint B (Dennis)

Pending (non-blocking). Skeptic round 1 found no fatal or major gap; its four minor gaps are fixed (review log).

Review log

• 2026-10-13, informal_proof stage (this revision). First version, written as a delta of W4-2's proof.md and .v.
• New mathematics: Lemma M (conjugacy, §3.1), Lemma E (detour) with the global "1 on F's right" argument, the eight one-digit lemmas with TP step counts, and Lemma L (phi_spec with the restated PF clause and the case table showing that the induction closes, §3.2). RS and OV are W4-2's runs because they never read F1 (§3.3). The level-1 rules have new step counts (§3.4).
• Carried over unchanged, restated in full: the phi lemmas (§3.5), the macro rules with every precondition (§3.6), I, Lemma S and Lemma C (§4). Their proofs are W4-2's and do not mention the machine. The .v counterparts are listed; check V verifies on the file that none of them executes the machine.
• Start: the 73-step segment from F, with the S0 run spelled out row by row (§6).
• check_proof.py is new. It reuses W4-2's checker as a library for the shared arithmetic and adds 14 sections on TP and 349. Bugs found in the script, none in the proof:
  • the teeth check for the unrestated TF2 first demanded that all 400 sampled contexts fail. A few of them (21 of 401 in a quick run; the blank context among them) meet an equal configuration later, because configurations are tapes up to translation. The check now asks for one counterexample (l = 1, r = 0 0^inf) and logs the count;
  • a harvested check name had a doubled B. prefix (cosmetic).
• A self-review pass before the final runs fixed five slips in the text, none of which changes a rule or a bound: SW (iii) now states c = 2^(P+1)-1; O3/O4 state their domains (k ≥ 1, 1 ≤ r < 2^(L-1)) and when the final gap exists; Lemma S's i ≥ 1 case shows the step m ≥ 2^L+1, and its S3 case the bound 3m ≥ 4k-6; the p11 definition no longer reuses c for a cell; the §6 table first showed a wrong word after step 23. Two checks were added for §6 and §3.2: every row of the §6 table, and "every F read after step 0 has a 1 on its right" along the lockstep run.
• Results: 204/204 PASS with seed 1 and seed 2 (default) and seed 1 --full.
• Rocq plan check (§8 Risks): W4-2's .v up to PA_spec with TP, TF2'/TF3' and the restated phi_spec compiles in 1.2 s (rocq/plan_check_phi.v); W4-2's unrestated TF2 on TP fails (rocq/plan_check_phi_neg_TF2.v). The tactic note is in atlas/rocq-notes.md.
• Open: Checkpoint B; a skeptic pass by a second agent; formalization (§8).
• 2026-10-13, skeptic round 1 (sound; 4 gaps, all minor; no fatal or major gap). All four fixed and re-checked.
• Plan compiles (§8, item 6, Risks; header; status.json). The skeptic's trial file is now rocq/plan_check_full.v, written by rocq/mk_plan_check_full.py (the skeptic's generator, moved here; its output is byte-identical to the skeptic's file). Recompiled here against vendor/ busycoq: 65.5 s, Print Assumptions nonhalt = Closed under the global context (work/plan_check_full.log). Not a check_kill run. Item 6 now gives the initF proof that compiles, the "Start from F" risk is marked resolved, and §8 lists what is left for the kill file (349 header comment, §1 as closing comment, no trailing Print Assumptions, file name, check_kill). New check section P: 15 static checks on the plan file and its log (the file is the compiled one; the head is plan_check_phi.v's; the rest is W4-2's .v verbatim except initF and the tail; tm = line 349; tmP = TP; the cited statements; f349 = f; no forbidden keyword).
• funext sentence (§8). Replaced: flip_halts and perm_halts do not use flip_involutive, and the closed Print Assumptions confirms that the reduction adds no assumptions.
• c0 in §1. Cells are now w_d (w_0 = the cell A reads) in the definitions of phi, L and p11; c0 is used only for busycoq's start, which the start line now spells out. Check P.proof_md_rule_block_c0_only_start.
• Self-contained text (§2–§4, §6, §7.2). Every proof that was cited from W4-2's internal proof.md is now written out here: the L1 scan on TP (new text: an induction over the offsets, with the detours), the RS chain, SW with its proof, the sweep corollary, the increments and the orbit lemmas, the overflow words and the full macro-rule runs, where a macro rule ends and which overflows occur inside one, Lemma S and Lemma C with every inequality, and the parity facts of §7.2. The definitions of Hi·W_h(c, o), tz and the l <S r notation moved into §2. No rule, bound or step count changed. A submission write-up made from this file therefore needs no W4-2 document. Check P.proof_md_no_internal_W42_citation (it finds 9 citations in the previous version).
• Results: 219/219 PASS with seed 1 and seed 2 (default) and seed 1 --full.
• Open: Checkpoint B (Dennis); the formal stage (the kill-file edits listed in §8, then check_kill).