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. check_proof.py checks every claim, exhaustively on small cases and on random large ones (§9). Not yet formalized; the one non-routine piece of the .v delta (the restated phi_spec) already compiles in a plan check (§8).
• 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 = ... c2 c1 c0 (offset 0 = the cell A reads); W(e,o): bit d of e at offset 2d, bit d of o at 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): last cell 0 -> 1;  else (e,e+1) := lowest pair of adjacent 0 cells: cell e+1 := 1, cells 0..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 c0 = 0, else 2e+3+2*p11(w)
    p11(w) = #{c : 1 <= c <= e-1, cell c-1 = cell c = 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 c0 -->(14) K'(0^inf,0,1) = S(std,0,1) -->(59, S0) S(std,2,2) at step 73, which satisfies I
       (TP: F;; tape0 -->(73) K(std 2,0,2); the first F1 is TP's 122nd transition)

2. Notation and families

These are W4-2's (its proof.md §2), repeated so this file can be read alone.

• 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. In Rocq this is WS e o.
• 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).

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. - If the last cell of w is 0, this is L0 = A0 (1 step). - Otherwise let (e, e+1) be the lowest pair of adjacent 0 cells. The scan reads offsets 0..e+1 as in W4-2 (its §3.1 L1), and every F1 on the way is a detour. F reads cell c with value 1 exactly when cells c-1 and c are both 1 (1 ≤ c ≤ e-1). - So the step count is L_TP(w) = 2e + 3 + 2·p11(w), where p11(w) counts the adjacent 11 pairs among offsets 0..e-1. - The scan never reads right of offset 0: a detour from F at offset c ≥ 1 reads offset c-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. W4-2 proof.md §3.1 gives the 8-row chain. The run reads F only as F0 (in the shift 01 <A --> <A 11, transitions A1 F0) and never reads 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. Their proofs are W4-2 proof.md §3.3, unchanged. 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.

The overflow words of clean counters (N+1 = (2k+1)2^i): phi(std(N)) has q = 2i and x = W(0, k). For pk with k = 0, q = 2i-1 and x = 0^inf (R3 applies, with m + (q+3)/2 = b). For pk with k ≥ 1, q = 2i and x = W(2^(L-1), r). Check M re-runs W4-2's checks of all of these (SW exhaustive for h ≤ 5 and every high word up to 6 cells plus 30,000 random cases; O3–O6 exhaustive for small parameters and random up to 60 bits; overflow words for N < 8,192 plus 5,000 random).

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.

Where a macro rule ends (W4-2 proof.md §3.4). - The overflow states met before the end are dirty (in S2, S3, P3, P4) or empty. - The empty state K(0^inf, 0, M) = S(std, 0, M) occurs once, only in S2 (M = b+L+2) and P0 (M = b). It violates I (N = 0 < M), and S0, which has no hypothesis on m, takes it to the result. - Inside a macro rule every overflow is of kind R2 or R3. R4 and R5 never occur inside a macro rule.

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.

4. Invariant, coverage, closure

The induction runs over clean overflow states (typ, N, m) with N ≥ 1. All of §4 is W4-2 proof.md §4, unchanged: it uses only the closed forms of §3.6. 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): under I, exactly one macro rule applies

The preconditions exclude each other by construction. It remains to rule out the dirty cases that have no rule.

std, k not a power of 2 (k ≥ 2^(L-1)+1). If T = 2k+b+1 ≥ 2^(L+1), S1 or S2 applies. Suppose T < 2^(L+1), so b < 2^L - 3. - i ≥ 1 is impossible: N+1 ≥ 2(2k+1) gives N ≥ 2^(L+1)+5, and N ≤ 2m+3 (I, std with N odd) gives m ≥ 2^L+1, so b ≥ m+2 > 2^L - 3. - i = 0 in class X is impossible: N = 2k ≤ m+3 gives T ≥ 4k-1 > 2^(L+1). - i = 0 in class P (m even): 4k ≤ 3m+6 gives 3T = 6k+3m+6 ≥ 10k. Hence k < 0.6·2^L < 3·2^(L-2) (bit L-2 of k is 0) and T > 3·2^(L-1). T = 2k+m+2 is even, so u ≥ 1 and h ≤ L-3. Finally 3m ≥ 4k-6 ≥ 2^(L+1)-2 gives n = m+2+u > 2^(L-1) ≥ 2^(h+1) - 2g. So S3a or S3b applies.

pk, k not a power of 2 (r ≥ 1). If T = 2r+b+1 ≥ 2^L, P2 or P3 applies. Suppose T < 2^L, so b ≤ 2^L - 4. - i ≥ 2 is impossible: N ≥ 4·2^L + 11 and 2N ≤ 5m+6 give b > 2^L. - Class X is impossible: for i = 1, N ≥ 2^(L+1)+5 and N ≤ m+3 give b > 2^L; for i = 0, N = 2k ≤ m+3 gives T > 2^L. - i = 0, class P: m ≥ k-1, so T ≥ 3r + 2^(L-1) + 1. Hence r < 2^(L-2), T > 2^(L-1), T is even (u ≥ 1), and n ≥ k+1 > 2^(L-1). - i = 1, class P: 5m ≥ 8k-4, so 5T ≥ 18r + 4·2^L + 11. Hence r < 2^(L-2), T > 2^(L-1), T is even (u ≥ 1), and n > 2^(L-1). - In both class-P cases P4a or P4b applies.

4.3 Lemma C (closure): the result of every macro rule satisfies I

Every result is N' = m' + D with D ≥ 0 and m' ≥ 1. So I0 holds, and it remains to bound D.

W4-2 proof.md §4.3 writes out every inequality. 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 (W4-2 proof.md §7.3).
• 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, using only linear bounds and two parity facts (W4-2 proof.md §7.2). 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 40 changed or added lines of code, plus comments. The file then has one top-level Definition tm (349's string), as check_kill requires. Flip.v uses functional_extensionality_dep, which is already in the kill baseline. W4-2's .v compiled in 66 s (native).

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. esx takes its fast path only from c0. 73 steps are short enough for symbolic es, but solve_initF is the tested route (#24, rocq-notes). - 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, 204/204 PASS, 43 s each) and work/check_proof_full_seed1.log (--full, 204/204 PASS, 77 s).

10. Checkpoint B (Dennis)

Pending (non-blocking).

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