/machines/1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LB0RC/notes.md · raw

1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LB0RC

Status: STUCK (tight stage done 2026-10-11, hard stop: tight failures pinned by a closed form (TF) and the next eat proved safe up to the first C-meets-v event; the head dynamics after it, and so the leading-spacer recovery lemma, unproved; no further stages) Class guess (agent / Dennis): Bell eats counter. It is a BECv1 tm108 twin (E1 differs) whose counter has 3-cell digits and whose eat shifts the grid / — Spreadsheet notes / Discord thread: Results tab: blank status, Classifications tab "Bell eats counter", no notes. Not in dyuan's Oct 1 list (24) or mxdys's Aug 24 UBRRBA list (86). No row in data/solved_index.tsv (no exact, notation or mirror/renamed match). Still on the 2026-10-07 list of 778 (line 202). I had no live Discord access, so I could not search the threads. Not SKIPPED. Viewer: https://bbchallenge.org/1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LB0RC Pool: #29 (reports/targeting.md §4.3). R2 = 1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LD0RC is the 1-transition sibling (F0).

Observation

Candidate rules

All of these are validated by scripts/validate_rules.py, which writes validation.json (random instances, fixed seed):

rule from -> to steps validated
R1 (= HR1) l A> 101^n r -> l 010^n A> r 7n 60/60
R2 l A> 111 r -> l 000 A> r 3 60/60
R3 (= HR3) l 010^n <B r -> l <B 101^n r 3n 60/60
R4 carry l 100 <B r -> l <B 111 r 3 60/60
R5 turn l 000 <B r -> l 100 A> r 5 60/60
R6 overflow 0^inf <B r -> 0^inf 100 A> r 5 60/60
R7 marker step (= HR2) l A> 101 00 101 r -> l <B 00 101 101 r 13 60/60
R8 marker birth (= HE2) l 010 A> 0^inf -> l <B 00 101 0^inf 6 60/60
ROUND K(W,b+1,c) -> K(inc W, b, c+1) 10b+21+10s+6o 372/372 (steps exact)
OVERFLOW (macro) 0^inf <B W 101^b 00 101^c -> 0^inf <B 111 W 101^(b-2^D) 00 101^(c+2^D), b > 2^D 150/150
EAT shape, aligned W K(W,0,c) reaches the next K without halting 400/400 (shape only)
EAT exact open untested

In ROUND, inc(W) works as follows. Write W = U 000 V with V in {010,100}*. Then inc(W) = U 100 V', where V' is V with every 100 replaced by 000; s and o are the counts of 010 and 100 in V. If W contains no 000, then inc(W) = 100 V' (overflow).

Coverage from blank (scripts/analysis/kscan2.c dumps every K-moment; coverage.py classifies them; summary in data/coverage_K_1e10.json): - To 1e10 there are 872,742 K-moments, and 870,221 transitions are exactly ROUND, with 0 mismatches. - 334 more are rounds whose carry enters a shifted segment. - 1,756 follow a b = 0 eat, and 430 are other mini-eat transitions. - So 0.29% of transitions are not ruled. - Every clean left-record pair within an epoch obeys OVERFLOW (2,382/2,382).

Probes of the eat: - Aligned words over {010,000,100} never halted in 400 random eats. - Random words that also contain 001 units halt often. All 6 halting samples I printed contained 100 001. Banning that pair still leaves about 5% of samples halting (29 of 542; scripts/analysis/closure.py). - So the reachable language is finer than "no 100 001". The t-units come from the grid re-read of old spacers. To 1e9 they always follow s, z or t (never o), are never among the last 3 units at eat time, and often appear in runs (ttt).

Halting mechanics (for the invariant later): the only undefined transition is D1. D is entered only by C1 = 0LD, so the machine halts only if B reads 0 at p+1 while cells p-1, p are 11 (B0 -> C reads 1 -> D reads 1). A-swept aligned words contain no 11, which is why rounds cannot halt (argument; also 870,221 rounds observed). The 11s come only from shifted segments (001 100).

Template check: tm108 at verify/BECv1_6x2_solved.v:872 differs only in E1, and its right half (HR1/HR2/HR3/HE2) carries over unchanged. The left counter does not carry over: - In tm108, E carries over single-cell digits, and m0 = 00 separates the counter from the unary. - Here, E1 = 1LB hands the carry to B (R4), so each digit is a 3-cell unit, spacers can sit between digits, and the eat shifts the grid.

solve_BECv1 cannot express any of this. The closest proof styles are BECv7.v (carry heads, mutually strengthened modes) and BECv8.v (two-track suffix transducer).

Sibling R2 (F0 = 0LD) passes R1, R3, R4 and R5 (20/20 each) but fails R7 (0/20). It has the same counter and a different marker step.

Cryptid check (ground rule 6): I found no Collatz-like or pseudo-random arithmetic rule. However, the eat consumes the counter's bit pattern at eat time (about N mod 2^D). If the safety of the later mini-eats depends on those bits, the question becomes arithmetic. Not flagged as CRYPTID_CANDIDATE: undecided until the eat is ruled.

Checkpoint A (Dennis)

Questions are on the card (machines/…/card.html). Confidence is med, so proof work waits for an answer. In particular: rule the eat (one more stage), or park as STUCK?

Informal proof

Not started (blocked on the eat rule and Checkpoint A).

Formalization log

None.

Outcome

Parked STUCK at the leading-spacer recovery lemma, after the hard-stop stage tight (2026-10-11). The open part is now only the head after the first C-meets-v event (see the last funded-stage section). Earlier stages: observe, deepen, size_invariant and recovery (2026-10-10).

Decision (2026-10-10)

Question: #29's rounds, overflow and marker are ruled (99.7% of K-transitions to 1e10), but the grid-shifting eat is not. Spend one ~2 h deepen stage ruling the eat, or park #29 as STUCK? Answer: deepen (Fund one ~2 h deepen stage on the eat). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, deepen)

Scripts: scripts/deepen/ (C oracles episode.c, epochfuzz.c; phase_table.py, validate_deepen.py, sweeps.py, generators). Data: data/deepen/. Validation summary: scripts/deepen/validate_deepen.json. Seed 20261010 where random.

What was done. The machine reduces to two exact sweep laws, and the eat is now a ruled process. - A-sweep law. A moving right rewrites each cell p to [x[p]=0 and x[p+1]=1] up to the first 00, where it bounces: 00 becomes 01 and D reads the cell to its left. So A-swept cells never contain 11. Checked 3,000/3,000 random strings. - Leftward sweep = a unit phase table (phase_table.py -> phase_table.json, derived from the TM). The entry state X at cell 3 of a unit decides what happens. On the A-swept units:

X s=010 o=100 z=000 t=001
B (normal) 101, B 111, B (carry) 100, turn 100, C
C 111, C 110, turn 010, turn 110, C
D (after a bounce) 001, B 011, D 111, E on the unit to the left halt
E 011, turn 101, turn 001, turn 111, E

Composing the table reproduces the TM's leftward sweep on random unit words in 3,000/3,000 cases. D is entered only at a bounce and survives only over o units, so a halt needs a bounce with t o^k (k >= 0) directly to its left. - The eat, as unit rewrites. At b = 0 the round increments W and A bounces right after W' = inc(W) (D phase). Write W' = Y x o^k: - o^k becomes u^k = 011. - x = s: it becomes t, the new marker. Y is incremented with the trailing spacers of Y as its bell. This is the mini-eat, and the same rule then applies to inc(Y). - x = z: E turns on the unit to its left. - x = t: halt (cannot happen when W is t-free, because every level only sees increments of t-free prefixes). - Finally A runs through the old bell to the right end, the marker is reborn there (R8), and the grid shifts by one cell. This is the observed re-read o->s, z->z, s->t. - EAT law (validated). For every t-free W (over o/z/s, last unit a digit), K(W,0,c) with c >= 2 reaches the clean K(P, c+delta(W), 1) without halting. P and delta in [0, 13] do not depend on c. - Exhaustive at c = 3: all 354,293 t-free words up to 12 units. - All 39,365 words up to 10 units give identical outputs at c = 2, 12 and 30. - Random 13..45-unit words: 1,500/1,500, same output at c = 3 and c = 17. - Real run: the oracle reproduces the episode at step 37,393 (867 steps, ossssssssz, b = 40). - Counter invariant (new, exact on all 529 epochs from blank to 1e10). - At every epoch eat, W is t-free and value(W) = c + 1, reading o = 1, z = 0 and skipping s. So the counter has bitlen(c+1) digits. - At every post-eat K-moment, value(P) = 2, skipping both s and t. - ROUND keeps value - c fixed. Eats occur exactly when the counter value has caught up with the bell. - Epochs with t units. - For all 529 real post-eat words P, the rounds from P never halt (checked over the first min(N, 600) rounds). - The t units are gone after k0 rounds, with (k0+1)/N <= 0.286 (the worst case is N = 7). For N >= 100 the ratio is <= 0.207, and for N >= 1000 it is <= 0.124 (so the margin is >= 8x). Data: data/deepen/epoch_tlifetime_1e10.txt. - 304 of these epochs contain internal bounces. These are the "carries into shifted segments": the carry runs in the C phase through the t segment as a carry in the old grid, and the A sweep bounces inside it. They are not ruled at unit level. - The size condition is real. Forcing the eat early (at round k <= k0+3 of each real epoch) halts in 173 of 7,830 runs (data/deepen/early_eat_summary.txt.gz). So non-halting needs every t to clear before the next eat. This is the same reduction that sibling R2 reached in its own deepen stage. - Closure fuzz from random counter-consistent states (gen_consistent.py + epochfuzz). Each start is a random t-free W (random bits and spacer runs, D = 3..12 digits) with c = value(W) - 1, then several epochs are run. - Results: 400 starts x 3 epochs, plus 3000 random starts (D = 3..12) and 300 power-of-two starts (value 2^(D-1), the most zero digits; D = 3..13), 4 epochs each: 0 halts. - At the first eat after a random start, 253 of 3300 starts break the value invariant. At the second eat, 5 of 3300 still carry t units, yet still do not halt. Random starts lie outside the reachable set. - At the third eat, 3 of 3,300 still carry t units. All 3 are spacer-heavy starts with a tiny bell (c <= 13), and none halts. At the fourth eat, all 3,300 are t-free and value-consistent. Data: data/deepen/closure_fuzz_{in,out}.txt.

Cryptid check. Not flagged. - The eat itself is local: every t-free word eats safely (exhaustive to 12 units). - What depends on the counter's bits is the size race k0(P) < N. Here k0 grows with the number of digits below the highest t, and those digits come from the zero digits of the eaten value c + 1. - That is an inequality with a >= 3.5x margin (>= 8x for N >= 1000). In the fuzz, random bit patterns (power-of-two counters included) never break it from the fourth eat on, and never cause a halt. - It is not a pseudo-random arithmetic rule. The decision's cryptid exit (eat safety depending on N mod 2^D non-locally) is therefore not triggered: the eat does not depend on the bits; the epoch's size margin does, through an inequality.

Still open (why confidence stays med): 1. A unit-level rule for rounds whose carry enters a t segment, including their internal bounces, and an exact formula for the t lifetime k0(P). 2. A proof of the size invariant on the reachable set: every t created by an eat clears before the next eat. Random starts show it can fail off the reachable set (3 non-t-free eats), so the invariant needs the reachable spacer structure, not only value(W) = c + 1. 3. An epoch model (W, c) -> (W', c') that runs far past 1e10 steps. Only 529 epochs exist to 1e10. R2 used an epoch model to reach N = 1e7.

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

Question: With #29's eat ruled and safe for every t-free counter, fund one ~2 h stage on the last size invariant (eat-made t units clear before the next eat), or park #29 as STUCK at it? Answer: size_invariant (Fund one ~2 h stage on the size invariant). 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, size_invariant)

Scope (decision size_invariant): rule the rounds whose carry enters a t segment, give an exact t-lifetime formula, build an epoch model and run it far past 1e10, then look for the inductive reason the size margin holds. Exit: a closed invariant gives proof.md at medium-high confidence; a shrinking margin or an unruled shifted carry parks #29 as STUCK. Scripts: scripts/sizeinv/ (C: emodel.c epoch model, kround.c direct one-epoch oracle; Python: wround.py, cascade.py, lemma_test.py, generic_test.py, layout_test.py, leadbits.py, leadhalt.py, leadhalt_real.py, bits_test.py, fuzz_b.py, val_real.py, ksim.py). Data: data/sizeinv/. Each test writes a JSON summary next to its script.

Result in one line. The shifted carry is now ruled, and the t-lifetime law is exact. The epoch model runs from blank to N = 1e8 with no halt and no t at any eat. The size invariant splits into a generic case and a leading-spacer case. The generic case is a universal lemma by exhaustive test, with no reachability needed. The leading-spacer case is rare (6 of about 7.1 million epochs), its bound is exactly tight, and it depends on the counter's low bits. When it fails, a top t survives one eat, but it has never halted and clears within two epochs. No closed invariant yet, so confidence stays med. Neither exit fired: the carry is ruled, and the margin does not shrink with N but is structurally tight.

1. Epoch model (emodel.c). It works on the state K(W, b, 1) after an eat: - Rounds whose carry stays in the t-free suffix V (right of the lowest non-{z,o,s} unit) are jumped in bulk with the ROUND rule. - Rounds whose carry leaves V are simulated cell by cell with the real TM on 0^inf W 101101 00 101101. The round ends when A enters the first bell cell. - Once W is t-free, the remaining rounds are a binary add. - The eat K(W,0,c) is simulated cell by cell at a small c and checked again at a second c (EAT law: P and delta do not depend on c). b' = c + delta.

The 1e7 and 1e8 runs used the first build, whose left padding was 12 cells. A round that grows W by more than 4 units at the top makes that build stop with flag 4, and neither run stopped. The current build pads 3(n+16) cells.

Validation: - One step from each of the 528 real post-eat states to 1e10: the next eat word W and c, the next P and b, and k0 all match (528/528). Here k0 is the number of rounds until W is t-free; it is checked against the direct simulation kround, which skips pseudo-K-moments inside a round (val_real.json). - Free run from epoch 1: it reproduces all 527 later epochs.

2. Far run (data/sizeinv/emodel_1e7.txt.gz, every epoch; emodel_1e8_summary.txt, epochs with slack <= 2 plus every 100,000th). To N = 1e8 (about 7.1 million epochs, very roughly 2.5e23 TM steps if the span stays about 3N; the model does 1.4e11 cell steps): - 0 halts and 0 t at any eat. - value(W) = c+1 at every eat, and D(W) = bitlen(N+1) at every eat (804,148/804,148 to 1e7). - The EAT law's c-independence is re-checked at every eat (two c values each), with 0 mismatches.

3. The shifted carry, ruled (cascade.py; cascade_validate.json). This is one unit-level rule for every round on {z,o,s,t} words. The carry enters at the bottom in phase B and moves up: - B phase: o -> z (the carry continues), s passes, z -> o (STOP), t -> s (and a C run starts above it). - C run: the maximal {s,t} run directly above that t. In the run, s -> z (a new digit) and t stays t. The first unit above the run is the TURN unit: z -> s, where 0^inf counts as z. A turn on o is outside the rule; real words never meet it. - After the C run: - if the run was empty, B continues above the TURN unit; - if the run's lowest unit was an s, it becomes o (STOP); - if it was a t, that t is entered from below in turn (t -> s, then a new C run on the converted units).

Read in the old grid (s = old 1, z = old 0, t = old spacer), a C run is a binary increment of the old counter above the t. The rule matches the cell-level TM on 3,821/3,821 random {z,o,s,t} words. The other 1,179 random words hit a turn on o, outside the rule; 660 of the 5,000 random words halt in the TM. It also matches 10,371/10,371 of the exact rounds in 3,000 sampled real epochs, with 0 rounds outside the rule. It is the composition of the deepen stage's phase table and A-sweep law.

4. t-lifetime law (exact). - k0 + 2 = 2^h holds in all 7,015,292 epochs with t to N = 1e8 (npow2bad=0) and for all 66,530 distinct P = eat(W) of t-free words up to 12 units. - h is the number of digit positions below the top t when the carry enters it, which happens when the counter value (starting at 2) reaches 2^h. - Since value(W) = c+1 at the next eat, the t's clear before the next eat iff 2^h <= N_new + 1, that is, h <= bitlen(N_new+1) - 1. - Explicit upper bound Hub(P) = #{s,z strictly between the top t and the lowest t} + #{z,o below the lowest t}. h <= Hub(P) holds in all real epochs and all 66,530 exhaustive P (lemma_test_L12.json). - Hub is not tight (Hub - h ranges over 0..6 on short words). No closed formula for the exact h was found; it follows by iterating CASCADE.

5. The margin of the deepen stage was not structural. - The deepen stage measured >= 3.5x overall (>= 8x for N >= 1000) to 1e10 (N <= 3,516). - From blank to N = 1e8, h <= D_old - 1 holds in every epoch, where D_old = digits of the previous eat word, which is at most bitlen(N_new+1). But the slack D_old - 1 - h is 0 in 4 epochs: N = 8, 8,110, 16,221 and 4,193,610. In the last three, k0/N = 0.505, so the margin is about 2x. - Slack histogram: 0:4, 1:1, 2:8, 3:31, … (emodel_1e8_summary.txt END line). No new tight epoch appears between N = 1e7 and 1e8. - So no numeric-slack argument is possible: the invariant is the structural bound itself.

6. Generic case versus the leading-spacer case. - Generic (the eat word's first unit is a digit o; every real epoch except 6). h(eat(W)) <= D(W) - 1 holds for every t-free W of this shape: exhaustive to 12 units (177,135 words, all bit patterns) and on 14,098 random words of 13..70 units, with 0 failures (generic_test_L12.json). This is a universal lemma about the eat plus CASCADE, with no reachability and no arithmetic. It still needs a proof. - Leading spacer (W = s …). It arises when a C run reaches 0^inf through a top run of old 1-digits, for example ssssssstoooo… -> szzzzzzos…. It lasts 2 epochs. In the full log to N = 1e7 this happened only at N = 8,101/8,110, 16,219/16,221 and 4,193,605/4,193,610 (leadbits.py). The 1e8 summary logs only epochs with slack <= 2, and it shows no new ones between 1e7 and 1e8. Slack 0 (above N = 8) occurs only in leading-spacer epochs. - Here the bound depends on the bits. On the 4 real leading-spacer layouts with D <= 14, all bit patterns were tried (4,096 or 8,192 per layout; the two D = 22 layouts, with 2^21 patterns each, were not enumerated). Exactly one pattern breaks the bound on each of the two first-epoch layouts, and none on the two second-epoch layouts, for example value 8,101 instead of the real 8,102 on layout sdddddddsddddsssdsssssssd (leadbits.json). - Exhaustively, 1,164 of 88,507 short leading-spacer words break it (one bit pattern per failing layout). - The failures are benign in every test. A top t survives one eat, then everything is clean: - all 24,576 patterns on the 4 real layouts with D <= 14, over 5 epochs: 0 halts, all clean after 2 epochs (leadhalt_real.json); - all 88,507 short leading-spacer words over 6 epochs: 0 halts and 942 with a t at the next eat; 88,363 are clean after epoch 2 (the other 144 still show some flag later) (leadhalt_L12.json). - Random-bit variants of 3,000 real eat words (20 each, 58,840 with t): 0 failures (bits_test_11.json). - Burn-in fuzz from 2,000 random counter-consistent starts over 12 epochs: a t at the eat only in epochs 1-4 (13, 11, 1, 1), the exact slack >= 0 from epoch 3 on, and 0 halts (fuzz_b_7.json).

Cryptid check. Not flagged. The arithmetic touches only the leading-spacer epochs, and only through whether a top t survives one eat. In every test that survival is harmless: no halt, cleared within 2 epochs. If the recovery itself turns out to need the bits, flag then.

Still open (why confidence stays med): 1. A proof of the generic lemma (h(eat(W)) <= D(W) - 1 for t-free W whose first unit is o). It needs the eat recursion (the deepen-stage mini-eats) together with CASCADE. 2. The leading-spacer case. Either replace the bound by a recovery lemma (a top t that survives one eat is cleared in the next epoch, without halting), or show the failing bit pattern cannot meet a reachable leading-spacer layout. The recovered states briefly contain units outside {z,o,s,t}, for example v = 110 in tzvsssssstzzzosssz, so the recovery lemma needs one more rule. 3. Formal proofs of CASCADE and the k0 law. These are mechanical, from the phase table.

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

Question: With every #29 round ruled and the size bound proven by test except in rare leading-spacer epochs (where a surviving t has always recovered), fund one ~2 h recovery stage, or park #29 as STUCK? Answer: recovery (Fund one ~2 h recovery stage). 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, recovery)

Scope (decision recovery): write the informal proof of the generic size lemma (h(eat(W)) <= D(W)-1 when the eat word starts with a digit) from CASCADE and the eat recursion; for the leading-spacer case prove a recovery lemma instead (a top t that survives one eat is cleared later without halting), with one more rule for the v = 110 unit, checked by layout over all bit patterns. Exit: proof.md at medium-high confidence; CRYPTID_CANDIDATE if the recovery depends on the counter's bits; otherwise STUCK. Scripts: scripts/recovery/ (common.py, eatu.py, lemma_h.py, generic_chain.py, leadrec.py, survshape.py, survprefix.py, trace_eat.py). Each test writes a JSON summary next to its script. Light compute only (Python plus the existing C oracles ../deepen/episode and ../sizeinv/emodel); no Rocq.

Result in one line. The generic lemma is now proved (informally), through a closed unit-level form of the eat (EATU) and a potential that never grows under CASCADE (Hub). The leading-spacer recovery holds in every test (265,642 words, all layouts and bit patterns up to 13 units, 8 epochs each, 0 halts, at most 3 epochs with a t), but it is not proved. The surviving-t states are not safe in general: 862 of 2,179 arbitrary ones halt. Exit: STUCK at the recovery lemma; not a cryptid.

1. EATU: the eat in closed form (eatu.py). Let W be a t-free eat word (units o, z, s; the last unit is a digit) at K(W,0,c). Then: - Level 1: W_1 = inc(W). This is the round that empties the bell. - Level i: write W_i = Y x o^k, with k >= 0 trailing o's and x the unit before them (0^inf counts as z). - x = z: stop. - x = s: write Y = Y0 s^j, where Y0 is empty or ends in a digit, and set W_{i+1} = inc^(j+1)(Y0). Here x becomes the marker, and the trailing spacers of Y are its bell, which gives j+1 rounds. - x = t: halt. This cannot happen for a t-free W, because inc never creates a t. - Then X = reread(Y) o, with reread o -> s, z -> z, s -> t, and P = cascade(X), the first round in the new grid. The bell is b' = c + delta, where delta = the number of units removed by the levels (k of the last level, plus k+1+j for every x = s level). - Derivation from the phase table: - D passes o (Do: o -> u). Ds turns s into the marker t and goes on in B, which gives the mini-rounds. Dz writes D = 111 and E enters the unit y to its left. - E turns on y and writes a 1 into its third cell: Es s -> u, Eo o -> S, Ez z -> t. - The A sweep then turns u^M into o^M, the new bell, and the marker is reborn at the right end (R8). - Read one cell to the left, the E-modified y gives exactly reread(y), and its third-cell 1 turns the x position into the new digit o. - No c appears anywhere, which explains the deepen stage's "P and delta do not depend on c". - Validation: P and delta are exact on 1,070,595/1,070,595 words: all t-free words up to 13 units, plus 20,000 random words of 13..90 units, against the cell-level oracle (eatu_validate.json).

2. Lemma H: the Hub potential (lemma_h.py). Hub(X) = #{s,z strictly between the top and the lowest t} + #{z,o below the lowest t}. Invariant I: no o lies above the lowest t. On {z,o,s,t} words satisfying I, one CASCADE round: - (a) never meets the uncovered case (a turn on o); - (b) keeps I; - (c) adds exactly 1 to the value (o = 1, z = 0, s and t skipped); - (d) never increases Hub while a t remains; - (e) creates no t; - (f) leaves a value of 2^m with m <= Hub when it removes the top t.

Proof sketch: - I, (a) and (b). A STOP writes its o either where B stops, below the lowest remaining t (B cannot pass a t), or at the lowest unit of a run, which is directly above the t just entered and below every t the run passed. So I is kept. A C run only walks above the lowest t, where I says there is no o, so a turn on o never happens. - (c). By I every digit above the lowest t is z, so the z digits that C runs insert (s -> z) or delete (turn z -> s) do not change the value. The rest is a binary +1. - (d) and (e). Hub counts, below the top t, the z/o units and the s units that have a t below them. No unit ever becomes a t, and t's never move. The only conversion to a digit is s -> z inside a C run, which sits above the entered t, so that s was already counted. Every other change only removes counts: - a turn z -> s that ends up below the lowest t; - an s whose last t below it is gone; - an entered t, which becomes an s with no t below it. - (f). The carry that removes the top t turns every digit below its o into z, and by I every digit above is z, so the value is 2^m. The m digits below that o are units Hub counted at the start of the round. Usually the top t is the lowest t by then; the case where two adjacent t's go in one round (tzt -> ossss) is in the exhaustive check.

So from value(P) = 2 the top t goes at round k0 with k0 + 2 = 2^h and h <= Hub(P). This is the size stage's exact t-lifetime law, now with a proof.

Validation: - (a)-(f) hold on all 649,539 I-words with a t up to 11 units (39,424 of them remove the top t; 20,481 of those are tight). - CASCADE equals the cell-level TM round on all 17,496 I-words up to 8 units (lemma_h_L11.json).

3. Proof of the generic lemma (generic_chain.py). For every t-free W:

h <= Hub(P) <= Hub(X) <= G(Y)+1 <= G(W_final) <= G(W_1) = G(W),

where G = the number of digits strictly below the top spacer and W_final = Y z o^k is the last level. - h <= Hub(P) <= Hub(X): Lemma H. X satisfies I, since its only o is the last unit. - Hub(X) <= G(Y)+1: the t's of X are the spacers of Y. Its counted units are the digits of Y between its top and lowest spacer, the z digits of Y below its lowest spacer, and the appended o. - G(Y)+1 <= G(W_final): W_final = Y z o^k. - G(W_final) <= G(W_1): inc keeps the spacers in place and only prepends digits above all of them, and a level removes a suffix s^(j+1) o^k.

If the first unit of W is a digit, G(W) <= D(W)-1. Then 2^h <= 2^(D-1) <= value(W) = c+1, so k0 = 2^h - 2 <= c-1 < b' = c+delta: every t clears before the next eat, and the next eat word is t-free with value = c'+1 again. The eat cannot halt on a t-free word (EATU, x = t impossible), and neither can a round (I-words, Lemma H (a)). Every link holds on all 294,590 words with a t in P (348,151 t-free words up to 12 units), with 0 failures (generic_chain_L12.json). So the generic case now rests only on validated, finite unit rules: the phase table, the A-sweep law, ROUND, EATU and CASCADE.

4. The leading-spacer case is exactly one short. For W = s ..., G(W) = D(W), so the chain only gives h <= D. A t survives the epoch iff h = D and value(W) + delta + 1 < 2^D. Every link of the chain must then be an equality, so all of the following hold: - every level has k = 0; - Y has no o below its lowest spacer; - no round lowers Hub, so no C run turns strictly between two t's below the top.

These conditions are logical consequences of the proof and were not tested separately.

5. Recovery: what was tested. - All leading-spacer words (leadrec.py). Every t-free W = s^a … (a >= 1; first digit o) at the consistent c = value(W) - 1 goes through EATU, then several epochs of the exact epoch model. - All 265,642 words up to 13 units, 8 epochs each: 0 halts, 0 model flags, and the value invariant never broken. A t is present at the eat in 1 epoch for 1,137 words, in 2 epochs for 1,130 and in 3 epochs for 109. There are never more than 3 consecutive t-epochs, and the word is t-free afterwards (leadrec_L13_E8.json). - Up to 11 units over 10 epochs: 29,469 words, 0 halts, the same at-most-3 pattern (leadrec_L11_E10.json). - With the size stage's 24,576 patterns on the real layouts, this covers every bit pattern of every leading-spacer layout up to 13 units. - But a surviving t is not harmless in general (survshape.py). Take eat words pre·t·Z with Z any t-free word up to 8 units, pre = s or empty, at the consistent c: - 207 of 2,179 halt in the first eat, because the levels reach the t (e.g. stooz: inc gives stooo, so x = t); - 655 more halt in later epochs; - this holds for both prefixes (survshape_s_L8.json, survshape_none_L8.json). - Halting mechanisms in a transient. These were checked on single rounds with the cell-level TM: - The eat halts if the level recursion reaches the t. - A round halts if the B carry reaches a v = 110 unit: Bv writes 101 and D then reads a 1. This happens directly (vo, tzvo halt) or after an empty C run (vzto, tzvzto, tzvsszto halt). - A C run that reaches v through s's is safe: Cv = 011 L F (tzvsto -> tstzosz). - v itself is the re-read of a surviving t followed by o. The t's third-cell 1 moves into the next unit: o -> v, s -> S, z -> o. - The failure-produced shapes are varied (survprefix_L11.json). - They show 17 eat-word prefixes, multi-t ones (stto, sttt) among them. - stoz occurs 127 times, and its post-eat word starts tzvz 62 times. That is the halting-prone v z layout, yet none of these halted. - So the recovery does not follow from a local shape rule. A proof has to use how a failure builds the next word. - In the real run no t has ever survived an eat (0 to N = 1e8, size stage), so the lemma is needed only to close the proof.

Cryptid check. Not flagged. The bits decide whether a t survives and for how long (1 to 3 epochs). They never decided halting in any test: every bit pattern of every leading-spacer layout up to 13 units recovered. No pseudo-random arithmetic rule appears. The open part is a structural lemma about the words that a tight failure produces. The decision's exit therefore gives STUCK, not CRYPTID_CANDIDATE.

For R2. This does not settle R2's R1 (T_k + 1 <= I_k). The Hub/G potential is specific to #29's eat (re-read plus one new-grid round). I found no exact transfer, so there is no R2 section.

Still open: 1. Recovery lemma. For every t-free leading-spacer eat word W with value(W) = c+1, the machine reaches a t-free, value-consistent eat word within 3 epochs without halting. It is true by exhaustive test to 13 units but unproved. A possible route: - use the equality conditions of section 4 to pin down which words a tight failure produces; - then show (i) that the next eat's levels stop below the surviving t (a value margin under 2^D), and (ii) that every v is reached first by a C run through s's, or is rewritten before the B carry can reach it. 2. proof.md lemmas for EATU and CASCADE, written out from the phase table (sketched in sections 1 and 2). Step counts per macro rule.

Decision (2026-10-11)

Question: With #29's generic size lemma proved and only the leading-spacer recovery left (true on all 265,642 test words, unproved), fund one last ~2 h stage on it with a hard stop, or park #29 as STUCK now? Answer: tight (One last ~2 h stage on the recovery lemma). Dennis: go with recommendations (2026-10-11).

Funded stage (2026-10-10, tight)

Scope (decision tight, answered 2026-10-11, Dennis: go with recommendations): use the equality cases of the proved chain (h = Hub = G = D) to pin down the words a tight leading-spacer failure produces; then prove that the next eat stops below the surviving t and that every v unit is met by a C run, never by the B carry. Exit: proof.md at medium-high confidence. Hard stop: if the recovery lemma is not proved in the stage, park #29 as STUCK with no further stages. Scripts: scripts/tight/. Validators: tightf.py (closed form), tf_validate.py, tight_validate.py, next_eat.py, cv_event.py, tight_list.py. Exploration: explore*.py, rounds_show.py. Each validator writes a JSON summary next to it. Light compute: Python plus the existing exact oracles (../recovery/eatu.py, ../sizeinv/emodel, ../sizeinv/wround.py); no Rocq.

Result in one line. The first two steps the decision asked for are now proved: - the words a tight failure produces are pinned exactly, by a closed form of tightness (TF); - the next eat never reaches the surviving t; - the first unit to touch the new v is always a C run.

What is still unproved is the head after that C run (a v-triggered event in the head, and how long the head lives), so the recovery lemma as a whole is not proved. The hard stop fires: STUCK, no further stages. Not a cryptid. No test run of this stage halted (about 990,000 word runs in all).

1. Equality cases (proof). Let W = s^a M (a >= 1, M t-free and starting with o) be a leading-spacer eat word with value(W) = c+1 and D digits. A t survives the epoch iff h = D and value(W) + delta + 1 < 2^D (recovery stage, section 4). h = D forces every link of the chain to be an equality: - G(W_final) = G(W_1). A level with k >= 1 removes k digits below the top spacer, and inc never adds any there. So k = 0 at every level. Since W_1 = inc(W) ends in a digit, k = 0 means it ends in z, and the eat stops at level 1. Hence W ends in o, the eat has a single level (W_final = inc(W)), and delta = 0. - Hub(X) = G(Y)+1. Y = inc(W) minus its last z has no o below its lowest spacer. - h = Hub(P) = Hub(X). Hub never drops during the epoch. - Consequences: value(W) is odd, so V := value(W)+1 is even, and V >= 2^(D-1) + 1.

2. TF: tightness in closed form (proof sketch from CASCADE; exact in every test). Write Y = s^a Z and split Z = g_0 s^e1 g_1 … s^em g_m into maximal digit groups g_i (o = 1, z = 0; value o_i, length L_i) and spacer runs. Then W is a tight failure iff: - W ends in o, m >= 1, g_m is in z*, value(W) <= 2^D - 2; - for i = m-1 down to 0: o_i + N_i ≡ 0 (mod 2^L_i), where N_(m-1) = e_m and N_i = e_(i+1) + C_(i+1), with C_i = (o_i + N_i) / 2^L_i.

Why. In X = t^a s r(B1) o, read every group above the lowest t-run as one old binary counter (s = 1, z = 0, t-runs as spacers). Entering a t is one old increment, by the C run above it. All the t's of a run T_i are entered in one round, which exposes the group G_(i-1) above them to the new counter. Hub does not drop in that round iff the last of these increments rolls G_(i-1) over from all ones. Otherwise a turn leaves an s in G_(i-1), below the lowest t. G_(i-1) receives e_i increments plus one carry per rollover of G_i, which gives the recursion. The C_0 carries out of the top group pass the block t^a and build an old counter above it, starting from 0^inf.

Consequences: - For every layout there is at most one tight bit pattern: the recursion fixes every o_i. Seen as exactly 1 per layout on all 942 tight layouts to 12 units. - Validation (tf_validate.py; TF against the exact EATU + emodel chain): - all 265,642 leading-spacer words to 13 units: TF agrees 265,642/265,642 (1,986 tight; tf_exh_L13.json); - 100,000 random words of the forced shape s^a M0 z V with 10..45 units: 100,000/100,000 (175 tight; tf_both_100000_s5.json); - 3,000 words built from random layouts by the recursion (2,145 with 20..50 units): all 3,000 are exact tight failures, 0 halts over 6 epochs (tf_build_3000_s11_E6.json).

3. T1: the word a tight failure produces (proof). With B := inc(W)[a:] = Z z, the next eat word is

W_next = bin(C_0) t^a B (bin in s = 1, z = 0, no leading z).

Proof. - Give every unit position below the top a type: spacer positions hold t, or s once entered; digit positions hold s (an old 1 not yet converted), z or o. CASCADE keeps the types (t -> s; s -> z, z -> o, o -> z and the turn z -> s on digit positions; nothing becomes t), and t's are entered from the bottom up. - Hub = (digit positions below the top t) - (unconverted s below the lowest t), and the first term is D. - Every t below the block is entered before the next eat: the highest such t has at most D-1 digit positions below it, and the value reaches V > 2^(D-1). The block goes all at once, and only at value 2^D > V, so it survives. - No unconverted s is left below the block: that would make Hub < D, so h < D. - So the region below the block is t-free, has B's layout and has value V, and a layout plus a value fix a t-free word: the region is B. Above the block lies the old counter of section 2, holding C_0.

Validation (tight_validate.py): - all 265,642 words to 13 units, 8 epochs: 1,986 tight failures, single level / delta 0 / W ends in o 1,986/1,986, and the exact form 1,986/1,986 (tight_exh_L13_E8.json); - every bit pattern of the 4 real layouts with D <= 14: 2/2 (tight_real_E6.json); - 10 random layouts with D = 12..15, all patterns: 6/6 (tight_rand_10_D12-15_s20261011_E5.json); - 150,000 random words of the forced shape: 84/84 (tight_struct_150000_L8-40_s20261011_E5.json); - the predicted bin(C_0) prefix matches in all 1,986 + 175 + 3,000 TF cases.

4. The eat after a tight failure (proof, from TF). - N0. V is even, so B ends in z, and the eat's first round is inc(B), inside B. No carry reaches the block. - N1. The level recursion has at most two levels and never reaches the block: - g_m nonempty: level 1 has k = 1 and x = z, so it stops; delta = 1. - g_m empty: level 1 has k = 1 and x = s (the bottom of s^em), so it runs e_m mini-rounds on the prefix. By TF, o_(m-1) + e_m ≡ 0 (mod 2^L_(m-1)), so g_(m-1) ends all z and level 2 stops at x = z; delta = e_m + 1. - The mini-rounds are CASCADE rounds on an I-word (no o above the block), so they cannot halt, even when their carry overflows into the block and converts it. - Checked on all 942 tight failures to 12 units: stops inside B 734, mini-rounds overflow into the block 208, reaches the block 0 (next_eat_L12.json). - In the overflow case the block is converted inside the eat, and the word left at level 2 is t-free. Its post-eat word has no v. A t can still appear at the next eat (73 of these 208 to 12 units), through the ordinary leading-spacer mechanism; that case is not analysed further. - N2, first contact with v. When the levels stay inside B, the reread turns the block into z o^(a-1) and B's top o into v = 110. In epoch 2 the groups below v replay the same TF arithmetic: the same o_i and e_i; the top group loses its top bit, which keeps the congruence mod 2^(L_0 - 1); case g_m empty is the same after the mini-rounds' carries. So every exposure is again a full rollover, no C run is empty, and the B phase never rises above the lowest t-run. The first unit to reach v is therefore a C run (Cv: v -> u, then F), never the B carry. Seen in all 511 such epochs to 12 units: the real and shadow bodies agree below v until that round (cv_event_L12.json).

5. What happens after Cv (observed, not proved). The C state that meets v starts a pass through the head: v -> u, F turns the o above into s, D turns o^(a-2) into u, D on z gives 111, E climbs the reread t's and turns at the first z. The following A sweep then bounces inside the head, at the s u pair. I did not write a unit rule for this. - Observed: right after that round the real word is t + shadow (the shadow S_1 = s^a B run through the same rounds) in 241 of 511 cases (all with a = 1, A' = s). In the other 270 it is the shadow plus a few extra head units (cv_event_L12.json). - At epoch level, the earlier shadow regularity holds (tight_validate.py, to 13 units): - if the next eat word W_(k+1) still has a t, its body equals the body of the shadow's next eat word: 1,279 exact; 22 more where the shadow's own epoch keeps a t and W_(k+1) = t + shadow word; 1 with a longer head; - when W_(k+1) is t-free, the shadow is generic (1,962) or leading-spacer (24). - The head lasts 1, 2 or 3 eats (781 / 1,090 / 103 to 13 units; 689 / 2,302 / 9 on the 3,000 built words), never more.

Cryptid check. Not flagged. Tightness is now an explicit congruence on the layout (TF), and the eat after it is fixed by the same congruences. Halting never depends on the bits in any test: no run of this stage halted. No pseudo-random arithmetic rule appears.

Still open (why #29 is parked): 1. The head after Cv. The recovery lemma needs: - a unit rule for the Cv event (the F/D/E pass and the A bounce inside the head); - an invariant "real = shadow plus a head" through rounds and through the next eats, with the head's reread; - a bound of 3 on the number of eats the head survives. Everything below the head is now covered by TF and the earlier proved lemmas. 2. A route if #29 is ever reopened: write the Cv event as one more unit rule from the TM (as was done for EATU). Then prove the head invariant with the position bookkeeping of T1. The head's survival is again an exposure question, so it should reduce to a TF-like congruence on the shadow. 3. proof.md lemmas for EATU and CASCADE (sketched in the recovery stage).