Track B targeting memo

2026-10-09. Inputs: reports/kill-forensics.md (busycoq git history), reports/landscape.md (wiki, sheet, GitHub), data/crossref.md, atlas/examples_summary.md and atlas/tooling-notes.md. Holdouts: data/holdouts/2026-10-07_778.txt and 2026-10-07_eqv_1590.txt. Proofs: busycoq BB6 @ 0940bb9, data/solved_index.tsv. New for this memo: a simulation sweep of all 778 holdouts and of the 563 machines proof-killed since Dec 2025 (§2.5). Discord was not readable, so every "is someone on this?" question is listed for Dennis to check.

Dennis's brief: be calculated and targeted. Compute and time are plentiful but none should be wasted. Learn from the recent, largely AI-assisted kills which areas are vulnerable, which are picked clean, and which are tarpits.

1. Executive summary

1. Easy machines get absorbed within weeks. The list fell from 1,094 to 778 holdouts since June. There were 297 proof kills since Jun 29, and 44–64% of them came from files with AI-assistant markers. mxdys, the maintainer, uses LLMs himself and opens a new family file almost every week.
2. Picked clean (avoid): 7 classes have nothing left, for example Counter Class 1 and Skelet 17-like. The decider routes are exhausted: FAR/CTL, LongAcc/LongLoop, RWLAcc/UBRRBA certificates, and equivalence merging.
3. Actively mined by others (avoid): shift-overflow counters (128), Skelet 1-like Class 1 (101), Cubic Mess (50), SO bouncer counter (33), and the Bell-like and Quadratic Mess halting route. Chaotic Fractal Type 1, Monotone list, Counter Class 3, Translated Counter and the 21 mira-quine PR machines are also taken.
4. Targets: classes that cooled off in Jul–Aug and have reusable templates. These are Bell eats counter, Bouncer + Chaotic Edge, Skelet 1-like Class 2, SO structural counter, Structural counter + chaotic edge and Sync bouncer counter. Two counter classes nobody has touched since Dec are also targets: Structural counter + counter and Counter Class 4.
5. Tarpits (avoid): the 20 cryptids and 7 potential cryptids, the open BMO problems (including BMO 11's 20-machine group), and Machines at the Edge. Also avoid the chaotic Bell, 1dCA, Spaghetti and Ack-like classes (no hand proof ever; their only 2026 kills were decider certificates, the last in February), the 4 "probably incorrect" claims, and families where recent proofs cost 100–300 KB.
6. New evidence from a sweep. I ran all 778 holdouts and all 563 recent kills to 1e9 steps, ran Quick_Sim on the 778, and did a Hamming-≤2 neighbour search (up to symmetry) against 235,762 proved machines. - 47 groups of holdouts follow identical tape trajectories, and every group stays within one class. One proof idea should therefore cover several machines. - As a check, the method independently rediscovers 6 of mira-quine's 10 claimed equivalence pairs.
7. The best leverage is these families: - 3 Structural counter + counter machines with identical trajectories, out of 5 left in the class; - an identical-trajectory triple in Skelet 1-like Class 2, all three eligible; - nine Bell eats counter machines one transition from a proof already in busycoq (SOMDCv6.v TM7/TM8, the BECv1/FractalBEC instances, BMO7.v); - one Sync bouncer counter that differs from three SBCv7.v proofs only in F0.
8. Candidate pool: 40 machines across 11 classes plus 11 in reserve. All are byte-exact entries of the 778 list and have no row in solved_index.tsv in any tier, not even as a mention. The top 20 are one lead machine per mechanism (11 classes) and form the recommended pilot. Ranks 21–40 are mostly cheap follow-ons once a lead is proved.
9. Submission: post a per-machine Discord thread with a rule table, one short house-style .v and an AI disclosure. Expect mxdys to fold the idea into his own family files. Do not open large PRs: mira-quine's 8 open PRs have had no response.
10. Before compute starts, Dennis should get dyuan's Oct 1 list of 24 and mxdys's Aug 24 list of 86. He should also ask mxdys one question that covers 12 pool machines: did the templates in his SOMDCv6, SBCv7, SBCv2, BECv1, FractalBEC, IndBEC and BMO7 files fail on these one-transition variants, and why? (§5)

2. The map

Columns: left = representatives on the 778 list. eligible = left after our gate (§4.1): no row in solved_index.tsv in any tier, no claim or tarpit flag, not on the Level 1 or Category 1 tabs, blank sheet status. 430 of 778 pass.

2.1 Picked clean (nothing to find)

2.2 Actively mined by others (avoid: duplicate-work risk)

2.3 Stalled but plausible (targets)

2.4 Tarpits (no Track B time)

2.5 What the sweep adds

What was run (all on this box, about 15 minutes wall time on 12–16 cores; outputs are in the session scratchpad, see Appendix): - tools/sim/tmsim: every holdout to 1e9 steps, sampling the visited width every 1e7 steps. Then the same run on the 563 machines proof-killed since Dec. - tools/qsim.py (sligocki Quick_Sim, 20k loops): rules proven, steps reached, block size. - A neighbour search: every variant within 2 transition changes (about 38k per machine) was keyed by holdouts.equiv_key (mirror + state renaming) and looked up among the 235,762 proved 6x2 machines and among the other 777 holdouts.

Growth signatures are class-consistent: - Bell eats counter grows as t^0.31–0.36. - Bouncer + Chaotic Edge, Skelet 1-like Class 2, SO structural counter and Structural counter + chaotic edge grow as ~t^0.5. - Structural counter + counter grows as t^0.33. - Counter Class 3/4 barely grow (≤ 140 cells after 1e9 steps). - Translated Counter grows linearly.

That makes a cheap first check at Checkpoint A: a machine whose growth exponent disagrees with its sheet class is misclassified or special.

Trajectory twins: two holdouts count as twins when their visited width agrees to within 0.3% + 3 cells at every 1e7-step checkpoint up to 1e9 and their nonzero count at 1e9 agrees to within 0.5% + 3. - 47 twin groups were found, and every one lies within a single sheet class. - Validation: the detector flags 4 of mira-quine's 10 claimed equivalence pairs as exact twins, and 6 of 10 within 2%. - Twins that differ in 5–11 transitions are either non-obvious equivalences or the same mechanism under a different encoding. Either way, one proof idea serves the whole group.

Template neighbours: 95 of the 430 eligible holdouts are within 2 transitions of a machine with a hand-written proof (not a decider certificate). The pool uses the best of these.

What it does not tell us: a neighbour that is proved does not guarantee that its template transfers. For the one-transition variants, mxdys's own family search evidently ran and failed, so Checkpoint A has to name what the changed transition does.

3. Reusable proof templates and techniques per target class

All paths are under vendor/busycoq/verify/ at the pin. "Framework" means the module is built by make (its .vo exists), so a proof may Require it.

Cross-cutting techniques (from forensics §6.4, ranked by fit for us): 1. Copy-and-modify a module of mxdys's batch style. This is the default for any machine 1 transition from a proof. The smallest complete examples are Bouncer_v2.v (1.6 KB), TCv3.v TM3 and FIBv2.v TM2 (about 60–100 lines each). 2. Shared-lemma batch: one generic phase lemma plus per-machine instances, as in SOMDC_Class1.v (31 machines) and LongAccv1.v (17 in 6.7 KB). Use it for the twin groups. 3. Verified checker: a Fixpoint generator/interpreter, a soundness lemma, then vm_compute. Examples are SOC_4_3_Halt.v, Queue_v1.v and CounterClass3v2.v. This is what the AI-assisted files use. Reach for it only when the rule table explodes into many finite cases. 4. Proved accelerator for halting: LongAccHaltv1.v (23 halts in 4.6 KB) and Bell60.v (RLE + BigUint). Keep it in reserve for Structural counter + chaotic edge machines that turn out to halt.

Hygiene, enforced by check_kill.sh but worth knowing up front: - Imports from framework modules (Longitudinal, DivModCases, ES_v3, LongN, InfiniteRect, BinaryCounter*, UnaryCounter, SimplTape) are fine. Never import BBinf, TMLR, TMAddOneSymbol, TMLocalHistory or Inductive_inf, which carry unsound Admitted lemmas (zero-context's PR #3). - Keep each file to one machine (or one twin family), in house style, under about 15 KB where possible. mxdys's July hand proofs are 3.5–25 KB.

4. Candidate pool for the 20-machine pilot

4.1 How the pool was selected

The gate (applied to every representative and to every member of its equivalence group): 1. Index: holdouts.py solved verdict absent. There must be no row in data/solved_index.tsv in any tier (exact, halt notation, or equivalent up to mirror/renaming). This is stricter than "no proof": it also drops the 299 representatives that appear only as tm' in Eqv*.v lemmas. 2. Flags: not on any claim or tarpit list in §2.2/§2.4 (83 representatives). 3. Sheet tabs: not on the Level 1 (41) or Category 1 (16) tab. 4. Status: blank sheet Results status (excludes the 18 CRYPTIDs and the SOCSSv5 anomaly).

That leaves 430 eligible. Within the target classes of §2.3 they were ranked by: - (a) family leverage: trajectory twins, and open machines 1 transition apart; - (b) template distance: a hand-written proof 1–2 transitions away, preferably from 2026; - (c) class temperature: cooled or untouched beats hot; - (d) cost signals: slow growth, no 100 KB-class precedent.

Ranks 1–20 are leads, one per independent mechanism, spanning 11 classes; this is the recommended pilot. Ranks 21–40 are follow-ons (same mechanism as a lead, so cheap once the lead is proved) plus second-wave picks. If a lead dies at Checkpoint B, skip its follow-ons. R1–R11 are reserves.

Every machine in the pool and reserve is a singleton equivalence group, so each kill removes exactly one list entry.

Discord check codes (Dennis): - A, for every machine: search the string in #bb6 and the sheet. Confirm it is not in dyuan's Oct 1 list of 24 (message 1555244959840337973) or mxdys's Aug 24 UBRRBA list of 86 (1541486462330085496), and not claimed in a thread. - B: ask mxdys whether the named family template (SOMDCv6, SBCv7/v11, SBCv2, BECv1, FractalBEC, IndBEC, BMO7, SBCv6a/SOBL) was tried on this machine and why it failed. One message covers all of them. - C: who holds the numbered Skelet 1-like list behind Sk1Machines.v ("TM1..TM105"), and does it cover Class 2? - D: has anyone run FAR with larger DFA parameters, or a new edge decider, on Bouncer + Chaotic Edge since July? - E: has anyone simulated it past 1e15 or found it halting? 4 of the class's 6 recent kills were halts. - F: any informal analysis of Structural counter + counter or Counter Class 4? Both classes have been untouched all year. - G: who is behind the FractalType7/FractalMisc batch (SOC_FT7_CONSOLIDATION.md numbering), and are the remaining fractal holdouts on that list?

4.2 Ranks 1–20: recommended pilot (lead machines)

4.3 Ranks 21–40: follow-ons and second wave

4.4 Reserve

4.5 Watchlist: good-looking machines that the strict gate excluded

These are not in the pool because they appear in solved_index.tsv as Eqv*.v mentions (§4.1, rule 1), not because they are solved. A proof of any of them would still be a kill. Relaxing the gate is question 9 in §5. - 1RB---_1LC0RF_1RF0LD_0LE1LC_0RC0LC_1RB0RA (Unknown): "Possible bouncer with high params". - 1RB1RC_0LC1RE_1RA0LD_1LB0RD_0RF---_0RA0RF (Unknown): nerdyjoe's "Binary counting + bouncing". - 1RB0LB_0LC0RE_1LA1LD_0LB1LD_1RA0RF_1RA--- (Chaotic Bell Class 4): "possible bouncer". - 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB: the Counter Class 4 twin of #12, which a #12 proof should carry over to. - All 3 Counter Class 2 and all 3 Fractal in Bouncer leftovers. - 1RB1LC_0RC0RB_1LD0LA_1LE---_1LF1RA_1LA1LC: the SOCSSv5 sheet anomaly. Its sibling …_1LA1LA is proved in SOCSSv5.v.

4.6 Verification record (run 2026-10-09 on all 51 pool and reserve machines)

5. Questions for Dennis

1. Fetch two Discord lists before we spend compute: - dyuan's 24 "easy by longitudinal analysis" machines (Oct 1, message 1555244959840337973); - mxdys's 86 "easy to accelerate with UBRRBA" machines (Aug 24, 1541486462330085496).

Paste them into data/ and I will intersect them with the pool in seconds. Any overlap means someone else's pipeline will probably absorb that machine. 2. One message to mxdys covering pool #2, #4, #7, #8, #10, #15, #18, #23, #28–#31: each is 1 transition from a machine proved in a file he committed (SOMDCv6, SBCv7, SBCv2, BECv1, FractalBEC, IndBEC, BMO7). Did he try those templates on them, and does he know why they fail? His answer either hands us the obstacle or tells us to skip the machine. 3. Skelet 1-like Class 2: is the numbered list behind Sk1Machines.v (Class 1, TM1..TM105) also covering Class 2? If yes, drop #3, #11 and their follow-ons. 4. Structural counter + counter and Counter Class 4: no kill all year. Is that because they were tried and found hard, or because nobody looked? This decides whether #1, #12, #14 lead the pilot or move down. 5. Pilot composition: do you accept ranks 1–20 as the pilot (11 classes, one lead per mechanism)? Or would you rather swap in follow-ons for faster first kills, for example #21–#22, which only need the #1 argument re-targeted? 6. Halting outcomes: do HALT proofs count as pilot successes? This matters for #6, #27 and #38 (Structural counter + chaotic edge), where 4 of the class's 6 recent kills were halts. If yes, I would run an accelerated simulation on those three before Checkpoint A. 7. Fractal batch: do you know who produced the FractalType7/FractalMisc files (the SOC_FT7_CONSOLIDATION.md numbering)? If the remaining Chaotic Fractal Others (4) and Type 1 (4) are on their list, #16, #20, #39, R1 and R7 should go. 8. Submission format: a Discord thread per machine, or one per twin family? Is a single .v proving 2–3 twin machines welcome, given that mxdys prefers to fold results into his family files? What disclosure line should we use? The proposal is "Found and formalized with Claude Code; reviewed by Dennis." 9. Gate: should we relax rule 1 to let in holdouts that are only tm' mentions in Eqv*.v? That adds 299 machines, including the §4.5 watchlist (the "possible bouncer" notes, the Counter Class 4 twin, Counter Class 2 and Fractal in Bouncer). They are not solved; the strict reading of "not in solved_index in any tier" just excludes them. 10. Low-hanging but claimed: do you want to ask M-Abozaid whether anyone is porting his Lean proof of 1RB0RA_0LC0LA_1RF1LD_1LE0LD_1LC1LF_---1RA to Rocq? With permission and credit it could be the cheapest first kill, though it is outside the pool by our "nothing claimed" rule. 11. Budget: keep the default 2 h per stage? I propose a stop rule for correlated groups: if a lead stalls at Checkpoint B, mark its follow-ons SKIPPED rather than trying them separately.

Appendix: method notes and reproduction

• Sweep commands. The direct simulation ran as tools/sim/tmsim '<tm>' --max-steps 1000000000 --every 10000000. Quick_Sim ran as .venv/bin/python -B tools/qsim.py '<tm>' --max-loops 20000 --max-seconds 45 --every 0 --no-tape. Both were driven by xargs -P 12 over data/holdouts/2026-10-07_778.txt. The 563 killed machines are the reason=proof rows of reports/forensics/kills.tsv with list windows from Dec 2025.
• Where the outputs live. The scratch scripts (features, twin clustering, neighbour search, pool tables) are in the session scratchpad, not the repo, because this task scoped writes to this memo. Saving them as tools/analysis/targeting_*.py and the per-machine features as reports/targeting/*.tsv is a 10-minute follow-up if wanted.
• Neighbour search. For each holdout, all 1- and 2-transition variants (25 options per transition: {0,1} × {L,R} × {A..F} or ---) were normalized with holdouts.equiv_key and looked up. Proved = proves ≠ - in solved_index.tsv. A neighbour counts as "hand-written" unless its file is a decider_certificate or an equivalence file.
• Twin rule. Visited width (hi − lo + 1) agrees within 0.3% + 3 cells at all 101 samples (every 1e7 steps, 0 to 1e9), and nonzeros at 1e9 agree within 0.5% + 3. "Near-twin" in the tables means the maximum log-ratio over checkpoints 1e8..1e9 is below 0.02.
• Behavioural look-alikes to killed machines (same metric) are weak evidence, since many bells and bouncers share growth constants. They are cited only below 3% and only as hints.
• Caveats. Class labels come from the sheet's Classifications tab (Dec 2025), which has a few misfits. For example, R1 looks more like a sync bouncer counter than a fractal. "Hot", "cooling" and "untouched" come from commit dates and file headers, not from Discord.
• Vendor hygiene. vendor/ was used read-only, and find vendor -name __pycache__ is empty.

Update 2026-10-09 (late): Discord lists from Dennis

Dennis pasted two Discord threads; saved verbatim in data/discord/ with context notes.

Reading: - The UBRRBA list covers exactly our bouncer-like targets (Sync bouncer counter, Bouncer + Chaotic Edge, Structural counter + chaotic edge, SO structural counter). Those machines can fall to anyone's compute run (q64 offered ~500 cores; mxdys: 1e9 simulator step limit and corner-case early exits explain the failures). Hand-proving them risks duplicate work, so they leave the pilot unless Dennis learns the list was run and failed. - dyuan01 is developing longitudinal analysis on his 24 ("I don't think I have yet used this technique to its full potential"), so treat that list as claimed. - q64's warning on the same thread ("current LLMs are highly likely to make subtle mistakes in these informal reductions ... formalization before claiming") matches our check_kill-only rule. Flintt's AI-assisted halting certificate was confirmed in Rocq by mxdys within ~3.5 h: a clear, auditable artifact gets formalized fast.

Revised pilot (ranks 1–20 minus both lists, refilled from 21–29): #1, #2, #3, #7, #10, #11, #12, #14, #15, #16, #17, #18, #20, #21, #22, #23, #24, #25, #28, #29. Classes: Bell eats counter 8, Structural counter + counter 4, Skelet 1-like Class 2 4, Counter Class 4 1, Chaotic Fractal Others 1, Chaotic Fractal Type 1 1, Unknown 1 (7 classes). Dependencies: 8 of the 20 (#2, #7, #10, #15, #18, #23, #28, #29) hinge on the mxdys template question (§5 Q2); #16 and #20 on the fractal-batch question (Q7); #3, #11, #24, #25 on the Sk1Machines question (Q3).

Dennis's decisions (2026-10-10)

• UBRRBA_TODO machines: treat as tried-and-failed, fair game. Of the 86, 7 are solved; prurq's screenshot (UBRRBA block 12 on 1RB1LC_0LA0RD_1LA0LA_0RF1RE_1LA1RB_---0RB, halts) is one of them. q64's ~1e6427 halter 1RB1RF_1RC1RB_1LD0RA_1LA1LE_---0LF_0LC1LF was not on the list (solved by 2026-08-31).
• mxdys template neighbours: fair game; we check the templates ourselves.
• Fractal thread (Discord, Dec 2025 to Sep 2026): every machine named there is already solved. mxdys 2026-09-21: the "Chaotic Fractal Type 1" batch (18 solved) was done by LLM ("simulate them further, and they all fall into some kind of self-similar loop"). The 4 Type 1 left therefore probably resisted that approach: fair game, likely harder.
• Final pilot = the original ranks 1–20 (§4.2). #4 is also on dyuan01's longitudinal list (a technique filter, not a claim): keep it, but check the Discord thread before submitting.