1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA

Status: KILLED_NONHALT (2026-10-11; delta of kill #30, see ## Kill at the bottom). Not a cryptid candidate. Class guess (agent / Dennis): Bell eats counter, BECv1 tm10 with a broken carry (spaced-digit binary counter + unary marker) / – Spreadsheet notes / Discord thread: Results row 1022, "Bell eats counter", no status/notes/sources/done-by. Not in links, strikethrough, xlsx comments, dyuan01 or UBRRBA lists. Not in solved_index. No Discord check needed (template neighbours are fair game, 2026-10-10). Viewer: https://bbchallenge.org/1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA

Observation

• 1e9 steps (C core): no halt; span 7,783 cells (-7511..271), 4,191 nonzeros. Left edge ~t^0.36, right edge ~t^0.27.
• Diagrams in img/: stateEL_3e5.png (best: one row per E-left entry, left frame), recordsL_left_1e7.png, blaze_1e7.png, default_site.png, viewer.html (all views).
• Commands: --mode state:E:L --frame left --steps 3e5 --scale 2 and --mode records:L --frame left --steps 1e7 --width 150 --scale 2. The records view shows only the 150 leftmost cells. Every card diagram's labels (start, rows, window, legend, style) are in observe.json → diagrams.
• Picture: counter on the left, then a long run of 110 blocks with a 00 marker. One round = A sweeps right to the marker, marker moves 1 block left, B sweeps back, counter +1.
• Counter digits are 111110 ("5") blocks spread through the 110 run; the MSB end has a 11110 ("4") mode. A carry walks left over filler blocks to the next digit.
• Left-edge E records (dense form) are the clean observation point: 0^inf <E 110 W (110)^G 00 (110)^M 0^inf. Epoch from step 20,053,019: W = 5 2^3 5 2^7 5, 4 5 2^3 5 2^7 5, 5 2 5 2^3 5 2^7 5, … G drops 8, 32, 16, 64, 32, 128, 64 (= 2^f, 2^(f+2)).
• When the marker reaches the lowest digit (EatDigit): the digit is eaten, a fresh marker starts near the right end (+2 cells), and the gap list reshuffles irregularly (3,7 → 10 → 17 → 11 → 8,4 …). The transition shows 3/6 blocks and a transient second marker.
• Tools: qsim (block 3) gets only 3.6e7 steps in 200k loops, 17 local rules: no acceleration. rulefit: 2 rules, coverage 6–8 %, not useful. compress: fine at left E records.

Candidate rules

All validated by simulation from concrete configs, random small/large parameters and random contexts (validate_rules.py → validation.json).

X = (110)^g1 111110 … (110)^gk 111110, gi ≥ 1, k ≥ 0, f = k+1, G, M ≥ 0.

Open: the EatDigit case table (G < 2^f or 2^(f+2)). Small cases are probed: P/Q with X ∈ {[], [1], [3]} and every G below the threshold all reach a new left record, none halts. The outcomes are varied (2 4 3, 2 4 6, 2^2 4, z3 inside W).

Template check (BECv1_6x2_solved.v tm10, line 88; diff E1 0LA vs 1LE): our TM satisfies 10/11 cert hypotheses (HR1-3, HE0-3, HL1, HL3, HL4/5: 25/25 each). HL2, the binary carry 1 <E 1 → <E 1 1, fails 0/25. Partly: the unary half carries over, the counter does not.

Cryptid check: no. Halting does not hinge on arithmetic in the observed shape family: - 0 halts in 1,500 random realistic shapes (4e6 steps each) and 60 more at 1e8 steps; - 0 halts in 106 marker shifts (±1, ±2) and 145 gap edits (insert/delete 110, move a digit) of real records. - "Wild" shapes (random 3/4/5 blocks anywhere, adjacent 5s) do halt, so the invariant must be the right language.

Pitfall: a 3-cell 000 marker is not the machine's marker (it's 00); an early fuzz with 000 produced false halts.

Checkpoint A (Dennis)

Informal proof

(not started; proof.md after Checkpoint A)

Formalization log

Outcome

Card data pass (2026-10-10)

• Figures on the card: Fig 1 = img/stateEL_3e5.png, Fig 2 = img/recordsL_left_1e7.png, Fig 3 = img/blaze_1e7.png, Fig 4 = img/default_site.png. Figs 1-2 are the primary figures, shown beside the checkpoint.
• The card's mechanism is cut to 3 bullets. The full list before the cut:
• Tape = a counter on the left, then a long run of 110 blocks with a 2-cell gap (00) marker in it.
• Each round: A sweeps right to the marker, moves it 1 block left, B sweeps back, counter +1 (same as tm10).
• Counter digits are 111110 blocks spread through the 110 run; a carry walks left over filler to the next digit (the E1 change).
• Each overflow grows the left edge by 4-5 cells: 2 5 X -> 2 4 5 X -> 2 5 2 5 X, after 2^f and 2^(f+2) rounds (f = #digits).
• When the marker reaches the lowest digit it eats it, restarts near the right end (+2 cells), and digit gaps reshuffle.
• Checkpoint questions are now yes/no questions about the figures. Moved off the card (strategy calls, not figure reading; settle them in proof.md / Checkpoint B):
• "OK to aim for a shape-invariant proof (any digit gaps, any G/M) instead of tracking the irregular gap values?"

Deepen pass (overnight 2026-10-10)

Result: the mechanism is now exact at the round level for ~99 % of the run, but confidence stays med. Not cryptid. No non-halting argument yet.

What the counter is. Look at the tape just left of the LSB at each round start. After the A-sweep it is in swept form: dense 1^k 0 becomes swept 1 0^k. Write a swept token 1^a 0^k as k when a = 1, else as a.k. - 2 = 100 is filler. - A token with k ≥ 4 zeros is a binary digit. Its bit cell is index k−3 (the cell E reads when the B-sweep stops there). Bit 1 splits the token: - 5-digit: 5 / 1 3 - 4-digit: 4 / 2.3 - 6-digit: 6 / 2 3 - 7-digit: 7 / 3 3 - A plain 3 token always reads as bit 1, so a carry continues through it. - Left end: 3 (P-mode) or 3 4 (Q-mode). - The LSB sits next to the unary. Each round is one increment plus one marker step. So tm10's binary counter is still there; only the digit encoding changed.

Round start. RS(S,P,b,g,m) = 0^inf S P b <E (110)^(g+1) 00 (110)^m 0^inf. - P is the LSB prefix: 1 (=10) for a 5-digit LSB, 0 (a single 1) for a 4-digit LSB. - b is the LSB bit, g is the marker distance, m is the run right of the marker. - No-marker state: NM(S,P,b,n) = 0^inf S P b <E (110)^n 0^inf. - A round start is an E-left event whose right side is exactly (110)^+ [00 (110)^+].

Rules. All validated from random concrete instances: random left words, every bit value, small and large h/g/m. Script: scripts/deepen_rules.py, results in scripts/deepen_validation.json, 440/440 passed.

EAT0 is BECv1's EatDigit: drop an LSB whose bit is 0, and the next digit becomes the LSB with g = its gap.

Generic carry transducer. Derived from the micro-steps (B/C/E/A) and checked only against the blank-tape run, not validated separately. It scans the counter from the right: - 2: skip. - (a,k≥4): set the bit, giving (a,k−4)(1,3). Stop. - 2.3: the previous token gains 2 zeros and 2.3 becomes 2. Stop. This is the 4-digit walking left. It is how the record-level 4 moves and how 6/7-digits are made (5+2 → 7). - 3: borrows a zero. - (a,j≥2)(1,3) → (a,j−1)(1,4), and the scan continues. - 1 3 → 5. - 2.1 3 → 6.

Coverage from the blank tape (scripts/deepen_coverage.py, scripts/deepen_coverage_1e9.json). To 1e9 steps: 150,891 round transitions, 98.88 % predicted exactly with 0 mismatches.

The 1,687 transitions not covered: - 1,319 are the left-end overflow. At record level that is OP/OQ, but it has no round-level rule yet. - About 280 are the B-sweep crossing a lone 1 token (10). It turns 10 into 00, which leaves a stale marker. That is where 0^2 inside W comes from: the A-sweep then reflects there, and digits right of it freeze until an eat. - About 70 are EAT variants: EAT1 with a bit-1 next digit, h = 0 after a walk, a 4-digit LSB, an LSB at the left end. - 4 are NM with b = 1, and 10 are the first rounds from the blank tape.

Token alphabet looks finite. - Interior tokens: {1,2,3,4,5,6,7,2.1,2.3,2.5}. LSB prefixes: {0,1,2,3,4}. - 74 round-start bigrams, listed in scripts/deepen_token_bigrams_1e10.json. - No new bigram appeared between 1e9 and 1e10 steps (671,489 round starts).

The bigram language is NOT an invariant (scripts/deepen_closure_fuzz.py). Random paths through the bigram graph produce new bigrams and some halts: - weighted sampling: 1/400 halt, 18 new bigrams; - uniform sampling: 11/300 halts, 64 new bigrams.

The halting samples put digits next to each other with no filler, for example 1 3 4, 3 2.1 3 L4. So the invariant has to work at digit level: digits separated by fillers, plus a short list of allowed transients. The observe pass's "realistic shapes" fuzz, 0 halts in 1,500, fits this.

Cryptid check. Not cryptid. Every round is a local rewrite over a finite token alphabet. Arithmetic (the counter value when the marker arrives, i.e. the irregular gaps) only chooses which local case fires.

Still open (next pass): 1. A round-level overflow rule, matching OP/OQ. 2. The stale-marker regime: how it is created, A reflecting at the stale 00, how it is absorbed. 3. The EAT case table for bit-1 next digits, 4-digit LSBs, h = 0, and the left end. 4. A digit-level shape invariant, closure-fuzzed with the transitions above. 5. A concrete non-halting argument. The candidate: (1) the only halt patterns are A reading 0 1 0 (dense 1 token) and B reading a 1 that has 1 on its left and 0 on its right, and (2) the invariant excludes both. - Still running when this pass ended: the same coverage check to 1e10 steps (python3 -B scripts/deepen_coverage.py 1e10 scripts/deepen_coverage_1e10.json, detached, under the 6 GB ulimit). If scripts/deepen_coverage_1e10.json exists, read it. If it doesn't, the run died: check reports/watchdog.log.

Deepen pass 2

Result: round 1's overflow and EAT1 gaps are closed, a 4-gram invariant candidate passes closure fuzzing with 0 halts, and the stale-1 regime is now located. Confidence stays med. One regime, the stale-1 cascade, still has no rules, and there is no proof of the invariant. Not cryptid.

New rules. Predictor v2 is scripts/deepen2_predict.py; round 1's rules are unchanged. Validation: scripts/deepen2_rules.py, results in scripts/deepen2_validation.json. All 380/380 targeted instances pass, and the predictor agrees on all 380. Notation: Y = ∏(2^hj (1 3)) is a run of bit-1 5-digits, and Y' = ∏(2^hj 5) is the same run after a carry (hj ≥ 1).

Random words from the 4-gram language below (600 samples): every transition the predictor claims is exact, 386/386 (INC0 153, CARRY 53, CARRY_WALK4 60, CARRY_ovf 41, EAT0 12, EAT1 11, EAT1_c 34, BIRTH 22), and none of the 600 halts. The other 214 samples fall outside the rule set: stale-1 cascades, eats with a 4-digit or 7-digit LSB or h = 0, and counter-empty words.

Coverage on the blank tape. Scripts: scripts/deepen2_dump.py (writes every round start as TSV), scripts/deepen2_coverage.py. Outputs: scripts/deepen2_coverage_1e10*.txt. - To 1e10: 671,488 transitions, 99.898 % predicted exactly, 0 mismatches (round 1: 99.43 %). By rule: INC0 335,298; CARRY 328,605; CARRY_ovf 3,004; CARRY_WALK4 3,154; BIRTH 252; EAT0 240; EAT1 142; EAT1_c 109. - From step 320,000: 99.904 %. All 644 uncovered transitions are stale-1 cascades. Everything else that is uncovered (about 40) belongs to the counter-empty restarts at steps < 2e5 and around 3.15e5. An init lemma would handle those by direct simulation.

What the counter really does. This changes round 1's picture. - The 4-digit LSB is a walker. It soaks up increments and moves one filler left every 2 rounds. - When it reaches the next digit D, it merges into it: - D = 5 (bit 0, MERGE5, 197 times to 1e10): a 7-digit LSB forms. LSB7 then turns D into filler, sends one carry into the counter, and the walker continues. - D = 1 3 (bit 1, MERGE13, 249 times): a stale 1 token is left behind. - The next carry that reaches a stale 1 starts a cascade. Micro-level: the left sweep erases 10 → 00 (B1→0LD, D0→0LB), and the round becomes a multi-bounce excursion. The cascade turns a run of digits into fillers and usually spawns a new 2.3 walker. - Cascades are the counter resets. The counter keeps falling back to just a left end plus the LSB, for example 7 2^30 1 at step 1.8e9 and 3 2^11 1 at 7.1e6. - Cascade shapes to 1e10 (scripts/deepen2_stale_classify.py, scripts/deepen2_stale_1e10.txt):

The cascade results are not a simple +1. One example is 3 5 2 1 3 2 1 3 2 5 2^3 1 1 → 3 1 3 2 5 2 1 3 2 2.3 2^4 1. These are not yet ruled.

Invariant candidate: the 4-gram language L4. Scripts: scripts/deepen2_closure_fuzz.py, scripts/deepen2_kiter.sh. The 4-grams are in scripts/deepen2_kgrams4.json. - How words are abstracted: a round-start word becomes ^ tokens P<lsb> |b<bit> <g0|g+|NM>. Filler runs 2^1, 2^2 and 2^≥3 are written f1, f2 and F. L4 is the set of words whose 4-grams all lie in K. - Fixed-point fuzz: K was seeded from the 1e9 run and iterated with uniform sampling, 300 samples × 20 rounds per iteration. New 4-grams per iteration: 88, 17, 3, 0, 7, 0. That is 645 → 760 4-grams, with 0 halts in 1,800 samples (about 36,000 rounds). - Union run: K was then merged with the 4-grams of the 1e10 run (768) and fuzzed with weighted sampling, 250 samples × 30 rounds per iteration. New 4-grams per iteration: 15, 21, 2, 0, 0, 0. That is a fixed point at 806 4-grams, with 0 halts in 1,500 samples (about 45,000 rounds). Over both runs: 0 halts in 3,300 samples. The final K is scripts/deepen2_kgrams4.json. - Where the escapes land: every new 4-gram is in the tiny-counter corner (left end and LSB within 1–2 tokens), which the resets do revisit. - Compared with round 1: the bigram language was not closed and fuzzing it halted. The 4-gram language has not halted in any sample.

Non-halting argument, current status. 1. Halting needs B to read a 1 with 1 on its left and 0 on its right, which shows up as A> 0 1 0 or 11 D> 0. 2. All observed and fuzzed round starts lie in L4. No configuration started from an L4 word has halted within its fuzzed rounds (≈20–30 per sample). 3. What is missing: - a proof that L4 (or a regular refinement of it) is closed under the round map; - rules for the stale-1 cascade and for the rare eat variants that the closure includes. The random-language sample shows eats with a 4-digit or 7-digit LSB, eats with h = 0, and counter-empty words.

Proof lead. The invariant is a locally testable token language with repeated-filler compression. That is close to what busycoq's CTL deciders certify: CTL.v, with certificates RWL_mod (repeated word list) and NG (n-gram CPS), concluding ~halts from the blank tape. The machine is a holdout, so the default parameters failed. Two parameter choices to try first: - RWL_mod with block length 3 (100/110) and threshold ≥ 3; - NG with n ≈ 12–16.

Search the parameters natively first. The rocq-notes lesson stands: do not search inside Coq. Only then check the winning certificate in Coq. If a CTL certificate exists, no rule table for the cascade is needed.

Still open: 1. Rules for the stale-1 cascade in its 3 shapes, validated. 2. The eat variants reachable in the closure: P = 0 / 3 LSB at g = 0, and h = 0. 3. Closure of L4 checked exhaustively up to a length bound (rocq-notes: use length ≥ 12), not only by random sampling. 4. A native CTL (RWL_mod / NG) parameter search.

Decision (2026-10-10)

Question: Make the next stage a closure stage (exhaustive L4 closure check plus a CTL certificate attempt), hand-derive the stale-1 cascade rules first, or park? Answer: closure_ctl (Closure stage: exhaustive L4 closure to length >= 12, plus a CTL certificate attempt (RWL_mod with block length 3, or NG with n about 12-16)). Dennis: go with all recommendations (2026-10-10).

Funded stage (2026-10-10, closure_ctl)

Result: the invariant candidate L4 is refuted, and no k-gram language of this kind (k ≤ 10) can replace it. L4 contains words that halt. No CTL certificate was found either: every native sweep run so far returned false. Confidence stays med. Not cryptid: every halting word combines transients that the real run never shows together. The open question is whether that exclusion can be written as a regular language.

Tooling. Both tools were checked before use. - scripts/closure/rsim (C, rsim.c): a batch round simulator, from one round start to the next (or HALT/CAP). - Check (selftest_rsim.py): it reproduces 15,759/15,759 consecutive blank-tape round starts to 3e7 exactly (tokens, b, g, m and step counts). - The smallest halting word below was re-checked with tools/sim/tmsim: it halts at step 197. - scripts/ctl_extract/ctlx: busycoq's CTLDecider62.decide_nonhalt (CTL.v), extracted to OCaml. - Build steps are in README.txt. One manual fix is needed: the extracted 'a Parray.t type is wrong and must be patched. - Check: two known busycoq certificates come out true: NG 0 1e6 1e6 9 48 0 0 false on 1RB1LF_1LC0RD_0LD0LC_1LA1RE_1RA1LB_---1LE (busycoq lemma nonhalt321, 1.8 s) and CPS_LRU 100000001 400000 400000 12 3200 2 6 0 0 on CTLv2 nonhalt1 (73 s). - A native parameter search is therefore cheap now. Only a Coq solve_cert re-check plus check_kill would count.

Exhaustive L4 closure (K = the 806 4-grams in scripts/deepen2_kgrams4.json). Scripts: scripts/closure/closure_check.py, classify_L4.py, halt_shapes.py; numbers in scripts/closure/summary.json. - Concretization rules: - g0 = (g = 0, m ≥ 1); g+ = (g ≥ 1, m ≥ 1); NM = (no marker, n ≥ 3). - F runs are all 3, all 4, all 5 or all 7, plus 2 random mixes in 3..9. - g/m: g+ takes (1,1), (2,1) and (4,3); g0 takes m = 1 and 3; NM takes n = 3, 4 and 6. - Every word with ≤ 14 symbols: 67,601 words, 1,000,548 concretizations. - 752,208 successors lie in L4. - 248,016 escape: they have 4-grams outside K. - 324 halt. - Split by the round-2 predictor: - 759,169 concretizations are covered by a validated rule, and every prediction is exact (0 mismatches). That is an exhaustive check of the round-2 rules. - Yet 110,054 of these (14.5 %) still leave L4. L4 is not closed even under the validated rules. - The other 241,379 have no rule: 103,093 stay in L4, 137,962 escape, 324 halt. - All 324 halts are unruled CARRY_stop: a carry meets a stale 1 (the cascade). They come from 86 words. - ≤ 10 symbols: 3,546 words, 43,340 concretizations: 9,463 escapes (366 new 4-grams) and 9 halts. - Smallest halting word: ^ 1 3 f1 3 F 1 P1 |b1 g+, i.e. 0^inf 1 3 2 3 2^3 1 1 <E (110)^2 00 110 0^inf in tokens. It halts after 197 steps (card Fig 5). - Random long words (20–40 symbols): 4,000 words, 12,034 concretizations: 4,113 escapes and 14 halts. - Why the deepen-2 fuzz missed this: halts are about 0.03 % of concretizations and need specific filler lengths (mostly F = 3).

Halting shapes (halts_L4_L14.json). In 285 of the 324, a stale 1 sits right before a bit-1 LSB, in a context the blank run never shows:

The other 39 have two walkers, 4 4, and LSB 2. In the blank run, the context left of a stale-1-before-LSB is only 1 3, 2 5, a left-end 3, or 2.3 5.

k-gram closure iteration (kclosure.py). It seeds K with the k-grams of the blank run to 1e9 (150,891 round starts), then iterates K ← K ∪ k-grams(successors of all words ≤ LMAX). That is the least closed k-gram language over the run, up to the length bound. If it contains a halting word, no k-gram invariant at that k exists for this abstraction.

So no window size up to 10 tokens works, and the languages keep growing.

What the real run has that the windows lose (special.py). Call a token a special unit when it is a transient: - the walker (4/2.3, or LSB 0); - a stale 1; - a 6-/7-digit piece (6, 7, 2.1, 2.5, or a 3 not after 1); - an odd LSB prefix (2/3/4).

Results: - The blank run after 3.2e5, to 1e9 (150k round starts), shows only 16 signatures, with at most 2 special units. The 2-unit cases are left-end ones (X3 W 768, W W 328, X3 P0 6, W P0 4). - Every one of the 324 halting concretizations has a signature never seen in the run (2–4 units, e.g. X7 6b1 S 228, X7 W W P2 39, X7 S 30, W S 18, S S 3). - So the invariant needs a global "at most one transient (plus the left-end exceptions)" constraint. That is regular, but no bounded window can see it.

CTL sweep (scripts/ctl_extract/sweep.py, results sweep_{A,B,C}.jsonl; one run at a time per sweep, nice 10, ulimit -v 6 GB). 118 runs, 0 true: 117 false, plus 1 run aborted at the memory cap (exit 134, 5.3 GB). The parameter sets were: - plain NG (no history), n = 10–20: 11 runs, each false within 0.3 s; - RWL_mod with block length 3, mnc 3, mod 1/2/3, len1 4–16, len2 0/2: 28 runs, up to 166 s and 5.3 GB; - NG with cell-write history (len1 12–48, n 4–14): 24 runs; - NG with state history (asth, n 2–12, len1 12–24, len2 0/2): 36 runs; - CPS_LRU with block length 3–15 and simT 1001: 19 runs.

Not run: params_C.txt (RWL_mod at block lengths 1/2/4/5/6/9/12, and NG with LRU history). The quick falses (0.1–3 s) mean the abstraction reaches a halt almost at once. That fits the finding above that bounded windows contain halting words.

Still open: 1. A structural invariant: a small DFA over special units (≤ 1 transient away from the left end, the left-end cycle, the cascade's own transients), checked with kclosure.py-style exhaustive closure (≤ 14 symbols plus random long words) using rsim. 2. Rules for the stale-1 cascade, now pinned down to the contexts the run actually shows (the 3 shapes of deepen 2). 3. CTL: only as a background lottery. Every bounded-window token language up to k = 10 already fails, and CTL's abstractions are bounded windows too.

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

Question: Fund one stage for a hand-written structural invariant (at most one transient, plus the cascade rules, checked exhaustively), run only a bigger background CTL sweep, or park? Answer: struct_invariant (One stage: a hand-written structural invariant (at most one transient) plus the cascade rules, checked exhaustively). 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, struct_invariant)

Result: the structural invariant closes, with 0 halts, once eats are restricted to normal words. The hand-written grammar H ("at most one transient cluster, from a list of 37, anywhere in the counter") is closed under the round map in every check: 1,214,968 + 259,323 sampled successors and an exhaustive small-size pass. Every blank-run round start from step 3.2e5 to 1e10 lies inside it. Every halting word from the closure stage lies outside it. What is still missing is a quantitative flush lemma: transients must resolve before the marker comes back. That holds on the blank run with slack (at worst 0.34 of the epoch, 0.10 after 1e9), but it is not proved, and the flush time can be exponential in the number of digits to the right of the transient. Confidence stays med. Not cryptid. Per the stop rule this is not an escape, so no park, but proof.md needs the flush lemma first. #28 is stuck at the same point.

Scripts are in scripts/struct/ (README.txt) and the numbers in scripts/struct/summary.json. Every round is simulated by scripts/closure/rsim, which is exact on 15,759/15,759 blank-run rounds.

Shape abstraction (shapeclosure.py). - A filler run becomes f and a normal digit (5 or 1 3) becomes d. - Any run (d f)^+ becomes D*. - Every other token is kept as is: the transients, i.e. walker 4/2.3, stale 1, 3, 6, 7, 2.1, 2.5. - The LSB becomes P<tok>. - NORMAL = LE (D*)? P1, with LE ∈ {ε, 3, 3 4, 3 2.3}. NORMAL_EAT = LE D* P1, i.e. at least one digit.

Two negative results first. Both are needed to see why the flush rule matters. - Signature-partitioned 4-grams (sigclosure.py): k-grams kept separately for each multiset of transient units. With the old small marker values this halts at iteration 4 (21 halts, in class W P2 with NM b1). - Shape closure without a flush rule, even with a long unary (--um large): it drifts into eats on transient words (a P0 walker LSB at g = 0, giving P2 words) and halts at iteration 5 (358 halts). - So a closed invariant must forbid eats on transient words. That is a statement about the marker, not about the counter word alone.

The blank run's eat facts (3.2e5 to 1e10, rs1e10.tsv regenerated by deepen2_dump.py): - All 771 eat and no-marker events see a normal word: g0 with LE D* P1, NM with LE D* P0 b0. EAT0 always returns a normal word. EAT1 starts a transient epoch: walker → merge → stale 1 → cascade. - Flush slack (flush_slack.py): over 470 epochs (245 EAT1, 225 EAT0), τ is the number of rounds the word stays transient after an eat. - EAT1: the largest τ/epoch is 0.34 (at step 8.1e5), and 0.104 after 1e9; the median is 0.036. - EAT0: τ = 0 every time. - A transient cluster in the run never has more than 3 normal digits to its right. Round starts with 0, 1, 2 and 3 such digits: 12,302, 6,988, 2,976 and 512.

Exhaustive epoch check from normal words (epoch_check.py). Every normal word with r ≤ 5 digits and gaps 1-3 is checked, 37,324 words in all. - INC/CARRY keeps them normal: 74,648/74,648. - EAT0 keeps them normal: 37,320/37,324. The 4 exceptions are digit-free counters, which is why NORMAL_EAT needs a digit. - Eat epochs with M = 400: 74,644/74,648 return to a normal word, with 0 halts. The largest τ is 169 rounds, and 359 transient shapes are visited. - A second set, r ≤ 3 with gaps {1,2,4,7}: 4,676/4,680 return, 0 halts, largest τ 105.

Shape closure in flush mode (g+ words concretized with g ≥ 7; a g = 0 successor that is not NORMAL_EAT counts as a violation).

• All 670,604 blank-run round starts from 3.2e5 to 1e10 lie in S444.
• All 130 stored halting examples of the closure stage (35 shapes) lie outside S.

The hand-written invariant H (hand_grammar.py). Every S562 shape has at most one transient cluster: 526 have one, 36 have none. A cluster is a maximal run of transient tokens, with their fillers, between normal digits. There are only 37 cluster words, and only 62 contexts. That gives the grammar

H = LE · pre · X · post, with - LE ∈ {ε, 3, 3 4, 3 2.3} - pre ∈ {ε, D*, d, D* d} - post ∈ {ε when X ends in an LSB, D* P1, P1} - X ∈ {1, 4 f, 2.3 f, f 4 f, f 2.3 f, 7 f, 6 f, f 6 f, 3 f, f 3 f, 3 3 f, 2.5 f, 2.1 3 f, 2.3 2.3 f, 2.3 4 f, 2.3 f 2.3 f, 2.3 f 4 f, 3 2.3 f, 3 4 f, 3 f 2.3 f, 3 f 4 f, f 4 2.3 f, f 4 4 f, f 4 f 2.3 f, f 4 f 4 f, P0, f P0, 2.3 P0, 2.3 f P0, 3 P0, 3 f P0, f 4 P0, f 4 f P0, P2, f P2, P2.1, P3} or none.

That is 1,024 shapes. Every shape is taken with g+ and b = 0/1; P0 shapes also with NM b0; NORMAL_EAT shapes also with g0. In all, 2,180 keys. - Closure with ≤ 100 concretizations per shape: 259,323 successors in H. Two keys were added, both P- (the empty counter, g+ b0/b1). Fixed point at 2,182 keys. - Verification with ≤ 600 per shape, fillers {1,2,3,4,7}, D gaps {1,2,4} and a fresh seed: 1,214,968/1,214,968 successors in H, 0 halts, 0 flush violations.* - So "at most one transient" really is the invariant, as decision.json suggested, once eats are restricted to normal words and the cluster comes from the list of 37. - All 130 stored halting examples of the closure stage are outside H: - 70 have two or more clusters; - 58 have a single cluster whose word is not on the list (3 f 1, 3 3 f 1, 4 f P2, …); - 2 are eats (g = 0) on a transient word (3 2.1).

Flush time (tau_check.py on S444, 8,824 concretizations, G = 700 rounds). - 8,501 return to normal, with 0 halts. - 323 do not return within 690 rounds. All of them have a transient with 3 or more normal digits to its right. Carries reach such a transient only every 2^(r+1) rounds, so τ grows exponentially in those digits. - H as written (post = D* P1) therefore cannot carry a linear flush bound. The refinement suggested by the run is post ∈ {P1, (d f){1,3} P1}: the run never has more than 3 digits right of a cluster.

Non-halting argument, current form. - (1) H is closed under every g+ round, and under eats from NORMAL_EAT words. Checked above, bounded. - (2) No word of H halts within a round. - (3) Flush lemma (open): at every EAT1 the new marker distance (≈ the unary length U) is at least the flush time τ of the EAT1 output. - (4) Init: direct simulation to step 3.2e5, where the word is normal. - (3) needs: - (a) the bounded-post refinement of H, closed; - (b) τ ≤ c·L for those words (L = counter cells); - (c) U ≥ c·L at every EAT1. U only grows (+2 or more per eat), and on the run U/L rises from 2.1 (6.5e5) to ~17 (1e9). A proof needs a bound on how fast L grows: L grows only at left-end overflows, and eats move counter cells into the unary.

Still open: 1. The flush lemma: bounded-post H closed, then τ ≤ c·L, then U ≥ c·L. 2. Explicit token-level cascade rules. The shape-level transitions are implicit in S562/H, but proof.md needs them as rewrite rules. 3. An init lemma to 3.2e5. 4. The CTL lottery stays parked. Bounded windows cannot express the flush condition.

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

Question: Fund one stage for the flush lemma (cap the digits right of the transient, bound the flush time by the counter length, show the unary outgrows it), or park? Answer: flush_lemma (One stage: the flush lemma (bounded-post refinement of H, flush time <= cL, unary >= cL)). 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, flush_lemma)

Result: the stop rule fires. The bounded-post refinement of H escapes, and the flush time from real eat outputs is not linear in the counter length. The reason is now clear: the transient cluster is a slow carry. It moves left through bit-1 digits, turning each into a bit-0 digit right of it, so the number k of normal digits right of the cluster is set by the run of 1-bits it meets. Carries reach the cluster only every 2^(k+1) rounds, so the flush takes about 2^(j/2) rounds for a 1-run of length j. This is the same shape as #28's flush (F = 2^(1+D_F) <= 2 val <= N), so the right bound is in the counter value, not in L. Parked per the stop rule; confidence stays med. Not cryptid. Every check below has 0 halts. Scripts are in scripts/flush/ (README.txt), numbers in scripts/flush/summary.json.

Tooling. - shapeR.py: H's shape abstraction with the post digits spelled out, so k is part of the shape (D* is kept only left of the cluster). On the run it reproduces the previous stage's counts exactly: 12,302 / 6,988 / 2,976 / 512 round starts with k = 0 / 1 / 2 / 3. - flush_epoch.py: the flush time τ of an EAT1 output, from any NORMAL_EAT word with b = 1. The marker is re-placed at g = 6 every round, which makes this fast. The trick is safe: 60/60 epochs are identical (τ, kmax, end word) to runs with the true unary M = 3000. - One escape transition was re-checked with tools/sim/tmsim (tmcheck.py): same successor, 228 steps.

(a) Bounded-post H does not close. - H_3 (H with post in {P1, (d f)^k P1, k ≤ 3}; 3,820 keys) escapes at iteration 1: 867 of 1,054,812 successors have k = 4. - First escape: 3 4 5 2 1 3 2.3 2 2 (1 3 2) (1 3 2 2) (1 3 2^5) 1 |b1 → 3 4 5 2 1 5 2^3 5 2 5 2^2 5 2^5 1 |b0. The 2.3 walker meets the bit-1 digit 1 3 on its left, leaves a stale 1 and turns the digit into 5. The cluster has moved left past that digit, so k goes 3 → 4. - After 30 iterations: 1,273,992 successors, 219,915 with k > 3, k up to 6 and still growing. - From the 24 normal shapes plus the run's 508 refined keys: 49 iterations, 783,642 successors, k up to 8. The fixed point there (1,252 keys) is only an artefact of the concretization size. - All closure runs: 0 halts, 0 flush violations.

(b) No linear flush bound from eat outputs. - Random NORMAL_EAT words: 3,000 words (≤ 10 digits, gaps 1-3) and 2,000 words (≤ 6 digits, gaps 1-12). All return to a normal word, with 0 halts. τ/L is at most 4.71, and it rises with kmax: 2.27, 2.51, 3.45, 4.09, 4.71 for kmax 0..4. - The family LE (1 3 2)^(j+1) 5 2 1 |b1, j = 0..14 (60 words), is a run of j+1 bit-1 digits above one bit-0 digit, so v = 2^(j+3) − 3: - τ/L rises from 1.2 to 27.3, while L grows only linearly in j; - kmax ≈ j/2; - for LE 3 and even j, τ = 2^(j/2+5) − 3 exactly (29, 61, 125, …, 4093), which is about 11.3·sqrt(v+3). - The same family with gaps 2^3 (j = 0..11) is slower to blow up: τ/L goes from 1.0 to 2.45, with kmax up to 4. - So H (which contains every NORMAL_EAT word) admits eats whose flush is exponential in the 1-run length, and no τ ≤ c·L holds on it.

Run facts (3.2e5 to 1e10, budget_run.py, run_eat1.py). - Value budget: v ≤ m − 5 at all 647,826 normal round starts, where v is the digit value (5 = 0, 1 3 = 1, then b) and m is the unary right of the marker. At all 245 EAT1s, m − v ≥ 158. - At EAT1, the 1-run above the LSB is j1 ≤ 8:

The j1 = 8 eat is at step 4.48e9, with v 511, m 4,253, τ 180 and kmax 3. - Over all EAT1s: max τ/N = 0.351 (N = m + 1, at step 8.1e5), max τ/L = 2.58, min m/L = 3.4, and kmax ≤ 3 throughout.

What a proof needs now (the #28 route). 1. A flush bound in the counter value: τ ≤ f(v) plus a linear term for the bit-0 digits and fillers the walker crosses. The ones family suggests f(v) ~ sqrt(v), with exact powers of two, like #28's L2. 2. The budget lemma v ≤ m, proved inductively: INC/CARRY add 1 to both, EAT0 halves v and adds 2 to m, and a flush must end with v ≤ m. 3. For the linear term: m ≥ c·L at every EAT1, which is still the unproved growth comparison.

Still open. All of the flush lemma (now in value form), the cascade rules as rewrite rules, the init lemma to 3.2e5, and proof.md.

Decision (2026-10-10, open)

Question: Keep #7 parked until #28's flush lemma is proved and then port it (value-form bound), fund a value-form flush stage here now, or park for good? Options: after_28 (recommended; no compute now, one porting stage after #28 closes), value_route (one stage now, likely several), park (for good). The flush_lemma answer is filed in decisions/2026-10-10-flush_lemma.json.

Delta route via kill #30 (2026-10-10): supersedes the STUCK analysis above

#7's earlier STUCK analysis (Deepen passes 1-2, closure_ctl, struct_invariant, flush_lemma, and the open decision.json) is superseded by this route. It stays above for the record and is not used. - The Wave 4 ranker found that #7's table is kill #30's table 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC, mirrored and renamed. Under σ: A,B,C,D,E,F -> E,A,B,F,C,D (with L<->R), #7 = #30, started in #30's state E. The halting transition #7 F0 is #30's D0. σ is unique among 720 x 2 maps. The third start of the same table is Wave 4's W4-1 (#30's B, no mirror), worked by another agent. - proof.md is now a delta proof against #30: - Δ1: the conjugacy. - Δ2: the initial segment. In #30's frame from 0^inf E> 0^inf the left records are e1 = L(0,0001)@15, e2 = L(1,000010010001)@81, e3 = L(3,0001000010001)@183, e4 = L(5,…)@573 and e5 = L(16, 0001)@1059. The restart gives K(1,17,t1) at step 1114. - Δ3: #30's invariant (I1)-(I4) at e5: special residue t1, κ = 0, N = 17 ≥ N_lo(0) = −8. e1-e4 cannot be the base. - Δ4: the rest of #30's argument is start-independent except the base and the finite part. - Δ5: #7's own finite part. On the informal route, e5..e591 (587 epochs) lie below N = 14,796. On the .v route, orbit 687 17 t1 = (17724, Y_692), and Inv 10 holds there (Mw 66 ≤ 2,219, M2 1,032 ≤ 5,601, x 16 ≤ 2,291). - Δ6: the Rocq plan. It is #30's .v plus init7, fin7, inv7 and the #24 flip_halts/perm_halts bridge. - The old dead end, in #30's terms: the "slow carry" whose flush time 2^(j/2) the flush_lemma stage could not bound linearly is #30's nested digestion (D6). Lemma D bounds it by about sqrt(N) against a budget N, a value-form bound, as the flush_lemma decision guessed. - #7's orbit never merges with #30's or W4-1's below N = 20,000, so #30's finite part cannot be reused (X6). - Checks: check_proof.py imports #30's check_proof.py and runs its table-level sections and its section D unchanged (only the start differs, by an asserted source substitution). It adds X0-X6 and V0-V2 (direct simulation of both tables, the base, the .v's Inv). scripts/delta30/orbit_E.c is #30's fs_orbit.c with start E. Its 1e11-step log is data/orbit_E_1e11_LE.txt. - Result: check_proof.py ALL PASS on seeds 1 and 2: 100 claim groups each, about 100 s per seed, logs and JSON in data/check_proof_seed{1,2}.*. Section D from e5 runs to N = 400,004 (11,077 epochs), the ranker's figure. The C log reaches 1e11 steps (517 records, N up to 12,674) with no halt. Status: CHECKPOINT_B*. Next: the Rocq delta (proof.md Δ6). Do it together with W4-1, and post the three starts as one family.

Kill

• 2026-10-11: KILLED_NONHALT. Kill file 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA.v (1,790 lines, 2,028 sentences, sha256 dfb0fb2c8b2ab8a0d302bd3b271f7d81964d9e6e3baa710eef79e0036f700f28) proves top-level Lemma nonhalt: ~halts tm c0.. It is #30's kill file with the proof.md Δ6 delta: #30's table kept as tm30 (notations on it), solve_initE + init7 : E;; tape0 -->* K 17 t1 (1,114 steps), B692/Y692/fin7 (687 model epochs by vm_compute to N = 17,724), inv7 : Inv 10 17724 Y692, nonhalt_from_c, nonhalt_E, phi = σ, perm7 : Perm (flip tm) tm30 phi, and nonhalt by flip_halts + perm_halts. Header cites "the kill for 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC" and "verify/FractalBEC.v, tm10".
• tools/check_kill.sh: PASS 3 times on the same sha256, each with ulimit -s unlimited and ulimit -v 8000000, one check at a time.
• Formalizer (round 1): compile 15.1 s (native on), coqchk -norec pass 66.1 s, 0 assumptions (rocq/log.md, rocq/check_kill.out).
• Independent audit, --json: 17/17 PASS, compile 16.1 s, coqchk -norec pass 71.7 s (no timeout), 0 assumptions. It also confirmed line 405 of data/holdouts/2026-10-07_778.txt (holdouts.py contains, one exact-line match), read the whole file, checked the mirror/rename correspondence of both tables (12/12 + the undefined entry) and that flip_halts/perm_halts are the framework's own (Flip.v, Permute.v).
• Fresh human-readable run for the submission, 00:06:36-00:08:07 PDT (checked_at 2026-10-11T07:08:07Z): 17/17 PASS, compile 17.3 s (native on), coqchk -norec pass 71.5 s, 0 assumptions (closed), 91 s wall (submission/check_kill.txt). Only warning: the second TM_from_str literal (tm30). The watchdog showed about 12 GB available just before, and nothing was killed.
• holdouts.py lookup: in every snapshot from 2024-06-14 to 2026-10-07 (line 405 of the 778 list), and line 381 of data/holdouts/BB6_holdouts_740.txt. holdouts.py solved: absent from busycoq verify/ (no byte-exact, renamed or mirrored proof).
• Table neighbours noted in the public header: mirrored #30 is FractalBEC tm10 except C1; #7 is also BECv1_6x2_solved.v tm10 except E1 (0LA vs 1LE, same start, no renaming), but BECv1's counter (HL2) fails here.
• Submission package: submission/.
• The .v, unchanged (same sha256).
• proof.md: the public delta write-up, rewritten from the working proof.md (sha256 213154ce…, untouched). Header (lists, parent, template FractalBEC tm10 via the parent, Flip.v/Permute.v, the BECv1 tm10 neighbour, status, section map) + Summary + §1-§5 = working Δ1-Δ5 with the math unchanged (#7/#30/W4-1 written as "this machine"/"the parent"/"the third start", #30 §n as "parent §n") + §6 the formal proof (Δ6 rewritten as a description of the .v; the draft/timing items dropped; the comment-stripped diff against #30's .v confirms only tm, the 3 notations, init, B694/Y694/fin694/inv694, nonhalt_from, nonhalt were removed) + §7 numerical checks (Δ7 without script names, paths or the RQ draft check). The "Earlier analysis (superseded)" section is dropped. tools/writeup_lint.py: 0 errors, 0 warnings.
• parent-proof.md: #30's public write-up (submission/proof.md of #30, verbatim), cited as "parent §n" (same §0-§7 numbering as #30's working proof.md; §8.3 is the .v's invariant). Lint 0/0.
• check_kill.txt (the 00:08:07 run, verbatim; contains absolute local paths like the other packages' copies), README.md (lint 0 errors; 1 warning, the holdout snapshot dates).
• discord.md: a draft of 1,617 characters plus <LINK>. Not posted. Its before-pasting list: post #30 first or together; W4-1 (third start) not mentioned, post the three together if it is killed soon; search #bb6 first; PR #15 queue; numbers; check_kill.txt paths.
• Still open: decision.json (the parked after_28/value_route/park question) is moot now and unanswered; it still shows on the decisions dashboard until it is moved or withdrawn.