1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC never halts

This machine keeps a binary counter on the right of the tape and a word of 10 pairs on its left. The word carries one flaw, an extra cell called the defect.

Each trip of the head from the counter into the word and back adds 1 to the counter. Every second trip also moves the defect two pairs further from the counter.

When the defect has left the word, the next trip runs to the blank left edge. A sweep there shifts the whole word by one cell, eats the lowest digits of the counter and plants a new defect. The word grows with every eat, and the counter stays at most twice the number of pairs. That bound keeps every eat inside the cases the rules cover, and no rule reaches the machine's only undefined transition.

• Machine: 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC, viewer https://bbchallenge.org/1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC
• A BB(6) holdout, on every holdout list since June 2024 (line 134 of the 740-machine list). Class "Bell eats counter". Its only undefined transition is F0.
• The proof is written for the string itself (no mirror, no renaming). No other holdout has this table up to renaming and mirror.
• Template: verify/BECv5.v, Module TM1 (1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB), architecture only.
• Shared: a BinInc counter, a budget word with a one-cell defect, one budget pair per count, an eat of low counter digits, BigStep lemmas and progress_nonhalt_cond with a linear invariant (TM1: a ≤ 1+b; here N ≤ 2p).
• Different: the counter sits on the right (RBinInc_spec), and the defect walks away from it. The eat happens at the far blank edge, through a sweep over the whole word. It removes 1–3 digits depending on N mod 8, and N ≡ 6 (mod 8) adds a misaligned counter and a two-defect transient.
• Status: formalized. The accompanying 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v (530 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9), importing Individual62 and BinaryCounter_v2.
• Print Assumptions nonhalt: Closed under the global context.
• It compiles in about 3.4 s with -native-compiler yes, and coqchk re-checks it in about 1 s.
• Where each part lives in the .v (every lemma is top level; §8 has the full table):
• §2.2: C, C_odd, C_split; §2.3: Dk, Q, Dk_inc, IncQ;
• §3.2: L1, L0, L011, RIncG, RInc, Inc, Cnt1, Cnt0, Cnt011, ROvf;
• §3.3: LEat, Y1C, Y2C, Y3, Y4, Y1Q;
• §3.4: Wk, W2, W2Q, Bk, W0k;
• §3.5: BS1 … BS5; §4: step_J; §6: init; §7.1: nonhalt.

0. Summary

The tape holds two things side by side.

• A budget word on the left: (10)^p, possibly with one defect (an extra cell, 1 or 0).
• A binary counter on the right: the number N in digits 11 = 1 and 00 = 0, lowest digit first. This is busycoq's BinInc [1;1] N.

Each count is one round trip of the head from the counter into the word and back. It adds 1 to the counter and changes the defect:

• an extra 1 becomes an extra 0 in the same place (rule INC1);
• an extra 0 becomes an extra 1 two pairs further left (rule INC0).

So two counts, INC1 then INC0, move the defect two pairs to the left.

When the defect has left the word, the next round trip finds no defect. It runs into the blank left edge, and a C/F sweep shifts the whole word by one cell into the counter's low end. This is an eat.

• For N odd, N ≡ 0 (mod 4) and N ≡ 2 (mod 8), the eat removes 1, 2 or 3 low digits. It plants a new defect at the counter end of the word, and the defect walks left again.
• For N ≡ 6 (mod 8), the eat leaves the low digits misaligned by one cell: a short fixed-width counter Q sits between the word and the rest of the counter. The machine counts Q up, eats once more, and then runs a transient with two defects that cancel each other.

The proof is an induction over the eat configurations E(p, N), with the invariant J(p, N): 1 ≤ N ≤ 2p. Five macro rules M1–M5, one per residue class, take E(p, N) to a later eat configuration E(p', N'). Each one is a chain of exact rules, and J holds at the result.

1. Rule table (busycoq comment-block style)

1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC          (only F0 is undefined; only C0 enters F)

counter    C(0) = 0^inf,  C(2n) = 0 0 C(n),  C(2n+1) = 1 1 C(n)        = BinInc [1;1] n
           t1(n) = number of trailing 1 bits of n
           D_k(x) = the k digits of x < 2^k, lowest first;   Q_k(x, y) = D_k(x) 0 C(y)
configs    G(w, R) = 0^inf w 0 1 1 B> 0 R          (count configuration: w a word, R a right half-tape)
           E(p, N) = G((10)^p, C(N)),  N >= 1       (eat configuration)
           Y(v, R) = 0^inf v 1 1 0 A> R
           R = (11)^k 0 0 R'  has  R+ = (00)^k 1 1 R'
           C(n)+ = C(n+1)  (k = t1(n));   Q_j(x, y)+ = Q_j(x+1, y) if x+1 < 2^j  (k = t1(x))

count rules, for every word u and every R = (11)^k 0 0 R'                               steps
INC1    G(u 1 (10)^b, R)              -> G(u 0 (10)^b, R+)                              6b + 4k + 24
INC0    G(u 0 1 0 0 (10)^b, R)        -> G(u 1 0 1 0 (10)^b, R+)                        6b + 4k + 32
INC011  G(u 1 0 1 1 0 0 (10)^b, R)    -> G(u 0 1 0 1 1 0 (10)^b, R+)                    6b + 4k + 40
OVF     G(u 1 (10)^b, Q_j(2^j-1, 2m+1)) -> G(u 0 (10)^(b+1) 1^(2j+1), C(m+1))           6b + 2j + 4 t1(m) + 29

eat rules, for every u, v, R'
EAT     G(u 0 0 0 (10)^b, R)          -> Y(u (10)^(b+2), R)            (any R)          4b + 17
Y1      Y(v, (11)^s 0 0 R')           -> G(v 1, (00)^(s-1) 1 1 R')     s >= 1           4s + 9
Y2      Y(v, 0 0 0 0 R')              -> G(v 1 1 1, R')                                 7
Y3      Y(v, 0 0 1 1 (11)^s 0 0 R')   -> G(v 1 1, 0^(2s+1) 1 1 R')     s >= 0           4s + 20
Y4      Y(v, 1 1 0 1 1 (11)^i 0 0 R') -> G(v 1 1 0 1, (00)^i 1 1 R')                    4i + 18

walks, for every u
W(a,b)  G((10)^a 1 (10)^b, C(n))      -> E(a+b+[a odd], n+a+1)          a+1 counts INC1, INC0, INC1, ...
W2      G(u (10)^2 1 (10)^b, R)       -> G(u 1 (10)^(b+2), R++)          INC1, INC0
W0      G(u 0 (10)^(2c+1) 0 (10)^d, R) -> G(u (10)^(2c+2+d), R+^(2c+1))  INC0, INC1, ..., INC0
B(t)    G(u 1^(2t+1), R)              -> G(u 0 (10)^t, R+^(t+1))         t+1 times INC1

eat to eat                                                                  E(p, N) -> E(p', N')
M1  N odd                EAT,Y1; W(p+2,0)                                   p+2+[p odd],  (N+1)/2 + p + 3
M2  N = 0 (mod 4)        EAT,Y2; INC1; W(p+2,1)                             p+3+[p odd],  N/4 + p + 4
M3  N = 8m+2             EAT,Y3(0); OVF(0,0); W(p+4,0)                      p+4+[p odd],  m + p + 6
M4  N = 16m+6            EAT,Y3(1); INC1; EAT,Y4; INC1; INC011; INC1; INC0  p+7,          m + 5
M5  N = (2m+1)2^(t+3)-2, t >= 1, p+7 >= 2^t
                         EAT,Y3(t+1); INC1; EAT,Y1(1); W2^(2^(t-1)-1);
                         OVF(2^t-2, t); B(t); W0(2^(t-1)-1, t)              p+7+t,        m + 2^t + t + 1

invariant J(p, N):  1 <= N <= 2p.   J(p, N) -> exactly one of M1..M5 applies, and J(p', N')
start      c0 -->(7) G(1, C(0)) -->(24, INC1) E(0,1) -->(134, M1) E(2,4)   (step 165),  J(2,4)
           (.v form, §8: EC 2 4 = E(2,4) after TS, at step 171)

2. Notation and configurations

2.1 Tapes and rules

• l X> r: state X reads the first cell of r. l <X r: state X reads the last cell of l.
• w^n is n copies of the word w. [P] is 1 if P holds and 0 otherwise.
• A rule L → R between partial configurations holds for every context: the run touches only the written cells. "→(k)" means exactly k steps.
• Words are written left to right in tape order. A word stands next to 0^inf on its left. So a leading 0 of a word is a blank cell, and G(0 w, R) is the same tape as G(w, R).

2.2 The counter

For n ≥ 0 the right half-tape C(n) is defined by

C(0) = 0^inf,    C(2n) = 0 0 C(n),    C(2n+1) = 1 1 C(n)

For n ≥ 1, C(n) lists the binary digits of n below its leading 1, lowest first, as 11 for 1 and 00 for 0. Then comes 11 for the leading 1, then blanks.

This is busycoq's BinInc [1;1] n. The three equations are BinInc_O, BinInc_mul2 and BinInc_mul2add1 in BinaryCounter_v2.v.

Let t1(n) be the number of trailing 1 bits of n, and n'' = n >> (t1(n)+1). Then

C(n)   = (11)^k 0 0 C(n'')
C(n+1) = (00)^k 1 1 C(n'')         with k = t1(n)

This is the increment R → R+ used by every count: for R = (11)^k 0 0 R', R+ = (00)^k 1 1 R'. So C(n)+ = C(n+1).

2.3 The misaligned counter Q

For k ≥ 0, 0 ≤ x < 2^k and y ≥ 0, let D_k(x) be the k digits of x (lowest first, 11/00), and

Q_k(x, y) = D_k(x) 0 C(y)

This is a fixed-width counter followed by one extra 0 cell and then an ordinary counter. Only odd y = 2m+1 occurs, so Q_k(x, 2m+1) = D_k(x) 0 1 1 C(m).

• If x + 1 < 2^k, the lowest 0 digit of x lies inside D_k(x), so Q_k(x, y)+ = Q_k(x+1, y) with k' = t1(x).
• If x = 2^k − 1, then Q_k(x, 2m+1) = (11)^k 0 1 1 C(m) has no 00 before the odd cell. This is the overflow, rule OVF.

For odd y, Q_k(x, y) is never a counter word C(n): after its first k digit pairs comes the pair 0 1. (For y = 0 it would be one, since Q_k(x, 0) = D_k(x) 0^inf = C(x), but y = 0 never occurs.)

2.4 Configurations

G(w, R) = 0^inf w 0 1 1 B> 0 R          count configuration
E(p, N) = G((10)^p, C(N)),  N >= 1       eat configuration
Y(v, R) = 0^inf v 1 1 0 A> R             the head after an eat sweep

(10)^a X (10)^b with X ∈ {1, 0} is a word with a one-cell defect.

A count is one G → G transition by INC1, INC0, INC011 or OVF. An eat is one G → G transition by EAT followed by a Y rule.

An eat configuration is a configuration E(p, N). A macro rule (§3.5) goes from one eat configuration to the next. M1–M3 contain one eat and M4–M5 contain two, so the run has more eats than eat configurations. Counts along the run below are always counts of eat configurations, or of eat-to-eat transitions (one fewer).

3. Rules

3.1 Low-level rules

Each rule is an exact run that never reads a cell outside the cells written in it (check L0 runs each one with every outside cell unknown). The five rules with a parameter n are shift rules: one block, then the induction hypothesis.

What the main ones do:

• TS (tail start) lends the counter's leading 0 to the word: 0 1 1 [0] becomes 1 0 1 1, and E starts left. Note DE(1) = A0 followed by TS.
• EB is the left sweep over 10 pairs. It stops at the first cell that breaks the pattern: a 1 read by E (X1), or 0 0 read by E and B (X0, F011, EAT0).
• AS is the right sweep back. A1s runs over the counter's 11 digits.
• DE writes 1 1 on a 00 digit and erases the run of 1s to its left. CARRY is DE followed by X1, A1, A0; it is the binary carry.
• EAT0 is the eat: B0 and C0 write two 1s into the blank, and the C/F sweep shifts the word one cell to the right. Every F step reads a 1.

3.2 Count rules

INC1. For every word u, b ≥ 0 and R = (11)^k 0 0 R':

G(u 1 (10)^b, R)  -->(6b+4k+24)  G(u 0 (10)^b, R+)

INC0. Same, with X0 and AS(b+2) instead of X1 and AS(b+1):

G(u 0 1 0 0 (10)^b, R)  -->(6b+4k+32)  G(u 1 0 1 0 (10)^b, R+)

After EB(b) the head is at u 0 1 0 0 <E (10)^(b+1) 1 1 R, and X0 gives u 1 0 A> 1 0 (10)^(b+1) 1 1 R. If u is empty, the 0 of 0 1 0 0 is the blank cell left of the word.

INC011. Same, with F011, A01 and AS(b+1):

G(u 1 0 1 1 0 0 (10)^b, R)  -->(6b+4k+40)  G(u 0 1 0 1 1 0 (10)^b, R+)

F011 ends at u 0 1 0 1 1 A> 0 (10)^(b+1) 1 1 R, and A01 moves A past that 0. This rule occurs only in M4 (b = 0).

OVF. For every u, b ≥ 0, j ≥ 0 and m ≥ 0, with i = t1(m):

G(u 1 (10)^b, Q_j(2^j-1, 2m+1))  -->(6b+2j+4i+29)  G(u 0 (10)^(b+1) 1^(2j+1), C(m+1))

The left part is that of INC1. The right part starts at u 0 (10)^(b+1) A> 1 1 (11)^j 0 1 1 C(m).

The last line is G(u 0 (10)^(b+1) 1^(2j+1), C(m+1)) by §2.2. The overflowed digits stay on the tape as the block 1^(2j+1), and the next counts take it apart (rule B).

In the form used in the .v (§8), every count is "left part, then right part". The left part is the same for all R, and the right part is the same for all words.

3.3 Eat rules

EAT. For every word u, b ≥ 0 and right half-tape R:

G(u 0 0 0 (10)^b, R)  -->(4b+17)  Y(u (10)^(b+2), R)

An eat configuration has blank cells left of its word, so EAT applies to every E(p, N) with u empty and b = p. It also applies to G((10)^q, Q_s(1, y)) in M4 and M5.

Y rules. Each one starts at Y(v, R) = v 1 1 0 A> R.

Y1 is CARRY on the last two cells 1 0 of 1 1 0. In Y3, Z0 gives v 1 1 1 0 1 A>; after A1s the 1-run behind the 0 has length 2s+3, and DE(2s+3) ends with E reading the third 1; X1, A1 and A0 then stop at a G configuration.

What the Y rules do to the counter. These are the identities of §2.2 applied to the low digits of C(N) (check CQ).

For the misaligned counter:

The cases N ≡ 2 (mod 4) split by s: s = 0 is N ≡ 2 (mod 8), s = 1 is N ≡ 6 (mod 16), and s ≥ 2 is N ≡ 14 (mod 16).

3.4 Walk lemmas

W(a, b). For a, b ≥ 0 and n ≥ 0:

G((10)^a 1 (10)^b, C(n))  -->*  E(a + b + [a odd], n + a + 1)        in a+1 counts INC1, INC0, INC1, ...

Proof. By induction on a, in steps of 2. - a = 0: INC1 with u empty gives G(0 (10)^b) = G((10)^b) = E(b, n+1). - a = 1: INC1 gives G(1 0 0 (10)^b). INC0 with u empty (its 0 is the blank cell) gives G(1 0 1 0 (10)^b) = E(b+2, n+2). - a ≥ 2: W2 with u = (10)^(a−2) gives G((10)^(a-2) 1 (10)^(b+2), C(n+2)), then the induction hypothesis. ∎

W2. For every u, b ≥ 0 and R with two increments:

G(u 1 0 1 0 1 (10)^b, R)  -->  G(u 1 0 1 0 0 (10)^b, R+)  -->  G(u 1 1 0 1 0 (10)^b, R++) = G(u 1 (10)^(b+2), R++)

The first step is INC1. The second is INC0 with the word (u 1) 0 1 0 0 (10)^b.

W0(c, d). For every u, c, d ≥ 0 and R with 2c+1 increments:

G(u 0 (10)^(2c+1) 0 (10)^d, R)  -->*  G(u (10)^(2c+2+d), R+^(2c+1))        counts INC0, INC1, ..., INC0

Proof. By induction on c.

For c = 0 the word is u 0 1 0 0 (10)^d. Its first 0 is the first defect, and the last 0 of 1 0 0 is the second. INC0 cancels both:

G(u 0 1 0 0 (10)^d, R)  -INC0->  G(u 1 0 1 0 (10)^d, R+)

For c ≥ 1, INC0 and INC1 move the second defect two pairs left:

G(u 0 (10)^(2c-1) 1  0 1 0 0  (10)^d, R)  -INC0->  G(u 0 (10)^(2c-1) 1 (10)^(d+2), R+)
                                           -INC1->  G(u 0 (10)^(2c-1) 0 (10)^(d+2), R++)

The hypothesis applies with (c−1, d+2). ∎

B(t), the block stage. For every u, t ≥ 0 and R with t+1 increments:

G(u 1^(2t+1), R)  -->*  G(u 0 (10)^t, R+^(t+1))        t+1 counts INC1, with b = 0, 1, ..., t

Proof. For 0 ≤ j < t, INC1 with b = j takes (u 1^(2t-2j)) 1 (10)^j to u 1^(2t-2j) 0 (10)^j = u 1^(2t-2j-1) (10)^(j+1). At j = t, INC1 takes u 1 (10)^t to u 0 (10)^t. ∎

3.5 Eat-to-eat macro rules

Each macro rule goes from E(p, N) to a later eat configuration E(p', N'). The table of §1 gives the chains and the results. Here are the chains in full.

M1 (N odd).

E(p, N)  -EAT,Y1->  G((10)^(p+2) 1, C((N+1)/2))  -W(p+2,0)->  E(p+2+[p odd], (N+1)/2 + p + 3)

M2 (N ≡ 0 mod 4). INC1 with u = (10)^(p+2) 1 1 and b = 0:

E(p, N)  -EAT,Y2->  G((10)^(p+2) 1 1 1, C(N/4))  -INC1->  G((10)^(p+2) 1 (10), C(N/4+1))
         -W(p+2,1)->  E(p+3+[p odd], N/4 + p + 4)

M3 (N = 8m+2). OVF with j = 0, u = (10)^(p+2) 1 and b = 0. Note Q_0(0, 2m+1) = 0 1 1 C(m).

E(p, N)  -EAT,Y3(0)->  G((10)^(p+2) 1 1, Q_0(0, 2m+1))  -OVF->  G((10)^(p+2) 1 0 1 0 1, C(m+1)) = G((10)^(p+4) 1, C(m+1))
         -W(p+4,0)->  E(p+4+[p odd], m + p + 6)

M4 (N = 16m+6).

M5 (N = (2m+1)·2^(t+3) − 2, t ≥ 1, precondition p + 7 ≥ 2^t). Here s = t+1 ≥ 2.

Notes on M5:

• (d) moves the defect from a = p+5 down by 2 per W2, while Q_t counts x = 1, 2, …, 2^t − 1 (every increment has x + 1 < 2^t).
• Number the W2 steps i = 0, 1, …, 2^(t−1) − 2. Step i starts with a = p+5−2i pairs left of the defect, and W2 needs (10)^2 there, so a ≥ 2.
• The last step, i = 2^(t−1) − 2, has a = p + 9 − 2^t. So the condition is p + 9 − 2^t ≥ 2, which is exactly the precondition p + 7 ≥ 2^t.
• (e) is the overflow of Q_t. Its block 1^(2t+1) becomes the second defect in (f).
• (g) walks the second defect left until it meets the first one and both cancel. In W0, 2c+1 = 2^t − 1 and d = t.
• If p + 7 = 2^t, the first defect 0 of (e)–(g) is the blank cell left of the word. W0's last INC0 reads it as its 0, so (g) still holds (check M runs p = 2^t − 7 directly).
• For t = 1, phase (d) is empty.

The closed form. The counter value is f = (N+1)/2, N/4, (N+6)/8 for M1–M3, and the number of low digits eaten is e = 1, 2, 3. Then

p' = p + 1 + e + [p odd],    N' = f + p' + [p even]

Where a macro rule ends. The induction does not need this paragraph: it only uses that each macro rule takes E(p, N) →+ E(p', N'). The checks below compare sampled eat configurations with the macro-rule orbit.

• A boundary is a configuration where one count or eat of the chain ends and the next one begins. Every boundary is a G configuration.
• In M4 and M5, the boundary after the first INC1 (step 2 of M4, phase (b) of M5) has the word (10)^(p+3) with no defect. But its right side Q_s(1, 2m+1) is not a counter word (§2.3, with y = 2m+1 odd), so it is not an eat configuration.
• Every other boundary strictly inside a macro rule has a defect in its word (and in M5 phase (d) also a right side Q).
• The pattern w 0 1 1 B> 0 R also occurs in the middle of some counts. For example, in INC011 after TS and the first step of F011, B reads a 0 with 0 1 1 to its left. Such configurations are not boundaries. The checks below found no eat configuration among these intermediate occurrences.
• Finite runs check this step by step. Check M watches every TM step of 177 direct runs from E(p, N), among them all 66 boundary cases of the 6 mod 8 precondition. In each run the first eat configuration after the start is the end of the chain. Check Z does the same for every step of the blank-tape run to step 3,000,000.

In all checked runs, the first eat configuration after the start was the macro endpoint; the nonhalting proof needs only positive reachability.

4. Invariant, coverage, closure

J(p, N):   1 <= N <= 2p

4.1 Coverage: under J, exactly one macro rule applies

The classes N odd, N ≡ 0 (mod 4) and N ≡ 2 (mod 4) partition N ≥ 1. For N ≡ 2 (mod 4) write N + 2 = (2m+1)·2^(s+2), with s, m determined by N. - s = 0 is M3 (m = (N−2)/8). - s = 1 is M4 (m = (N−6)/16). - s ≥ 2 is M5 with t = s − 1.

M5's precondition follows from J:

(2m+1) 2^(t+3) - 2 = N <= 2p    gives    (2m+1) 2^(t+2) <= p + 1,    so    2^t <= p + 1 <= p + 7

M1–M4 have no precondition.

4.2 Closure: J(p, N) implies J(p', N')

In every case N' ≥ 4. It remains to show N' ≤ 2p'.

• M1. N odd and N ≤ 2p give N ≤ 2p − 1, so (N+1)/2 ≤ p. Then N' ≤ 2p + 3 < 2p + 4 ≤ 2p'.
• M2. N' = N/4 + p + 4 ≤ p/2 + p + 4 ≤ 2p + 6 ≤ 2p'.
• M3. N' = (N+6)/8 + p + 5 ≤ (2p+6)/8 + p + 5 ≤ 2p + 8 ≤ 2p'.
• M4. 16m + 6 ≤ 2p gives m ≤ p/8, so N' = m + 5 ≤ p + 5 ≤ 2p + 14 = 2p'.
• M5. From (2m+1)·2^(t+2) ≤ p + 1 we get m·2^(t+3) + 2^(t+2) ≤ p + 1, so m + 2^t ≤ p + 1. Then N' = m + 2^t + t + 1 ≤ p + t + 2 ≤ 2(p + 7 + t) = 2p'.

∎

The bound is used with very little room only in M1 (N' ≤ 2p + 3 against 2p' ≥ 2p + 4). Along the blank-tape orbit, N/p = 2 at the start E(2, 4). After that it stays below 2 and comes close to it: over the next 2,000,000 eat configurations the maximum is 1.9999996, at E(5598694, 11197386).

5. Progress and halting

• Progress. Every macro rule contains at least one count, and each count takes at least 24 steps. Also p' ≥ p + 2.
• Halting. The only undefined transition is F0, and F is entered only by C0. Among the rules of §3.1, C0 occurs only in EAT0 (and in CF inside it). There every F step reads a 1: first the cell B0 has just written, then the 1 of each 01 pair that CF shifts. Every rule is an exact run, so no chain of rules executes F0.

So the halting transition is reachable only through a C/F sweep that meets C> 0 0. The only C/F sweep in the rules is EAT0 inside EAT, and it runs over (10)^(b+1) 1, which has no 0 0. In every macro rule, EAT's three 0s are the blank cells left of the word.

6. Initial segment (exact)

c0 = 0^inf A> 0^inf  -->(7)   0^inf 1 0 1 1 B> 0 0^inf = G(1, C(0))         A0 B0 C1 D0 E1 A1 A0
                     -->(24)  G(0, C(1)) = E(0, 1)       at step 31          INC1 with u empty, b = 0, k = 0
                     -->(134) E(2, 4)                    at step 165         M1 with p = 0, N = 1

J(2, 4) holds: 1 ≤ 4 ≤ 4. (J(0, 1) does not, so the induction starts at E(2, 4).)

From there the orbit is E(2,4) → E(5,7) → E(8,12) → E(11,15) → E(14,22) → E(21,6) → … , with E(21,6) at step 3,097.

The macro rules, with their step formulas, reproduce a stored direct run to 10^11 steps (check Z). It has 2,092 eat configurations, from E(0,1) at step 31 to E(7367, 197) at step 99,939,266,761, so 2,091 eat-to-eat transitions. Configurations and step numbers all agree.

A second simulator, run fresh from the blank tape, agrees at every eat configuration as well:

• 174 eat configurations (173 transitions) to step 59,308,869 in the default run;
• 337 eat configurations (336 transitions) to step 399,190,301 in the long run.

Run step by step to step 3,000,000 (20,000,000 in the long run), the blank-tape run meets no eat configuration off the orbit.

7. Conclusion

7.1 Non-halting

1. The run reaches E(2, 4) at step 165, and J(2, 4) holds (§6).
2. If J(p, N), exactly one of M1–M5 applies (§4.1). It takes E(p, N) →+ E(p', N') as a finite chain of exact rules (§3), and J(p', N') holds (§4.2).
3. No rule executes F0 (§5).

By induction the machine runs forever. In busycoq terms this is multistep_nonhalt to E(2, 4) (in the form of §8, EC 2 4 at step 171), then progress_nonhalt_cond with P := J on pairs (p, N).

7.2 Why it is not a cryptid

The branch taken at each eat depends on N mod 8 and on the 2-adic valuation of N+2. Along the orbit these look pseudo-random. But J is closed under every branch, by linear bounds and one power-of-2 bound in M5. No branch needs to be predicted, and none halts. So the proof rests on no claim about the order in which the branches occur.

8. Mapping to busycoq

8.1 What carries over from the template

The template is busycoq's verify/BECv5.v, Module TM1. The .v keeps its architecture:

• a binary counter BinInc with an increment lemma from BinaryCounter_v2;
• a budget word with a one-cell defect, one budget pair per count, and an eat of low counter digits;
• BigStep-style lemmas between eat configurations, a start by solve_init, then multistep_nonhalt and progress_nonhalt_cond with a linear invariant (TM1: a ≤ 1+b; here N ≤ 2p).

What is different:

• The counter sits on the right, so the increment comes from RBinInc_spec (TM1 uses LBinInc_spec).
• The defect walks away from the counter. Each count is a full round trip over the word, not a bounce at the counter.
• The eat happens at the far, blank edge, through a C/F sweep over the whole word (EAT0).
• The eat removes 1–3 digits depending on N mod 8. N ≡ 6 (mod 8) adds the misaligned counter Q and a two-defect transient (M4, M5).
• TM1's shifted counter LIncs' has no analogue. Here the eat leaves a clean counter, except for Q.

8.2 Configurations in the .v

The .v takes every configuration 6 steps later than the G form, after TS:

HF l r  :=  l <{{E}} [1;0;1;1] *> r            G(w, R) after TS, with l = 0inf <* w
EC p N  :=  HF (0inf <* [0;1]^^p) (C N)         E(p, N) after TS
C n     :=  BinInc [1;1] n                     the counter C(n) of §2.2

So in EC p N, state E reads the last cell of the word. Steps from EC to EC are the same as from E to E, so the macro rules are unchanged.

Only the start moves. init : c0 -->* EC 2 4 takes 171 steps: 165 to E(2, 4), then the 6 steps of TS.

List orientation. In busycoq a left side l <* xs lists xs from the head outward. So 0inf <* [0;1]^^p is (10)^p in tape order, and u <* [1;1;0;1] {{A}}> r is the tape u 1 0 1 1 A> r.

8.3 Counts as a left lemma and a right lemma

Every count is a left lemma followed by a right lemma.

• A left lemma holds for every right side r. It goes from HF w r to w' <* [1;1;0;1] {{A}}> r, the head on the right after AS and A1s(2). These are L1, L0, L011 and, for the eat, LEat.
• A right lemma holds for every left side l. It is packaged as

Inc r r'  :=  forall l, l <* [1;1;0;1] {{A}}> r -->+ HF l r'

The counter gives IncC n : Inc (C n) (C (1+n)). The misaligned counter gives IncQ k x y : Inc (Q k x y) (Q k (S x) y) when x+1 < 2^k. A single 00 digit gives Inc00.

The count rules Cnt1, Cnt0 and Cnt011 take an Inc fact as a hypothesis. So the walk lemma W2 works on both counters:

• on C, inside Wk;
• on Q, inside W2Q.

8.4 Correspondence table

Small helpers:

• pt3, pt_pre, pt_eq and HF_eq rewrite a configuration between two runs;
• lp1, lp2 and lp4 regroup powers of [0;1].

8.5 The residue split in step_J

step_J states: if 1 <= N <= 2*p, then EC p N -->+ EC p' N' for some p', N' with 1 <= N' <= 2*p'. The proof splits N in three steps.

1. Nat.Even_or_Odd N. The odd case is M1 (BS1).
2. For N = 2K, Nat.Even_or_Odd K. The case K even is M2 (BS2).
3. For N = 4K'+2, busycoq's lowbitS_cases K' writes K'+1 = (2x+1)·2^i. Then i = 0 is M3, i = 1 is M4 and i ≥ 2 is M5.

In the M5 case, the proof names T := 2^i and adds x <= x*T by nia. Every remaining bound is then linear in T and closes by lia.

No decider certificates are involved.

9. Numerical sanity checks

These are evidence only; the result rests on the .v file alone. Every claim of §1–§6 was also tested numerically, with simulators that are independent of the .v.

A windowed run starts from the cells written in a rule, with every other cell unknown. Reading an unknown cell fails the check, so a rule that passes holds for every left and right context.

All 108 checks pass with two random seeds, and in a longer run with larger ranges.

The windowed runs (L0, L1) are proofs of the finite rules. Each parametric rule is proved by the composition written in §3. The windowed runs on parameter ranges and the direct TM runs check that the compositions and step formulas are right.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic); corrections from an independent audit by GPT-6 Astra (OpenAI).