1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC: never halts (informal proof)

• Machine: 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC, viewer https://bbchallenge.org/1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC
• Holdout lists: byte-exact in data/holdouts/2026-10-07_778.txt (line 748). Sheet: results.csv row 1053, class "Bell eats counter", status/notes blank. No Discord thread found.
• Written for the string itself (no mirror, no state permutation).
• Status of this text: every rule in sections 3 and 4 is an exact configuration transition with a proof by composition of finite runs. Lemma D (section 5) is proved from those rules. The overflow count per digestion, the open link of the first version, is now bounded by Lemma C (D.0), which needs no orbit data; the constants of D.2–D.7 depend on it, and the threshold is N* = 14,796 (first version: 2917 under the unproved c ≤ 1). Epochs below N* are the explicit rules-only orbit (D.8).
• Checks: check_proof.py (machine dir) tests every numbered claim against the TM: exhaustive small cases plus random large ones. The Lemma D links are tested on the rules-only orbit. Results are in section 9.

0. Picture in one paragraph

The tape is (110)^a 0 (011)^b C> X. The 0 between the two block runs is a marker. Each bounce moves the marker one block to the right, adds 1 to the counter word X, and costs one 011 block of budget (rule B). This is FractalBEC's marker bounce. When the budget b reaches 1, the machine eats the lowest digit of the counter. The eat either gives more budget (E1g) or sweeps the whole (110)^a run into a new left record L(k, T) (E2g). At a left record the next epoch restarts with budget N = k + 1 and residue T = 000 Y. The residue Y is not a clean counter, and the first bounces of the new epoch digest it. The digestion is recursive: when it meets a 1-digit, one single bounce runs a whole sub-epoch on the rest of the word (rule D6). Halting needs an eat to happen before the digestion has finished. Lemma D shows the digestion always fits in the budget. Its cost is about 2^(k/2) with k ≈ log2 N - 3, so roughly sqrt(N), against a budget of N.

1. The machine and its only halting transition

      0     1
 A   1RB   0RF
 B   1RC   1RF
 C   1LD   0RE
 D   ---   0LE
 E   1LA   0LE
 F   0RA   0LC

The only undefined transition is D reading 0. Every rule below is an exact run that never executes D0. So the machine halts only if the run reaches a configuration that no rule covers. Section 4 shows that the only such configurations are eats at a word outside the grammar G, and Lemma D shows these never occur.

2. Notation, families, words

• Configurations use the wiki/busycoq notation. l q> r means the head is in state q and reads the first symbol of r. l <q r means it reads the last symbol of l.
• Chunks: a = 001, b = 101, z = 000.
• A block is c = d01 a^e: an a-block if the digit d = 0, a b-block if d = 1. The exponent is e ≥ 0.
• Words are finite 0/1 strings taken up to trailing zeros. Written words are normalized: they have no trailing 0, and X 0^inf follows them. For example '10' ≡ '1' and '00' ≡ ''.
• Tails: t0 = '', t1 = 1, t2 = 010001, t3 = 110001.
• Grammar G (counter words): G ::= t_s | c (z c)* [z t_s] with s ∈ {1,2,3} after a z.
• The digits are LSB first. A word W = c_0 z … z c_{k-1} [z t_s] has k = k(W) blocks.
• Its value is m(W) = (4+s)·2^k + Σ d_i 2^i, which lies in [4·2^k, 8·2^k).
• The clean words D(k,s,v) of the observe stage are the case where every block except the last has e = 1 and the last block has e = 0.
• One-level residues O: '11' a^x z W, '01' a^x z W, '00' W, '10' W, with x ≥ 0 and W ∈ G (when W = '' the z W vanishes). O also contains the 23 end words E* listed in 3.4.
• Hub words H: H ::= G | O | c z H, i.e. a run of blocks in front of a G or O word.
• Families (a, b, k ≥ 0 as stated):
• Hub: K(a, b, X) := 0^inf (110)^a 0 (011)^b C> X 0^inf with b ≥ 1. The 0 after (110)^a is the marker. The cells x0-3..x0-1 hold the last 011, and X starts at cell x0.
• Left record: L(k, T) := 0^inf <A 101 (001)^k T 0^inf. Here A reads a blank.
• Pre-record: L'(k, T) := 0^inf E> 0 01 (001)^k T 0^inf. This is one step before L(k,T), since E0 = 1LA.

3. Rules

3.1 Window rules (finite runs; each is one es)

In each rule, every executed transition reads a cell inside the shown window. So each rule holds in every context. check_proof.py runs each one with random junk around the window.

3.2 Shift rules (induction on n, one IH use each)

3.3 Region pass (any left context l)

The region pass reads nothing to the left of the marker. That is why a bounce works in any left context (used in D6).

3.4 Local pass LP

Definition. LP(X) is the run from 011 C> X 0^inf until the head first enters the cell left of that 011, which is cell x0-4. LP never reads cell x0-4 or anything to its left. Every rule below ends in one of two exit forms: - d = 0: <A 100 X'; - d = 1: <A 101 000 X'.

We write LP(X) = (X', d).

GI (inc on G) is a corollary. Write inc W for the LP result on a G word. It is a binary +1, LSB first: - An a-block toggles to a b-block (LP0). - A b-block carries (LPC): it becomes an a-block, and the rest is incremented. - Tails step '' → 1 → 010001 → 110001 (LP0, LPT, LP0). - 110001 → 001 with d = 1 (LP11). This is an overflow: a new block, and the absorbed 001 goes into the block in front of it (LPC with d_R = 1), or into the hub when the word is a bare tail.

G is closed under inc. For a word with at least one block, inc returns d = 0. Positions are stable: inc changes digits, and on an overflow it adds +1 to the last block and appends a new last block with e = 0. It never changes any other exponent.

The old names are instances: - HT (toggle), D2 ('01' V → '11' V), D4 ('00' V → '10' V) and the tail steps are LP0. - D1 ('11' a V → '01' V, d = 1), D3 ('11' z V → '00' V, d = 1) and '11' → '' are LP11. - HC (carry into a nested word) is LPC with any rest that has an LP rule. - D5 is LP5, D6 is LP6, and T is LPT.

End words E is the closure of the LPT outputs and of 010010001 under LP until G (23 words, computed in check_proof.py). Its largest own-level cost until G is τ = 13* bounces.

3.5 Bounce

B. K(a, b+1, X) → K(a+1, b+d, X') for b ≥ 1, a ≥ 0 and LP(X) = (X', d). Steps: s_LP(X) + 8b + 4 (d = 0) or + 8b + 7 (d = 1). - Proof: LP(X), then RP0 or RP1 with n = b. - The run never reads left of the marker, so B also holds with any l in place of 0^inf (110)^a.

3.6 Eats (b = 1; the LP exit then meets the marker, A reads 0)

These cover every G word at b = 1. A G word is '', a tail, an a-block first, or a b-block first. Here first is the first cell of (110)^a. L'(k,T) → L(k,T) takes one step (E0 = 1LA on a blank).

3.7 Restart

R. L(k, 000 Y) → K(1, k+1, Y) in 3k + 7 steps, for any Y. The run never moves left of the A cell.

3.8 D6, the nested bounce

Epoch map. For N ≥ 1 and a word R, Φ(a, N, R) is the deterministic sequence: - B while b ≥ 2; - the eats of 3.6 at b = 1; - it stops at the first pre-record L'(k, T).

Φ is defined when every eat it meets is at a G word. Inside D6 this holds: R ∈ G and G is closed under inc and under E1g.

Φ terminates for every R ∈ G (D.0, Lemma P): only E1g moves the front, finitely many positions are ever created, and between two eats the budget falls by 1 per bounce except for at most one bare-tail absorption. So Φ reaches E2g, E0, Et1, Et2 or the Et3 chain after finitely many steps, and LP6 below is a total rule. The same argument shows that the counting phase of every epoch (after its digestion) ends.

LP6 proof. Write x0 for the first cell of X. 1. Right pass (3e + 14 steps). It goes W11 (C> 10 → 11 F>), then W1, then F0 and A1, then S2(e), then W3: - from 011 C> 10 101 a^e z R - to 011 1 · 110 0 (011)^(e+1) C> R.

The part after · is the hub K(1, e+1, R) whose 0^inf has been replaced by … 011 1. Its first cell is x0+1, so first−1 = x0 holds a 1. 2. Sub-epoch. By 3.5 and 3.6, every bounce and every E1g of Φ(1, e+1, R) reads only cells at or right of its marker. Its final eat (E2g, E0, Et1, Et2, or the Et3 chain) reaches cell first−1 for the first time in state E, exactly when the standalone run reaches L'(k, T). So, cell for cell, the run in context equals the standalone run up to that moment, except that cell first−1 holds 1 instead of 0. 3. Exit (W10, 4 steps). 011 E> 1 01 (001)^k T → <A 100 0 01 (001)^k T = <A 100 a^(k+1) T. Every pre-record has T = 000 Y, so X' = a^(k+1) z Y and d = 0.

The sub-residue Y is one of: - '11' a^x z W' with W' ∈ G (from E2g); - '1' (from E0 and from the Et3 chain); - '01' a z 1 (from Et1); - '10 00 010001' (from Et2).

All of these are in O ∪ G.

4. Coverage

Lemma H. Every H word has exactly one LP rule, and LP maps H into H.

Case split on the normalized word w: 1. w ∈ G. GI applies (LP0, LPC or LPT). 2. w = c z H' with H' ∉ G. - a-block: LP0. - b-block: LPC with R = H', which has an LP rule by induction on length. 3. w ∈ O, by its prefix: - 11: LP11. The result is 01 a^(x−1) z W, or 00 W, or ''. - 01: LP0. The result is 11 …. - 00 W with W ≠ '': LP0. The result is 10 W. - 10 W: by W. - W = '' or t1: the word is t1, or b-block 101 with R = ''. - W = t2 or t3: LPT. - W starts with an a-block: LP5. The result is 01 a^(e+1+d) z inc R ∈ O. - W starts with a b-block: LP6. The result is a^(k+1) z Y ∈ H. - E* words: by the table.

Closure holds because every output listed above is in H. Since normalization identifies 10 with 1 and 00 with '', each word has exactly one rule.

Eats. By 3.6 every G word at b = 1 has an eat rule. The eat leaves either a hub with a G word or a pre-record L'(k, 000 Y) with Y ∈ H. An eat at a word outside G is not covered and may halt; such an eat is unsafe.

Corollary (one epoch). Start an epoch at K(1, N, Y) with Y ∈ H. - Bounces follow B while b ≥ 2. The budget b never increases: each bounce changes it by d − 1 ≤ 0. - Let β be the budget used until the first hub whose word is in G ("digestion"). - If β ≤ N − 2, every eat of the epoch is at a G word. After digestion every word stays in G (GI, E1g), and the first non-E1g eat gives L'(k', 000 Y') with Y' ∈ H. - The counting phase terminates (D.0), so this first non-E1g eat exists. - Then L and R give the next epoch K(1, k'+1, Y'). - The next budget satisfies N' = k'+1 = N + 1 + A + Σ_{E1g}(e_i + 2) ≥ N + 1, where A is the top-level absorption count.

5. Lemma D (the digestion fits in the budget)

Lemma D. For every epoch t ≥ 3 of the orbit from the blank tape, β_t ≤ N_t − 2.

Notation for epoch t: - The residue Y_t is ordinary, '11' a^x z W with W ∈ G (from E2g), or special: Y_t ∈ G ('1' from E0 or the Et3 chain; t2 at epoch 3) or Y_t ∈ E* ('01' a z 1 from Et1, '10 00 010001' from Et2). - k = k(W) (k = 0 for a special residue). The exponents of W are e_q at position q = 0..k−1. - The excess of a block is η_q = e_q − 1, or e_q for the last block. Suffix sums are S_t(q) = Σ_{q' ≥ q} η_{q'}, with S_t(q) = 0 for q ≥ k. - L_t is the number of D6 steps in the digestion. Level 1 is the top level; the sub-epoch of the j-th D6 creates level j+1. - c_t is the number of positions created during the digestion (D.0). - κ_t = max_{3 ≤ s ≤ t} k_s is the running maximum of k.

D.0 Positions, the front, and the overflow bound

Fix an ordinary residue and follow its digestion.

Positions. The blocks of W are positions 0..k−1. A new position is created only by an overflow, a tail step 110001 → 001. This can happen anywhere: inside GI, in the inc of LP5 or E2g, in a counting bounce of a sub-epoch, or as Et3. The new block a(0) is appended at the end. The absorbed 001 goes to the old last block if there is one. If the word being incremented is a bare tail, it goes to the context instead: the block c' of LP5, the exponent of E2g's residue, or the budget or a of the sub-hub. c_t counts all of these, Et3 included. Positions keep their index.

Actions on W. The front f is the lowest unconsumed position. Every step of the digestion that touches W is one of two kinds: - an increment of the G word R formed by the unconsumed positions: a sub-epoch bounce (GI), the inc of LP5 or E2g, or Et3; - a consumption of the front block: LP5 (strip, a-block), LP6 (trigger, b-block), E1g (a-block) or E2g (b-block).

All other steps leave W alone: LP0/LP11 on a level's O-prefix, and HT/HC through the merged blocks, which carry one step down to the deepest level. Positions are consumed in increasing order, because each level works to the right of the one before it.

The W-phase ends when the word of the deepest level enters G or E*. At that moment every position has been consumed. The reason: an O word followed by at least one block never parses as a G word. For example, '00' 101 … starts with 001 010 …, which is not a block followed by z.

(P1) One extra unit per position. A block's exponent changes before its consumption at most once: +1, when it is the last block at an overflow. In that case a later position exists, so at its own consumption the rest R is not a bare tail, and the consumption absorbs nothing. Hence every position satisfies

e_cur + d ≤ e_orig + 1,

where d is the absorption at its consumption (LP5's d, E2g's d') and e_orig = 0 for created positions.

(P2) Increments per front. Let D_f be the number of increments while the front is f. - D_0 = 0, since level 1 strips its prefix before it consumes position 0. - For f ≥ 1, D_f ≤ e_orig(f−1) + 1: - after LP5 or E2g at f−1 there is exactly one increment; - after LP6 or E1g at f−1 the (sub-)hub has budget e_cur(f−1)+1, which gives e_cur(f−1) bounces; - add at most one more, from a bare-tail absorption (b stays) or from Et3. Not both: after a bare-tail overflow, R has a block for as long as the front stays at f; - if e_cur(f−1) = e_orig(f−1) + 1, then R is never bare (P1), and there is no extra increment.

Lemma P (potential). Let V be the value of R, n its number of blocks, and Z = 2^f·V. - V ∈ [4·2^n, 8·2^n), so ⌊log2 Z⌋ = f + n + 2 = (number of positions so far) + 2. - An increment adds 2^f to Z, since inc is binary +1 on the value, overflow included. - A consumption replaces (f, V) by (f+1, (V − d_f)/2), so Z does not increase.

Hence at every moment Z ≤ m(W) + Σ_{f' ≤ f} 2^{f'} D_{f'}.

Lemma C (overflow bound). If c ≥ 1, then

3·2^{k+c} ≤ 9·2^k + Σ_{q<k} 2^{q+1} η_q − 5.

Proof. Let P = k + c. Take the overflow that creates the last position, P−1. Just after it, Z ≥ 2^{P+2}, and the front is at most P−1. By Lemma P and (P2), with m(W) ≤ 8·2^k − 1, e_orig + 1 = η + 2 for non-last original blocks, η + 1 for the last one, and 1 for created ones:

2^{P+2} ≤ 8·2^k − 1 + Σ_{q=0}^{P−2} 2^{q+1}(e_orig(q)+1) = 8·2^k − 1 + Σ_{q<k} 2^{q+1}η_q + 2^k − 4 + 2^P. ∎

By Abel summation, Σ_{q<k} 2^{q+1}η_q = 2S(0) + Σ_{q=1}^{k−1} 2^q S(q). So Lemma C reads

2^c < 3 + (2/3)·[2^{−k}S(0) + Σ_{q=1}^{k−1} 2^{q−k−1} S(q)].

Consequences: - A clean word (η ≡ 0) has c ≤ 1. - A deep trigger with a large exponent in front of a short all-ones suffix can push c to about log2(excess). This is the effect of the Checkpoint B examples, which reach c = 2 to 6 inside the old invariant. - On the orbit itself, c ∈ {0, 1} on every epoch checked (section 9). The proof does not use this.

Termination. Lemma P applies unchanged to a lone sub-epoch Φ(1, e+1, R), or to the counting phase of an epoch. There only E1g moves the front, and D_0 ≤ e + 1. It gives 3·2^P ≤ 9·2^{k(R)} + Σ 2^{q+1}η_q + e − 4. So finitely many positions are ever created, there are finitely many E1g, and each phase between two eats is at most budget + 1 bounces. This is the termination used in 3.8.

D.1 Cost recursion (from the rules)

Let J(w) be the number of own-level bounces until w ∈ G. Then: - J('11' a^x z W) ≤ 2x + 2 + J('10' W). The terms are LP11 and LP0 alternately: D1/D2 pairs, then D3 and D4. Equality holds unless a tail coincidence (D.3) ends the word earlier. - J('10' a-block(e) z R) = 2 + J('11' a^(e+1+d) z inc R) (LP5, then LP0). - J('10' b-block(e) z R) = 1 + 2·J(Y) (LP6). After LP6 the word is a^(k+1) z Y. Its first block alternates LP0 and LPC, so Y is incremented once every 2 bounces and no absorption reaches the hub. - End words: by the table, at most τ = 13.

At the top level the D1/D3 steps absorb (d = 1), so β = J − A. Unfold over the levels j = 1..L+1, where x_j is the residue exponent and S_j the set of a-block strips of level j:

β ≤ (x_1 + 1) + Σ_{S_1}(e + d + 4) + Σ_{j ≥ 2} 2^j [(x_j + 1) + Σ_{S_j}(e + d + 3)] + (2^L − 1) + 2^L·τ.

Check: the recursion nest_cost.JA equals the bounce-by-bounce β on every epoch (D.1 row in section 9).

D.2 Levels consume positions

• Level 1 strips positions 0..p_1−1 and meets its trigger b-block at p_1.
• For j ≥ 2, the sub-epoch of level j consumes the trigger p_{j−1}, then its E1g a-blocks, then the E2g block q_j ≥ p_{j−1}+1. Its exponent gives x_j = e_cur(q_j) + d'.
• Level j then strips q_j+1..p_j−1 and meets trigger p_j ≥ q_j + 1.

This gives q_j ≥ 2j − 3 and p_j ≥ 2j − 2. The trigger p_L is an existing position, so p_L ≤ k + c − 1, and

L ≤ ⌊(k + c + 1)/2⌋.

A position q consumed at level j has j ≤ (q+3)/2. Positions include created ones, and created positions can be triggers. A position created while the front is at the bare tail cannot be a trigger: when a level meets it, it is still a(0), unless its own sub-epoch has already eaten it.

Check: L ≤ ⌊(k+c+1)/2⌋ and 2(L−1) + #strips ≤ k + c.

D.3 Shape after digestion, and the merged blocks

Shape. The digestion ends exactly when the deepest level's word enters G. By D.0 the front is then at the bare tail. This happens either through an end word (E) or through a tail coincidence*: - '11' a z 1 → '01' z 1 = 010001 = t2 (LP11); - '11' z 1 → '00' 1 = 001 (LP11); - '10' t0 = t1 and '10' t1 = 101 (already in G after normalization), and '11' z '' = 11 → '' (LP11).

(The first version's "none of D1–D5 outputs is in G" was wrong exactly at these tails.)

Enumerating every O word over a bare tail and every E* word shows the final word ρ of the deepest level is one of '', 1, 010001, 110001, 001, 101, 001000010001 (section_D3 of check_proof.py). So ρ has at most one block, and that block has e = 0. The post-digestion word is

B_1 z B_2 z … z B_L z ρ,

so k_post ∈ {L, L+1} and m_post < 2^(L+4).

Merged blocks, itemized. B_j is the D6 block a^(k'+1) of level j, of exponent k'. It grows by the absorptions of level j+1 (via HC). Let C_j be the positions consumed by the sub-epoch of level j+1 and by level j+1's strips.

• For j < L, C_j = {p_j, …, p_{j+1}−1} and e(B_j) = Σ_{q∈C_j}(e_cur(q) + 2) − 2.
• The sub-record is k' = 1 + e_cur(p_j) + Σ_{E1g}(e_cur + 2): a starts at 1, gains 1 per bounce and 2 per E1g, and the budgets are e+1.
• Level j+1 then absorbs x_{j+1} + 1 = e_cur(q_{j+1}) + 1 on its prefix (LP11 steps), and e_cur + 2 per strip.
• None of these levels meets a bare tail, because the front is left of p_{j+1}. So there are no other absorptions.
• For B_L, C_L = {p_L, …} is every remaining position, created ones included, and

e(B_L) = Σ_{q∈C_L}(e_cur(q) + 2) − 2 + (bare-tail absorptions) + τ_end, with τ_end ≤ T := 5.

The value of τ_end depends on how the deepest level ends:

check_proof.py computes T from these chains (end_extra).

Mass bound. For 1 ≤ J ≤ L:

Σ_{j=J}^{L} e(B_j) ≤ S_t(p_J) + 3(k + c − p_J) − 2(L − J + 1) + T.

Reason: the positions consumed by levels ≥ J+1 are exactly those ≥ p_J. - Each original one brings e_orig + 2 ≤ η + 3. - Each overflow brings 1 (its absorption, wherever it lands in these levels), and its created position brings 2. - The overflows counted here map injectively to created positions ≥ p_J.

D.4 Excess flow

• (e) Every non-last block of every W has e ≥ 1, i.e. η ≥ 0.
• A merged block has e ≥ k' ≥ 1.
• ρ's block and blocks created after the digestion have e = 0 while last and e = 1 once an overflow passes them.
• Counting does not change any η. On an overflow, the old last block gains 1 and stops being last.
• The eat removes h ≥ 1 leading blocks of the counted word. So W_{t+1}[q] is B_{q+h+1}, ρ's block, or a block created after the digestion. The last two kinds have η = 0.

(a) If S_{t+1}(q) > 0, then

S_{t+1}(q) ≤ S_t(2q+2) + 3(k_t + c_t) + T − 8 − 6q.

Proof. Let J = q + h + 1 ≥ q + 2. A positive suffix needs a merged block at position ≥ q, so J ≤ L. 1. Among B_J..B_L at most one is last, i.e. has η = e rather than e − 1. So S_{t+1}(q) ≤ Σ_{j=J}^{L} e(B_j) − (L − J). 2. By the mass bound this is ≤ S_t(p_J) + 3(k + c − p_J) − 3(L − J + 1) + 1 + T. 3. Use p_J ≥ 2J − 2 ≥ 2q + 2, L − J + 1 ≥ 1, and S nonincreasing (by (e)). ∎

(b) x_{t+1} ≤ S_t(0) + 3(k_t + c_t) + T − 1. - By (P1) applied after the digestion, x_{t+1} = e_cur + d' ≤ e(W_post[h−1]) + 1. - For h ≤ L, use e(B_h) ≤ Σ_{j ≥ h} e(B_j) and the mass bound. - Otherwise x_{t+1} ≤ 1.

(r) Resets. After a special residue, or an ordinary epoch with L_t = 0, the post-digestion word has at most one block with e = 0. So S_{t+1} ≡ 0 and x_{t+1} ≤ 1. The special residues have c = 0 (no W) and β ≤ τ: - '1' and t2 are in G, so β = 0; - '01' a z 1 → '11' a z 1 → t2 costs 2; - '10 00 010001' costs 11.

(c) Unrolling. Let Δ_s := 3(k_s + c_s) + T − 8, which is ≥ 0 when k_s + c_s ≥ 1. Apply (a) along q_0 = q, q_{i+1} = 2q_i + 2, i.e. q_i + 2 = 2^i(q+2). The chain stops at the first i with q_i ≥ k_{t−i} (there the suffix is 0), at a reset (r), or at epoch 3 (whose residue t2 is special). Since k_{t−i} ≤ κ_t:

S_t(q) ≤ n(κ_t, q)·max_{s<t} Δ_s, where n(κ, q) := max(1, ⌈log2((κ+2)/(q+2))⌉).

Compared with the first version, this uses the running maximum κ, not the current k. It also needs no condition on the epochs before t − ⌈log2 K⌉.

D.5 Value bound

• After digestion, m_post < 2^(L+4) (D.3).
• Counting adds at most one per bounce, and there are at most N_{t+1} − 2 bounces.
• E1g halves the value.
• E2g leaves m(W_{t+1}) = (m_eat + 1)/2.
• Since m(W) ≥ 4·2^k:

2^(k_{t+1}+3) ≤ N_{t+1} + 2^(L_t + 4), with L_t ≤ ⌊(k_t + c_t + 1)/2⌋ (D.2), and L_t = 0 after a special residue.

D.6 Constants along the orbit (closes the first version's open link)

Lemma C bounds c_t by the profile S_t. D.4(c) bounds the profile by the earlier k_s + c_s. A fixed point turns the two into one induction. For κ ≥ 0, define (check_proof.py: Gfix, gamma_k): - U(κ, q) := n(κ, q)·Δ(κ) and xmax(κ) := U(κ, 0) + Δ(κ) + 7, where Δ(κ) := 3G(κ) + T − 8; - Γ(k, κ) := the largest c with 3·2^(k+c) ≤ 9·2^k + A_k − 5, where A_k = 2U(κ,0) + Σ_{q=1}^{k−1} 2^q U(κ,q) (and A_0 = 0). This is Lemma C with S ≤ U(κ,·) inserted. - G(κ) := the least G ≥ κ with max_{k ≤ κ}(k + Γ(k, κ)) ≤ G when Δ is computed from this G. It is reached by iterating from G = κ. The map is monotone in G and in κ, so G(κ) is nondecreasing in κ, and so are Δ, U and xmax.

Orbit invariant. For every epoch t ≥ 3 the following holds: - (I1) Y_t is ordinary or special. - (I2) If ordinary: η ≥ 0, S_t(q) ≤ U(κ_t, q) and x_t ≤ xmax(κ_t). - (I3) c_t ≤ Γ(k_t, κ_t), hence k_t + c_t ≤ G(κ_t) (c = 0 if special). - (I4) N_t ≥ N_lo(κ_t) := 2^(κ_t+3) − 2^(⌊(G(κ_t)+1)/2⌋+4).

Proof by induction on t. - Epoch 3: κ = 0, special. - (I2) at t+1: from D.4(a)–(c) and (r). If L_t = 0 (in particular whenever k_t + c_t = 0, since a trigger needs a position), (r) gives S_{t+1} ≡ 0 and x_{t+1} ≤ 1 ≤ xmax. Otherwise k_t + c_t ≥ 1, so Δ_t ≥ 0. Use Δ_s ≤ 3G(κ_s) + T − 8 = Δ(κ_s) ≤ Δ(κ_{t+1}) by (I3) at the epochs s ≤ t. Also n(κ_t, q) ≤ n(κ_{t+1}, q), and x_{t+1} ≤ S_t(0) + Δ_t + 7 ≤ xmax(κ_{t+1}). (U(κ, q) is only used for q < k ≤ κ, so κ ≥ 1 and Δ(κ) ≥ 0 there; xmax(0) = 1.) - (I3) at t+1: Lemma C with (I2). - (I4) at t+1: if κ_{t+1} = κ_t, use N_{t+1} > N_t. Otherwise k_{t+1} = κ_{t+1}, and D.5 with L_t ≤ ⌊(G(κ_t)+1)/2⌋ ≤ ⌊(G(κ_{t+1})+1)/2⌋ gives it. - The induction also needs epoch t to finish, i.e. β_t ≤ N_t − 2. That is D.7.

D.7 Assembly and the threshold

By D.1 and D.2, a position q consumed at level j carries weight 2^j ≤ 2^⌊(q+3)/2⌋. By (P1), its cost is at most e_orig + 4: - x_j + 1 ≤ e_orig + 2; - a level-j strip costs e_cur + d + 3 ≤ e_orig + 4; - a level-1 strip costs e_orig + 5 ≤ 2(e_orig + 4).

The D6 terms and the end word give (2^L − 1) + 2^L τ ≤ 2^⌊(k+c+3)/2⌋(τ+1). So

β ≤ Bnd := x + 1 + Σ_{q < k + c} 2^⌊(q+3)/2⌋ (e_q + 4) + 2^⌊(k + c + 3)/2⌋ (τ + 1), with e_q := e_orig (0 for created positions).

Worst case. Write Σ_q w_q e_q = Σ_q (w_q − w_{q−1}) S(q) + const. The weights w_q are nondecreasing, so Bnd is largest at S = U(κ, ·), c = Γ(k, κ) and x = xmax(κ). Call the maximum over k ≤ κ Bnd_worst(κ). Under (I2) and (I3), Bnd_t ≤ Bnd_worst(κ_t).

Threshold. Let F := {κ : Bnd_worst(κ) + 2 > N_lo(κ)}. - Exactly, for κ < 160: F = {0, …, 11}. - With T = 5 and τ = 13: N* := max_{κ ∈ F} Bnd_worst(κ) + 2 = 14,796, attained at κ = 11.

For an epoch with N_t ≥ N*: - if κ_t ∉ F: β_t ≤ Bnd_worst(κ_t) ≤ N_lo(κ_t) − 2 ≤ N_t − 2 by (I4); - if κ_t ∈ F: β_t ≤ Bnd_worst(κ_t) ≤ N* − 2 ≤ N_t − 2.

Tail κ ≥ 64 (closed form). 1. G is small. Let ℓ = log2(κ+2) and γ = log2(5κℓ). Then G(κ) ≤ G' := κ + ⌊γ⌋. Indeed A_k ≤ 2^k U(κ,0) and U(κ,0) ≤ ℓ·3G', so 2^c ≤ 3 + ℓG' ≤ 5κℓ while G' ≤ 2κ. The fixed-point iteration therefore stays ≤ G'. 2. Bnd is small. With Σ_q e_q ≤ S(0) + κ: - Bnd_worst(κ) ≤ 2^((G+3)/2)·(2U + Δ + κ + 4G + 22); - 2U + Δ + κ + 4G + 22 ≤ 20κℓ; - so Bnd_worst(κ) + 2 ≤ 2^(κ/2)·128(κℓ)^1.5. 3. The subtracted term in N_lo is small. 2^(⌊(G+1)/2⌋+4) ≤ 2^(κ/2)·51(κℓ)^0.5. 4. Conclusion. Both together are ≤ 2^(κ+3) as soon as 2^(κ/2) ≥ 23(κℓ)^1.5. This holds at κ = 64 (4.3·10^9 against 1.8·10^5), and the ratio increases from there on.

check_proof.py checks both inequalities, and that the closed form dominates the exact value, for 64 ≤ κ < 160. It also checks G(κ) ≤ κ + γ for 16 ≤ κ < 160. So F = {0..11} for every κ.

D.8 Finite part

• Epochs with N_t < 14,796 (epochs 3 to 593, i.e. 591 epochs; epoch 594 has N = 14,819; printed by the checker as finite_part): the rules-only orbit is computed explicitly. It is the composition of the rules above, with no TM inside. None of these epochs has an unsafe eat or a word without a rule, and every one has β_t ≤ N_t − 2.
• The same orbit equals the TM left records to 10^11 steps: 517 epochs, N up to 12,668 (O2).
• The explicit check runs on to N = 400,000 (11,074 epochs) with every D-link verified (section 9). The nest-stage run reached N = 3.49·10^6 with no unsafe eat.

6. Initial segment

From c0 = 0^inf A> 0^inf, by direct simulation: - L(1, 0001) at step 28; - L(2, 0001000010001) at step 124; - L(7, 000010001) at step 304. The second epoch, K(1,3,1000010001) at step 137, eats at the non-G words 11000010010001 (step 213, giving K(4,1,00010010001) at step 228) and 00010010001, and does not halt.

From L(7, 000010001) (epoch 3) on, everything follows from the rules: R, then B/LP, then the eats, then L', then L.

7. Conclusion

By induction on t ≥ 3: - the TM reaches L(k_t, 000 Y_t) with Y_t ∈ H; - N_t = k_t + 1 grows by at least 1 per epoch; - Lemma D gives β_t ≤ N_t − 2 (jointly with the orbit invariant of D.6, which is carried along the same induction), so every eat of epoch t is at a G word (section 4); - the epoch ends at L(k_{t+1}, 000 Y_{t+1}).

Every epoch takes at least 3k + 7 ≥ 1 steps, so the sequence of left records is infinite and the machine never halts.

Why D0 is never read: - The only D-on-0 situations in the transducer are an F-turn two cells right of a 0, and E finding the pattern 010. - Every rule above is an exact run that avoids both. - The only uncovered situation is an eat at b = 1 on a non-G word (for example 11 z Dn(3) or 00 Dn(3), the unsafe states seen in observe). - Lemma D rules that out.

8. Lemma plan for Rocq

Nearest template: verify/FractalBEC.v, module tm10 (1LB0LF_1LC1LF_1RD1LB_---0RE_1RA0RE_0LA0RC). Mirrored, it differs from ours only in C1 (1RB vs our 0RE).

What carries over: - RInc ≈ RP0 (marker bounce l |> R(1+n) m r -->+ l <| R n (1+m) r, with w1 = 110, w0 = 00). Our RP0/RP1 are the same es + shift-rule proofs (W5/S1 and W2/S2). - Window rules W1–W10: es each. Shift rules S1–S3: ind n with one IH.

What does not carry over: - LInc and Ov (BinaryCounter_0 with 2-cell digits, whole-counter eat). Our counter has 3-cell blocks with exponents, z separators, a 4-stage tail and nesting. - The FractalBEC section therefore cannot be instantiated. We would copy its proof style, not its hypotheses.

Proposed files and lemmas: 1. Word type: blocks (d, e), tails s, nested H as an inductive type; enc : H → list sym. 2. LP_rule : ∀ w ∈ H, 011 C> enc w →+ <A 100 enc w' (or the d = 1 form), by induction on w (LP0, LP11, LPC recursive, LP5, LPT by es). 3. LP6 needs the epoch map. Define phi : nat → H → option (nat × H) (fuel-bounded, computable) and prove phi_sound (TM simulation of the abstract run, using B and the eats). LP6 is then phi_sound composed with the context lemma (bounce and E1g read only cells at or right of the marker, as an l-generic statement) and W10. Lemma P (D.0) gives an explicit fuel: the number of positions is bounded by 3·2^P ≤ 9·2^k + Σ 2^(q+1) η_q + e − 4, and each phase between eats is at most budget + 1 bounces. 4. epoch_step : Lemma D hypothesis → L t →+ L (t+1), and progress_nonhalt_cond with the invariant (I1)–(I4) of D.6 (residue ∈ H, the D.4 profile against U(κ, ·), the bound on x, k + c ≤ G(κ), N ≥ N_lo(κ)); κ is carried as part of the state. 5. Finite part: vm_compute of the abstract orbit for 591 epochs (N < 14,796) inside Rocq, using the computable phi. This is heavier than the first version's 150 epochs (which rested on the unproved c ≤ 1) but far below the nest stage's 40,112 threshold; the constants of D.7 (factor 2 slack in the τ term, the +4 per position) could be tightened if it matters. 6. The analytic part (D.4–D.7) is integer arithmetic plus induction; G, Γ, U and the threshold table are computable and can be checked by vm_compute for κ < 64, with the closed-form tail for κ ≥ 64. The hard pieces are the bookkeeping lemmas over a nested digestion: the front/positions abstraction of D.0 (Lemma P), and the itemized merged blocks of D.3.

Risk: the nested epoch map (D6 calls the epoch map) is new for busycoq. No existing file has a "bounce that runs a sub-epoch". Estimated effort: large.

9. Evidence (check_proof.py, seeds 1 and 2; data/check_proof_seed{1,2}.json)

• W1–W10, S1–S3: in random contexts, n ≤ 13.
• RP0/RP1: n ≤ 30 with random X and l, step formulas 8n+4 and 8n+7.
• LP rules:
• LP0: all r with |r| ≤ 10.
• LP11: all r with |r| ≤ 9.
• LPC and LP5: e ≤ 8 against G rests and non-G O rests, plus 100 large G words (exponents to 40).
• GI as their composition, against the G-level inc: 300.
• LPT: the 6 constant words.
• D6: the right pass (e ≤ 11, step formula 3e+14), and one TM bounce against the rules-only epoch map (250).
• B: in random left contexts, with the step formula and "never reads left of the marker" (500).
• Eats: E1g and E2g with a ≤ 400 and e ≤ 80 (600 each); E0 and Et1–Et3 for a ≤ 59.
• R: k ≤ 60 with random Y (200).
• H1: every word of an enumerated H sample (10,505 words: G with up to 3 blocks and exponents ≤ 2, all O forms, E*, 1–2 extra front blocks) has exactly one rule, its image is in H, and 700 are checked against a TM bounce.
• H2: every enumerated G word has an eat rule.
• I: initial segment exact (steps 28, 124, 304).
• O1/O2: rules-only orbit = TM left records (fresh Python run to 2e7 steps; stored C log to 1e11 steps, 517 records).
• D.0/D.3 end of digestion: an O word whose W has a block is never in G (random, 11,360 words for seed 1); from every O word over a bare tail and every E* word, LP reaches G by LP0/LP11/LPT steps only and ends in ρ ∈ {'', 1, t2, t3, 001, 101, 001000010001} (87 words). T = 5 and τ = 13 are computed from the end chains.
• Lemma D on the orbit: every epoch of the rules-only orbit to N ≥ 400,000 (11,074 epochs; special residues: 4 in G, 1 end word). Overflows are now counted everywhere: GI inside LP5/E2g/LPC, GI and the fast counting add_G inside D6 sub-epochs, and Et3. The first version missed the fast-counting ones.
• Lemma C, c_t ≤ Γ(k_t, κ_t), k_t + c_t ≤ G(κ_t);
• D.1 (exact), D.2, D.3, D.4(a)/(b)/(c)/(e)/(r), the bound on x;
• D.5, N_t ≥ N_lo(κ_t);
• β ≤ Bnd ≤ Bnd_worst(κ_t) and β ≤ N − 2.
• Observed on the orbit: c_t ∈ {0, 1} (7,137 / 3,937 epochs), β/Bnd ≤ 0.38. This is not used.
• Adversarial residues (Checkpoint B round 1): 1,504 per seed, plus 2 × 12,004 in a stand-alone stress run (check_proof.py --adv N, seeds 11 and 12; data/check_proof_adv_seed{11,12}.txt). Two thirds come from inside the invariant for random κ ≤ 16 (extreme or random profiles, all-ones suffixes, x up to xmax). One third are unconstrained, with η ≥ 0 and exponents up to 40.
• Checked: Lemma C, D.2, D.3, D.4(a)/(b)/(e), β ≤ Bnd, and c ≤ Γ, Bnd ≤ Bnd_worst for the in-invariant ones.
• 40 whole epochs per seed against the TM.
• Named cases: the skeptic's '11' z b(17) z b(1) z t3 (c = 2), '11' z b(8) z t1 at N = 100 (x_{t+1} = 17), the k = 3 case at N = 2917, and the k = 16 case (c = 4).
• Largest slack used: D.4(a) −5 against the bound −3 (T − 8); D.4(b) 2 against the bound 4 (T − 1); c up to 6.
• Threshold: exact table for κ < 160 (F = {0..11}, N* = 14,796), monotonicity of G and U, G ≤ κ + γ for κ ≥ 16, and the closed-form tail for 64 ≤ κ < 160.

Numbers from the latest full run are in the review log.

Review log

• 2026-10-10 (informal_proof stage, agent):
• First version. The bounce is now split into LP (word-local) and RP (region), which turns every word rule of the deepen/nest stages into an exact run built from 10 window rules and 3 shift rules:
  • D1/D3 are one rule (LP11);
  • D2/D4/HT and two tail steps are one rule (LP0);
  • HC is LPC;
  • D6 is proved: right pass, context-free sub-epoch, W10 exit.
• Lemma D: D.1–D.5 and D.7 are written from the rules. The new constants give N* = 2917, replacing 40,112 from the nest stage; the finite part is now about 150 epochs.
• Open: D.6 (c_t ≤ 1, checked on every epoch, argument only sketched). D.3's absorption bookkeeping at end words is folded into the +c+1 and +5 slack, not itemized. D.4(c) needs the epochs before t − ⌈log2 K⌉ to be in range; this is covered by the finite part.
• Checker: check_proof.py ALL PASS on seeds 1 and 2 (about 45 s each; data/check_proof_seed{1,2}.{log,json}).
• Confidence: high for sections 3–4 and for the mechanism; medium-high for Lemma D as written (one open link, and the D.3/D.4 bookkeeping deserves a careful second read at Checkpoint B).
• 2026-10-10 (Checkpoint B, skeptic round 1, agent):
• Fatal gap (D.6, c_t ≤ 1): correct. The invariant allows c ≥ 2: the skeptic's residues are reproduced in the checker, with c = 2 and c = 4, and up to c = 6 in the stress run. Replaced by Lemma C (D.0), proved from the rules alone:
  • the front and positions abstraction;
  • (P1), at most one extra unit per position;
  • (P2), at most e + 1 increments per front;
  • the potential Z = 2^f·V, which consumption never increases;
  • result: 3·2^(k+c) ≤ 9·2^k + Σ 2^(q+1) η_q − 5.
• D.2–D.7 are redone with c-dependent constants. The fixed point G(κ) makes "k + c ≤ G(κ)" part of the orbit induction (D.6). New N* = 14,796. The finite part below it (591 epochs) is the explicit rules-only orbit: the 1e11 TM log covers its first 517 epochs (N ≤ 12,668), and the checker's explicit run reaches N = 400,000.
• Major gap (D.4(b) false; D.3 formula incomplete): correct (TM-confirmed: x_{t+1} = 17 for '11' z b(8) z t1, N = 100). D.3 now itemizes e(B_j):
  • exact for j < L;
  • for B_L: bare-tail absorptions plus τ_end ≤ T = 5, tabulated per ending (E2g + '10' t2 chain 5, '10' t3 2, Et2 1+4, Et1 1+1, E0 2, Et3 chain 2).
  • A mass bound over suffixes of merged blocks gives D.4(a): S_{t+1}(q) ≤ S_t(2q+2) + 3(k+c) + T − 8 − 6q when positive, and D.4(b): x_{t+1} ≤ S_t(0) + 3(k+c) + T − 1.
  • With Et3 counted as an overflow, the skeptic's example has c = 2 and bound 21 ≥ 17.
• Major gap (checker undercounted overflows inside add_G): correct. The counter now also wraps add_G and Et3. The orbit's c-histogram changed from about 23% to 35.6% c = 1; c ≤ 1 still holds on the orbit, but the proof no longer uses it. Wording in sections 5 and 9 is corrected, and data/check_proof_seed{1,2}.* are regenerated.
• Minor (threshold mixed epochs): the threshold now uses the running maximum κ throughout:
  • D.4(c) unrolls against κ and stops at epoch 3 or at a reset;
  • (I4) gives N_t ≥ N_lo(κ_t);
  • Bnd_t ≤ Bnd_worst(κ_t);
  • the case split is on κ_t ∈ F;
  • closed-form tail for κ ≥ 64, so "every κ" is proved, not only κ < 120.
• Minor (D.3 "none of D1–D5 is in G"): replaced by the D.0 fact (an O word whose W has a block is not in G) and the list of tail coincidences, with an exhaustive check of the end words (ρ has at most one block).
• Minor (Φ termination): Lemma P bounds the positions of a lone sub-epoch, which gives termination and an explicit fuel (3.8, D.0, section 8).
• Minor (special residues): D.4(r): after a special residue (or L = 0) the next W has S ≡ 0 and x ≤ 1; special residues have c = 0 and β ≤ τ; checked.
• Checker: check_proof.py ALL PASS on seeds 1 and 2; stress run --adv 12000 on seeds 11 and 12 ALL PASS.
• Confidence: high for Lemma D as now written. What is left is a careful human read of D.0 (the front abstraction over a nested digestion) and of the D.3 itemization; both are checked on the orbit and on about 27,000 adversarial residues.