1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC (W5-3): never halts (informal proof)

• Machine: 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC (740 list, line 134; on every snapshot since 2024-06-14), viewer https://bbchallenge.org/1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC
• Sheet: "Bell eats counter", no claim, no Discord thread. No siblings: from all six start states, the canonical form (renaming + mirror) matches only this entry, and its group in the 778-list equivalence file is a singleton.
• Written for the string itself (no mirror, no renaming). Its only undefined transition is F0.
• Template: verify/BECv5.v, Module TM1 (1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA0RB). Only the architecture carries over (§8).
• Status: informal proof, complete. Finite rules are exact windowed runs. Parametric rules are compositions of them, derived in §3 and checked by machine (§9). Not yet formalized.
• AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

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 the next 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)
           (H form, §8: S(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 H form used for Rocq (§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 the next 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 paragraph explains why the eat configurations of the run are exactly the ones on the macro-rule orbit, which check Z compares with a direct run.

• 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, and none of them is an eat configuration.
• This last point is checked 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.

So the next eat configuration after E(p, N) is the end of its macro rule.

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 H form of §8, S (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. Lemma plan for Rocq (template: BECv5 TM1, architecture only)

Shared with TM1. - 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 lemmas, multistep_nonhalt with an esx start, and progress_nonhalt_cond with a linear invariant: TM1 has a ≤ 1+b, here N ≤ 2p.

Different from TM1. - 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 LIncs' (shifted counter) has no analogue. Here the eat leaves a clean counter, except for Q.

The H form. The Rocq configurations are taken 6 steps later than G, after TS:

H l R     := l <{{E}} [1;0;1;1] *> R                 (G(w, R) after TS, with l = 0inf <* w)
S '(p,N)  := H (0inf <* <[1;0]^^p) (C N)              (the eat configuration E(p, N), after TS)

So S (p, N) is E(p, N) followed by TS: E reads the last cell of the word. It is named S as in TM1, since E is a state name. Steps from S to S are the same as from E to E, so the macro rules are unchanged. Only the start moves: c0 -->(171) S (2, 4), that is 165 steps to E(2, 4) and then the 6 steps of TS.

Every count then splits into two lemmas. - A left lemma holds for every right side r. It goes from H w r to w' <* <[1;0;1;1] {{A}}> r, the head on the right after AS and A1s(2). - A right lemma holds for every left side l. It goes from l <* <[1;0;1;1] {{A}}> R to l <{{E}} [1;0;1;1] *> R+.

Risks.

List orientation. Left words go in reading order with <[..]. The H form's right list [1;0;1;1] is already in tape order.

M5's exponents. M5 chains three inductions: 2^(t−1) − 1 W2 steps, then B(t), then W0 with c = 2^(t−1) − 1. Name T := 2^t and keep every bound linear in T, so that lia closes them.

The carry hypothesis. RBinInc_spec needs its hypothesis for every n. A single es over a power can overshoot, so prove the A run and the D run as shift lemmas first.

The blank edge. EAT on E(p, N) reads three blank cells left of the word. Rewrite 0inf as three 0 cells followed by 0inf before applying the lemma.

No decider certificates are involved.

9. Machine checks

Every claim above has a named check. The checks are run by one self-contained script with its own simulators. All 108 checks pass in the default run with two random seeds, and in a long run with larger ranges.

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.

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.

Appendix (working copy only): evidence and files

This appendix and the review log below are not part of the public write-up. When submission/proof.md is made, it is everything above this heading, with the title shortened to the machine string and ": never halts", the header Status line updated, and §8 rewritten for the finished .v. That part passes tools/writeup_lint.py with 0 errors (only the WARN on the word "plan" in the §8 heading and on the snapshot date in the header).

• Checker. python3 -B check_proof.py [--seed S] [--quick | --full] ("long run" in §9 is --full). Logs: work/check_proof_seed1.log, work/check_proof_seed2.log (default) and work/check_proof_full_seed1.log (--full). The stored run of §6 and check Z is work/mev_1e11.txt (from scripts/mev.c).
• Checkpoint B (Dennis). Pending (non-blocking).
• Correspondence with the observe notes (notes.md, observe.json):
• their M(a, X, b, N) is G((10)^a X (10)^b, C(N)), and their K(q, N) is G((10)^q 1 1 1, C(N));
• their four eat types are the residue classes of §3.3; their "EAT3" is Y3(0) followed by OVF with width 0;
• their "EAT4" is M5 phases (a)–(e) together, and their "transient" is (f)–(g);
• the closed form of §3.5 is theirs;
• they started the induction at E(21, 6) (step 3,097) because their invariant also required p ≥ 20; J does not need it;
• the ratio N/p of §4.2 is from scripts/abstract_run.py (2,000,000 eats from E(0, 1)); check Z now reproduces it from E(2, 4).
• Cryptid protocol. Ground rule 6 does not apply (§7.2).
• Template. BECv5 TM1 is also W4-2's template.

Review log

• 2026-10-13, informal_proof stage (first version).
• Built from the observe notes. Every rule there is now derived from 16 exact low-level rules, and the macro rules are chains of the count, eat and walk rules.
• New: the misaligned counter Q_k(x, y) = D_k(x) 0 C(y) explains the N ≡ 6 (mod 8) case. The first eat leaves Q (Y3), Q counts up, a second eat shortens it (Y1 or Y4), Q overflows (OVF), and the overflow block becomes the second defect (B, then W0).
• Unifications: the notes' EAT3 is Y3(0) + OVF with width 0, and their EAT4 is M5 phases (a)–(e). Their K(q, N) is G((10)^q 1 1 1, C(N)). The hub rule R1 is not needed.
• Corrections to the notes:
  • the invariant does not need p ≥ 20; J: 1 ≤ N ≤ 2p is closed for all p, so the start is E(2, 4) at step 165 (not E(21, 6) at 3,097);
  • from blank, the first G configuration is G(1, C(0)) at step 7, which INC1 takes to E(0, 1) at step 31.
• New: step formulas for every rule. With them the model reproduces the step numbers of all 2,091 stored eats.
• The t = 0 case of N ≡ 6 (mod 8) (M4) needs its own left rule, F011, for the word … 1 0 1 1 0 0.
• check_proof.py is new and self-contained (its own simulators, no project imports). On its first run it found two bugs in itself and none in the proof:
  • a wrong slice in the Q identity for Y1(1) (Q[6:] for Q[4:]);
  • a check that assumed no G configuration before step 31.
• Added after the first runs: a check that C0 occurs only in EAT0 and CF, and a mutation test (TEETH): all 77 single-transition changes of the used transitions fail some windowed L1 check.
• Self-review fixes before the final runs: the orbit after E(2,4) is E(5,7), E(8,12), … (a first draft said E(5,10)); the last stored eat is at step 99,939,266,761 (a first draft gave the step of a later post-eat configuration); the low-level table has 16 rules, not 17. None of these changes a rule or a bound.
• Results: 100/100 PASS with seed 1 and seed 2 (default, about 40 s each) and seed 1 --full (80 s: INV for p ≤ 3000, fresh direct run 336 eats to step 399,190,301).
• Open: Checkpoint B; a skeptic pass by a second agent; formalization (§8).
• 2026-10-13, skeptic round 1 (verdict: sound; 7 gaps, all minor; all fixed and re-checked).
• §2.3: "Q_k(x, y) is never a counter word" was false for y = 0 (Q_k(x, 0) = C(x)). It is now stated for odd y, the only case used, with the y = 0 exception noted. New CQ checks for both.
• §3.5 "Where a macro rule ends": now stated for boundaries (where one count or eat ends and the next begins), since the pattern w 0 1 1 B> 0 R also occurs inside counts (inside INC011, after TS and the first step of F011). The paragraph is marked as not needed by the induction. New per-step checks: M tests every TM step of 177 (seed 1) and 191 (seed 2) direct runs, among them all 66 boundary cases of the 6 mod 8 precondition; Z tests every step of the blank-tape run to step 3,000,000 (--full: 20,000,000). In every run the first eat configuration after the start is the predicted one.
• §3.5, M5 note (d): the W2 steps are numbered i = 0, …, 2^(t−1) − 2 ("i-th" read as counting from 1). The arithmetic is unchanged.
• §0: INC1 does not move the defect. The summary now says that INC1 turns an extra 1 into an extra 0 in place, INC0 moves it two pairs, and so two counts move it two pairs.
• Counting convention: §2.4 defines eat configuration (M4 and M5 contain two eats each). §0, §4.2, §6 and §9 now count eat configurations, or eat-to-eat transitions, which is one fewer: stored run 2,092 / 2,091; fresh run 174 / 173 (--full 337 / 336). The checker's check names follow the same convention.
• §8: the Rocq definitions are stated: H l R := l <{{E}} [1;0;1;1] *> R and S '(p,N) := H (0inf <* <[1;0]^^p) (C N), named S as in TM1 because E is a state. The init is 171 steps (165 to the G form, then TS), and the BigSteps go from S to S. New Z checks: H form at step 171, and S(2,4) → S(5,7) in exactly the macro steps.
• Public text: §9 has no file paths or script names; the observe-notes cross-references, "ground rule 6", the W4-2 mention, Checkpoint B and the file list moved to a working-copy appendix. Everything above the appendix lints with 0 errors and 2 warnings (the snapshot date, and "plan" in the §8 heading), with no density warnings.
• Found while fixing: the §4.2 remark "N/p stays below 2" was not true at E(2, 4) itself, where N/p = 2. It now says strictly below 2 after E(2, 4), with maximum 1.9999996 at E(5598694, 11197386) within the next 2,000,000 eat configurations. This is new check Z (300,000 configurations by default). No rule or bound changed.
• Results: 108/108 PASS with seed 1 and seed 2 (default, about 40 s each) and seed 1 --full (87 s: per-step watch on 466 direct runs, 66,910,134 TM steps; blank run step by step to 20,000,000 with 118 eat configurations, all on the orbit; fresh run 337 eat configurations to step 399,190,301; max N/p 1.9999996). Logs: work/check_proof_seed1.log, work/check_proof_seed2.log, work/check_proof_full_seed1.log.
• Status: CHECKPOINT_B. No fatal or major gap remains. Still open: Dennis's Checkpoint B notes (non-blocking) and formalization (§8).