/machines/1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA/notes.md · raw

1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA

Status: CRYPTID_CANDIDATE (funded stage prove_l9, 2026-10-11): L9 cannot be closed by a local invariant; #28 is #10 started in E, and the two orbits merge; see decision.json Class guess (agent / Dennis): Bell eats counter. It is BECv1 tm10 with E1 = 1LB: a binary counter in 3-cell blocks with fillers, plus tm10's unary run and marker. Eats shift the counter one cell (phase debris). / – Spreadsheet notes / Discord thread: Results row 1026, "Bell eats counter", no status/notes/sources/done-by. Also listed in the Classifications tab ("Bell eats counter" column). Not in links, strikethrough, levels, categories, archive, discarded, unverified tabs, nor in either data/discord list. No claim, so it is fair game. Byte-exact: line 632 of data/holdouts/2026-10-07_778.txt. Viewer: https://bbchallenge.org/1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LB_---0RA Pool: #28 (reports/targeting.md §4.3), follow-on to #7 (…_1RF0LA_---0RA, E1 differs). We only read #7's directory; we never write there. Exact trajectory twin: 1RB0RA_1LC0LD_1LE1LD_0LB0RF_1RA1LB_1RA---. Both give identical pos/lo/hi/nonzeros at 1e9 (gate-excluded: Eqv mention).

Observation

A round is INC + marker one block left, about 8n+16 steps. - Counter = binary in 3-cell digits. The carry walk goes left one cell per state: E reads a digit, then B and C read the two filler cells. - E1 = 1LB, B0 = 1LC, C0 = 1LE: so 001<E -> <E111, a digit 1 carries. - E0 stops the carry, and A sweeps back right clearing the 1s. - A block 010 is walked as B0 C1 D0, so carries skip it (filler). - This is where tm10's 1-cell digit (HL2: E1 = 1LE) changes. - Eats. When the marker reaches the counter (n = 0), the case depends on b and the low end of W (EAT0f / EAT0z / EAT1). - EAT0z and EAT1 absorb the marker. They also move every counter block one cell right: phi: 1->f (100->010), 0->0, f->s (010->001). The marker is then reborn at the right end (BIRTH), and the next epoch lasts about n = m+1 rounds. - Read from b in phase 0, a phi-shifted word reads f as filler, 0 as digit 0 and s as a phase shift. So a new counter starts at 0 in the low part, and the old value sits left of the first s as debris (phase C: f=1, 0=0, s=filler). - A carry that reaches an s runs a second pass (the A clean-up hits a 0 and restarts a walk, then an E-walk crosses the unary and back). The net effect is CARRY_S: X s Y -> inc(incC X) f Y0, recursive if inc meets another s. - Epochs late in the run (1e10): about 3,800 rounds each, unary growing by 1-4 blocks per epoch. W has about 20 blocks, e.g. 1 1 1 0 1 1 0 1 1 f f f 0 f…. The eats seen are EAT0f 498, EAT1 495, EAT0z 73.

Candidate rules

All of them are validated by direct simulation from random concrete instances. Random W over {1,0,f} (INC0/BIRTH also with s; CARRY_S with Z over {f,0,s}, Y over {1,f}), random b, n, m up to 60. Script: scripts/validate.py, results in scripts/validation.json. The micro rules come from scripts/template_check.py (scripts/template_check.json).

rule from -> to passed
R1 A-sweep (=HR1) l A> 011 r -> l 010 A> r (5 steps per block) 25/25
R2 marker (=HR2) l A> 011 00 011 r -> l <B 00 011 011 r 25/25
R3 B-sweep (=HR3) l 010 <B r -> l <B 011 r 25/25
INC0 RS(W,0,n+1,m) -> RS(W,1,n,m+1), 8n+16 steps 100/100
CARRY RS(W,1,n+1,m) -> RS(inc W,0,n,m+1). inc: from the right, f skip, 1->0, 0->1 stop, overflow prepends 1 100/100
CARRY_S at an s: X s Y -> inc(incC X) f Y0. Y in {1,f}*, Y0 = Y with 1->0; incC: f=1, 0=0, s skipped, overflow prepends f 200/200 (S1 special case X = Z f: incC(Z) 1 f Y0, 100/100)
BIRTH NM(W,0,n+1) -> RS(W,1,n,1), 8n+16 steps; BIRTHC NM(W,1,n+1) -> RS(inc W,0,n,1) (never fires from blank) 200/200
EAT0f RS(W' d f^k 1^j,0,0,m) -> RS(W',d,k-1,m+2+j), k >= 1, d in {0,1} 100/100
EAT0z RS(W' 0 1^j,0,0,m) -> NM(phi W',0,m+2+j); W = 1^j: W' empty 200/200
EAT1 RS(W,1,0,m) -> NM(phi(inc W),0,m+1) 100/100

Coverage from the blank tape. Scripts: scripts/predict.py on scripts/rounds_1e10.tsv, written by scripts/dump_rounds.py 1e10, about 5 min. - Init: the first round start is NM([],0,1) at step 6. - After that, all 1,008,130 round transitions to 1e10 are predicted exactly by the rules above: 100.0000 %, 0 mismatches. - By rule: INC0 503,071; CARRY 503,424, of which 1,293 are CARRY_S; BIRTH 569; EAT0f 498; EAT1 495; EAT0z 73. - Nothing is left uncovered.

Invariant facts on the blank run (to 1e10): - (I1) W only ever uses the blocks {1,0,f,s}. - (I2) No 1 lies left of an s (0 / 7,246 round starts with s). - (I3) No eat ever sees an s (0 / 1,066 eats).

On words satisfying (I1)+(I2), inc/incC are total and stay in the language (argument sketch in the strategy below). The eat rules need (I3).

Flush slack (scripts/slack.py): the epoch counts rounds from the end of one eat to the next. The debris is gone after a fraction of the epoch: - worst 0.44 (the epoch at step 664); - worst 0.107 after 1e9; - median 0.005.

Fuzz (scripts/fuzz.py): - Reachable-like starts, W = (debris over {f,0,s}) s (counter over {1,0,f}), random b/n/m, stopping when a word leaves the alphabet: 300 samples, 13,651 rounds, 0 halts, 0 mismatches. - Every off-alphabet word (102) comes from an eat with s present. That is exactly what (I3) excludes. - Continued past the alphabet: 26 halts in 1,200 samples (random + reachable-like). So (I3) is necessary, and the invariant must carry it.

Template check

Nearest proved neighbour: verify/BECv1_6x2_solved.v tm10 (line 88), 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF1LE_---0RA, with E1 = 1LE vs our 1LB. Its proof is solve_BECv1 with cert B A E A [0] [1] [1] [0] [1] [0;1;1] [0;1;0] [0;0] [] [] [0;0] [1] [1;0;1;1;0;1;1] [0;1;0;0;0] 1 0 0 on the BECv1.v Section template. - I simulated our TM on every cert hypothesis from random l/r: 10/11 hold (HL1, HL3, HL4/5, HR1-3, HE0-3; 25/25 each). HL2 fails 0/25. As a control, tm10 itself passes 11/11. - HL2 is the 1-cell binary carry. With E1 = 1LB our carry goes through B and C, so the digits are 3 cells apart, there are fillers, and eats shift the counter. - Applies: partly. The unary half (RDec, HE0-HE3 shapes) carries over. LeftBinaryCounter (positive -> d0/d1 cells) and EatDigit/BigStep do not; tm10 only ever eats a 0-digit (Counter(2k)), while we have three eat cases plus debris. - Structural template for the counter: verify/BECv7.v. It has an inductive RIncs carry relation over lists of 3-cell blocks 110/000/100 (toRC), a canonical shape invariant and progress_nonhalt_cond. Our counter is the same kind of object: a block list with a mutually recursive carry (inc / incC). - #7 (E1 = 0LA) has a different counter (swept tokens, stale-1 cascades), so its rules do not transfer. Its closure stage found that no bounded k-gram/CTL window works there.

Cryptid check (ground rule 6)

Not cryptid-like: - Every round is one of 6 local block rewrites over a 4-letter alphabet, and the rules are exact on all 1e10 rounds. - The counter arithmetic only chooses which eat fires: b and the trailing digits at the moment the marker arrives. - Every eat branch is validated non-halting on s-free words. - The one quantitative condition is (I3): the debris is flushed before the marker returns. That is a size bound (about 2^(digits right of the leftmost s) vs the epoch length, about the unary length), not a parity or Collatz condition, and it holds with large slack. - No halt to 1e10.

Checkpoint A (Dennis)

(open: see card.html Q1-Q3 and decision.json)

Informal proof

(not started: med confidence, waiting on the decision)

Plan for proof.md: - (1) the rule table above, with step counts; - (2) the invariant: (I1)+(I2) as a regular language of W, plus (I3) via a flush lemma. The lemma bounds the number of rounds to clear all s blocks by the length of the phase-0 part right of the leftmost s, and compares that with the epoch length m+1. The epoch length is the unary length, which only grows. - (3) closure of the language under every rule (inc/incC total on it); - (4) init (6 steps) and progress_nonhalt_cond.

Formalization log

(none yet)

Outcome

CRYPTID_CANDIDATE (2026-10-11, stage prove_l9). The chain case is closed given L9 (C0-C5), and L9 is reduced to the hard case H (W1-W5). But L9 cannot be closed by a local invariant: #10's counter-family, translated, satisfies INV and still reaches an eat with an s block. #28 is #10 (CRYPTID_CANDIDATE) mirrored and started in E, and the orbits merge by epoch 350,328. proof.md is the conditional write-up.

Files

Decision (2026-10-10, auto-applied)

Question: Fund one stage for the flush lemma and proof.md (hand route, BECv7-style carry relation), run a native CTL search first, or park? Answer: flush_proof (One stage: prove the flush lemma informally, then write proof.md (rule table, invariant, closure)). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was at lunch). Override any time.

Funded stage (2026-10-10, flush_proof)

What was done. I worked out the flush exactly on the abstract round system (the 9 validated rules), proved it for every case but one, and narrowed the open part to one arithmetic case. Stop rule applied: no clean bound covers that case yet, so proof.md is not written. - New scripts: scripts/flush_check.py (epoch simulation with lemma checks; exact = round by round, fast = flush round by round, then each sub-epoch as one arithmetic jump) and scripts/flush_random.py (random instances, writes scripts/flush_random.json). - Data: data/flush_fast_200k.json.

Notation. - At a phi-eat (EAT1 or EAT0z), U is the s-free word before the shift: inc W for EAT1, W' for EAT0z. Then V = phi(U), and N is the new n (the epoch length in rounds). - d = number of digit blocks (0/1) of U; val(U) = its phase-0 value (f skipped); v(W,b) = 2 val(W) + b. - The f-runs of U are (e_i, p_i), where p_i = digits right of run i. r is the leftmost run, Q = p_r. - X = val(U) + sum_{i<r} e_i 2^p_i, and PC = X + e_r 2^Q.

Lemmas (short proofs, all checked below): - L0. (I2) holds at every round start: phi outputs no 1, and inc puts its 1 right of every remaining s. So incC only ever sees {f,0,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. - Proof: it starts at 0, since phi outputs no 1. CARRY_S, unrolled over a run of e s blocks, is X' s^e Y -> inc(incC^e X') f^e Y0. inc puts its 1 at the lowest 0 of the segment just left of the run, or recurses into the next run, which is bit position t either way. - L2, flush time. F = 2^(1+D_F), with D_F = Q - popcount(X mod 2^Q). So F <= 2^(1+Q). - Proof: in phase C the non-s blocks of V read as U's digits. Clearing run i adds e_i at bit p_i, and inc and Y0 leave the phase-C reading unchanged. So the digits right of the leftmost run when it clears are the zero bits of X mod 2^Q, and by L1 it clears at t = 2^(1+D_F). - L3, after the flush. v(W,b) = t = m. The filler/digit pattern on U's digit positions (plus any new top) is binary PC (1 = f), and the old f-runs stay f. - L4. v(W,b) <= m at every later round start of the epoch. INC/CARRY add 1 to both. EAT0f gives v' = 2 val(W') + d < v and m' = m + 2 + j. - L5, generic flush bound. If U starts with 1: F <= 2^(1+Q) <= 2^d <= 2 val(U) <= N. - For EAT1: 2 val(U) = v + 1 <= m + 1 = N. - For EAT0z: N >= 4 val(U). - L6. At an EAT0z phi-eat, N > m >= v >= 4 val(U) >= 2^(d+1) >= F, whatever U starts with. - L7, leading digit. If U_k starts with 1, then U_{k+1} has leading digit 1. After the flush, the capacity right of the leading f is C = 2^(1+zeros(PC)) <= 2 val(U_k) <= N_k, unless PC = 2^d exactly ("top exact carry"). In that case t still reaches C/2 = 2^d <= N_k, so the digit under the leading f is 1, and EAT0f right-shifts keep it. - L8. U_{k+1} starts with f only after an epoch with no overflow. When U_k started with 1, that requires a top exact carry.

Case analysis when U_k starts with f at an EAT1 (d = d_k): - (iii) X mod 2^d != 0: F <= 2^d <= N. - (iv-1) X = 0 mod 2^d ("bottom exact"), epoch k-1 had an EAT0f, and U_{k-1} started with 1: N_k > N_{k-1} >= 2^(d_{k-1}) >= 2^(d_k+1) >= F. - (iv-2) Bottom exact, epoch k-1 had no EAT0f, and U_{k-1} started with 1: impossible. The runs of U_k are those of U_{k-1} at the same positions and val(U_k) = (N_{k-1}+1)/2, so bottom exact forces N_{k-1} = 2 val(U_{k-1}) - 1, which contradicts L4. - (iv-3) U_{k-1} also started with f (a chain): OPEN. L7 inside a chain is open too. - Sketch for closing it: the chain's top run has e = 1, and the carry floor(X/2^d) is at most 1 at the chain's first step (because sum_lower = 2^d - val(U_{k-1}) < 2^(d-1)). That bound has to be carried along the chain.

Checks. - Exact mode against rounds_1e10.tsv (567 epochs, 1,004,198 rounds identical, 0 mismatches): - L1-L5 hold at every round and phi-eat. - U never starts with f. - 8 top exact carries; 1 epoch without overflow (step 314), rescued by an EAT0f and the EAT1's inc. - Fast mode (identical to exact mode on those 567 epochs): 200,000 epochs, 2.2e11 rounds (far past 1e10 steps). - 0 lemma violations, 0 s at an eat. Worst F/N is 0.505 (epoch 1115); on the 1e10 run it is 0.444. - U starts with f in 4 epochs: 1115, 1116, 2061 and 2062, which are two chains of length 2. - Bottom exact occurs twice: 1115 is case iv-1 and 2061 is an EAT0z (L6), both at F/N 0.505. - Case iv-3 never occurs. 17 top exact carries in all. - Random instances (flush_random.py 20000 300 2810): - Abstract level, 19,236 random U with an f (up to 24 blocks): L1, L2 and L3 hold 19,236/19,236. - TM level, 256/256 random small U: the real machine's flush takes exactly F rounds and ends in the predicted word.

Still open. - The chain case: (iv-3), plus L7 for a step whose U starts with f. It is one narrow arithmetic case: a phi-eat whose word starts with f right after another one. Chains of length 2 occur twice from blank in 200k epochs (epochs 1115-1116 and 2061-2062, flush F/N 0.002 at the second step), but the bad sub-case iv-3 never does. - proof.md and the formal side are not started. - Confidence stays med, but the gap is now one stated case, not the whole flush lemma.

Decision (2026-10-10, auto-applied, round 3)

Question: Fund one more stage to close the chain case and then write proof.md, write proof.md now with the chain case as a stated open lemma, or park? Answer: close_chain (One stage: prove the chain case (two phi-eats in a row whose word starts with f), then write proof.md). auto-applied: Claude's recommendation, under Dennis's standing instruction 'do your recommendations and continuously orchestrate' (2026-10-10, while he was away). Override any time.

Funded stage (2026-10-10, close_chain)

What was done. I closed the chain case on the abstract round system. Every phi-eat whose word U starts with f now flushes in time, chains of them included. The proof needs one bound on words that start with 1 (L9 below). Last stage's L7 already used L9 without stating it. L9 holds at every phi-eat checked, but it is not proved. So the open part moved from the chain case to L9. proof.md is not written; the stop rule and the scope of this stage put it in the next stage. - New script: scripts/chain_check.py. Its modes are blank, exh, rand, chainrand and tm. - Data: data/chain_blank_1M.json, scripts/chain_exh.json, scripts/chain_rand.json, scripts/chain_chainrand.json and scripts/chain_tm.json.

Notation (new). - S1: U starts with a digit 1. S2: U starts with f. - sigma(U) = sum over the f blocks of 2^(digits right of the block). PC = val + sigma, the same PC as in L3. - For S2, e is the leading f-run. Y = val(U) + sigma(U) - e 2^D, c = Y div 2^D and P = Y mod 2^D. - By L2, F = 2^(1+zeros(P)), with zeros counted over D bits. - Bottom exact means P = 0. - Z_k is the number of digits right after flush k. "Overflow in epoch k" means a new top digit appears. - tau_k = 0 when epoch k ends with EAT1 at its first eat. tau_k >= 1 when digits are cut, by an EAT0f or by a closing EAT0z.

Lemmas (proved by hand on the abstract system, by induction on k, assuming F <= N for earlier phi-eats): - C0. N_{k+1} >= N_k + 1. At the first eat m = N_k, an EAT0f only adds, and N' = m+1 or m+2+j. - C1. tau_k = 0 implies N_{k+1} = N_k + 1 = 2 val(U_{k+1}). At the first eat v = m = N_k with b = 1, and U = inc W. - C2. tau_k = 0 implies tau_{k+1} >= 1. N_{k+1} is even, so the first eat of epoch k+1 has v = m = N_{k+1} and b = 0, which makes it an EAT0f or EAT0z. So two uncut epochs never come in a row. - C3, capacity. If epoch k has no overflow, then 2^(Z_k) <= N_k. - U_k in S1: Z_k <= D_k by L9, because a number below 2^(D+1) with a 1 bit has at most D zeros. Also 2^(D_k) <= 2 val(U_k) <= N_k. - U_k in S2 with c = 1: the word after the flush is f 1 f ... and Z_k = 1 + zeros(P_k). So 2^(Z_k) = F_k <= N_k. - c in {0, 2}: the word after the flush starts with a digit 1 (1 f ... or 1 f f ...). So U_{k+1} is in S1 and C3 is not needed. - C4, shape. Every S2 word is f 1 ...: one leading f, then the leading digit 1, with c <= 2. - From S1, no overflow plus L9 force PC = 2^D (a top exact carry). The word after the flush is then f followed by U's own pattern: the same f blocks, with the digits holding the counter. - The counter passes N_k >= 2^(D_k) during the first N_k rounds, so the top digit is 1. - Cuts only remove the bottom, so it stays 1. - sigma_low(U_{k+1}) <= sigma(U_k)/2^tau < 2^(D_{k+1}), so c <= 1. - From S2 with c_k = 1, the word after the flush is f 1 f ..., so U_{k+1} = f 1 f .... - No overflow together with N_k >= 2^(D_k) forces zeros(P_k) to be D_k - 1 or D_k. - So sigma_low(U_{k+1}) <= 0.75 * 2^(D_{k+1}) when P_k = 0 (c <= 1), and <= 2 * 2^(D_{k+1}) when P_k = 2^q (c <= 2). - C5, the chain case. F_{k+1} <= N_{k+1} whenever U_{k+1} is in S2. - tau_k >= 1: F_{k+1} <= 2^(1+D_{k+1}) <= 2^(Z_k) <= N_k < N_{k+1}, by C3 and C0. - tau_k = 0 and U_k in S1: this is the old iv-2 argument. Y_{k+1} = val(U_{k+1}) - val(U_k) mod 2^D, and val(U_{k+1}) = (N_k+1)/2 > val(U_k). So the word is not bottom exact, and F <= 2^D <= 2 val = N. - tau_k = 0 and U_k in S2 (old iv-3): - By C2, tau_{k-1} >= 1, so N_k > N_{k-1} >= 2^(Z_{k-1}) >= 2^(D_k+1). - No overflow then forces P_k = 0, which gives Y_{k+1} = 2^(D_{k+1}) + val(U_{k+1}) - val(U_k). - Also val(U_{k+1}) >= 2^(D_k) > val(U_k), so the word is not bottom exact. - State form, used for the exhaustive checks. INV(U,N) says: - N >= 2 val(U); - S1 implies L9; - S2 implies 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.

Open: L9, the S1 bound. PC(U) < 2^(D+1) at every phi-eat whose word starts with 1. - C3 and C4 use it, and so did last stage's L7. - It holds on the blank run: max PC/2^D = 1.5625 (epoch 22) over 1,000,000 epochs, and at most 1.4994 after epoch 100 (200k-epoch scan) - It is not closed by INV alone. Small hand-made words break it. For example 1 f 0 f with N = 5 gives 1 f 1 f f f, where PC = 2^(D+1). So does an S2 word with c in {0,2} and many low f's. - So the proof needs an invariant that ties sigma of the word after a flush to N. The needed form is sigma(after flush k) < 2^(floor(log2 N_k)), less what the counter holds. It holds with slack on the run (epoch 62442 is the tightest case seen) but is not proved.

Checks (all on the abstract rules unless marked TM): - Blank run, chain_check.py blank 1000000 (N reaches 1.26e7): - 0 violations of C1-C5, L9 or F <= N. - 337,508 uncut epochs (tau = 0), never two in a row. - 6 S2 phi-eats in 3 chains of length 2: epochs 1115-1116, 2061-2062 and 350330-350331. - Each chain opens with a bottom-exact word that has N >= 2^(D+1) (F/N 0.505, 0.505, 0.500). It closes with a short flush (F = 16, 32, 64), then an overflow. - Worst 2^Z/N over the 6 epochs without overflow: 0.506. - Exhaustive, chain_check.py exh 9 40: every U with up to 9 blocks, each with 41 values of N near 2 val(U) and near 2^(D+1). - 758,058 states satisfy INV; one epoch each. - Of these, 2,985 are S1 -> S2 and 3,512 are S2 -> S2 transitions. - 0 breaks of C1, C2, C3, C5 or F <= N, and the S2 part of INV is never broken. - The only breaks are L9 at an S1 successor: 7,880, all from small hand-made words. - Random, rand 20000 2810: words of up to 24 blocks. 0 chain-lemma breaks; L9 breaks 1,247. - Chain range, chainrand 20000 2811: S2 words built to sit in the chain-continuing range (L9 breaks at S1 successors: 9,909, from the f-heavy sampling). - 6,262 have P = 0 with N >= 2^(D+1), 6,803 have P = 2^q with N = 2 val, and 6,935 have P = 2^q with N >= 2^(D+1). - This gives 3,345 S2 -> S2 epochs, all of them inside INV. 0 chain-lemma breaks. - TM level, tm 1000 2812: the real machine runs one whole epoch from NM(phi U, 0, N), for random small U and N <= 48. - 1,000/1,000 end in exactly the predicted next phi-eat: 553 S1, 372 S2 and 75 other f-start words. - 37 degenerate draws were skipped. In those, the word is eaten down to f^k 1^j, which uses the untested "d from 0^inf" EAT0f branch. That never happens on the blank run. - I fixed a helper bug along the way. For W = 1^j at EAT0z, the U cut must be empty. chain_check.py has the fix. flush_check.py has the same slip but only uses it for the flush prediction, so its results stand.

Still open. - L9, stated above. - proof.md and the formal side. - The degenerate small-word edge (EAT0f with d from 0^inf) has to be excluded in proof.md. It cannot happen once the word has digits above the eaten run. - Confidence stays med. The chain case is closed, but it rests on L9.

Decision (2026-10-11)

Question: Fund one more stage to prove L9 (PC < 2^(D+1) for words that start with 1) and then write proof.md, write proof.md now with L9 as an open lemma, or park? Answer: prove_l9 (One stage: prove L9, then write proof.md). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, prove_l9)

What was done. I tried to prove L9 on the abstract round system. I proved it everywhere except in one arithmetic case (the hard case H) and at S2 -> S1 steps. I then found why no local invariant can close those: #28 is #10 mirrored and started in #10's state E, and #10's counter-family breaks L9 and the flush in #28's own rules. Outcome: CRYPTID_CANDIDATE, the same verdict as #10. The stop rule applies, so proof.md is written with L9 as the one open lemma (conditional, flagged). - New scripts: scripts/l9_check.py (modes arith, reduce, blank, escape, perturb), scripts/conj10.py, scripts/family10.py, scripts/tm_family.py. - Data: scripts/l9_arith.json, scripts/l9_reduce.json, scripts/l9_escape.json, scripts/conj10.json, scripts/family10.json, scripts/tm_family_B8.json, data/l9_blank_400k.json.

Notation. - s(U) = sigma(U)/2^D is the normalized debris weight. - X = PC(U), with top bit T, popcount q and zero bits Z0 = T + 1 - q. L = floor(log2 N). - g(X) = sum over the 1-bits i of X of 2^(zeros of X below i). - h(U) = sum over U's f blocks at p of 2^(zeros of X below p).

Proved (proof.md §6). U and U' are consecutive S1 phi-eat words, and L9 holds at U. - W1. After the flush, s never grows. Increments keep it, an overflow halves it exactly, and EAT0f, EAT0z and EAT1 do not raise it. - W2. sigma(W_post) = g(X) + h(U), and digits(W_post) is Z0 or Z0 + 1. - Lemma G. g(X) <= q 2^(T+1-q) <= 2^T, and g(X) <= X. - W3. s(U') <= sigma(W_post)/2^max(L, Z0+1). - W4. Three cases give a bound: - (a) T = D-1 gives s(U') < 1. - (b) T = D and L >= D+1 give s(U') <= 1/2 + s(U)/2. - (c) X = 2^D gives s(U') <= 3/4. - (H) the hard case, T = D, L = D, q >= 2, has no bound. - W5. s(U') < 1 implies L9 at U'. - Reduction. s < 1 propagates along S1 -> S1 steps outside case H. So L9 holds on the orbit unless a case-H epoch, or an S2 epoch with an S1 successor, leaves s >= 1 behind (Lemma H, open).

Why it cannot close locally. - Conjugacy (conj10.py). Map A..F -> E,A,B,F,C,D and mirror. All 12 table entries match, and 3,000,000 steps run in lock-step from the blank tape. - Merge. #28's first-eat state at epoch 350,328 is (4,193,605, [3,15,3,0,11,0,0,1]), which is #10's cascade state at t = 350,272. From there the orbits coincide, with an offset of 56 epochs. Before that they differ: our N are 2, 5, 6, 9, 10, 19, ... and #10's n are 2, 5, 6, 11, 12, 18, ... - Family (family10.py 8 18 6). #10's sigma0(B) = (3*2^(B-2) - 7, [3, 0^(B-6), 10, 0, 2]), read as #28's eat state RS(W, n mod 2, 0, n). For every B = 8..18: - the first phi-eat satisfies all of INV, L9 included (PC/2^D = 1.875; s = 1.13-1.15); - the next two phi-eats break L9 (PC/2^D = 2.125, then 2.0); - the third is f-start with the wrong shape and a late flush (B = 8: F = 256 > N = 194; B = 18: F = 262,144 > N = 196,610); - so an eat sees an s block, and no rule applies.

The eats for B = 8 are N = 186, 191, 192, 194, the same as #10 reports for its own TM. - TM (tm_family.py 8 3000). #28's own table matches the abstract rules on 779/779 round starts up to that eat (W = fs11f100fffffff, b = 1, m = 206). It then leaves the block alphabet for one round (a 110 block) and recovers: phi-eats come at N = 207, 208, 222, ... with no halt in 2.8e6 steps.

Checks. - l9_check.py arith 20: Lemma G holds for every X < 2^20 (0 violations). - l9_check.py reduce 100000 2810: 100,000 random S1 states with L9 (up to 31 blocks; N = 2val+0..3, N in [2val, 2^(D+1)), or N >= 2^(D+1)). - W1, W2, W3, W4(a)-(c) and W5: 0 violations. - Cases: a 47,348; b 15,268; c 2,402; H 34,982. - In case H, 1,836 of 34,699 S1 successors have s >= 1. - l9_check.py escape 20000 2812: 20,000 random case-H S1 starts with s < 1 and INV (6-18 extra blocks), 12 epochs each. - s >= 1 is reached in 982 runs, and L9 fails at some later phi-eat many times (431 at the first successor). - No eat with an s block appears within 12 epochs. - So L9 is much more fragile than the flush itself. The rule-level failure needs the sharper coincidences of #10's super-cascade. - The first run with words up to 31 blocks (l9_escape_big.json) timed out on 254 huge-N samples, because the flush is simulated round by round; it was replaced by this one. - Blank orbit: l9_check.py blank 400000 -> data/l9_blank_400k.json. This passes the merge point and the S2 chain at 350,330. - 0 violations of INV, L9, F <= N or s < 1 at S1. - S1 cases: a 398,224; b 1,208; c 16; H 544. - Max s at S1 is 0.875 (epoch 22). Max s after a case-H epoch is 0.875 (epoch 21). Max s after S2 -> S1 is 0.0145 (epoch 2062). - A 3,000,000-epoch run did not finish within the stage and was stopped: its round-by-round flush of the rare S2 chains is slow. - The last stage's 1,000,000-epoch run had max PC/2^D = 1.5625 (epoch 22). - On 100,000 epochs, case H occurs 319 times. Its max successor bound S/2^D is 0.754 after epoch 100 and 0.501 after epoch 1,000. - Max s at S1 is 0.875 (epoch 22), and 0.688 at epoch 62,443, where Y is dense and the successor bound is 0.0009.

Still open / next. - L9 (equivalently Lemma H), and with it the unconditional non-halting. That is #10's Lemma X on the shared orbit. #10's funded stage showed the entry patterns form an infinite family, so a finite case analysis cannot work: ground rule 6. - The cryptid-protocol deliverable: an AntiHydra-style Rocq rule reduction, best done once for #10, its twin and #28 (decision.json).

Decision (2026-10-12)

Question: #28 is #10 mirrored and started in E, and the two orbits merge: park it with #10 as one cryptid candidate, fund the shared Rocq rule reduction now, or fund research on the shared Lemma X? Answer: park_with_10 (Park with #10 as one cryptid candidate). Dennis: apply recommendations (2026-10-12).