1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- never halts

This machine is a "Bell eats counter" machine seen in a mirror. Swap left and right in its table and rename its states, and you get a table we call TP. Started on the blank tape, the machine does exactly what TP does when TP is started in its state F, on the mirror-image tape.

TP keeps a binary counter in a word to the left of the head and two blocks of 10 pairs to the right. Each bounce of the head applies one step to the counter word (on a clean counter it adds one) and moves one 10 pair from the first block to the second. When the first block is empty, the right side eats the low end of the counter (an overflow) and the first block is refilled.

TP agrees with busycoq's BECv5 machines TM1 and TM2 except in one entry, F1. That entry only changes how long one kind of step takes. So the counter's mathematics is the same as for the variant with F1 = 1LF, and an invariant on the overflow states shows that the halting entry is never reached.

• Machine: 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---, viewer https://bbchallenge.org/1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---
• A BB(6) holdout, on every holdout list since June 2024: line 349 of the 740-machine list, so we call it 349 below. Class "Bell eats counter". Its only undefined transition is F1.
• Template: verify/BECv5.v, Module TM1 (1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB) and Module TM2 (..._1LA1LB).
• 349 is TP mirrored and renamed, where TP = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC agrees with TM1/TM2 except in F1.
• The .v extends our proof of 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF (F1 = 1LF, called the 1LF machine below), which is adapted from the same template.
• What is new for 349: the detour that replaces F1 (§3.2), the start from F (§6) and the mirror conjugacy (§3.1).
• Status: formalized. The accompanying 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---.v (1,278 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c), importing only Individual62.
• Print Assumptions nonhalt: Closed under the global context.
• It compiles in about 64 s with -native-compiler yes, and coqchk re-checks it in about 27 s.
• Where each part lives in the .v (every lemma is top level; §8 has the full table):
• §3.1: tm, f349, perm_349, nonhalt (end of the file);
• §3.2: tmP (top of the file), PA/PF, TA0–TA2, TF0–TF3, TB, phi_spec;
• §3.3–§3.4: RS, OVe, OVo, bounces, OV_even, OV_odd;
• §3.5: Gap, Sweep, INC_std, INC_pk, O3_merge;
• §3.6: BS_S0 … BS_P4b;
• §4: I, Cov_S3, Cov_P4, C_S1, C_P1, C_P2, step_std, step_pk, step_I;
• §6: initF; §7.1: nonhalt_F, nonhalt.

0. Summary

349 runs the 1LF machine's counter in a mirror, started in the 1LF machine'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 the 1LF machine'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 the 1LF machine's map phi, with 2 extra steps per F1. The right step and the overflow never read F1, so they are the 1LF machine's runs.
• Everything above the rules carries over. The level-1 rules R1–R5 hold on TP with new step counts. The macro rules S0–S3 and P0–P4, the invariant I, Lemma S and Lemma C are statements about phi and integers, so they hold unchanged.
• Start. From F the run reaches the clean state (std, 2, 2) at step 73, which satisfies I.

1. Notation

Configurations. l <S r is state S reading the last cell of l, and 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 of w is the cell at offset d, written w_d. Offset 0 is the cell A reads.
• Even offsets are E-cells, odd offsets are O-cells.

The pair (e, o). 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.

Shifted words. 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. There are two encodings of a number N.

• Standard: std(N) = W(N, 0).
• Packed, for N ≥ 2 with 2^(P+1) ≤ N < 2^(P+2): pk(N) = W(N - 2^(P+1), 2^P). The top two bits share one digit pair. For example pk(6) = 1100 and pk(7) = 1101.
• std(N) and pk(N) are clean words. Every other word is dirty.

Configurations of TP. For n, m ≥ 0,

K(w, n, m) = 0^inf w <A 1 (10)^(1+n) 0 (10)^m 0^inf

The right part is R n m of the .v (BECv5's w <| R n m). A clean overflow state is S(typ, N, m) = K(typ(N), 0, m), 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.

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 and L = bitlen(k);
• for pk with k ≥ 1, r = k - 2^(L-1);
• tz(x) = the number of trailing 0 bits of x.

The map phi. On a word w:

phi(w):  if w_0 = 0:  w_0 := 1
         else:        (e, e+1) := the lowest pair of adjacent 0 cells (the 0s above w count);
                      w_(e+1) := 1,  w_0 .. w_e := 0

2. Rule table (busycoq comment-block style)

This block collects the statements of §3–§6 in one place. Its symbols are defined in §1 (v, u, h, g, n and D in the block itself). The rules are proved in §3, the invariant in §4 and the start in §6.

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   (the 1LF machine = ..._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  (1LF machine: 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)

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 from Permute.v:

tm (q,s) = None              ->  tm' (f q, s) = None
tm (q,s) = Some (s', d, q')  ->  tm' (f q, s) = Some (s', d, f q')

Consequence. Two framework lemmas turn a halting run of 349 into a halting run of TP.

• flip_halts (Flip.v) gives halts tm349 c0 → halts (flip tm349) (A;; tape0), because the blank tape is its own mirror.
• perm_halts (Permute.v) then gives halts TP (f A;; tape0), which is 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.

A related upstream result. busycoq's verify/Eqv_v3.v, Module TM518, relates 349 to 1RB1RA_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---. That table is the 1LF machine mirrored and renamed by the same f, and it differs from 349 only in A1 (349: 1LD; TM518's tm: 1RA). That one cell is exactly TP's F1. This proof does not use that file: the .v is a direct proof that imports only Individual62.

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

The 1LF machine's F1 = 1LF does the same in one step:

l 1 <F r   -->(1)   l <F 1 r

With r = 1 r', that is the right-hand side of Lemma E.

Why the 1 is always there. The only transition into F is A1 = 1LF. 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. The only exception is the very first read of a run started in F.

In 349's letters, mirrored, the detour is:

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, the 1LF machine's TF2 with l = 1 and r = 0 0^inf never reaches its right-hand side within 40 steps on TP.

In the .v the two restated lemmas put [1] *> r on the right of both sides:

Lemma TF2 l r: [1;0] *> l <{{F}} [1] *> r -->+ l <{{A}} [1;1] *> [1] *> r.
Lemma TF3 l r: [1;1] *> l <{{F}} [1] *> r -->+ l <{{F}} [1;1] *> [1] *> r.

The left step as a relation. The .v reads phi digit pair by digit pair through two relations.

• PA e o e' o': A at an E-cell.
• 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.

Lemma L (phi_spec). On TP, for all e, o and every right side r:

(PA)  PA e o e' o'  ->  WS e o <A r     -->+  WS e' o' B> r
(PF)  PF e o e' o'  ->  WS e o <F 1 r   -->+  WS e' o' B> 1 r

Proof. Mutual induction on the derivation. Each case first rewrites the lowest digit pair, then uses the steps below.

• The PF hypothesis is only ever applied to a right side that starts with 1, which is what the (PF) clause demands.
• TF2' and TF3' are only used in PF cases, whose goal has 1 r on the right by the (PF) clause.
• The PA clause is the 1LF machine's, 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, on TP:

0^inf w <A r   -->   0^inf phi(w) B> r

• 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.
• 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. The 1LF machine's run of L1 takes e reads below offset e, then F0, A0 and e+1 B1 steps: 2e+3 in all.

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),    p11(w) = the number of 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.

3.3 Right step and overflow on TP

These runs are the 1LF machine's, cell for cell, because they never read F1, and TP differs from the 1LF machine only in F1.

Right step RS (n ≥ 1). For every l, in 10n+7 steps:

l B> R n m   -->   l <A R (n-1) (m+1)

Write R n m = 1 1 0 (10)^n 0 X with X = (10)^m 0^inf. The run is this chain:

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.

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 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). 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, in q+8 steps. Then E reads the last cell of x.

The three cases of OVo:

None of these enters F except the last, nested case. In the .v these are RS, OVe and OVo, the 1LF machine's statements and proofs.

3.4 Level-1 rules

R1 is L followed by RS. R2–R5 are L followed by OV, with the cases of §3.3. The step counts are the 1LF machine's with L replaced by L_TP.

Iterating R1 gives

K(w, n, m)   -->*   K(phi^n(w), 0, m+n)

3.5 phi in E/O coordinates

These lemmas concern only the map phi, which is the same for TP and the 1LF machine. None of them mentions the machine.

In the .v they are lemmas about the relations PA and PAs:

• Gap, Gaps, F_inc, F_carry and Sweep;
• the increments INC_std and INC_pk;
• the orbit lemmas, used inside the macro rules.

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.
• In that case 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.
• Then 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, the barriers 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). 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     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.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 §1, and for S3/P4 also v, u, h, g, n, D of §2.

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.

• In S3, the O-cells 2L-3 and 2L-1 move to E-cells 2h and 2h+2.
• In P4, the O-cell 2L-3 and the E-cell 2L-2 move to E-cell 2h and O-cell 2h+1.

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 all come before j0 ≤ n (the last possible one, at T = 2^h, has 01 or 11 above it). They happen during bounces, where R1 applies to any word, so they do no harm.

4. Invariant, coverage, closure

The induction runs over clean overflow states (typ, N, m) with N ≥ 1. This section uses only the closed forms of §3.6, so it is the same as for the 1LF machine.

In the .v this section is the following lemmas, none of which executes the machine:

• the invariant I;
• the coverage lemmas Cov_S3 and Cov_P4;
• the closure lemmas C_S1, C_P1 and C_P2;
• the steps step_std, step_pk and step_I.

4.1 The invariant

• I0: 1 ≤ m ≤ N (pk: N ≥ 2).
• Class P (N ≡ m mod 2): the bounds below.
• 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). Here 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). Here 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 two: 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 an overflow and at least one bounce, so it takes at least 9 steps. Also m' ≥ m+1 in every rule.

Halting. TP's only undefined transition is E1 (349's 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 the 1LF machine's run from F.

In the .v this is

Lemma initF: F;; tape0 -->* K 2 0 0 2.        (K 2 0 0 2 = WS 2 0 <{{A}} R 0 2 = St (false, 2, 2))

From there the macro rules give the orbit below, with the step number of each overflow state after @:

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

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:

• multistep_nonhalt with the 73-step start from F, then progress_nonhalt_cond with P := I on states (typ, N, m), give nonhalt_F : ~halts tmP (F;; tape0);
• then flip_halts and perm_halts give nonhalt 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.

7.3 Remark: the run is the 1LF machine's run, stretched

By §3.2 (Lemma E and "why the 1 is always there"), TP's run from F is the 1LF machine's run from F with every F1 replaced by the three steps F1 C1 A1. Nothing else changes.

The proof above does not use this remark. It proves the machine-level lemmas on TP directly, which is also what the .v does.

8. Mapping to busycoq

Template: BECv5 TM1/TM2. The .v keeps from the template:

• the right side R n m and the configuration shape w <| R n m;
• the right-step run (the template's RIncs, here the one lemma RS);
• the standard counter (LC0 N is WS N 0);
• the top-level shape: big-step lemmas per rule, a start, then multistep_nonhalt and progress_nonhalt_cond.

The template's left-side lemmas 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.

Conventions. The .v writes l for L-1 (so 2^l ≤ k < 2^(l+1)) and true/false for pk/std. States are St (typ, N, m), with

K e o n m := WS e o <{{A}} R n m
St (false, N, m) = K N 0 0 m          St (true, N, m) = K (pkE N) (pkO N) 0 m

The two step notations -->* and -->+ are bound to tmP (TP), so everything up to nonhalt_F is about TP.

What differs from the 1LF machine's .v. That file has 1,217 lines; this one has 1,278. The changes are:

• its tm becomes tmP with F1 = 1RC, and the two notations use tmP;
• TF2, TF3 and the PF clause of phi_spec are restated with [1] *> r on the right, with the matching instances in the proof script;
• its 32-step start from c0 is replaced by initF (73 steps from F) and the tactic solve_initF;
• its nonhalt becomes nonhalt_F, and tm, f349, perm_349 and nonhalt are added at the end.

Every other lemma is the 1LF machine's text. 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.

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