1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA (#28): non-halting argument (CONDITIONAL on L9; CRYPTID_CANDIDATE)

• Machine: 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA, viewer https://bbchallenge.org/1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA. Byte-exact on line 632 of data/holdouts/2026-10-07_778.txt. Sheet: Results row 1026, "Bell eats counter", no status or notes.
• Status (2026-10-11, end of the funded stage prove_l9): CRYPTID_CANDIDATE. This file does not prove that the machine runs forever, and the machine is not a kill.
• §4–§6 are proved on the abstract round system. The round rules themselves (§2) are validated against the machine by simulation, and are not yet proved.
• The one open link is L9 (§7): PC(U) < 2^(D+1) at every phi-eat whose word starts with a digit 1.
• §6 proves L9 along the orbit except after two kinds of epoch (the hard case H, and an S2 epoch with an S1 successor). §7 shows that no local invariant can close those cases. A translated counter-family from #10 satisfies the full state invariant, yet reaches an eat with an s block three epochs later, for every B checked (exact for B = 8..18 in this file's rules; TM-confirmed on #28's own table at B = 8).
• Relation to #10. #28 is #10 = 1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC mirrored and with its states renamed, started in #10's state E (§1). This is the relation #7 has to kill #30. #10 is a CRYPTID_CANDIDATE (machines/1RB0RF_1RC1RF_1LD1RA_---0LE_1LA0LE_0RA0LC/proof.md §5.8). The two orbits merge: #28's state at epoch 350,328 is #10's cascade state at t = 350,272 (§1). Our L9 is #10's Lemma X in different coordinates, so the cryptid verdict carries over.
• Notation: l q> r means the head is in state q and reads the first cell of r; l <q r means it reads the last cell of l. Exponents repeat words.

0. Picture in one paragraph

The tape is a binary counter W of 3-cell blocks on the left and tm10's unary run (blocks 011, with a 00 marker) on the right. Each round adds 1 to the counter and moves the marker one block left. When the marker reaches the counter, the machine eats. Two eat kinds (EAT1, EAT0z, the phi-eats) shift every counter block one cell right: 1 → f, 0 → 0, f → s. Read from the new phase, the old value is debris: a second number written in the f/0 blocks, with the s blocks as fillers. The next epoch's first increments carry through the debris and turn every s back into f (the flush). The machine is safe as long as every flush ends before the next eat (I3). The flush takes F = 2^(1+D_F) rounds, against an epoch of N rounds. Words that start with a digit 1 flush in time; words that start with f need L9. L9 bounds the weight of the filler blocks that pile up from flush to flush, and that weight is driven by exact carries PC = 2^D + (sparse).

1. The machine, and its conjugacy with #10

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

The only undefined transition is F reading 0. Every rule in §2 is an exact run that never executes it.

Conjugacy (scripts/conj10.py, scripts/conj10.json). Let σ map #28's states A, B, C, D, E, F to #10's E, A, B, F, C, D. For all 12 pairs (q, s), δ28(q,s) = (w, d, q') iff δ10(σq, s) = (w, -d, σq'). So #28 run from the blank tape is #10 mirrored, started in #10's state E. Lock-step simulation agrees for 3·10^6 steps.

Merge. #28's orbit and #10's orbit (from state A) differ at first: our epoch lengths are 2, 5, 6, 9, 10, 19, … and #10's are 2, 5, 6, 11, 12, 18, …. By epoch 350,328, our first-eat state is (n, c) = (4,193,605, [3,15,3,0,11,0,0,1]), which is #10's cascade state at its t = 350,272. The epoch map is the same, so from there on the two orbits coincide with an offset of 56 epochs. #10's skeptic run followed that orbit to 10^10 epochs with no unsafe eat; that run lives in #10's directory and is not re-run here.

2. Families and rules

Round start, with b the lowest counter cell: - RS(W,b,n,m) = 0^inf W b <E 11 (011)^n 00 (011)^m 0^inf - NM(W,b,n) = 0^inf W b <E 11 (011)^n 0^inf (no marker; written m = -1)

W is cut into 3-cell blocks from the right. Only four blocks occur: 1 = 100, 0 = 000, f = 010, s = 001.

• inc: binary +1 on the digits 1/0, MSB on the left, f skipped, overflow prepends 1.
• incC: the same in phase C, where f = 1, 0 = 0 and s is skipped; overflow prepends f.
• Y0 is Y with 1 → 0. phi: 1 → f, 0 → 0, f → s.
• Checks: scripts/validate.py (random W, b, n, m up to 60; scripts/validation.json) and scripts/template_check.py for R1–R3.
• Coverage: all 1,008,130 round transitions from the blank tape to 10^10 steps are predicted exactly (scripts/predict.py).

Initial segment. The first round start is NM([],0,1), at step 6.

What can go wrong. On words over {1,0,f} the rules are total and stay in the language (L0 below). A round start with no rule is an eat (n = 0) whose word still holds an s. So the machine never halts if (I3): no eat sees an s.

3. Notation for the epoch map

At a phi-eat, U is the s-free word before the shift (inc W for EAT1, W' for EAT0z), V = phi(U), and N is the new n, the epoch length in rounds. For U: - D = number of digit blocks; val(U) = its phase-0 value. - sigma(U) = Σ over the f blocks of 2^(digits right of the block). This is the debris weight. - PC(U) = val(U) + sigma(U); s(U) = sigma(U)/2^D is the normalized debris weight. - S1: U starts with a digit 1. S2: U starts with f. - L = ⌊log2 N⌋.

4. The flush (proved; scripts/flush_check.py, scripts/flush_random.py)

• L0. (I2) holds at every round start: no 1 lies left of an s. phi outputs no 1, and inc puts its 1 right of every remaining s.
• L1, flush counter. While s blocks remain, the part right of the rightmost s (with b) has phase-0 value t, the number of increments since the phi-eat.
• L2, flush time. F = 2^(1+D_F), where D_F = Q - popcount(X mod 2^Q), Q is the number of digits right of the leftmost f of U, and X = val(U) + Σ_{i<r} e_i 2^(p_i) over the f-runs right of the leftmost one. So F ≤ 2^(1+Q).
• L3, after the flush. The counter value is v = t = m. On U's digit positions, plus a new top position if needed, the f/digit pattern is binary PC(U), with bit 1 = f. The old f blocks stay f.
• L4. v(W,b) ≤ m at every later round start of the epoch.
• L5. S1 flushes in time: F ≤ 2^(1+Q) ≤ 2^D ≤ 2 val(U) ≤ N.
• L6. Every phi-eat by EAT0z flushes in time: N > m ≥ v ≥ 4 val(U) ≥ 2^(D+1) ≥ F.

Checks: 19,236/19,236 random abstract U; 256/256 flushes on the real machine; every flush to 10^10 steps.

5. The chain case (proved, given L9; scripts/chain_check.py)

For S2, write e for the leading f-run, Y = val + sigma - e·2^D, c = Y div 2^D and P = Y mod 2^D, so that F = 2^(1+zeros(P)). τ_k = 0 means epoch k ends with EAT1 at its first eat (it is uncut).

• C0. N_{k+1} ≥ N_k + 1.
• C1. τ_k = 0 ⟹ N_{k+1} = N_k + 1 = 2 val(U_{k+1}).
• C2. No two uncut epochs come in a row.
• C3 (uses L9). If epoch k has no overflow, then 2^(Z_k) ≤ N_k, where Z_k is the number of digits after the flush.
• C4 (uses L9). Every S2 word is f 1 … with c ≤ 2.
• C5. F ≤ N at every S2 phi-eat.

State invariant INV(U, N): - N ≥ 2 val(U); - S1 ⟹ L9; - S2 ⟹ the shape f 1 …, c ≤ 2, and either N ≥ 2^(D+1) or (N = 2 val(U) and P ≠ 0).

INV implies F ≤ N. One epoch maps INV to INV, except possibly for L9 at an S1 successor. Checks: exhaustive to 9 blocks (758,058 states), 40,000 random states, and 1,000/1,000 whole epochs on the real machine. Proofs are in notes.md, "Funded stage (2026-10-10, close_chain)".

So (I3) follows from L9 at every S1 phi-eat.

6. Debris-weight lemmas (proved this stage; scripts/l9_check.py)

Let U be S1 at a phi-eat with L9, and put X = PC(U). Let T be the top bit of X, q = popcount(X), and Z0 = T + 1 - q (the zero bits of X). Write W_post for the first s-free round start of the epoch, and U' for the next phi-eat word. Define: - g(X) = Σ_{1-bits i of X} 2^(zeros of X below i); - h(U) = Σ_{f blocks of U at p} 2^(zeros of X below p), where p is the number of digits right of the block.

W1 (debris never grows after the flush). At round starts after the flush, s(W) is unchanged by INC0 and by CARRY without overflow, exactly halved by an overflow, and never raised by an eat. Proof. - Increments change digits only. - An overflow prepends a digit, which leaves sigma alone and doubles 2^D. - EAT0f takes W = W' d f^k 1^j to W', so sigma(W') = (sigma(W) - k 2^j)/2^(j+1) and D(W') = D(W) - j - 1. Hence s(W') = (sigma(W) - k 2^j)/2^(D(W)) ≤ s(W). - EAT0z (W = W' 0 1^j) keeps s. - EAT1 is an increment. ∎

W2 (debris after the flush). sigma(W_post) = g(X) + h(U), and digits(W_post) ∈ {Z0, Z0+1}. Proof. By L3, the f blocks of W_post are the 1-bits of X on U's digit positions, plus U's own f blocks in place, and the digits of W_post are the 0-bits of X. A block's weight in W_post is 2^(number of 0-bits of X below it). The +1 is a counter digit that the flush itself may prepend. ∎

Lemma G (arithmetic). g(X) = Σ_j 2^(i_j - j) ≤ q·2^(T+1-q) ≤ 2^T, where i_0 < … < i_{q-1} are the 1-bits. Since i_j - j ≤ Z0, also g(X) ≤ X. Checked for every X < 2^20.

W3 (successor bound). If U' is S1, then s(U') ≤ sigma(W_post)/2^max(L, Z0+1). Proof. - No eat comes before the first eat, at which the counter holds N ≥ 2^L, so the word there has at least L digits and the same f blocks as W_post. - The pattern's top block, bit T of X, is an f, because X ≥ val ≥ 2^(D-1). So U' is S1 only if some digit sits above it. - Such a digit was prepended, either by the flush (the case digits(W_post) = Z0 + 1) or later. Either way the word has had at least Z0 + 1 digits with the same f blocks. - Then use W1. ∎

W4 (cases). Let U and U' both be S1. Then: - (a) T = D-1 ⟹ s(U') < 1. Here g ≤ 2^(D-1) by Lemma G, h ≤ sigma, and sigma = X - val < 2^D - 2^(D-1), while L ≥ D. - (b) T = D and L ≥ D+1 ⟹ s(U') ≤ (2^D + sigma)/2^(D+1) = 1/2 + s(U)/2. - (c) X = 2^D ⟹ s(U') ≤ 1/2 + s(U)/2 ≤ 3/4. Here Z0 = D, h = sigma and sigma = 2^D - val ≤ 2^(D-1). - (H) T = D, L = D, q ≥ 2: the hard case. W3 only gives s(U') ≤ 2^(-popcount(Y)) + (g(Y) + h(U))/2^D with Y = X - 2^D, and that can exceed 1.

W5. s(U') < 1 implies L9 at U', since PC = val + sigma < 2^D + 2^D.

Reduction. Call an S1 phi-eat good if s < 1. By W4(a)–(c) and W5, a good S1 phi-eat whose epoch is not in case H has a good S1 successor, which satisfies L9. Starting values: s = 0 at the first phi-eat, U = 1. So L9 holds at every S1 phi-eat of the orbit unless an earlier epoch is in case H, or is an S2 epoch with an S1 successor, and leaves s ≥ 1 behind.

Checks (l9_check.py reduce 100000 2810): on 100,000 random S1 states with L9 (up to 31 blocks; N = 2 val, N < 2^(D+1), and N ≥ 2^(D+1)), W1, W2, W3, W4(a)–(c) and W5 have 0 violations. Of the S1 successors of case-H states, 1,836 of 34,699 have s ≥ 1.

7. L9 is open, and cannot be closed by a local invariant

L9 (OPEN). At every phi-eat of the orbit whose word starts with a digit 1, PC(U) < 2^(D+1). By §6, this is equivalent in practice to:

Lemma H (OPEN). On the orbit, every case-H epoch and every S2 epoch whose successor is S1 leaves s < 1.

Case H needs 2^D < val + sigma < 2^(D+1) and N < 2^(D+1). On the orbit, N < 2^(D+1) essentially means N = 2 val, i.e. right after an uncut epoch. W3's bound is then 2^(-popcount(Y)) + …, which is large only when Y = val + sigma - 2^D is sparse. That is an exact-carry coincidence between the counter value and the debris weight. This is the same kind of event as #10's cascades and super-cascades (P = 2^B).

A counter-family that satisfies the invariant (scripts/family10.py, scripts/family10.json). #10's family is σ0(B) = (n, c) = (3·2^(B-2) - 7, [3, 0^(B-6), 10, 0, 2]). Under the conjugacy it is #28's eat state RS(W, n mod 2, 0, n), where W holds n >> 1 and has c_j f blocks just right of its j-th digit. With #28's own rules, for every B = 8..18: - the first phi-eat satisfies all of INV, L9 included (PC/2^D = 1.875), with s ≈ 1.13–1.15; - one epoch later L9 fails (PC/2^D = 2.125), and it fails again at the next phi-eat (PC/2^D = 2.0); - three epochs later the word starts with f but has the wrong shape, and its flush is late (B = 8: F = 256 > N = 194). The next eat sees an s block, and no rule applies.

The phi-eat lengths for B = 8 are N = 186, 191, 192, 194, the same eats #10 reports for its TM.

TM confirmation on #28's table (scripts/tm_family.py 8, scripts/tm_family_B8.json). - Started from NM(phi U0, 0, 186), the real machine matches the abstract rules on all 779 round starts up to that eat. - At round 779 it meets the eat with an s block (W = fs11f100fffffff, b = 1, m = 206). - It then leaves the block alphabet for one round (a 110 block) and recovers. Phi-eats resume at N = 207, 208, 222, 233, … with no halt in 2.8·10^6 steps.

So the rule-level safety condition can fail, and here the machine survives it. That is not usable for a proof, but it means a failure would not by itself be a halt.

Consequence. - No invariant that the family's first state satisfies can prove L9. That includes INV and every strengthening that does not restrict s. - The stronger invariant s < 1 is preserved everywhere except in case H and S2 → S1 (§6), and case H breaks it on random states (1,836 times). - So a proof would have to show that the orbit's exact values never produce the coincidence pattern. #10's funded stage showed that the entry patterns form an infinite family and do not close into a finite list (#10 proof.md §5.8). By ground rule 6, #28 is flagged CRYPTID_CANDIDATE, with the same verdict as #10.

8. Heuristic evidence for non-halting

• The orbit (l9_check.py blank 400000, data/l9_blank_400k.json): 0 violations of INV, L9, F ≤ N or s < 1 at S1. Case H occurs 544 times. Max s at S1 is 0.875 (epoch 22), max s after case H is 0.875 (epoch 21), and max s after S2 → S1 is 0.0145. The 1,000,000-epoch run of the last stage (data/chain_blank_1M.json) had 0 violations of C1–C5, L9 or F ≤ N, and max PC/2^D = 1.5625 (epoch 22).
• The merged orbit: #10's skeptic run to 10^10 epochs of the shared orbit found no unsafe eat (#10 proof.md §5.3, §5.6).
• Slack: in the first 100,000 epochs, case H occurs 319 times. Its W3 bound is at most 0.754 after epoch 100 and 0.501 after epoch 1,000. Large s (0.688 at epoch 62,443) comes with a dense Y, and there the bound is 0.0009.
• The machine survives the family's unsafe eat (§7).

9. Evidence table

10. Rocq plan (cryptid protocol)

Formalize the rule layer only, AntiHydra-style: the round rules of §2 as -->+ lemmas over RS/NM with block lists, CARRY_S as a relation on lists (as BECv7's RIncs), and the epoch map. Non-halting stays conditional on L9 (equivalently Lemma H). Low priority, as for #10.