CB3 closure explorer: progress log
Direction 4, option A (Dennis, 2026-10-14). Stages 1-2 of at most 3 done; stage 2 hit the stop rule (see the stage 2 log below). Option A is stopped until Dennis picks the next step (decision.md, section "Next"). Code and outputs: reports/cb3/explorer/.
Outcome (2026-10-14, after stage 2)
No closed set, so no kill. The explorer did not close a tape language for any table. It did not even close the write-0 sibling S0LC, which FAR proves upstream and which we close first as calibration. So nothing was exported, packaged through Astra's generator or run through tools/check_kill.sh. T1 was run only in stage 1, and T2 and T3 were never explored.
Which stop condition fired. Option A's stop rule has two triggers: - The size trigger fired in both stages. In stage 1 the cluster alphabet went past 40 words. In stage 2 it went past 40 words again, or a cluster went past 20 cells. This happened after about 5.75 agent-hours, well inside the 1.5-day budget. - The gap-length trigger never fired. No closure needed a long-gap length or parity condition. The cryptid check stays negative.
What we learned. These facts hold for any later method on this class:
1. Long gaps need a length class. "Any length ≥ 3" gives abstract halts from lone defects 3 or 5 cells apart. Real orbits keep them at least 7 apart. With exact lengths below K and "≥ K, even or odd" above, no abstract halt appeared in any run.
2. Packs of separators are real but transient. These are runs of 2-segments, the period-4 stripe 0110 0110 ....
- Real orbits reach 14-cell clusters (3 packed separators). Small structured tapes reach 14-17-cell packs, and the widths plateau over 3e6 steps.
- Tapes seeded with packs up to 32 cells: 0 halts in 80 runs of 1e5 steps on T1 and T2.
3. The real orbit bounds its runs; the abstraction does not. To 3e6 steps on S0LC and T1:
- at most 2 consecutive 5-segments on the left;
- every cluster has at most 8 segments (14 cells);
- the orbit uses 11-14 cluster words on S0LC.
An automaton with a finite cluster alphabet and gap classes, but no run-length bound, lets 5-segments repeat. A left sweep then turns them into touching separators.
4. More history does not help. History 2 made the drift worse in stage 1 and left the stage-2 leak in place.
5. Discovery from scratch feeds on its own junk. Seeding the automaton from the real orbit is needed.
6. No gap-parity condition was ever needed, on S0LC or in the stage-1 T1 runs. T2 and T3 were never explored, so this is not yet tested against their persistent even gaps (study.md).
Reusable code. All in reports/cb3/explorer/:
- segx.py: its step semantics match tools/sim on 31,340 sampled symbolic steps (5,981 in stage 1 and 25,359 in stage 2), with 0 mismatches.
- export_cert.py and check_cert.py: certificate export and an independent checker, smoke-tested.
- walk_cert.py: written but never run, because nothing closed.
Ledger. Each stage has its own row in coord/attempts.tsv. On 2026-10-14 the following were added:
- a row that closes the stage-1 in-progress row;
- the concrete pack and wide-configuration probes (halting-sim);
- the real-orbit bounds (observe);
- a method row with the design lessons, so that a future closure explorer (for example on the CB1 core) starts from them.
To see them all, run python3 -B tools/attempts.py query CB3 or query 'closure explorer'.
What the explorer is
It searches for a regular tape language that contains the real orbit and is closed under single machine steps. A closed language with no halting step is a non-halting certificate.
Segment view of a tape side. Each side of the head is read nearest-first and cut into segments: maximal alternating blocks (no two equal neighbours). Two consecutive segments meet at a defect (two equal cells), so a side is fully given by its first cell and its list of segment lengths.
In this view:
- the stripe (01)^n is one long segment;
- a separator 00110 between stripe runs is the short-segment cluster (2,2);
- a glider is a lone defect between two long segments (the empty cluster).
Shapes. A side shape is (first cell, segment tokens, tail):
- a token is an exact length below K, or "length ≥ K with a given parity";
- the tail is the blank tape, or X(q), the rest-of-tape automaton of that side started in state q.
The rest-of-tape automaton X. A unit is a cluster of short segments (length < T) followed by one long segment, with its length class (exact T..K-1, or "≥ K even/odd"). The automaton's state is the previous unit (history 1). Its transitions are "unit u may follow unit q" and "after q the tape may end with this short cluster". There is no condition on long lengths beyond their class, and no parity condition on long gaps.
Exploration. This is a lazy closed-tape-language search in the dual-head semantics of the certificate checker:
- a key is (left shape, right shape, state, direction);
- a step pops the scanned cell (exact splits) and pushes the written cell onto the side behind the move;
- a pushed side keeps its first N long segments explicit and folds the rest into X(q), after checking that the rest is in X(q);
- missing automaton transitions are added (discovery), and the run is repeated until a run adds nothing.
Every shape's language is exactly the union of its split edges. These are the edges that the exported certificate and the checker use.
Checks
validate_steps.py: takes sampled symbolic transitions, builds random concrete members, runs one step of tools/sim, and checks membership of the result with a structural test that does not use the edge lists.check_cert.py: an independent certificate checker. It reads only the exported JSON and checks closure (every edge into every scanned state, existential push, listed successor key) and acceptance of the concrete entries by NFA simulation.
Log
Stage 1 (2026-10-14, about 3 h): explorer built and validated; no closed set yet
Verdict. No table closed in stage 1. No configuration tried produced an abstract halt once long gaps were kept as length classes. The obstacle is a third token: packs of separators (runs of length-2 segments, i.e. the period-4 stripe 0110 0110 ...). The explorer folds them into the cluster alphabet one width at a time, so the alphabet grows without closing.
The stop rule fired for these configurations: more than 40 cluster words, without closing. It did not fire on gap-length conditions: no closure here needed a long-gap length or parity condition, so the cryptid check stays negative.
Calibration first. Every configuration was run on the write-0 sibling S0LC (proved upstream by FAR) before the holdouts, since an explorer that cannot close the sibling will not close T1-T3.
| # | configuration | S0LC (sibling) | holdouts | what it showed |
|---|---|---|---|---|
| 1 | X = free cluster sequence, long gaps "any length ≥ 3"; K=6, T=3, N=2..4; entry blank or step 1e5 | abstract halt at once | not run | X let lone defects sit 3 or 5 cells apart; a left sweep then reads 1 1 in F. Real orbits keep them at least 7 apart (a right sweep turns each S 01 into a defect plus a 7-cell segment). |
| 2 | units carry the long-length class (exact 3..K-1, else ≥K even/odd); K=8/10, N=2..4 | no halts; stops on clusters wider than 12, then 20, cells | not run | real orbits themselves reach 14-cell clusters (3 packed separators; realwidth.py, 3e6 steps), so the 12-cell width guard was raised to 20 |
| 3 | X with history 1 (state = previous unit), discovery from scratch, N=1/2/3 | N=1: wide at once; N=2: about 2,900 R-transitions and wide after 785 s; N=3: 3M-key cap | not run | discovery feeds on its own junk (tiny abstract tapes ending in odd packs) |
| 4 | history 1, automaton seeded from the real orbit (6e5 steps, every 37 steps), N=2 | stop rule: 41 cluster words, after +3,913 R-transitions and +722 ends | T1 (4 starts): seeded 29 words, stop rule at 44 words after +1,144 R-transitions | the additions are runs of 2-segments, up to 24 cells; the left automaton stays at lone defects and gains nothing |
| 5 | history 2, seeded, N=2 | stop rule: 41 words after +74,000 R-transitions | not run | more history makes the drift worse, not better |
| 6 | as 4, plus folds where the segment before X was shortened (merge into X's first unit) | stop rule at 43 words after 65k keys | T1 same, 44 words | packs now grow through the merge itself |
Checks done.
- Step semantics: 5,981 sampled symbolic steps on S0LC, T1, T2 and T3 (about 1,500 per table). Each step was compared with one tools/sim step on a random concrete member. There were 0 mismatches (validate_steps.py).
- Certificate pipeline: export, then check_cert.py. The smoke test closes on 1RB---_0RA---, catches a halting machine, and FAILs a certificate with one key removed.
- Packs on the real machine: packs are real and transient. Small structured tapes reach 14-17-cell packs, and the widths plateau over 3e6 steps (tinytapes.py, packgrowth.py). Tapes seeded with packs up to 32 cells give 0 halts in 80 runs of 1e5 steps on T1 and T2, and the packs mostly dissolve (packs.py).
- The explorer's wide abstract configurations, run concretely, stay at width 20-21 for 1e6 steps.
Stage 2 plan (about 2-3 h).
1. Add a pack token, "2^m with m ≥ M and a parity". It works like the long-gap class, both in explicit shapes and in X units. Packs then never enter the cluster alphabet, and the cluster words should stay near the real orbit's 14 (S0LC) to 29 (T1).
2. Keep history 1 and seeding from the real orbit, and log every addition.
3. Close S0LC first, as the calibration, then T1, T2 and T3.
4. On a closed run: export, check with check_cert.py, run the multi-step tools/sim walk, then package through Astra's generator. The entry is blank with startup 0, or a left-end configuration below 1,000,001 steps.
Stop for stage 2. Stop if the cluster alphabet still passes 40 words with packs tokenised. Also stop if an abstract halt appears that a concrete member reproduces, or if a closure needs a long-gap length or parity condition (that triggers the cryptid re-check).
Stage 2 (2026-10-14, about 2.75 h): pack tokens added; the stop rule fired on the calibration sibling
Verdict. The stop rule fired: with packs as tokens, the cluster words still went past 40. No closed set was found, not even for the write-0 sibling S0LC, so T1, T2 and T3 were not run. There is nothing to export or package.
Two things the stop rule watches for did not happen: - No abstract halt appeared in any stage-2 run. - No long-gap length or parity condition was ever needed. The cryptid check stays negative.
What was built. In segx.py:
- A pack token P(n): a run of m length-2 segments, with m ≥ n and m of the same parity as n.
- Every maximal run of 2-segments and packs merges into one token.
- An exact run of 2s becomes a pack once it is M long. Pack counts above M+1 are capped to M or M+1 by parity.
- Split stays exact: it never caps, and a leading P(1) splits into one exact 2 or a P(3).
- Fold expands small packs into canonical units.
- The rest-of-tape automaton X became an NFA, with moves (q, unit, q2).
- Stage 1's fold forced X(q) ⊇ X(q2), which merged unrelated contexts. Now the last folded unit goes straight into the tail's own state.
- Short segments in front of an X tail become a derived state ('m', cell, shorts, q2). Its moves are computed from q2's moves when needed.
- Two options: a different window per side (N=(NL,NR)) and history 1 or 2. Snapshots: logs/segx_stage1_final.py, logs/segx_stage2_packs_hist1.py, logs/segx_stage2_nfa_v1.py.
Runs on S0LC. All runs are seeded from the real orbit and are in logs/s2_*.txt and logs/s2_*.json. The word guard was raised to 300 so the trajectory could be seen. The real orbit itself uses 11 to 14 cluster words.
| # | automaton | K, N, M | result | cluster words | what it showed |
|---|---|---|---|---|---|
| 1 | stage-1 (history 1, conflating fold) + packs | 8, 2, 3 / 8, 2, 4 / 10, 2, 4 | stop rule in round 0 | 303 / 345 / 305 | packs are tokenised, but clusters become free words over {1, 2, P}: chains P,1,P,1,2 and touching separators SS = 2,2,1,2,2 |
| 2 | same | 8, 3, 3 / 8, 3, 4 / 10, 3, 4 / 6, 3, 3 | key cap (3M) / wide / wide / wide | 24 / 35 / 35 / 19 | a wider window keeps the words down, but the keys explode (8M keys, 3.3 GB at N=(2,3)) or a cluster goes past 20 cells (SSS) |
| 3 | NFA (no conflation) | 8, 2, 3 / 6, 2, 3 / 8, 3, 3 | stopped (fold discovery never settled) / wide / key cap (6M) | - / 25 / 30 | an explicit short run in front of X(q) fed X(q) back into itself; fixed by derived states (row 4) |
| 4 | NFA + derived states, seeded from 1e5 | 6, 2, 3 / 8, 2, 3 | wide at 17k / 1.9M keys | 18 / 44 | same SSS pattern |
| 5 | as 4, history 2 | 6, 2, 3 / 8, 2, 3 | wide at 44k / 1.9M keys | 16 / 32 | history 2 does not remove it |
Why it does not close (why_wide.py, realruns.py). Every "wide" trace has the same shape:
1. The head sweeps left over a left side made of lone defects 5 cells apart.
2. Each 5-cell segment it crosses becomes one separator on the right, so the separators touch: 00110 00110 00110 ....
3. The left automaton lets 5-segments repeat without bound.
The real orbit never does this. To 3e6 steps, there are at most 2 consecutive 5-segments on S0LC and on T1, and every cluster has at most 7-8 segments (14 cells).
So the invariant would need a run-length count on the left side. History 2 does not give it: an unbounded run of 5s comes back through the fold's tail move and through long classes whose split leaves a 5.
Each leak fixed so far (gap length classes in stage 1, then packs, then the NFA fold, then derived states) uncovered the next one. Every fix has stayed inside the family "finite cluster alphabet plus gap classes".
Checks.
- Step semantics: 17 runs, 25,359 sampled symbolic steps compared with one tools/sim step each on random concrete members, with 0 mismatches (validate_steps.py, with pack instantiation).
- Shape algebra (test_packs.py): about 4,000 random members per run on S0LC and T1. Three properties were checked:
- every member is covered by a split edge;
- every edge stays inside its shape;
- push followed by fold only enlarges.
There were 0 failures after one fix: split had been capping exact 2-runs into packs, an enlargement inside split that the test caught.
- walk_cert.py (a multi-step tools/sim walk against an exported certificate, using only the certificate's NFAs) is written but has not been run, because nothing closed.
What a stage 3 would have to do. This goes past the stop rule, so it needs Dennis's go-ahead.
- Give the left X a run-length counter: at most 2 consecutive 5-segments, matching the real orbit.
- Find the remaining source of repeated 5s (the tail move into q2, or the split of ≥K classes).
- Then re-close S0LC before T1-T3.
Expected odds are low. The more useful hand-off is option B: give Astra's automaton synthesis these facts: - clusters have at most 8 segments (14 cells); - at most 2 consecutive 5-segments on the left; - no gap-parity condition is needed; - packs are transient.
Files (all in reports/cb3/explorer/).
- Explorer and drivers: segx.py, run_explore.py, run_seeded.py, seed.py, run_stage2.py (stage-2 driver).
- Stage-2 checks and diagnosis: test_packs.py, walk_cert.py, why_wide.py, realruns.py, realvocab.py.
- Diagnosis: why_grow.py, trace.py, realtrace.py.
- Checks: validate_steps.py, export_cert.py, check_cert.py.
- Real-machine probes: realwidth.py, tinytapes.py, packgrowth.py, packs.py, forward.py.
- Run outputs: logs/ (run logs; the discovered automata are in lang_S0LC_K8N2H1.json and lang_T1_K8N2H1.json).