1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC: never halts (CONDITIONAL, Lemma N open; revision 2)

• Machine: 1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC, viewer https://bbchallenge.org/1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC
• Holdout lists: pilot #10. Sheet: Results row 1047, class "Bell eats counter"; status, notes and sources are blank. No Discord thread is linked. Twin 1RB0RE_1RC1RE_1LD1RA_1LA0LD_0RA0LF_1LD--- (row 1032) is also blank.
• Written for: the string itself (no mirror, no state permutation).
• Status (2026-10-10, after the funded Lemma X stage): CRYPTID_CANDIDATE. This file does not prove that the machine runs forever, and the machine is not a kill. The funded stage (§5.8) found that the excursion entries do not close into a finite list of safe types, which was the agreed exit. §5.5–5.6 and §5.8 are the heuristic.
• Revision 2 status, kept for the record: STUCK at informal_proof after the skeptic review.
• Done: the rule layer (§1–§4) is exact, and every rule now has its L1 lemmas written as exact -->+ statements (§2.5). The epoch map has a closed form (§3).
• Open: Lemma N (§5.1). It says the counter is normalized at every eat.
• Revision 1 stated Lemma N in the form "Inv_S holds for all t ≥ 20". That form is false. Inv_S fails on the machine's own orbit at t = 350,274 (§5.3), so it is withdrawn.
• New and proved: Lemma Z and Lemma R (§5.5). Together they reduce Lemma N to the epochs that follow an excursion, i.e. an epoch where the potential P = ⌈n/2⌉ + C reaches 2^{B(n')}. The open piece is now the excursion lemma X (§5.7).
• Notation: tapes are written left to right. C> means the head is in state C and reads the cell to its right. <E means the head is in state E and reads the cell to its left. Exponents repeat words.

1. Families

Groups are 3 cells and are read left to right:

A counter word is X = x0 g1 g2 …gk, where x0 is one cell and each gj is a group. Its value is value(X) = x0 + Σ 2^j, where j runs over the digit-1 groups and counts digit groups only (inert and pending groups are skipped; the first digit group has weight 2). The word is normalized when it has no 100 group. The language is L_X = x0 {000,001,010}* {100,010,000}*.

K(a, b, X) := 0^inf (110)^a 0 (011)^b C> X 0^inf          a >= 1, b >= 1, X in L_X        (hub)
L(n, Q)    := 0^inf <E (010)^n 001 Q 0^inf                 n >= 1, Q in {100,010,000}*     (left record)

Family predicate used by the epoch argument (§4): every hub reached in the bounce phase satisfies value(X) = a. It holds at K(1, n, 1Q), because Q has no digit-1 group. Rule B preserves it, because B adds 1 to a and inc adds 1 to the value (Lemma V, §2.3).

2. Rules

2.1 Cell-level rules (L0)

The transition table, regrouped by direction of motion. F splits by predecessor: Fa is F entered from A1, and Fb is F entered from B1.

moving right   A:  0 -> 1, B            1 -> 0, Fa
               B:  0 -> 1, C            1 -> 1, Fb
               C:  1 -> 1, A            0 -> write 1, turn: D at the cell to the left
               Fa: 0 -> 0, A            1 -> turn: cells (q-1,q) := (1,0), D at q-2       [via F1=0LC, C0=1LD]
               Fb: 0 -> 0, A            1 -> cell kept, B at q+1                          [via F1, C1, A0]
moving left    D:  1 -> 0, E            0 -> HALT (D0 = ---)
               E:  1 -> 0, E            0 at p: if cell p-1 = 1: keep both, D at p-2;
                                                if cell p-1 = 0: cells (p-1,p) := (1,1), Fb at p+1

The only undefined transition is D0, so the machine halts exactly when D is about to read a 0. Note that D1 = E1 = 0LE: on a 1, D and E act the same. The lemmas below use this when a left pass may arrive in either state.

Shift rules (check 2.1a, k = 1..40):

  A> (001)^k   -->  (111)^k A>        3k steps     carry passes digit 1
  A> (010)^k   -->  (110)^k A>        3k steps     carry passes an inert group
  B> (010)^k   -->  (111)^k B>        3k steps     toggle passes an inert group
  F> (001)^k   -->  (011)^k F>        3k steps     J-walk passes digit 1
  (110)^k <E   -->  <E (010)^k        5k steps     return pass restores inert groups / builds (010)^n
  1^k <E       -->  <E 0^k            k  steps     return pass clears passed digits (111 -> 000)

Single-group rules (checks 2.1b and 2.5 "L0x"; the step count follows each rule):

  A> 000      --> <E 001     5     carry stops
  A> 100      --> 001 B>     3     carry meets S: placeholder 001, toggle starts
  B> 000      --> <E 010     3     toggle stops
  B> 100      --> 101 B>     3     toggle skips S
  111 <E      --> <E 000     3
  1 101 <E    --> <E 0 100   6     S restored on the return pass (E reads the last 1 of 101; the 1 to its left is cleared)
  1 1 0 <E 0  --> <E 0 1 0 0 5    the same restore after TG's IH has already cleared the last cell (used by TG)
  0 0 <E 0    --> 1 1 0 A>   4     placeholder restart (E reads the middle cell of the cleared placeholder 000)
  000 <E      --> 011 F>     3     end of JW-010 (the carry came back to a cleared 010)
  F> 010      --> 000 A>     3     start of JW-010
  F> 000      --> 011 C>     3     JW-000
  0 011 C> 0  --> 110 11 F>  9     even eat entry (marker, last bouncer block, x0 = 0)
  0 011 1 <E  --> 110 11 C>  9     odd eat exit (E reads x0 = 1 after the carry)

2.2 High-level rules (comment-block style)

1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC

start: c0 -->(27) L(2, [])

R  (restart) L(n, Q)      -->  K(1, n, 1Q)        exactly 3n+5 steps        n >= 1, Q in {100,010,000}*
B  (bounce)  K(a, b+1, X) -->+ K(a+1, b, inc X)                             a >= 1, b >= 1, X in L_X
E  (eat)     K(a, 1, X)   -->+ L(a', Q')                                    a >= 1, X normalized; (a', Q') = eat(a, X)

halt: only if an eat starts on a non-normalized X (not covered by E); see §5

K(a,b,X) := 0^inf (110)^a 0 (011)^b C> X 0^inf
L(n,Q)   := 0^inf <E (010)^n 001 Q 0^inf

Rule E is stated with the block count a and the word X as separate arguments. The parity of the eat is read from x0, and the new block count a' is computed from a (§2.3). In the run, E is applied only at K(n, 1, X) with value(X) = n (the family predicate), so x0 = n mod 2.

One epoch is L(n,Q) -R-> K(1,n,1Q) -B^(n-1)-> K(n,1,X_end) -E-> L(n',Q'). The counter goes from 1 to n, since value(1Q) = 1 and Lemma V applies. B needs b ≥ 1 after the step, so exactly n-1 bounces fit.

Note for the formalizer: an even eat whose J-walk drops 010 and then meets 001 passes through a configuration that is literally a hub K(a+2, 1, X'') (seen on the TM, check 8c). This is harmless. E is a -->+ statement and does not care about intermediate configurations, and X'' is normalized. Section 3 counts the whole eat as one step of the map.

2.3 inc (rule B) and eat (rule E), every case

inc(x0 g1 g2 …): - x0 = 0: set x0 := 1. - x0 = 1: set x0 := 0, and a carry enters g1. carry(w) is defined by cases on the first group of w: - 010: pass, go to the next group. - 001: becomes 000, pass. - 000: becomes 001, stop. - past the end: append 001, stop. - 100: becomes 010. Then tog toggles the groups after it, up to and including the next 000: 010 -> 000, 100 is skipped, and past the end a 000 becomes 010. The carry then resumes at the group immediately after the former 100. That group lies inside the segment that was just toggled, so it may itself have just changed. In symbols: carry(100 w) = 010 carry(tog(w)).

The other reading, "resume after the toggled segment", disagrees with the TM on 1,524 of the 14,580 words of L_X with ≤ 7 groups (check 2.3x).

The toggle is binary +1 on the i/0 string to the right (i = 1, 0 = 0), skipping S groups. It never meets a 001, because S groups occur only in the tail {100,010,000}*.

Lemma V (value). For X in L_X, inc X is in L_X and value(inc X) = value(X) + 1.

Proof. In the prefix {000,001,010}*, the carry is binary +1 over the digit groups, and it passes inert groups. If the carry enters the tail, every tail digit group is 000, so the tail contributes 0 to the value. A 100 becomes inert (010), and tog only swaps 010 <-> 000 inside the tail, so neither changes the value. The carry then stops at the first 000 after the former S. That group has the same digit index as the position the carry had reached, so the value grows by exactly 1. Every rewrite stays inside {000,001,010}*{100,010,000}*. ∎

Check 2.3x verifies this on every word with ≤ 7 groups.

eat(a, x0 G), with G normalized: - x0 = 1 (odd case): H := carry(G), and a' := a+1. - x0 = 0 (even case): the J-walk drops groups from the front of G, starting with k := a+1: - 001: drop it, k += 1. - 010: drop it, replace the rest by carry(rest), k += 1. - 000 (or the end of G): drop it and stop. Then a' := k+1.

H := what is left. - Residue in both cases: Q' := regroup(cells(H)[1:]), i.e. group by group 010 -> 100 (S), 001 -> 010 (i), 000 -> 000.

2.4 Checks of the rule layer

• 2.2 (against the TM): R 1000/1000 with the exact step count, B 1000/1000, E 1000/1000. The instances are random, with a and b up to 2000 and words up to 55 groups.
• 2.2x: B on every word of L_X with ≤ 5 groups (2,876/2,876).
• 2.3x: B again, on every word of L_X with ≤ 7 groups (14,580/14,580). It also checks Lemma V and the closure of inc on the same words, and refutes the other reading of the 100 bullet.
• The skeptic checked the closed form independently on 26,744 arbitrary eat states, and the inc spec on 3,000 random words with up to 60 groups. Both agreed with the TM.

2.5 L1 lemmas (exact -->+ statements for the formalization)

Each lemma is proved from §2.1 by the induction named in its row. Check 2.5 also runs each one as a window rule on the TM: the head may not leave the window, the words must match exactly, and the step counts shown must hold.

A non-normalized eat is exactly where these lemmas stop applying. FT would meet a 1 after C> (an S group), and JW would meet F> 100, which is an Fa-turn.

Why --- (D0) is never read inside a rule. Each rule above is an exact -->+ lemma, so no D0 read occurs inside it. The only configuration the rules leave uncovered is an eat on a non-normalized word. This replaces revision 1's claim that "D only reads a 1 the same rule wrote one step before". That claim was wrong for the C0 entry, where C writes at q and D reads q-1, a cell C did not write.

A non-normalized eat does not always halt. About 1% of random non-normalized eats halt, some of them at a = 768. The violating starts the skeptic confirmed on the TM survive 2·10^9 steps. So Lemma N is sufficient for non-halting but may not be necessary. Tolerating some non-normalized eats is another possible route to a proof, but nothing about it is worked out (§5.7).

3. The epoch map in closed form

Agreement checks: - check 3a: agrees with the deepen map on 20,000/20,000 epochs; - check 3b: 17,141/17,141 random normalized states (revision-2 run); - check 3c: the TM's own records, 276/276 epochs to 1e9 steps; - the deepen pass: 1,142/1,142 epochs to 1e11; - the skeptic: 26,744 arbitrary eat states.

State at an eat. A normalized counter of value n is x0 = n mod 2, followed by a layout λ = i^c0 d i^c1 d i^c2 d …. The d-slots hold bits 1, 2, 3, … of n, and c_j ≥ 0 is the number of inert groups just before d-slot j. Write the state as (n, c) and define: - C(c) := Σ c_j 2^j (the inert weight); - J(c) := max{ j : c_j > 0 } (the slot of the top inert group, -1 if there is none); - B(x) := the bit length of x; - Z(M) := B(M) - popcount(M), the number of 0-bits of M below its top bit (Z(0) := -1); - the potential P(n,c) := ⌈n/2⌉ + C(c).

Lemma 3.1 (eat). Let M be the number the d-slots of the uneaten part H spell, plus C(H). - n odd: H = c, M = (n+1)/2 + C(c) = P, n' = n+1. - n even: let V = n/2 + C(c) = P and let t be the number of trailing 1-bits of V. Then H = (c_{t+1}, c_{t+2}, …), M = V >> (t+1), and n' = n + 2 + t + Σ_{r≤t} c_r.

Proof (n even). Induction over the J-walk with the invariant m + C(rest) = ⌊V/2^k⌋ after k digit slots have been dropped, where m is the value on the rest. - Dropping an inert slot before d-slot 0 adds 1 to m and removes weight 1 from C(rest). - Once those inert slots are gone, C(rest) is even, so the next digit is the parity of ⌊V/2^k⌋. - A digit 1 is dropped with m := (m-1)/2, which keeps the invariant at k+1. - The first digit 0 ends the walk. That is d-slot t. - n' counts the dropped groups: t+1 digit slots plus Σ_{r≤t} c_r inert slots, plus 1.

The odd case is one carry into slot 0, and that carry passes inert slots. ∎

Lemma 3.2 (next layout). In the next epoch the residue Q' has: - an S at each inert slot of H; - an i at each d-slot of H holding 1; - a 0 at each d-slot holding 0.

Once the bounce phase has carried through every S, the layout is λ' = merge(H, M). For each j it has c^H_j inert groups, then i if bit j of M is 1 and d otherwise; past the end of H the bits of M continue in the same way. Equivalently, with r(j) := #{0-bits of M below j}, every inert group of H at slot j and every 1-bit of M at position j lands at slot r(j) of the new layout. So:

C' = Σ_j (M_j + c^H_j) · 2^{r(j)}

Proof. The d-slots of H, read as i = 1 and 0 = 0, spell m_H. Toggles run left to right. An S sitting before d-slot j adds 2^j to the number spelled by the slots after it (inc, §2.3), and it never changes a slot to its left. So the final i/0 pattern spells m_H + Σ_S 2^{j(S)} = m_H + C(H) = M, and each S itself becomes i. The main counter's carries only ever stop on 000 groups, which are the d-slots. They never touch a slot to the right of the exploration frontier, which is where the remaining S groups are. ∎

Lemma 3.3 (normalization depth). In the next epoch, the last S is consumed by the main counter's D-th exploration, which happens at increment 2^D - 1. Here

D = 1 + #{ j < J(H) : bit j of M is 0 } = 1 + r(J(H))          (D = 0 if H has no inert slot)

So the next eat is normalized iff 2^D ≤ n', i.e. iff slack := B(n') - 1 - D ≥ 0. Also D ≤ 1 + J(H).

Proof. Each exploration ends on a d of λ'. The last S sits just before H's d-slot J(H). The d's of λ' before that point are the 0-bits of M below J(H). The counter runs from 1 to n', so the k-th exploration happens iff 2^k - 1 ≤ n' - 1. ∎

4. Coverage

Every member of the families that the run reaches is covered: - L(n,Q) with n ≥ 1 and Q ∈ {100,010,000}: R applies. - K(a,b,X) with b ≥ 2 and X ∈ L_X: B applies. inc keeps X in L_X and value(X) = a (Lemma V). - K(n,1,X) with value(X) = n: E applies if X is normalized*. It then produces L(n',Q') with n' ≥ n+1 ≥ 2 and Q' ∈ {100,010,000}*. The regroup of a normalized H only produces those three groups, because every group of H starts with a 0.

That leaves exactly one obligation: every eat sees a normalized counter, i.e. slack_t ≥ 0 for all t (Lemma 3.3).

5. The invariant

5.1 What is needed (the only form of Lemma N)

Lemma N (OPEN). Along the orbit (n_t, c_t) from §6, slack_t := B(n_{t+1}) - 1 - D_t ≥ 0 for every t ≥ 0.

Revision 1 also stated an "Inv_S form" of Lemma N. That form is false (§5.3) and has been withdrawn.

5.2 Sufficient conditions for one step (proved, but not invariant)

Lemma S-odd. If n is odd and C(c) < 2^{B(n+1)-1}, then the next eat is normalized.

Proof. H = c and 2^{J(c)} ≤ C(c) < 2^{B(n')-1}, so J(H) ≤ B(n') - 2 and D ≤ 1 + J(H) ≤ B(n') - 1. ∎

Lemma S-even. If n is even and J(c) ≤ B(n) - 1, then the next eat is normalized.

Proof. J(H) = J(c) - t - 1 ≤ B(n) - 2 ≤ B(n') - 2. ∎

Check 5.2 confirms both on random states.

Let Inv_S(n,c) := (n odd ⟹ C < 2^{B(n+1)-1}) and (n even ⟹ J ≤ B(n)-1). Inv_S at epoch t implies slack_t ≥ 0. It is only a one-step sufficient condition.

5.3 Inv_S is not an invariant of the orbit

• The orbit itself. A cascade (§5.4) starts at t = 350,272:
• t = 350,272: odd n = 4,193,605, c = [3,15,3,0,11,0,0,1], M = 2^21.
• t = 350,273: slack is exactly 0 (D = 21, B(n') = 22, and J = B-1 at even n).
• t = 350,274: n = 4,193,611 is odd and C = 3,145,901 = 1.5001·2^{B-1} ≥ 2^{B(n+1)-1}, so Inv_S fails. The slack at this eat is still 15.

Checks 6a and 6b reproduce this, and so did the skeptic's two independent implementations, in Python and in C. Through 10^10 orbit epochs (n ≈ 1.95·10^11) the skeptic found: - slack 0 only at t ≤ 15 and at t = 350,273; - slack never below 0; - for t ≥ 20, Inv_S fails only at t = 350,274.

Revision 1's "slack ≥ 2 for t ≥ 20" and "J ≤ B-2 at every even n" were true only up to its 200,000-epoch horizon. - Structural reason. By cascade lemma (ii), every cascade with c_0 odd and n''+1 < 2^B puts the orbit, two epochs later, at an odd n with C'' = 3·2^{B-2} + (C - c_0)/2 ≥ 2^{B-1}. - Witness of non-closure (check 5.3). n = 2049, c = [1023] gives (2050, C = 3071, J = 11) and then (3075, C = 3072), where Inv_S fails. Both eats are still normalized.

5.4 Cascade lemma (proved; check 5.4)

Let n be odd, B := B(n+1), and M = (n+1)/2 + C = 2^{B-1}. Write the next two epochs as (n', c') and (n'', c''), with n' = n+1. Then:

• (i) V' = n'/2 + C' = 2^B, M' = 2^{B-1}, J(c') = B-1, and D' = B - 1. So slack' = 0 if n'' < 2^B, and 1 otherwise. Here n'' = n + 3 + c'_0 = n + 3 + c_0.
• (ii) If c_0 is odd and n'' + 1 < 2^B:
• n'' is odd;
• C'' = 3·2^{B-2} + (C - c_0)/2 ≥ 2^{B(n''+1)-1}, so Inv_S fails at (n'', c'');
• M'' = 5·2^{B-2} + (3 - C)/2.
• (iii) For every c_0, D'' ≤ B - 1, so the eat after (n'', c'') is normalized (slack'' ≥ 0).

Proof. - (i) M has no 1-bit below B-1, so r(j) = j there. Also C < 2^{B-1} gives J(c) ≤ B-2. Hence C' = C + 2^{B-1} and V' = (n+1)/2 + C + 2^{B-1} = 2M = 2^B. So t' = 0 and M' = 2^{B-1}. By Lemma Z (§5.5), J(c') = max(D-1, Z(M)) = B-1, because D - 1 ≤ J(c) ≤ B-2. Then H' = c'[1:] has J(H') = B-2, and D' = 1 + r(B-2) = B-1 since M' has no 1-bit below B-1. Finally n'' = n' + 2 + c'_0 with c'_0 = c_0. - (ii) M' = 2^{B-1} again acts as the identity, so C'' = C(H') + 2^{B-1} = (C + 2^{B-1} - c_0)/2 + 2^{B-1}. n'' has the parity of c_0. Substituting n = 2^B - 2C - 1 gives M'' = (n''+1)/2 + C'' = 5·2^{B-2} + (3-C)/2. - (iii) By Lemma Z, J(c'') = max(D'-1, Z(M')) = B-1. - If n'' is even, J(H'') ≤ B-2, so D'' ≤ B-1. - If n'' is odd, D'' = 1 + #{0-bits of M'' below B-1}. Here M'' mod 2^{B-1} = 2^{B-2} - (C-3)/2, and 1 ≤ C ≤ 2^{B-2} because (n+1)/2 ≥ 2^{B-2} and c_0 is odd. This value lies in (2^{B-3}, 2^{B-2}+1], so it is nonzero, M'' has a 1-bit below B-1, and D'' ≤ B-1. ∎

So the eats right after a cascade are safe. The danger lies later in the excursion it starts (§5.5–5.7).

5.5 Lemma Z and Lemma R (proved; check 5.5)

Lemma Z (top inert slot). J(c') = max(D - 1, Z(M)). The first term counts only if H has an inert group; the second only if M ≥ 1.

Proof. Every inert group of H at slot j, and every 1-bit of M at j, lands at slot r(j) (Lemma 3.2), and r is non-decreasing. The top inert group of H lands at r(J(H)) = D - 1 (Lemma 3.3). The top 1-bit of M lands at r(B(M)-1) = Z(M). ∎

Lemma R (no violation without an excursion). If slack_{t-1} ≥ 0 and P_{t-1} < 2^{B(n_t)}, then slack_t ≥ 0.

Proof. D_t ≤ 1 + J(H_t) ≤ 1 + J(c_t) = 1 + max(D_{t-1} - 1, Z(M_{t-1})) by Lemma Z. - First term. D_{t-1} ≤ B(n_t) - 1 ≤ B(n_{t+1}) - 1. - Second term. M_{t-1} ≤ P_{t-1} < 2^{B(n_t)}: M = P at odd n, and M ≤ P/2 at even n. So Z(M_{t-1}) ≤ B(n_t) - 1, with equality only if M_{t-1} = 2^{B(n_t)-1}. - Without equality, D_t ≤ B(n_t) - 1, which is enough. - Equality is impossible at even n_{t-1}, because there M ≤ P/2 < 2^{B(n_t)-1}. At odd n_{t-1} it is exactly a cascade start, and cascade lemma (i) gives slack_t ≥ 0. ∎

Corollary (reduction). Call epoch s an excursion if P_s ≥ 2^{B(n_{s+1})}. Then Lemma N follows from the slack at t = 0 together with

Lemma X (excursion lemma, OPEN): for every t ≥ 1 such that epoch t-1 is an excursion, slack_t ≥ 0.

Proof. Induction on t, using Lemma R when epoch t-1 is not an excursion and Lemma X when it is. ∎

Lemma X cannot come from magnitude bounds alone. Take the super-cascade (check 8b): an odd n with M = (n+1)/2 + C = 2^{B(n+1)} exactly and n'' < 2^B. It has V' = 2^{B+1}, M' = 2^B, J(c') = B and D' = B, so slack' = -1. Example: n = 1019, c = [0,1,0,0,0,0,0,0,2]. It has C/2^{B-1} = 1.004, its first eat has slack 0, and the next has slack -1. The orbit reaches C/2^{B-1} ≈ 1.5 at odd n (§5.3). So whatever proves Lemma X must use exact values, as cascade lemma (ii) does. There, the dangerous value M'' = 2^B is excluded by arithmetic: 5·2^{B-2} + (3-C)/2 ≠ 2^B for C ≤ 2^{B-2}.

5.6 Evidence

• The orbit (check 6, 400,000 epochs, n up to 4.77·10^6):
• slack ≥ 0 at every eat; slack ≤ 1 for t ≥ 16 only at t = 350,273 (slack 0);
• for t ≥ 20, the excursion epochs are exactly t = 350,273 and 350,274, the ones after the cascade;
• Lemma R covers every other epoch. The two uncovered epochs have slack 15 (t = 350,274) and 17 (t = 350,275), checked directly (6c);
• the skeptic's run to 10^10 epochs adds no further slack-0 eats after t = 350,273.
• Other orbits of the map (check 7: 2,000 small random starts × 3,000 epochs; the skeptic: 20,000 × 100,000 epochs = 2·10^9 eats after burn-in; my scratch run: 100 × 100,000):
• 0 non-normalized eats.
• Check 7 has 1,052 slack-0 eats after burn-in, and all 1,052 come right after a cascade start. The skeptic classified 1,488 slack-0 eats, all of them cascades.
• Slack-1 eats do occur (155 in check 7).
• Inv_S fails 567 times in check 7's 6M eats.
• Max C/2^{B-1} is 1.624, and max P/2^{B(n)} is 1.25.
• Excursions are short, at most 2 consecutive epochs, with 2,178 excursion epochs in check 7. Of its 1,087 excursion entries, 1,052 come right after a cascade start and 35 do not. In a scratch run of 100 × 100,000 epochs, 125 of 127 entries followed a cascade, and the 2 I inspected followed a near-cascade M = 2^{B-1} + 2^{B-3}.
• Constructed cascade and near-cascade starts (check 5.6: 22,472 valid starts with B = 6..24, 40 epochs each; scratch runs: 302,484 starts): 0 non-normalized eats. The longest excursions last 4 epochs. One example is the cascade with C = 3 at n = 2^B - 7, which reaches P/2^B = 1.75 and has a second slack-0 eat at t+2, as cascade lemma (iii) allows.
• Arbitrary starts violate. Revision 1's claim of a "hard barrier on the image of a few iterations" is withdrawn.
• Random arbitrary c violate in epochs 0–2 in the revision-2 run of check 8 (20,000 starts), and in epochs 0–4 in revision 1's run. The skeptic's searches (2M starts per distribution) found violations at epochs 5, 6 and 7, at epoch 1 with B up to 28, at epoch 2 with B up to 23, at epoch 3 up to 15, and at epoch 4 up to 12.
• Starts that satisfy Inv_S also violate later.
• Two violating starts are confirmed on the TM. The start (20, [0,0,0,22]) (check 8c) gives TM eats at n = 22, 25, 26, 55, 56, 58, and the eat at n = 58 is non-normalized, exactly as the map predicts (check 8b). The skeptic confirmed (16384, [0]*13+[1295]) at epoch 1.

So the slack is not bounded below by 0 on Φ^k images for small k. A proof has to describe the residues that are actually reachable.

5.7 Plan for Lemma X, and the cryptid question

Plan. 1. Classify excursion entries. An excursion entry has P_t ≥ 2^{B(n_{t+1})} while P_{t-1} < 2^{B(n_t)}. Since P_t = ⌈n_t/2⌉ + Σ_j (M_j + c^H_j)·2^{r(j)} and ⌈n_t/2⌉ ≈ M_{t-1} - C_{t-1}, an entry needs r(j) close to j for the heavy terms. So M_{t-1} must have at most about two 1-bits at or near its top, with the inert weight below its lowest 1-bit. Examples are the cascade 2^{B-1} and the near-cascades 2^{B-1} + 2^{B-2} and 2^{B-1} + 2^{B-3}. 2. Follow each entry type exactly, as in cascade lemma (ii)–(iii), until the potential returns below 2^B. Each continuation of the excursion forces one more exact bit pattern, which pins C further. For example, the cascade continues past t+2 only if 2^{B-2} - (C-3)/2 is a power of two, i.e. only if C = 3. 3. In parallel, look for a 2–3 epoch invariant that names the post-cascade states explicitly (the skeptic's suggestion).

The risk is that the list of entry types turns out not to be small. The ψ-term depends on where the inert groups of H sit relative to the 1-bits of M.

Cryptid assessment (ground rule 6): not flagged as of this revision; this is a priority call for Dennis. - An excursion starts with a coincidence: ⌈n/2⌉ + C equals a power of two or nearly so. On the main orbit this happens about 0.1 times per binary level, and it happened once in 10^10 epochs. - Halting would need the excursion that follows to reach a violating pattern. In every case examined, that is excluded by exact arithmetic rather than by luck: - cascade lemma (ii)–(iii); - 0 violations in 302,484 constructed cascade and near-cascade starts; - 0 violations in more than 2·10^9 natural-orbit eats. - If Lemma X turns out to need an unbounded family of entry types, the condition does depend on exact coincidences of ⌈n/2⌉ + C with sparse binary patterns along one deterministic orbit. Then the right outcome is ground rule 6 (CRYPTID_CANDIDATE), with §5.5–5.6 as the heuristic.

5.8 Funded stage on Lemma X (2026-10-10): the exit fires

New proved results. All are checked by scripts/fs_lemmax.py, which passes for seeds 1 and 2 at N = 20,000. The counts are in notes.md, "Funded stage".

The notation is that of §3, plus two quantities: - m(M) = Σ_{1-bits p of M} 2^{r(p)}; - L(H,M) = Σ_j H_j (2^j - 2^{r(j)}) ≥ 0.

With them, C' = m(M) + C(H) - L(H,M).

• F4/F5 (potential identities).
• Odd n: P' = P + m(P) - L(c,P).
• Even n: P' = V + 1 + ⌈(s+σ_s)/2⌉ - C_lo - (2^{s+1}-1)C(H) + m(M) - L(H,M).
• Lemma A. No excursion starts at an even eat: even n and P < 2^{B1} imply P' < 2^{B1}, where B1 = B(n').
• Lemma B. P + m(P) ≤ 2^b + 2^{b-2} for P < 2^b. So an odd entry has P' ≤ 1.25·2^{B1}.
• Lemma R2. Suppose slack(σ) ≥ 0 and slack(σ') < 0. Then one of three things holds:
• σ is a super-cascade: n odd and P = 2^{B1};
• P ≥ 2^{B1+1};
• σ is an even cascade (V = 2^{B1}) with B(n) < B1.
• Lemma EC. Suppose n is even, V = 2^{B1}, B(n) = B1 and slack ≥ 0. Then slack' ≥ 0, and 1.125·2^{B1} < P' ≤ 1.25·2^{B1} + 1. This is cascade lemma (iii) for any residue.

So every failure has to pass through a super-cascade or through a potential ≥ 2^{B1+1}. Both of these can only be reached from inside an excursion, and every excursion starts at an odd eat. The entry shapes are P = 2^B - 2^k + x: a top run of w ones followed by a tail. That is an infinite family. Natural orbits use only the cascade and w = 1.

Counter-family (proved for every B ≥ 8; exact for B = 8..300; TM-confirmed at B = 8). Let σ0(B) = (3·2^{B-2} - 7, [3, 0^{B-6}, 10, 0, 2]). - It satisfies everything Lemma X may assume: slack is 2, it is not an excursion, and P0 = 15·2^{B-4} (w = 4). - Epoch 1: V = 17·2^{B-4}. - Epoch 2: P = 2^B at odd n, a super-cascade. - Epoch 3: V = 2^{B+1} and slack = -1. - On the TM, from K(185, 1, X(σ0(8))), the eats are n = 186, 191 and 192, and then a non-normalized eat at n = 194. - The TM then recovers: normalized eats resume at n = 207. The same happens at B = 9 and B = 10.

So a finite case analysis over entry types cannot prove Lemma X. What decides safety are equations like P_{t+2} = 2^B in the residue counts. Whether the main orbit ever solves them is a question about exact coincidences along one deterministic orbit. Following ground rule 6 and the agreed exit, the machine is flagged CRYPTID_CANDIDATE.

The heuristic still supports non-halting: - 0 non-normalized eats in more than 2·10^9 natural eats, and none to 10^10 main-orbit epochs; - natural entries are 1,769 cascades and 11 w = 1 near-cascades in 5.9M eats, and never w ≥ 2; - the TM recovers even from the family's non-normalized eats.

The rule layer (§1–§4, §2.5) remains formalizable as an AntiHydra-style reduction.

6. Initial segment

c0 = 0^inf A> 0^inf takes exactly 27 steps, with no halt, to L(2, []) = 0^inf <E (010)^2 001 0^inf (checks 4 and 4b). The first left record, at step 5, is a degenerate n = 0 record and is not a family member. From L(2, []) the epochs are exact (checks 3a and 3c):

t:   0      1      2         3        4           5          6            7               8                9
n:   2      5      6         11       12          18         21           22              25               26
Q:   []     []     ii        i        S0ii        i0i        Si0i         SiSSi0i         SS0iiS           SSi0iSiS

The slack is ≥ 0 at every epoch checked: 400,000 here (check 6a), 10^10 by the skeptic. The minimum is 0, at t ≤ 15 and at t = 350,273. The formal proof can handle the epochs before Lemma X's induction takes over by execute on the concrete configurations, as long as they are short. That is open until Lemma X fixes where the induction starts.

7. Conclusion (conditional on Lemma N, i.e. on Lemma X)

• By §6, c0 reaches L(2, []).
• By §4 and Lemma N, every epoch is the exact composition R ∘ B^(n-1) ∘ E. Each epoch takes at least 3n+5 ≥ 11 steps (R alone) and returns to the family L(n', Q') with n' > n.
• So progress_nonhalt applies and the machine never halts.

Each rule is an exact -->+ lemma (§2.5), so no D0 read occurs inside a rule. The only configuration not covered is an eat on a non-normalized word. Lemma N rules that out; it is sufficient but possibly not necessary (§2.5).

8. busycoq lemma plan

If Dennis prefers the ground-rule-6 route, the same rule layer (every row except "invariant") is the AntiHydra-style formal rule reduction.

9. Evidence and gaps

• check_proof.py (revision 2, seed 2, full run; output in scripts/check_proof_full.log). Every PASS check passes, and the INFO lines report data only:

Run python3 -B check_proof.py --quick for a fast pass. - Scratch runs cited in §5.6 (revision 2; they reproduce with these exact arguments): - scripts/rev2_cascade_search.py 1 200000 40 casc gave 189,084 cascade starts. - scripts/rev2_cascade_search.py 2 200000 40 near gave 113,400 near-cascade starts. - Together that is 302,484 starts, with 0 violations. - scripts/rev2_excursions_natural.py {1,2} 50 100000 covered 100 orbits × 100,000 epochs: 0 violations, and 127 excursion entries, of which 125 followed a cascade. - Deepen pass (scripts/): R/B/E 9,000/9,000, and TM records 1,142/1,142 epochs to 1e11. - Gap 1 (blocking, fatal for a kill): Lemma N. It reduces to Lemma X (§5.5), which is open (plan in §5.7). - Gap 2 (formalization only): the L1 lemmas of §2.5 are stated exactly and checked, but not yet in Rocq. - Step counts per bounce or eat are not derived, beyond BL (8b+6) and FT (5k+3). They are not needed, because -->+ suffices.

10. Review log

Skeptic review, 2026-10-10 (verdict: not sound; 1 fatal, 2 major, 4 minor). What changed:

Checkpoint B (Dennis)

• (answered 2026-10-10: Dennis funded one more stage on Lemma X, with the cryptid flag as the exit. The exit fired; see §5.8.) Lemma N now reduces to the excursion lemma X (§5.5). Lemma X looks like a finite case analysis over sparse values of M (§5.7), but it is not done. Should I spend another stage on Lemma X, or flag the machine CRYPTID_CANDIDATE now and formalize only the rule layer, AntiHydra-style?
• (open) Is §2.5 readable enough to formalize from?

Review log: validation run for revision 2

• python3 -B check_proof.py --seed 2 (full): all_pass: true, 69 s, 18 MB. Output is in scripts/check_proof_full.log.
• --quick --seed 3: all_pass: true.
• Revision 1's script and log were replaced by revision 2. Revision 2 keeps every revision-1 check except check 8. Check 8 used to assert "no violations at epochs ≥ 5 / at B > 10 after epoch 0"; it is now INFO. The new checks are 2.3x, 2.5, the revised 5.4, 5.5, 5.6, 6b, 6c, 8b and 8c.