1RB0LD_0RC---_0LD0RF_1LE1LD_0LA0RD_0RB1RA

Label: 693 (740 list, line 693). Sheet: Bell eats counter; Level-1 tab note "Chaotic bell eats counter" (mxdys, Discord 2024-11-03). Dennis (2026-10-13): fair game for this look. Twins: lines 528, 310 and 548 run time-rescaled copies of this bell trajectory (reports/bec-sweep/ranking.md, Critic). Viewer: https://bbchallenge.org/1RB0LD_0RC---_0LD0RF_1LE1LD_0LA0RD_0RB1RA

693 bursts (2026-10-13)

Verdict: STRUCTURED. No cryptid flag.

Every burst starts from a configuration that is an exact function of one integer n (the bell is about 2^n); the n = 12 tapes were predicted from the formulas before the run reached them, and appeared exactly. Between bursts, every reset obeys one drop law, and the catch-up after a reset is a fixed list that depends only on the ruler digit j. The odd-n burst is a 3/4 : 1/4 split followed by halving rounds whose offsets do not depend on n.

Everything seen is binary arithmetic with small fixed offsets (powers of 2, a period-3 cycle of counter shapes). No rule seen multiplies by 3/2 or branches on residues of the bell. The only case splits are the counter's period-3 shape and, apparently, j mod 3 in the short tails of the catch-up lists. So this is not Collatz-like.

Two pieces are not yet closed formulas: the catch-up lists for j >= 12 (seen only up to j = 11), and the last few rounds of an odd-n burst (the "cleanup", round 8 onward), which differ from n to n. A proof needs both lemmas.

Simulation is evidence only. Nothing here is a kill.

Data

• Left-edge records in state A from the blank tape to 4.1e11 steps: 5,372 records (not kept, ~0.5 MB). Rebuild with scripts/dumpL.py 2.4e11 out.jsonl (about 16 min), then a continuation from its last record with scripts/fromcfg.py for 1.7e11 more steps (steps offset by 239,934,530,469; about 11 min).
• Runs from the canonical burst configuration O(n) (below) for n = 7, 9, 11, 13, 15 (scripts/fromcfg.py; n = 13 to 3.7e10 steps, n = 15 to 2.3e11, both past the ruler restart). Their left-edge records are in work/burst_O<n>.jsonl (steps counted from O(n)).
• work/resets_41e11.txt: every reset to 4.1e11 (left-edge record where c falls), labelled ruler or BURST.
• work/canon.txt: exact-match check of the predicted canonical tapes (scripts/check_canon.py).
• No accelerated model helps yet: sligocki's simulator (tools/qsim.py) finds block size 1 and proves 0 rules on 693 (4.2e6 steps in 150 s), so everything here is direct simulation with the C core.

Notation

At a left-edge record the tape reads

0^inf <A  L  (w1)^c (w2)^d  R  0^inf

• L is the counter, in the words 010, 001, 100 (plus 1001 and a few mixed words near events).
• c and d are the two long runs. Their words are the four phases 0011, 1001, 1100, 0110 of one period-4 pattern.
• s = c + d is the bell.

A head crossing a long run rotates its phase. In state A moving right, 0011 becomes 1001; F right turns 1001 into 1100, C right 1100 into 0110, B right 0110 into 0011. Moving left: D turns 1001 into 0011 and 1100 into 1001, A turns 0011 into 0110, E turns 0110 into 1100.

A reset is a left-edge record at which c falls.

1. The ruler law (between bursts)

To 4.1e11 there are 882 resets. 836 of them have the counter in the form

L = (010)^k 011 (001)^j

and every one of these drops c by exactly

drop(j) = 3 * 2^(j-2) - 2        (j = 2..11: 1, 4, 10, 22, 46, 94, 190, 382, 766, 1534)

No exception (0 mismatches; to 8e10 it was 479 of 518, to 2.4e11 696 of 741).

• k + j is constant inside an epoch: n + 2 words while 2^n <= s < 2^(n+1). Ruler resets per epoch:

• The largest j in epoch n is n for odd n and n - 1 for even n (j <= 11 in epoch 11, checked to the end of the epoch).
• The j sequence cycles 2, 4, 3, X with X = 5, 6, 5, 7, 5, 6, 5, 8, ...: X = 4 + (1 + v2(t)), a binary ruler.
• After a large reset c catches up in halving rounds. The j = 2 reset that would follow X >= 8 does not show as a separate drop; it falls inside this catch-up.

1b. The catch-up is a fixed function of j

For every ruler reset to 4.1e11 I listed the gains of c at the following left-edge records, up to the next fall of c (scripts/catchup.py, output work/catchup_41e11.txt). The list depends on j only: it is the same at every occurrence, for every k and in every epoch (j = 7: 27 times, j = 8: 11 times, j = 9: 6 times; j = 2, 3, 4: 193-213 times each). The only variants are a last entry that is a canonical wrap (E, V, W), and one list cut off by the end of the data.

Three regularities, exact on this table:

• For j = 6..11 the m-th gain is 3 * 2^(j-2-m) + e_m while j - 2 - m >= 1, with offsets that do not depend on j:

e_1 .. e_9 = 2, -5, 4, 3, 4, -1, 3, 4, -1 (period 3 from m = 4: 3, 4, -1)

The term with 2^0 follows the same rule except for j = 8 (3 where the rule gives 2). After it comes a short tail. j = 5 deviates at m = 2 (3 instead of 1). - For j >= 3 the block lasts 3 * floor((j+1)/3) + 3 rounds: the counter eats its 001-words three per three rounds, as in the odd burst. - Over the block, c gains exactly 2 per round net, for every j = 2..11: (sum of gains) - drop(j) = 6, 12, 18, 24, 30 for blocks of 3, 6, 9, 12, 15 rounds.

So the left-edge values of c between canonical events are a closed function of the binary ruler: drop(j), then the fixed gain list of j. The open part shrinks to the gain lists for j >= 12 (they occur from epoch 13 on, beyond direct simulation) and their short tails, which look periodic in j mod 3 (j = 7 and 10 end in 2, 5, 4).

The odd burst runs the same halving with other constants: for n = 15 the c gains from round 2 are 12292, 6147, 3076, 1535, 771, 388, close to the j = 15 rule (12290, 6139, 3076, 1539, 772, 383) but not equal, because the counter words differ.

2. The bursts are canonical events

The other 46 drops are all accounted for:

• 12 in the start-up before step 127,661 (bell under 40);
• the rest at the canonical events below, or inside an odd-n burst. The 7 non-ruler drops between 8e10 and 4.1e11 are exactly E(12), V(12) and W(12,0..4).

Odd n: O(n). The bell reaches exactly 2^n - 1 with d = 0 and the counter all 010:

O(n) = 0^inf <A (010)^(n+2) (01100)^2 (1100)^(2^n - 1) (1001)^2 100011 0^inf

Even n: E(n), V(n), W(n,i). c overflows 2^n and wraps (drop 2^n):

E(n)   = 0^inf <A (010)^(n+2) (0110)^3 (0011)^(2^n - 1) (001)^2 1 (00110)^2 0^inf                 (c = 3)
V(n)   = 0^inf <A (010)^(n+1) 011001 (0011)^5 (1001)^(2^n - 1) (0011)^2 0^3 1^2 0^inf              (c = 5)
W(n,i) = 0^inf <A (010)^(n-1-2i) 01 (100)^(2i+4) (1100)^c_i (0110)^(2^n + c_i - 8) 01 (0011)^2 0^3 1^2 0^inf
         c_i = 2*4^i + 5 = 7, 13, 37, 133, 517, ...     for i = 0 .. (n-4)/2

After W(n,i) the ruler runs with largest j = 2i + 3, then the next W follows. After the last W, i = (n-4)/2, that is j up to n - 1, and then O(n+1) occurs.

Exact matches (whole tape, byte for byte, in this order):

V(n) also matches for n = 6, 8, 10, 12 (steps 958,793; 48,539,363; 2,922,713,505; 184,196,676,959). The steps of W(12,0..3) are 184,601,031,774; 186,224,346,174; 192,812,539,814; 220,718,381,542. W(12,4) follows at 359,177,463,994 (continuation run). In all, 26 of 26 predicted tapes for n = 5..12 occur, in the predicted order.

The n = 11 to n = 12 step is the first that was predicted before it was seen: E(12) and W(12,0..4) were written down from the formula when the run stood at 8e10 (work/canon_8e10.txt lists them as not seen) and found later at 1.84e11 to 3.59e11.

So the epoch map is closed at the level of these configurations:

E(n) -> V(n) -> W(n,0) -> ... -> W(n,(n-4)/2) -> [ruler up to j = n-1] -> O(n+1) -> [burst] -> [ruler up to j = n+1] -> E(n+2)

3. Inside an odd burst

Put Q = 2^(n-2). Round r is the r-th left-edge record after O(n).

with delta_2..delta_7 = 0, 2, 5, 3, 5, 8 for n = 11, 13 and 15. For n = 9 the same deltas hold up to r = 6, and d runs out at r = 7; n = 7 runs out at r = 5. The counter meanwhile cycles through three shapes, eating three 001 words every three rounds:

(010)^r 011 (001)^x (100)^2  ->  (010)^(r+1) 01 (100)^(x-1) (1001)^2  ->  (010)^(r+2) 01 (100)^x  ->  ...

The rounds seen only halve d (d to about d/2, minus a small offset). No round multiplies by 3/2, and nothing Collatz-like was seen; this looks like binary arithmetic, the counter recording the halvings.

Cleanup (r >= 8) and the flip. After round 7 the counter changes shape and the remaining d (about 3 * 2^(n-8)) is used up in a few irregular rounds. Then the field flips to a single run and the ruler restarts with d close to 2^n:

The cleanup words differ with n (n = 7 and 13 both use 1001001 words, n = 15 uses 10011001001001 and 10011001100; n = 13 also has one extra 2^n wrap, c = 8203 to 11, four rounds after the flip). For n = 13 and 15 the cleanup takes 5 rounds. For n = 15 its d values still roughly halve each round (376, 207, 97, 47, 18); for n = 13 the first step does not (88, 63, 25, 15, 10).

These are not new words, though. The ordinary catch-up after a large ruler reset uses the same counter words: 129 left-edge records of the main run contain 1001001-words. For example, after the j = 7 reset at step 113,589,153,096 the counter passes through

0 (100)^5 (1001001001)^3        (010)^8 (0100110010)^2 01

which are the shapes of the n = 13 cleanup (0 (100)^7 (1001001)^4 001, (010)^9 (0100110)^2 (001)^4). So the cleanup looks like the catch-up mechanism acting on a small gap, not a separate process.

How the ruler restarts, with k + j = n + 2 as in the table of section 1:

The catch-up lists after these resets are exactly the lists of section 1b (checked for the n = 13 run: j = 2, 3, 4, 5, 6; for n = 15: j = 2, and the start of j = 5). n = 15 has no extra 2^n wrap between the flip and the end of its run, unlike n = 13.

Reaching E(n+1): the main run checks it for n = 5, 7, 9 and 11, exactly (E(6), E(8), E(10), E(12)). For n = 13 and 15 it is out of reach of direct simulation (E(14) is near 1.2e13 steps, E(16) near 7e14).

What is open

• The catch-up law of section 1b for all j: the leading terms 3 * 2^(j-2-m) + e_m fit j = 6..11, but the short tails (after the 2^0 term) are seen only for j <= 11, and they may depend on j mod 3. A proof needs them for every j, from the word-level rules.
• The same halving inside an odd burst, whose offsets (delta_r and the cleanup) differ from the reset catch-up because the counter words differ.
• The cleanup after round 7 of an odd burst, for all odd n. Its input d grows like 3 * 2^(n-8), so it is not a fixed finite patch; it is probably the same catch-up mechanism on a smaller gap. It takes 5 rounds for both n = 13 and n = 15.
• That every odd burst ends in E(n+1): checked to n = 11 only.
• The round map itself at word level (normal round, reset round, catch-up round), from the transition table.

Route if funded

1. Word-level round map from the transitions, using the phase rotations above. Check it against all 5,372 left-edge records to 4.1e11.
2. Closed form for the catch-up. Check it against every reset to 4.1e11 and the bursts for n = 7..15.
3. With that round map, an abstract (record-level) simulator can run past O(13) and E(14), which direct simulation cannot reach. It must reproduce all 5,372 records exactly first.
4. proof.md: induction on n, E(n) -> O(n+1) -> E(n+2), with the ruler as a binary counter of n + 2 words.
5. The same abstract argument then carries 528, 310 and 548, each with its own word-level rules.

Stop rule for that stage: if the catch-up offsets do not close within 2 hours, park.

Proof stage (2026-10-14)

Funded by Dennis ("fund 693", 2026-10-14). About 2 h. Outcome: parked (STUCK). The catch-up law was not closed, and it turned out not to be the right lemma. Working version in proof.md, checker scripts/check_proof.py (C1-C7 all pass).

The left-edge records are not the rounds. Between two records the machine runs a binary counter with 3-cell digits (000, 001, carry 010), big-endian, between the marker 1 and a 13-cell interface. Each shuttle of the head between the counter and the wall of the period-4 field is one counter step, and it moves the wall one block (phase 1) or half a block (phases 2-4) to the left. Each time the wall reaches the interface the field has rotated one step and a new wall starts at the right end (phase change). Once per revolution (4 phases) the wall "eats" the lowest digit (it becomes a frozen 011 and the interface moves 3 cells left). A left-edge record is a counter overflow: the carry runs to the blank end, the counter gains a digit and restarts at 0. Example: the record at 1,128,713 is followed by 127 = 2^7 - 1 counter steps (8 in phase 1, 119 in phase 2) and the next record at 1,173,120 (work/inner_shapes_12rounds_from_1128713.txt, scripts/inner_shapes.py).

Rules proved or checked this stage (proof.md sections 2-3): - C1 eight rotation rules (4 steps), with B reading only 0 inside them; C2 halting criterion: halt iff A or F reads 0 with a 1 to its right (the undefined entry is B1, not C1). - Phase 1: X1(g,c+1,d) -(16c+49)-> X0(g,c,d+1); X0(g,c+1,d) -(16c+49+6t)-> X1(g+1,c,d+1), t = trailing 001 digits. Independent of d. - Phase 2: Z1(g,x,y+1) -(8x+19)-> Z0(g,x,y); Z0(g,x+1,y) -(8x+43+6t)-> Z1(g+1,x,y+2). Independent of y. - Checked on random constructed tapes (40 per rule in the checker); the pass-by-pass derivations are not written.

Random-parameter tests (evidence): 620 runs from tapes the orbit never produces (counter far too long or too short, random digits, random wall position, 5 record skeletons), 1e8-2e8 steps each: 0 halts (work/randparam_*.txt, scripts/randparam_*.py). So safety does not seem to depend on the counter/wall/field correlations that the drop law and the bursts describe.

Open lemma: closure of the shape family 0^inf 1 <g> I_k (u_k)^x h_k (v_k)^y R_k 0^inf (g any word over {000,001}, x, y free, up to 16 phase types = 4 phases x 4 interface alignments, plus the transient shapes of phase change, eating and overflow) under the machine, with no A/F-on-0-before-1 step. P1a/P1b/P2a/P2b are 4 of its cases.

Route for a next stage: a symbolic shape explorer (literals, runs w^(>=m), a star {000,001}*, C1 as accelerations) to compute that closure, then one checked rule per explored transition. This is a closed-tape-language proof, so it bypasses the catch-up law, the burst tapes and the record-level simulator. Same method for the twins 528, 310, 548 with their own words.

Proof stage 2 (2026-10-14)

Funded by Dennis ("fund_closure" on decision.json, 2026-10-14). About 2 h. Outcome: parked (STUCK). The closed-tape-language route does not close. Working version: proof.md section 8. Checker: scripts/check_proof.py --ctl (C1-C9 pass). Answered decision moved to decisions/2026-10-14-fund_closure.json; new decision.json (park, recommended, or a stage 3 with a counter clock).

Verified deciders (step 0). busycoq's CTL62 decider, extracted to OCaml (the #7 extraction), with a new driver for every numeric parameter kind (scripts/ctl_extract/main.ml, README there; calibrated on three upstream certificates). About 190 runs on 693, 0 true (work/ctl_sweep_A.jsonl, work/ctl_sweep_B.jsonl): - RWL_mod / CPS_LRU, block sizes 3, 4, 6, 8, 12: block 12 (field period 4 x digit width 3) runs out of 6 GB in about 2 min or times out at 120 s; the rest false. - NG (n = 2-20), NG_cr, RNGS_mod_QSym_FAR, RWL_mod_FAR, CPS_LRU_FAR in the upstream parameter shapes: all false within a second. - RWLAcc is a single-orbit loop detector and cannot handle a binary counter. Not run on the twins (nothing to transfer).

Shape explorer (step 1). scripts/ctl_explore.py: tokens are literals, exact runs (w)^n, runs (w)^>=m, the counter {000,001}^>=m and 0^inf; steps are single machine steps or run rules (any word that the head crosses in the same state, so C1 and more); exhaustive case splits; normalisation only enlarges the language (merge, absorb, cap at K, fold digits into the counter when a field run lies between counter and head). explore_macro stores only turns and splits (about 10x fewer shapes). scripts/ctl_validate.py: regex membership, step check, member runs, orbit check with C-simulator snapshots.

Three bugs/artefacts found and fixed on the way, each visible as junk or a spurious halt: 1. A start-shape typo (0011001101 for 00110011001) made the first pass turn at the interface. 2. Eaten digits look like counter digits (001 is also a field group). Folding them back into the counter gave 2 spurious halts at K = 4. Fix: digit cells carry a position mark; a digit loses it when it takes a value outside 000/001/010, or when the head enters it from the right in a state other than A (from the left: other than B). In BFS runs the entering rule fires only on the lowest digit, in state D; but the exact replay shows it also fires on real digits after the first eating (source 2 below). No halting step after the fix. 3. A small cap K (3-5) lets the field be short, and a short field behaves like the start-up (the phase change rebuilds the right end as R1). With K = 64 this did not show up in the runs (a phase ends only after a run with lower bound 64 is used up).

Validation (step 2). Step check: 5,996 (C8) plus 12,000 random concrete steps or run passes land in a symbolic successor, 0 failures. Orbit: all 947 head-turn configurations of steps 1,128,893 to 1,188,893 (phases 1-2, the 2-to-3 phase change, early phase 3) lie in the explored set (K = 64, 1.2 million shapes); C9 checks the first 108. Members: 300 random members of explored shapes (half from the newest quarter), 1e7 steps each, 0 halts.

Why it does not close. Runs: K = 3/4/5 to 400,000 single-step shapes; K = 20/64 with exact counts to 1.5 million; macro BFS at K = 64 to 2.5 million (Q = 0) and 2.6 million (Q = 3, short counters exact). None closes, no halting step. Distinct skeletons keep growing (Q = 0: 300 at 0.1 M, 1,215 at 1 M, 3,460 at 2.5 M). Late shapes have counter-to-field regions far longer than the orbit's 13-cell interface, e.g.

0^inf 1 {000,001}* 1001 (0000)^1 01 (0000)^2 00 (0110)^3 0 (1100)^>=59 111 B> 011101 (1001)^3 (0011)^2 00011 0^inf

(34 cells before (1100)^>=59). 0000 blocks by themselves are real: the orbit has them in the interface while the head is out in the field during P1a.

Source 1 (identified): the counter's value is free in the abstraction, so a branch can avoid overflows for ever while the wall eats one digit per revolution. The counter drops to 0-1 digits, then overflows and eatings alternate every few counter steps. On the orbit this never happens because overflows add digits as fast as eatings remove them (k + j constant). Q = 3 does not help: the counter is exact only once written out in full; while it is {000,001}^>=m its value is free and each eating lowers m.

Source 2 (an explorer defect): an unsound diagnostic run (--no-empty: the counter never runs out of digits) still grows (K = 64: 2,848 skeletons at 1.9 M shapes) with the same long interface regions. scripts/ctl_replay.py replays the orbit exactly through the explorer (X0 with exact counts, counter written out): the eaten-digit rule fires at the real eating (step 1,222,705), but after it the head enters the low digits in state D during ordinary counter steps, and the rule unmarks four real digits within about 440 symbolic steps (replay steps 12,151-12,589). So the rule "entered by a state other than A means eaten" is wrong after the first eating. At step 1,642,188 the real tape is 1 000 001 001 001 001 001 001 001 001 100 110 011 ... (head in D at position 6) and the replay shows 2 marked digits plus 5 plain 001 groups. Plain digits never fold back, so even the orbit's own configurations drift to long counter-to-field regions (the period-3 001001... of the junk shapes). Soundness is not affected, but the closure question cannot be answered until the bookkeeping is faithful on the replay. A quick mark-free variant (--gap G: fold digit groups while G cells remain before the field run) grows faster (G = 13: 1,321 skeletons at 0.7 M; G = 16: 3,935 at 1 M).

What carries over to 528, 310, 548. The explorer, the validator and the decider driver are generic in the machine string; the start shape, the digit words (000/001, carry 010) and the eating rule (counter entered in A from the right, in B from the left) are 693's. Since the obstruction is the counter/field coupling, the twins would hit the same wall: this route does not settle them either.

Route for a stage 3, if funded. First make the digit bookkeeping faithful: replace the entering rule (it unmarks digits that D enters in ordinary counter steps after the first eating) and require the exact replay to keep every real digit marked over many revolutions while unmarking exactly one digit per revolution; then rerun the no-empty diagnostic. Then a counter token with a clock: digit count D plus the lemma "a counter of D digits overflows within 2^D increments", and the phase lemma "a phase has at least s/2 counter steps". Together they bound the eatings between two overflows and keep D >= log2(s) - c. That is the inequality form of the catch-up law, much weaker than the exact lists of stage 1. Alternatively prove that every malformed interface heals within a bounded number of revolutions, but the list of malformed interfaces kept growing.

Proof stage 3 (2026-10-14)

Funded by Dennis ("fund_clock" on decision.json, 2026-10-14). About 2 h. Outcome: parked (STUCK) by the stop rule: the shape set does not close within the stage. Both sources of the stage-2 obstruction are repaired, though, and the explored set now behaves very differently. Working version: proof.md section 9. Checker: scripts/check_proof.py --ctl3 (C10, C11). Answered decision moved to decisions/2026-10-14-fund_clock.json.

The counter is two blocks. The eating is two local rules: 001 <D -> <A 011 (an eaten 1 becomes the frozen 011 and is carried on) and 000 <D (an eaten 0 becomes the low end of a counter shifted by one cell). So after a few eatings the counter is 1 H sep L, two digit blocks in different alignments with a short separator (1, 0011, 011); the records' (010)^k 011 (001)^j is H, sep, L at an overflow. Stage 2's positional marks could not represent the shifted block, which is why real digits fell out of the counter (source 2).

(1) Writer marks (scripts/ctl_explore3.py). A cell written by a left-moving E, D or A step is marked e, d, a; the carry runs A, D, E right to left, so every real digit reads e d a in its own alignment. A digit = marks e d a and value 000/001; several S tokens allowed. Guided replay (scripts/ctl_replay3.py: symbolic shape and real machine in lockstep, the counter folded, the case containing the real tape picked at each split) from step 1,128,893 to 21,129,033: 931,457 symbolic steps, 41,151 splits, 125 overflows, the eatings between them and the odd burst O(7); inside the shapes at every step, at most 40 non-digit cells between marker and field (stage 2: unbounded drift). C10 checks the first 2e6 steps.

(2) Counter floor = the clock. S now means "at least Q+1 digits"; splitting it gives S 000 | S 001 | every exact word of Q+1 digits (an identity of languages). S can no longer be eaten to nothing, and a counter that really is short becomes exact, so it overflows within 2^(Q+1) increments, well inside one phase (>= K = 64 counter steps). No symbolic parameter is needed.

(3) Closure. Step check (C11 and a larger run): 9,000 random concrete steps/run passes from explored shapes land in symbolic successors, 0 failures. No halting step in any run. Runs (macro BFS, Q = 2 unless stated):

Fixes on the way: carry-digit runs (010)^n are now compressed (a carry through a long all-ones S made literals grow), and digit runs (000)^>=m fold into S only when the block's language has at least Q+1 digits (an unsound shortcut was caught before any result was used).

What is left. With K = 64 the skeleton count levels off (949-950 from 1.6 M to 3.5 M shapes, against stage 2's steady growth to 3,460), but the shapes keep coming: the queue holds the same skeletons with new exact counts (two carry runs (010)^n, the run behind the wall, the field's lower bounds, each up to K). Capping the 3-cell runs lower (KD = 3) is too coarse (skeletons 2,435 at 1 M and growing); K = 16 or 32 brings back short-field artefacts (K = 16: 2,208 skeletons at 0.7 M; K = 32: 971 flat to 2.5 M, then 1,285 at 3 M); Q = 3 does not help (1,175 skeletons at 3.5 M). So the next step is mostly engineering: a compiled explorer (C or OCaml) to run K = 64 to 10^8 shapes, or a coarser count abstraction for the carry runs. Even a closed set would then need an independent certificate check (and a formal checker) before it is a proof.

Twins 528, 310, 548. Writer marks and the floor are generic; the digit words (000/001, carry 010) and the start shape are 693's. Nothing was run on the twins.

Data: work/stage3_replay_2e7.txt (guided replay), work/stage3_bfs_*.log (closure runs; logs of the K = 16/32/KD = 3 runs end where they were stopped). Scratch diagnostics (late skeletons, queue samples) were not kept.