BB(6) strategy: where to put effort next

2026-10-14. This merges five strategy lenses: census, verified deciders, family proofs, equivalence twins and cryptids. Paths are relative to [local working file] Numbers marked "est." are estimates; every other number comes from the lens data (reports/strategy/census*.tsv, reports/strategy/equivalence-candidates.tsv).

The short version

How the list shrinks. The 740 holdouts are only 477 distinct tables. 70% of all kills since December came from multi-machine batch files, and 19% from decider certificates. Single-machine proofs move the list one line at a time.

Our position. Our own route (one machine or one table at a time, near a proof we already have) is running out of targets: - No free holdout sits within 1 transition of any of our 30 on-list kills. - Two of Wave 6's 8 picks parked as cryptid candidates on their first day.

The opportunity. The biggest swath nobody is closing fast is a single Skelet-1 core, K42. It accounts for 40-45 lines (5.4-6.1% of the list), all free. It is also a hard residue: upstream has already proved 16 other exit variants of the same core (two deciders plus hand proofs), and these 40 have not moved since April (see the Critic section).

Two near-free cuts come first: - our 18 kills that are checked but not submitted; - about 8 twin ports of proofs that already exist upstream.

Recommendation. After those, fund three things: 1. K42, which turns into a 40-line cryptid write-up if it fails. The critic lowered its odds; it is a residue of upstream methods. 2. A halting-certificate pipeline. Keep it short: someone else is already sweeping these pools. 3. Chaotic Bell Class 3 as a "cryptid or family" probe. Start with the write-1 exit question in the Critic section.

Stop decider parameter sweeps, and run no more one-off waves after Wave 6.

Ranked directions

EV is the estimated number of list lines removed per 10 agent-hours, counting only kills that are ours.

Fund now: 0, 1, 2, 3 and 4. Run 5 in the background once Wave 6 frees the cores. Do not fund 6-10 (see the last section).

0. Bank the 18 pending kills

These 18 kills passed check_kill and have a submission/ folder, but have no PR:

What it does to the list. The 12 already merged take the list to about 728; these 18 take it to about 710. Counter Class 4 would be fully cleared.

Order (critic). 7 of the 18 are on mxdys's 08-24 UBRRBA list of machines that are "easy to accelerate": lines 14, 214, 410, 418, 636, 645 and 700. Lines 14 and 645 are also on dyuan's list. These are the most exposed to being re-proved in his framework, so submit them first. The other 11 are 8 Bell eats counter lines, 2 Counter Class 4 lines and line 301; none of them is on either list.

First step. Group the 18 into PRs by table, the way PRs #15-#18 were grouped. - Credit dyuan for lines 14 and 645, which are on dyuan's longitudinal list. - Check with Astra before posting the 3 Bouncer + Chaotic Edge kills. - This needs Dennis's yes; nothing is pushed without it.

Stop rule. None. Every day the kills sit unsubmitted is a day mxdys or someone else can take them first.

1. Twin ports and merges

The equivalence lens found list lines that run in lockstep with a machine upstream has already proved, up to a short detour. Porting the existing proof file then counts as a kill.

Hand-offs: - Line 118 is Astra's class: send it to Astra. - Lines 145 and 276 are Chaotic Bell Class 4 twins of RWLAccHaltv6.v halts (p 0.35-0.4) and belong to W6-5. Ask W6-5 to test the halting event itself before closing.

First step. Port 64 and 124: copy the TM1 and TM3 modules and swap in the TM string. The exit branch should re-derive symbolically. These are also K42 members, so this step tests our reading of the core for free.

Two caveats (critic): - The twin evidence is short. Lockstep was checked to 3e8 steps and covers only 3 exit events. TM1's proof runs 1,333,816 + 669,179 symbolic Inc steps, and its loop state has digit runs of 416,889, so the tape is at least about 2e6 cells. At 1e8 steps the tape is only about 24k cells. The port works only if every later exit reconverges in the same 12 steps. One coqc run settles it either way, which is why the odds are 0.6-0.8 and not 0.8. - 146 + 560 needs long concrete runs. The merge needs runs of 8.3e6 and 7.5e6 steps, 20 times upstream's longest Eqv run (386k). All 9 upstream Eqv*.v files are mxdys's own commits, so an outside equivalence proof is untested; expect him to re-prove it in his own framework. He could also find this merge himself by raising his step bound.

Stop rule: - Drop any port whose re-derived exit branch fails in coqc twice. - 728, 385 and 697 replay decider certificates. A replay that fails check_kill's assumptions gate (CTL62 uses PArray/Uint63) goes through Astra's gate-passing NFA package first. Only if that fails does it wait for Dennis's call on the baseline.

2. K42: one Skelet-1 core, 40-45 lines

The family. Every member is the same 5-state core 1RB0RC_1LC0RD_0LD0LC_1RE0LA_0RA0RF plus an escape state F (F1 is the only halt). Members differ only in: - F0 (16 (E1, F0) combinations in all: 9 F0 values with E1 = 0RF, 7 with E1 = 1RF); - whether E1 writes 0 or 1; - the start state, up to mirror.

Why it is attractive: - Size. 40 lines at 1 transition or less, on 16 tables (45 lines at 2 or less; the census component of 43 spans 17 tables). Not one is claimed by us, Astra or dyuan. - Shared grammar. At 1e8 steps all 43 census-component members show the same record shape: 0100^a 1^b 0001^c, or its mirror. - F is rare. It is first entered at 39,734-49,252 steps, then 0-6 more times up to 3e8. - The representation already exists upstream. At each F entry the tape is mxdys's digit representation from Sk1like_TC_v1.v. - Fit with our record. Our best class so far is Skelet 1-like Class 2 (12 of 14 killed, PRs #15-#18), and PR #18's closed-form Sk1Auto run reached 1.77e44 steps.

Why it may not work: - It is the residue of three upstream routes. Upstream proves 16 (E1, F0) exit variants of this exact core, not 6:

The 40 holdout lines are the other 16 variants. They have not moved since the 2026-04-26 list. The count was 69 in Aug 2025 and 46 in Feb 2026; the last 6 left between the Feb and Apr lists, when Sk1like_TC_v1/v2 landed (2026-03-11). Nothing has left since. - mxdys's note on line 496 says "~10^64 tape size and doesn't halt or become a TC yet". Running longer has already failed, so a kill needs an invariant. - The 40 variants split into 20 distinct F-entry histories. - One member (315) shows a residue branch toward halting.

Scoop risk: medium. The author of Sk1Machines.v works through a numbered "Sk1 Class1 TM1..TM105" list, but none of its 5 machines is on this core. mxdys's 8 Skelet 1-like Class 1 equivalence merges on 10-10 were outside it too: the core count was 40 on both the 778 and the 740 list.

First step (after the ports in section 1): an F-entry atlas, 6-8 h, Python only. Build an exact digit-level simulator, run the 20 distinct variant histories far past 3e8, and record the configuration at every F entry. Then answer three questions: - Do the F entries follow a recurrence in their parameters? - Can E ever read the 11 that leads to a halt? - Is there a digit-language invariant the core preserves, so each F0 only has to be checked once?

Some pairs already share near-identical histories (67 with 263; 64 with 124, offset by about 1.2k steps), which halves the per-variant work.

Why the atlas must be digit-level (critic). Sixteen members, 64 and 124 among them, enter F for the last time before 8e6 steps; lines 413 and 420 never enter it again after step 49,249. That looks like 64 and 124. But 3e8 steps is a tiny prefix: TM1's proof state alone is about 2e6 cells. So the step logs can only order the work. They cannot tell the members apart.

Gate. This lifts the "mined" exclusion on Skelet 1-like Class 1, so it needs Dennis's go. Ask in #bb6 first (message below).

Stop rule: - If the atlas finds no recurrence, or finds a pseudo-random digit map, apply the cryptid protocol: write the rules, flag it, stop. - If it is a go, write one core proof with Section + Variable premises (check_kill bans Hypothesis) plus generated per-variant modules. Stop if the first table takes more than 12 h without closing.

3. Halting-certificate pipeline

The idea. Find halters at the level of the abstract map, which is cheap with big integers. Then certify each one with a generated checked runner. Three of our kills were made this way: - C2-552 (PR #18); - W5-7; - W5-5 (1.82e18 steps in 751 chunks).

The family is the certifier, not an invariant.

Pools: - 136 lines with Collatz-type rules: Bell-like 63 of 77, Quadratic Mess 37 of 47, Cubic Mess 36 of 45. Rulefit has closed rule tables for 31 of them (11 + 8 + 12). - The Chaotic Bell Class 1 rate-2/3 cluster: 21 lines on 8 tables. W6-4 holds 6 of them. - mxdys's UBRRBA list: 74 lines still on the list. 20 are Astra's Bouncer + Chaotic Edge lines; coordinate on those.

Our halting hunt skipped the mined classes, so we have never swept this pool. Someone else almost certainly has (critic): - Cubic50.v, CubicMachines.v and CubicMachines_v2.v work through a numbered cubic.txt list (TM1 to TM50), on both the halting and the nonhalting side. - Bell60.v is a "complete RLE accelerator" with a halting certificate. - QuadraticMess30.v adapts lemmas "from the halting-proof archive supplied by the user".

So the Collatz-bell lines still listed are mostly the ones that author's RLE and affine-memo engine did not certify. Our edge is only map-level closed forms beyond RLE range. That is why the odds above are lowered to 0.2-0.25 for at least one halt.

Astra overlap. Astra is currently working on lines 257, 535 and 669 as nonhalting targets. These are one table of the Chaotic Bell Class 1 21-line cluster. Coordinate before touching that table.

Scoop risk is high. mxdys and the RLE-engine author posted Bell60.v, QuadraticMess30.v, Cubic50.v, CubicMachines_v2.v and ChaoticBell1Halt.v in a single week. Speed matters more than polish here: certify each halt and post it the same day.

First step, 8-12 h, Python only. Iterate the exact maps of the 31 closed-table lines, and run the 21 Chaotic Bell Class 1 lines at map level, coordinating with W6-4. The output is a list of predicted halters with step counts. Then: - Certifier generator: 8-12 h, adapted from W5-5's runner and the Sk1Auto / CBSim patterns. - Each halter: 2-6 h.

Stop rule: - If no line among the 31 + 21 reaches a halting branch within a certifiable range (PR #18 reached about 1e44 with closed-form batches), stop. Do not extend to the 105 lines without closed tables. - Optional extra: extract UBRRBAHaltv2.v's checker and rerun it on the 74 lines at 10x mxdys's budget. That is 6-10 h for p 0.2-0.3, but cheap budgets are probably exhausted (only 1 of 86 has fallen to it since 08-24).

4. Chaotic Bell Class 3: the two-array core

Why it is open. Chaotic Bell Class 3 has had no kill in 2026. Its 12-line core is just 3 tables, with 4, 5 and 3 listed starts (lines 23/206/403/415, 69/245/330/668/696 and 178/376/382). They share 11 transitions; the one slot that differs fires about 20 times per 1e9 steps. Its records are clean: 4-5 skeletons cover 100% at 1e9. All 9 of the class's past kills came from FAR certificates in 2025. Nobody holds any of the 12.

The risk. 19 of the 22 class lines carry Collatz or cryptid flags, and Wave 6 saw erratic epoch ratios (0.27-1.3).

First step, 1 day. For each of the 3 tables, fit the two-array update rules and an epoch map, then collect epoch statistics to 1e10 steps. The 12 lines are 23 69 178 206 245 330 376 382 403 415 668 696. Put these 3 tables first in the direction-5 automaton search, since FAR worked on this class before.

Stop rule: - If the epoch map has no conserved quantity or monotone potential and branches on residues, this is a cryptid: write the rules up (section "Cryptids") and stop. - If it is regular, one start-parametric proof per table covers 3-5 lines, and 12 if the three tables share the invariant (1-2 agent-days).

5. Regular-language search (background, after Wave 6)

The idea. mxdys's CTL and FAR deciders only try automata from a few generator families. A complete SAT / meet-in-the-middle search over arbitrary automata, at 16-24 states per side, is a different test. It can run table by table over the 115 chaotic and Unknown tables. A weighted-FAR screen (Iijil's MITMWFAR) adds exact counter comparisons, which CTL cannot express.

What is already in place: - A native checker (ctlm) already replays upstream's CTLCertv1.v certificates. - Hits can be emitted in that file's format, so no new soundness proof is needed.

Before starting. Coordinate with Astra, whose primitive-free regular-certificate checker avoids the PArray/Uint63 problem with our check_kill gate. As of 14:32 today, Astra's standalone NFA certificate generator (astra/autonomous-20261014/certificate-package/package.py) passes the unchanged check_kill gate with zero extra assumptions on known sources. So a hit can be packaged without touching the baseline. Astra has offered to package any finite certificate we route to it.

Stop rule. One funded stage. If there is no hit on the 115 tables, stop. For calibration, today's probe of mxdys's own generators returned 0 hits in 473 runs on 40 lines.

Cryptids: yes, start two, but as families

What a cryptid deliverable is worth. A cryptid write-up does not shorten the list. It explains lines, and the community records that. The established form is: - a Rocq file of verified macro rules ("halts iff ..."); - a wiki entry.

Upstream has 11 such files (for example AntiHydra.v, HaltingCryptidCandidate1.v, and 1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE.v, "add rules for cryptid candidate").

Pick families, not single machines. Our one-off work already drifts into cryptids by itself: 14 of our machines (all on the 740 list) are now parked as cryptid candidates, 2 of them today. So the two cryptid starts should be families, where one write-up covers many lines and the same probe can still produce kills:

1. K42 (40-45 lines). If the direction-2 atlas says "pseudo-random digit system", the deliverable is a rules file for the core plus a note covering all 40 lines. This is the largest unexplained family on the list.
2. The Chaotic Bell Class 3 core (12 lines, 3 tables). There is no competition. The deliverable is a two-array rules file and a write-up, unless the epoch map turns out regular, in which case it becomes kills.

Reserve: Chaotic Bell Class 1 x3/2 (21 lines on 8 tables). It has the Hydra shape: a 3/2 map with a halting residue. Take it up only if W6-4 and direction 3 find no halts there.

Not worth agent-hours: - the famous cryptids (Antihydra, the BMO problems): these are open mathematics problems; - more work on our 13 parked candidates.

The one cheap exception is a rules-only file for Skelet 1-like Class 2's last two lines (R4 and #32), which would close that class's story as "12 killed + 2 formal cryptids". Do it only if Dennis wants it.

What we will NOT do, and why

• No Wave 7 of one-off picks.
• No free holdout is within 1 transition of our kills, and only line 96 (already W6-2) is within 2.
• About 100 non-tarpit, unclaimed lines remain, and W6-3 and W6-5 parked on day 1.
• Finish Wave 6. After it, every pick is a table or cluster: shared tables average 2.6 list lines, so write start-parametric proofs.
• No decider parameter sweeps or new CTL generators.
• Today's probe: 0 of 473 runs, after about 885 earlier runs that also found nothing.
• Success is not monotone in the parameters, so a real sweep costs 20-200 CPU-hours per family.
• mxdys's 08-30 generator addition removed 0 list lines.
• No nonhalting work on Shift-overflow counter, Cubic Mess or Shift-overflow bouncer counter (except direction 1's twins).
• SOC is mxdys's active front: 130 SOC proofs since 08-30.
• Hint cards (direction 6) would move the list, but the credit would go to his files. Dennis's call if list movement matters more than credit.
• No nonhalting work on the Collatz tarpits: Bell-like and Quadratic Mess (nonhalting side), Spaghetti, the 1dCA classes, CAB.
• No more Bell eats counter mining. It is tapped: the BEC sweep found 4 fresh machines.
• No separate budget-plus-round-counter project. Only 8 free lines carry the signal, and Wave 6 holds 3 of them.
• No 1-transition template copies or decider certificates carried to another start. W5-2, W5-6 and W4-7 showed both fail.
• No family-file generator yet. Build it only once a core proof exists (K42 or Chaotic Bell Class 3).

Decisions for Dennis

1. Submit the 18 pending kills? PR groups by table; credit dyuan on lines 14 and 645.
2. Lift the "mined" exclusion for K42 (Skelet 1-like Class 1) and for the halting side of Bell-like, Quadratic Mess and Cubic Mess?
3. Ask in #bb6 before K42 stage 2. Suggested text:

is anyone currently working through the Skelet 1-like Class 1 holdouts (the TM1..TM105 list behind Sk1Machines.v)? I'm looking at a group of ~40 of them that share one 5-state core and differ only in the escape state, and I'd like to avoid duplicating someone's work

Send this after the 64/124 ports are in, so the hint does not give the ports away. 4. Extend tools/assumptions_baseline.txt to upstream's PArray/Uint63 primitives? This only matters if a CTL/FAR replay (728, 385, 697) or direction 5 produces a hit. It is probably moot: Astra's NFA certificate package now passes the unchanged gate, so the default should be to route hits through Astra. Extend the baseline only if a hit cannot be exported as an explicit automaton.

Critic (2026-10-14)

Verdict. The ranking survives; the odds behind it do not, quite. - Banking the 18 and porting 64/124 stay first. - The two family bets (K42, CB3) are residues of upstream methods. That lowers their odds, but it also says exactly what to try first. - The halting pipeline loses the most: someone is already sweeping the same pools.

What was re-checked

New probes

Both ran with 2 processes, nice 10 and ulimit -v 6e6. - hlin on K42. This is the decider behind 11 of the 16 proven variants, run at their exact config (default, fuel 1e6). - Calibration: true on two proven siblings, in 0.6 s and 1.1 s. - Holdouts: 0 of 8 (lines 44, 64, 67, 86, 100, 709, 713, 718), about 70 s each. - Stopped there: it only repeats mxdys's own Indv7 run. - FAR on CB3. Upstream has a FAR recipe that proves 5 siblings of the CB3 core (more under "New facts" below). - Calibration: the recipe, RNGS_mod_QSym_FAR 200000 100000 0 0 0 1 4 3 12 2, is true on a sibling in 0.16 s. - Holdouts: it is false on all 3 holdout tables in 1 s or less. - The RWL_mod sibling recipe times out at 60 s. - A 150-point grid around the recipe (RNGS_mod_QSym_FAR 200000 100000 0 0 0 1 a b c d, with a 2-6, b 2-10, c 12-48, d 1-2) on lines 23, 69 and 178: 0 of 450 true. Every run returned false within 10 s; none timed out. So this decider family, at the sizes that close the write-0 siblings, does not close the write-1 exits (see the next section). A false here does not rule out a larger automaton.

New facts that change the plan

1. K42 is what three upstream routes left behind: hlin, the TC decider and hand proofs. RWLAcc only re-proves an hlin variant from other starts. It has been flat for 6 months. That makes a family proof harder (odds lowered), and it makes our ask in #bb6 cheaper.
2. The CB3 holdouts are exactly the "write-1" exits. The same 11-transition core with an F0 that writes 0 is already proved upstream: - F0 = 0LD or 0RE: FARv1.v, 6 machines, 5 of them by one recipe; - F0 = 0RC: RWL_mod_v5.v; - F0 = 1LD, but with one other transition changed: CPS_LRU_v3.v (5 machines, a CTL certificate). So a write-1 exit does not rule out a regular invariant by itself.

All 3 holdout tables have F0 writing 1 (1LD, 1RE, 1RC). This gives CB3's first step a concrete question: what does the extra 1 left at an exit do? If it accumulates like a counter, that suggests (but does not prove) that no simple regular invariant exists, since even an unbounded unary counter has a regular representation (Astra, 2026-10-14); the epoch-map route would then come first. If it stays bounded, a larger automaton (direction 5) is the shortest path to all 12. Answer it before fitting epoch maps. 3. Someone is already sweeping the halting pools. The cubic.txt TM1-TM50 files, Bell60.v and QuadraticMess30.v (built from a "halting-proof archive") cover the same classes. Direction 3's odds are lowered; keep its Python sweep short and stop early. 4. Astra. Astra's NFA certificate package passes the unchanged check_kill gate (14:32 today), so Decision 4 is probably moot. Astra worked on the 257/535/669 table of the CB1 cluster until 15:20 on 10-14; that lane is finished and the table is free again (subject to fresh ownership checks). 5. Bank order. 7 of the 18 pending kills are on mxdys's UBRRBA-86 "easy" list; submit those first (section 0).

Missing direction: sibling-residue triage (cheap; do it with the ports)

Both family findings above came from one move: list the proven upstream tables one transition away from a holdout, and note which method proved them. This takes minutes of CPU, and for each line it says: - which decider almost works; - which hand proof's mechanism is next door; - whether the holdouts differ from the proven siblings in a systematic way (CB3: the bit written at the exit).

First full run (critic, all 740 lines; Eqv files excluded, so only proofs count): - 362 lines (49%) have an upstream-named table one transition away. The most common proving files are RWLAccHalt (160 lines), RWL_mod (123), CTL (82), CPS_LRU (79), hlin (70) and the TC decider (65). - 66 lines have their own table proved upstream from another start; 52 of these are free. - 52 of the 66 are decider or halting certificates. Reusing these from another start is Astra's lane, and it has been negative so far (W4-7, W5-6, Astra's nine halting calls). - 14 are hand proofs. All are already covered or old: - Wave 6 picks: 10, and 299/412/602 (ChaoticBell1Halt.v); - parked siblings of #16: 199/440/510 (FractalType4.v); - our own kills; - 2024 files whose other starts have survived two years: 167/322/487/594 (CubicCap.v) and 414 (CSv2.v).

So the scan finds no new single targets. Its value is the family triage, where it produced both facts above in minutes. Scripts: d1sib.py, k42match.py and genmatch.py, plus the probe outputs critic_hlin/ and critic_cb3/, all in /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/ (temporary; copy them if they are needed later).

Cost: 1-2 agent-hours to triage, no Rocq. It is not a kill route by itself; it sharpens the first step of every family direction and of any post-Wave-6 table pick.

Unchanged

The stop list, the cryptid picks, the hand-offs (118 to Astra; 145 and 276 to W6-5), and the order of directions 0-5.