Decision: Chaotic Bell Class 3 core (12 lines) after the write-1 exit study
2026-10-14. Background: study.md in this folder. Lines 23, 206, 403, 415 (T1), 69, 245, 330, 668, 696 (T2), 178, 376, 382 (T3).
Question
The extra 1 written at the exit turned out to be bounded: - it merges into the stripe within two bounces; - it leaves at most 9 loose marks and at most 7 parity defects over 10^10 steps.
So the 12 lines should have a regular invariant. It just isn't one that upstream's sibling recipes find. Should we build our own closure checker for this core?
Options
| id | option | what happens | cost | odds (est.) |
|---|---|---|---|---|
| A | Build a token-level closure explorer for the core (recommended) | (1) Shapes made of (01)^{>=K} runs, a finite set of mark clusters (00110, 0, 1 and their small composites) and a "rest of tape" token on each side, in both stripe phases. (2) Explore T1, T2 and T3; a closed shape set with no halting step is the invariant. (3) Compile it to left and right NFAs and send it through Astra's gate-passing package. (4) Per-line startups, then check_kill on each of the 12. |
1-1.5 agent-days to a closure verdict; then about 0.5 day to package the first table and a few hours each for the rest. No GPU. Coq time: 12 check_kill runs. | A closed language for at least one table: 0.35-0.5. All 12 lines given closure: about 0.7 (the risk is packaging size). Expected lines: about 3-4. |
| B | Hand the 3 tables to a generic automaton search | Either direction 5 (not yet funded), or Astra's new SAT/SMT automaton synthesis, which started at 16:13 today on two Unknown tables and excludes CB3 while we hold the claim. Seed it with the facts from this study: no parity constraint, small cluster alphabet, exit offset per table. Releasing the claim to Astra would need a claims.tsv handover line. | About 2 hours for us; the rest is the other lane's budget. | 0.15-0.25 (the generic FAR family already failed 450 times at sibling sizes; a new SAT search is untested here) |
| C | Park | Put the mechanism and the rules into an atlas note. Not a cryptid, so no rules file. | About 1 hour | 0 kills |
Recommendation: A, with a stop rule
Why A. - Every measurement says the holdouts live in the same stripe language as the proven siblings, minus the parity restriction: - random structured tapes: 0 of 5,100 halt; - tapes whose runs are at most 2 long: 0 of 2,400 halt; - random-start orbits: mark clusters stay at 4 tokens or fewer. - All 3 tables share their rules exactly except the exit offset. So one explorer covers all 12 lines. - The 693 explorer already gives us the split and fold machinery to adapt. - Nobody else holds these lines, and the class has had no kill in 2026.
Stop rule. Stop and fall back to C if, after 1.5 agent-days, either: - the explorer's cluster set grows past about 40 words or literal widths past about 12 cells without closing; or - closure needs a gap-length condition, which would mean the arithmetic matters after all. Then re-run the cryptid check.
What I need from you. A, B or C. If A: may packaging go through Astra (it offered, 14:32) once a closed set exists?
Answer
Dennis, 2026-10-14: A (build the token-level closure explorer; package any closed set through Astra's gate-passing certificate package).
Outcome of option A (stages 1-2)
The stop rule fired after about 5.75 agent-hours, so option A is stopped. There is no kill and no closed set: the explorer did not close even the calibration sibling S0LC, which FAR proves upstream. So nothing went to packaging or check_kill. T1 ran only in stage 1, and T2 and T3 were never explored.
Each stage stopped on the size trigger:
- Stage 1: the cluster alphabet went past 40 words. Runs of separators, the period-4 stripe 0110 0110 ..., entered the alphabet one width at a time.
- Stage 2: packs became tokens, but the cluster words went past 40 again, or a cluster went past 20 cells. The cause is that the abstract left side lets 5-segments repeat without limit, and a left sweep turns them into touching separators. The real orbit never has more than 2 in a row.
The other trigger never fired. No abstract halt appeared, and no closure needed a gap-length or parity condition, so the cryptid check stays negative.
The full log and the facts we learned are in explorer.md (section "Outcome"). Ledger rows are in coord/attempts.tsv; run python3 -B tools/attempts.py query CB3.
Next
Question. Option A stopped on its stop rule. Do we hand the CB3 core to Astra's automaton search, park it, or fund a third explorer stage past the stop rule?
| id | option | what happens | cost | odds (est.) |
|---|---|---|---|---|
| B | Hand the 3 tables to Astra's SAT/SMT automaton synthesis (recommended) | (1) We append a handover line in coord/claims.tsv that gives the class to astra, and mail Astra the 3 literal tables, the 12 lines with their starts and the facts below. (2) Calibration gate first: Astra's synthesis must find a certificate for the write-0 sibling S0LC (FAR proves it upstream). If it cannot close S0LC in its first bounded stage, CB3 is parked (C). (3) Any closed set goes through Astra's certificate package and then check_kill per line. A kill needs our audit as the second agent. |
About 1 hour for us. The rest comes from Astra's budget; Astra's 19:19 board entry says none of its compute is running. | 0.1-0.2 for at least one table. The search is untested on this core: on other tables it has 22 negative and 2 inconclusive ledger rows and no kills, and the sibling-size FAR grid already failed 450 times. |
| C | Park | Write an atlas note: the mechanism (study.md), the explorer facts and the open run-length problem. It is not a cryptid, so there is no rules file. Our claim stays, with a PARKED note. |
About 1 hour | 0 kills |
| A3 | Fund explorer stage 3, past the stop rule | (1) Give the left rest-of-tape automaton a run-length counter: at most 2 consecutive 5-segments, matching the real orbit. (2) Find where repeated 5s still come from: the fold's move into the tail state, or the split of the "≥ K" classes. (3) Re-close S0LC, then T1-T3. (4) Package and check_kill on any closure. Stop if S0LC does not close within the stage. | 2-3 agent-hours to a verdict on S0LC; then about half a day per table to package | Under 0.1. Each fix so far (gap classes, packs, the NFA fold, derived states) exposed the next leak, and all of them stay inside one abstraction family. |
Facts to send with B. These come from the real orbit to 3e6 steps on S0LC and T1, and from the explorer:
- long gaps need a length class (exact below K, "≥ K, even or odd" above), and lone defects are at least 7 cells apart;
- at most 2 consecutive 5-segments on the left;
- clusters have at most 8 segments (14 cells), and the orbit uses 11-14 cluster words on S0LC;
- packs of separators are transient (0 halts in 80 seeded runs on T1 and T2);
- no gap-parity condition was needed on S0LC or T1;
- the 3 tables share their rules except for the exit offset (study.md).
Recommendation: B, with the S0LC calibration gate. What is missing now is the right regular abstraction: one that bounds runs the real orbit bounds and nothing else. A solver-driven automaton search is built for exactly that, and our hand-guided fixes have each exposed a new leak. B costs us about an hour, and Astra has free capacity now. The S0LC gate means a search that cannot close the sibling stops at once, and then we park (C). A3 is the fallback only if Astra declines or cannot take it.
Also possible, cheap, not recommended on its own. One RWL_mod run with the sibling recipe at a higher memory cap. At 6 GB it ran out of memory on all 3 tables, while it proves S0RB in 7 s. A 14 GB cap for 1 hour would break the 6 GB rule for heavy processes, so it needs your OK.
What I need from you. B, C or A3. If B: may we hand the CB3 class claim to Astra with a claims.tsv line, and take it back if the calibration gate fails?