Recent-kill forensics for Track B targeting

2026-10-09. busycoq BB6 @ 0940bb9 (2026-10-07, read-only git). Holdout snapshots data/holdouts/ (26 lists, newest 2026-10-07_778.txt + 2026-10-07_eqv_1590.txt). Sheet: data/sheet/2026-10-09_*.csv. Proof index: data/solved_index.tsv.

Hypothesis under test (Dennis): many recent kills were done with AI help. Studying them should show which areas are weak to AI, which are now picked clean, and which strategies and tarpits exist, so we don't rediscover them.

Short answer: - The hypothesis holds for the last ~7 weeks. There is explicit evidence that at least one contributor works through an AI assistant, and since Sep 2026 the kill rate has spiked in exactly the files that carry assistant-style markers. - The AI-assisted front is narrow and still moving: shift-overflow counters, Skelet-like counters, Fractal Type 7, Cubic Mess, and long halters proved with verified accelerators. Avoid those areas. - The best targets are mid-size counter/bouncer classes that cooled off in August and have reusable templates. A few small classes nobody has touched since Dec are also worth a look.

TL;DR

1. What left the list since Dec 2025: 638 machines (13 windows, 1416 → 778). - 563 were real proofs: 473 nonhalt, 90 halt. - 75 were equivalence merges: list bookkeeping, not kills. - 553 of the 563 proofs landed in busycoq within the list window (±1 day), so attribution is tight. - 562 of the 563 were committed by mxdys (ccz181078). The one exception is univerz's PR #5, later renamed to SOBCv11.v. Commit authorship tells us nothing about who wrote a proof.
2. The pace roughly tripled after June. - Dec–Jun windows: 266 proof kills in 7 months. - Jun 29–Oct 7 windows: 297 proof kills in 3.3 months. - September alone: 215 removals, 203 of them proofs, mostly from two commits: 51fa271 (09-16, "add 78 SOC, 18 FractalType7…") and 3127e48 (09-23, "31 SOMDC_Class1").
3. The kind of proof changed. - Dec–Jun was dominated by mxdys's decider-style certificates (FAR, LongAccHalt, RWLAcc/UBRRBA: 35% of kills, about 160 B per machine) and terse batch files (LongLoop/LongAcc, SOCSS, es/follow style). The median over all Dec–Jun kills was 2.9 KB per machine. - Jun–Oct is dominated by large bespoke files: median 11.3 KB per machine, files up to 539 KB, with self-defined Inductive/Fixpoint checkers proved sound and run with vm_compute. - Decider certificates fell to 5% of kills. The FAR, RWLAcc and LongAcc routes look exhausted (last kills 07-29, 08-30 and 09-23).
4. AI evidence: - Explicit:
   • Three comments in the 10-07 commit address "the user": QuadraticMess30.v:1 and Queue_v1.v:1 say "…proof archive supplied by the user", and SOCMisc.v:5713 says "the user's machine".
   • One sheet note says "Analysed thoroughly using formal proofs from Claude Opus 4.6" (still-open holdout 1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF).
   • Probable:
   • Boilerplate headers ("Standalone; only BusyCoq and standard-library dependencies", "Consolidated checked proofs").
   • Citations of six audit/analysis .md files that are not in the repo, plus dozens of absent per-machine .v files.
   • Coverage: these markers cover 132 of 297 proof kills (44%) since Jun 29, and 189 (64%) if prose-heavy new-style files are included. None appear before 2026-08-15. No commit message, README or co-author trailer mentions AI.
5. Picked clean (0 left in the 778): Counter Class 1, Skelet 17-like, Quadratic Skelet 17-like, List merging, Bouncer + Complex Counter, Bouncer + Translated Counter, Structural counter + bouncer. Nearly clean: Chaotic Fractal Type 1 (4 left), Sync bouncer counter (4), Counter Class 2 and 3 (3 each), Monotone list (8).
6. Actively mined (avoid): - Shift-overflow counter (128 left, 130 proof kills since 08-30) - Skelet 1-like Class 1 (101 left; someone is working through a numbered "Sk1 Class1 TM1..TM105" list) - Cubic Mess (50 left; "completed machines from cubic.txt", plus 6 CubicCap Cert_WF stubs) - Shift-overflow bouncer counter, Monotone list, Counter Class 3, Translated Counter - Halting proofs in Bell-like and Quadratic Mess via RLE accelerators (Bell60.v, QuadraticMess30.v, 10-07)
7. Stalled but plausible (targets): - Cooled off in August, templates exist:
   • Bell eats counter (40 left)
   • Shift-overflow structural counter (11)
   • Structural counter + chaotic edge (11)
   • Bouncer + Chaotic Edge (20)
   • Skelet 1-like Class 2 (14)
   • No proof kill since Dec:
   • Structural counter + counter (5)
   • Counter Class 4 (2)
8. Tarpits: - Bell-like: 15 of the 18 sheet cryptids, 18 machines on the "worked on extensively" tab, 1 proof kill since Dec. - The chaotic classes:
   • Chaotic Bell Class 3 (FAR got 9 of 24 in 2025, nothing since)
   • Spaghetti
   • Chaotic 1dCA-like in bouncer and in bell
   • Chaotic Ack-like Bell
   • Four holdouts with "NONHALT (?) unlikely to be correct" claims.
   • Cost blow-ups: recent BLEC proofs cost 313 KB per machine, TranslatedBell 117 KB, SOBCv10 152 KB for one machine.

1. Method, validation and caveats

Pipeline (stdlib Python; run in this order; total runtime under 30 s):

Equivalence classes. forensics_common.equiv_key is a general n-state, m-symbol normal form: halt notation, L/R mirroring, and BFS renaming of non-start states. It agrees with tools/holdouts.py equiv_key on all 12,372 snapshot machines and handles e.g. 3x3 1RB2RA1LC_2LC1RB2RB_---2LA1LA.

Validation: - Per-window reason counts match data/crossref.md §2 exactly. For example, 1003→815: 176 proof (91 exact + 85 mirror) and 12 equivalence; 1161→1119: 2 proof and 40 equivalence. - The 815→778 split matches crossref §3.1: 18 removals from 27b8b41 and 19 from 0940bb9. - Commit attribution matches git log -S. In 88 random exact-tier attributions (8 + 80), the attributing commit equals git log -S'<tm>' --reverse -- verify/<file> in every case. - The rename fix was checked. Following renames moved one kill (SOBCv11.v) from a false "2025-09 Eqv" attribution to univerz's dba975e.

Caveats: - Commit author ≠ proof author. mxdys commits other people's work. Sometimes a header carries a credit (M-Abozaid); usually nothing does. - The sheet's Results tab is stale. It is keyed to the 1534 list, and its status column stops after ~Apr 2026: 315 of 316 removals since Jun 29 have a blank status. "Done By" is only informative for Dec–Apr. - There is no Discord access. The sheet's Discord links end in Mar 2026, so "is someone working on X right now" is inferred only from commits and file headers. - "Family" is derived from the filename (forensics_common.FAMILY_RULES). The "misc named mechanism" bucket lumps BMO, BC, BL, LM, FIB, RGR, S18, InfiniteRect and others. - "Kill month" is the commit month of the attributing proof. For equivalence rows it is the month the list dropped the machine.

2. Commit history

2.1 Coarse, back to the branch start (U3)

• The 2024Q4–2025Q1 string counts are the decider-certificate dumps: CTL/CPS/RWL files with up to 6 MB and 235k strings each.
• The 2025Q3 removals (1,538) include 783 equivalence merges in 2592→1618, the month Eqv*.v landed.
• 131 of the 133 commits are by ccz181078; the others are one by Shawn Ligocki (Antihydra proofs, 2025-10) and one by univerz (PR #5, 2026-09-23).

2.2 Every commit since 2025-12-01 and the removals it explains (U2)

Full table: reports/forensics/tables2.md §U2.

Commits come in weekly-ish batches, and mxdys shares a new list the same day or the next.

3. What was killed, Dec 2025 → Oct 2026

3.1 Per window

• Proof form: 343 proofs are byte-exact; 220 (39%) exist only in mirrored 1LB… form. Those would fail our check_kill.sh string rule as written. That is fine for them, but it means their templates must be re-targeted to the exact list string.
• Equivalence merges are concentrated in April (Eqv_Misc.v updates). They are not work on any mechanism.

3.2 Kills per month per technique family (T2)

Proofs are counted by the commit month of the attributed proof; equivalence rows by the month the list dropped them.

What the table shows: - Dec–Mar was mxdys's decider era: - FAR (his DFA generator), LongAcc/LongLoop (generalized longitudinal analysis) and SOCSS together gave 165 kills. - These routes then dried up: FAR's last kill was 07-29, RWLAcc/UBRRBA's 08-30, and LongAcc gave 2 more on 09-23. - April–June was nearly dead: 10 proof kills, plus equivalence bookkeeping. - July–August was mxdys-style individual proofs, small batches across many classes: CounterClass2, Bouncer_v3/v4, LM, BL, SBCv10/11, SOBL, BEC. - September–October is the burst analysed in §5: SOC ×88, SOMDC ×33 (31 of them SOMDC_Class1.v), Sk17/Sk1 ×26, FractalType7 ×20, CounterClass1 ×16, Cubic, and halting checkers.

3.3 Family proofs vs individual proofs (T4, U1)

How the 563 proof kills are packaged:

• The 563 kills come from 127 distinct files. 28 files with 5 or more kills account for 399 kills (71%); 57 files kill exactly one machine.
• Halting proofs were 31 of 266 kills (12%) in Dec–Jun and 59 of 297 (20%) since Jun 29.
• 53 of those 59 were never on the sheet's direct-simulation backlog. They are long halters proved by accelerated certificates or verified checkers, not by plain simulation: LongAccHaltv1.v, UBRRBAHaltv2.v, SOC23_Halt165.v, SOC23_PeriodicHalt.v, SOC43_Halt13/14.v, SOC_4_3_Halt.v, CubicMachines.v, Bell60.v, QuadraticMess30.v.

Median proof size (bytes of the attributed file ÷ machines it proves; U8):

For CounterClass1, the shared libraries CounterClass1Common.v and the K4Boundary*.v files bring the directory to 699 KB, about 44 KB per machine.

3.4 Who

• Commit authors: ccz181078 (mxdys) for 562 of 563 proof kills and all 75 equivalence merges. The exception is univerz (1), whose PR #5 CounterRegular.v mxdys renamed to SOBCv11.v the next day without a credit line.
• Credits inside files: M-Abozaid in BTCv4.v ("M-Abozaid M23 and its sibling… Sources, certificate conversion and audit: EXTERNAL_BOUNCER_PROOFS.md") and in SOTCv2.v ("M-Abozaid M7… Source and attribution: EXTERNAL_BOUNCER_PROOFS.md"). Older files credit only sligocki (Skelet1*, AntiHydra) and dyuan/mxdys (BB33_543). Nothing else names a contributor.
• Sheet "Done By" for Dec 2025+ removals:
• Windows 1416→1161 (Nov 28 – Mar 25, 255 removals): mxdys 224, Andrew Ducharme 18 (all FAR-certificate nonhalts), Alistaire 7, prurq 4, Peacemaker 3, Shawn Ligocki 2, Racheline 2, Dyuan 2.
• Windows 1161→1094 (Mar 25 – Jun 29, 67 removals): equivalence merges credited to "-d" (54) and mxdys.
• Jun 29+: 315 of 316 blank. The sheet stopped tracking, so recent proof authors are unknown except where a file header says.

3.5 Sheet classes of the killed machines

The full per-class table is in §4. Since Dec, kills by sheet class:

4. The 778 remaining: distribution and kill velocity

Sheet tabs and simulation backlog: - Classes: all 778 are in the Classifications tab. - Results status: - 759 blank - 18 CRYPTID: 15 Bell-like, 2 Quadratic Mess, 1 Shift-overflow bouncer counter - 1 NONHALT: the …_1LA1LC sheet mix-up already noted in STATUS.md - Category tabs: category-1 (bounded inductive rules or halts; most cryptids) 16, category-2 (mxdys's 50 random) 21, category-3 (Chaotic Bell Class 3, "two arrays of integers") 15. - Level tabs: level-0 115, level-1 ("worked on extensively") 41: Bell-like 18, Cubic Mess 7, Quadratic Mess 5. - Direct-simulation backlog: - 133 still not simulated to 10¹⁴ and 168 not to 10¹⁵. - The 10¹⁴ backlog is concentrated in chaotic classes: Chaotic Bell Class 1 19/19, Chaotic 1dCA-like in bouncer 14/14, Spaghetti 16/18, Chaotic Bell Class 3 11/22, Chaotic 1dCA-like in bell 9/9, Unknown 40/93. - Traces in busycoq: 299 are mentioned in verify/ but none is proved. 286 appear only as the tm' representative of an Eqv*.v lemma, and 6 Cubic Mess machines have only a Cert_WF stub in CubicCap.v. - Equivalence groups: in 2026-10-07_eqv_1590.txt, 291 of the 778 groups have more than one member.

Per class. Velocity = proof kills since 06-29 ÷ (that + remaining). State: - hot: a proof kill since 08-30 - cooling: proof kills in Jul–Aug only - stalled: Dec–Jun only - untouched: no proof kill since Dec

Full table with Discord-link counts and verify/ mentions: reports/forensics/tables2.md §U5. Per-machine detail: reports/forensics/remaining_778.tsv.

Is mxdys (or someone) actively mining a class?

The evidence is the file headers and commit cadence. The sheet and Discord links are stale, with the newest sheet link from 2026-03-29.

• Shift-overflow counter: yes, heavily.
• SOC files landed in three batches, 09-16, 09-30 and 10-07: SOC_2_3_v4/v5, SOC_2_4_v8, SOC_2_5_v2, SOC_3_3_v5, SOC_3_4_v1, SOC_3_6_v1, SOC_4_3_v1, SOC_4_3_Halt, SOC23_*, SOC43_*, SOCMisc.
• Their headers cite numbered work lists ("SOC_ex rows 8–14", "test_SOC_4_3.TM10", "SOC_FT7_CONSOLIDATION.md for numbering").
• Some 50 of the 128 remaining are already equivalence representatives in Eqv*.v, so mxdys has processed them at least that far.
• Skelet 1-like Class 1: yes, just started. Sk1Machines.v (09-30) is titled "Sk1 Class1: TM17 nonhalts; TM91, TM94, TM104, TM105 halt", so someone holds a numbered list of 105 or more of this class's 112 original machines.
• Cubic Mess: yes. CubicMachines.v (10-07) says "Completed machines from cubic.txt: TM1, TM17, TM18, TM39, TM41, TM49", and the 6 Cert_WF stubs in CubicCap.v are mxdys's own unfinished work.
• Bell-like and Quadratic Mess: the halting route is active. Bell60.v and QuadraticMess30.v (10-07) are RLE-accelerator halting certificates, the latter from "the halting-proof archive supplied by the user". The nonhalting side has barely moved (1 Bell-like and 5 Quadratic Mess proofs in 3 months).
• Everything "cooling" had a burst of mxdys-style batch files in Jul–Aug and nothing since 08-30: Bell eats counter, SO structural counter, Structural counter + chaotic edge, Bouncer + Chaotic Edge, Skelet 1-like Class 2, Sync bouncer counter, Counter Class 2, Fractal in Bouncer. The same templates could produce more if someone pushed. mxdys may come back to them, but there is no sign of a numbered work list for them in any recent header.

5. AI signals

5.1 Explicit mentions (searched: all 133 commit messages incl. bodies, README.md/README_old.md, every comment in every verify/*.v at the pin, the whole diff history of verify/, every cell of all 12 sheet tabs)

No hits anywhere for GPT/ChatGPT/LLM/Gemini/Codex/Copilot/DeepSeek/agent/auto-generated, no Co-authored-by trailers, and nothing in the README.

The three "user" comments are written in an assistant's voice, describing an archive "supplied by the user". A human author would not describe his own input that way. This is direct evidence that at least those three files were produced or rewritten by an AI assistant for someone, and merged by mxdys.

5.2 Probable markers (consistent with agent-produced files; none appear before 2026-08-15)

• Boilerplate self-description headers:
• "Standalone; only BusyCoq and standard-library dependencies" (SOC23_Nonhalt51.v)
• "Self-contained except for BusyCoq and the Coq standard library" (Sk1Machines.v)
• "This file needs only BusyCoq and the standard library" (SOC23_Halt165.v, SOC23_PeriodicHalt.v)
• "Only BusyCoq and standard-library dependencies; no stored long trace" (Bell60.v)
• "ported to current BusyCoq… generated and checked inside Coq; no external trace table or generator is needed" (CounterClass3v2.v)
• In total, 12 files carry such phrases, the first being Sk17.v on 09-08.
• Citations of audit/analysis documents that are not in the repo:
• SOC_FT7_CONSOLIDATION.md (10 citations; "Consolidated checked proofs. See SOC_FT7_CONSOLIDATION.md for numbering." heads 7 SOC files)
• EXTERNAL_BOUNCER_PROOFS.md (2: "Sources, certificate conversion and audit")
• SOC_EX_WEIGHTED.md ("Informal argument and compilation/audit records")
• SOC_ANALYSIS.md, section 49
• SOC51_BLOCK_PROOF.md
• SOC43_EX13_RUNS.md ("the independent simulations")
• Plus cubic.txt, m23_dfa_analyze.py, symsim.py.
• References to dozens of absent per-machine source files, i.e. a consolidated external workspace. Examples: SOC23_R2carry.v, SOC23_TM102Halt.v, FT7CallRules.v, FT7Compute.v, FT7TM16Nonhalt.v, SOCPair12Carry.v, SOCPair12Guard.v. FractalType7v2.v even keeps a dozen concatenated Require Import blocks from the files it was stitched from. A workspace of hundreds of small files plus *_ANALYSIS.md / *_RUNS.md / *_CONSOLIDATION.md records is the typical footprint of a coding-agent workflow. Speculation: we cannot see the workspace.
• Phrases like "untrusted input", "audit", "conservative checker… with primitive fallback at every unmatched edge" and "rechecked for this transition table, not assumed from TM13". These are careful-verification boilerplate typical of current coding agents. Weak evidence on its own.

5.3 Style statistics (proof files at the pin, by date the file was added; certificates excluded; medians per file; style_summary.md)

How the two styles differ: - Classic mxdys files are terse. - Short Lemma … Proof. es. Qed. / ind n Inc chains, short lemma names (mean about 6 characters), no comments. - About 3.6 KB per machine. - Example: verify/Bouncer_v3.v (3.5 KB) and the rules at the top of verify/CubicMachines.v TM1, which mixes both styles. - The new population reads differently. - Long, snake_case lemma names (partition_phase_columns_Forall), full-sentence explanatory comments with coqdoc [refs], and lines about twice as long. - It defines its own data structures and verified checkers: an Inductive tape/word type, a Fixpoint interpreter or generator, a soundness lemma against -->*, then vm_compute over finite data. - It barely uses the framework's es/follow. - The style shift starts on 2026-08-15 (BLECv3x.v, BLECv3y.v, SBCv6a2.v: prose comments, references to TM4x1.txt-style data files). Assistant-style headers start 09-08 (Sk17.v); the explicit "the user" comments appear on 10-07. - Caveat: "prose-heavy" is a style, not proof of AI. mxdys's own files also grew after mid-2026 (e.g. SOMDC_Class1.v, plain header, 2.8 prose comments per 1000 lines).

5.4 How many kills came from marked files (U10, U11)

Tiers, first match wins: - explicit: an "the user" comment - assistant header: self-contained/standalone/consolidated/attribution header or .md audit citation - absent refs: comments cite files not in the repo - prose-heavy: at least 1 full-sentence comment per 1000 lines - classic: none of the above - cert: decider certificate

Since Jun 29: explicit 10, assistant header 102, absent refs 20, prose-heavy 57, classic 92, cert 16 (297 total).

Which classes fell to marked files (Jun 29+, explicit + assistant header + absent refs):

The other recent kills are classic mxdys work: Counter Class 1 (16, CounterClass1/), Monotone list (Loop4Mono_v*), Sync bouncer counter (SBCv7.v, SBCv11.v), List merging (LMv1..v3.v), Structural counter + chaotic edge (BLv2.v, BLv3.v, Bouncer_v4.v), and SO structural counter (SBCv10.v, SOBLv1..v3.v).

Interpretation (labelled speculation): - The AI-assisted contributor(s) do best on arithmetic counters with a finite case structure that a verified checker can grind through: shift-overflow counters, Skelet-17/Sk1 column flows, Fractal Type 7. They also do well on long halters, where a proved accelerator (RLE, periodic tape) replaces simulation. - Those areas are weak to AI, and they are being harvested right now from numbered lists. - The AI-style files have not touched the chaotic classes, Bell-like nonhalting, Spaghetti, or the bouncer/counter hybrids that mxdys handled by hand in Jul–Aug.

6. Conclusions for Track B

6.1 Picked clean (nothing left in the 778; don't look here)

Nearly clean (≤ 4 left, high velocity): Chaotic Fractal Type 1 (4), Sync bouncer counter (4), Counter Class 2 (3) and 3 (3), Fractal in Bouncer (3), Chaotic Fractal Others (4). The leftovers are probably the ones the batch technique did not cover. They are worth a look only if their nearest template obviously fails for a nameable reason.

Methods that are picked clean (re-running them will not find more): - mxdys's FAR/CTL DFA generator: 73 kills Dec–Jul, none since. - LongAcc/LongLoop longitudinal deciders: 91 kills, last 09-23. - RWLAcc/UBRRBA halting certificates: last 08-30. - Equivalence merging (Eqv*.v): 75. It doesn't shrink the real problem.

6.2 Actively mined (avoid; duplicate-work risk)

6.3 Stalled but plausible (targets), ranked

Our activity signal comes only from commits and file headers. Before committing to any of these, still do the ground-rule-7 check (sheet row plus Discord thread).

1. Bell eats counter, 40 left. - Activity: 4 proof kills in Jul–Aug (SOMDCv6.v 2 in July, BECv7.v 2 on 08-15), plus 3 equivalence merges in August, none since 08-30. Only 2 machines are on level tabs and 1 has a Discord link (2024). - Templates: BEC is one of the oldest classes ("typical bell eats counters", 2024): verify/BECv1.v … verify/BECv8.v, most recently verify/BECv7.v, plus verify/SOMDCv6.v. - Caution: the two level-tab notes call members "chaotic bell eats counter". Triage for the regular ones first.
2. Shift-overflow structural counter (11) and Structural counter + chaotic edge (11). - Activity: 8 and 6 proof kills in Jul–Aug, none since. No level-tab notes for the second class, and only one "possibly tetrational" note for the first. - Templates, SO structural counter: verify/SBCv6a.v, verify/SBCv10.v, verify/SBCv6a2.v, verify/SOBLv1.v…SOBLv3.v. - Templates, Structural counter + chaotic edge: verify/BLv2.v, verify/BLv3.v, verify/Bouncer_v4.v.
3. Bouncer + Chaotic Edge, 20 left. - Activity: In Feb–Jun, decider certificates took 7 (RWLAccHaltv8.v ×3, FAR ×4). In July, individual proofs took 4 (InfiniteRect_v1.v, LongNv1.v, Bouncer_v3.v, UBRRBAHaltv2.v). None since 07-29. The certificate route is exhausted, so what remains needs individual proofs. - Templates: verify/Bouncer_v3.v (3.5 KB), verify/InfiniteRect.v, verify/LongNv1.v.
4. Skelet 1-like Class 2, 14 left. - Activity: 1 kill (SBCv6.v, 08-15). - Risk: it is adjacent to the actively mined Class 1. Check whether the Sk1Machines.v numbering covers Class 2 before investing. - Templates: verify/SBCv6.v; for the sibling Class 1, verify/Sk1like_TC_v1.v, verify/Sk1like_TC_v2.v, verify/TCv3.v (Mar) and verify/Sk1Machines.v (Sep).
5. Structural counter + counter (5) and Counter Class 4 (2). - Activity: untouched since Dec, while all their sibling counter classes were cleaned Jul–Oct. - Templates: verify/CounterClass1/ (parameterized), verify/CounterClass2v1.v…v4.v, verify/CounterClass3v1.v, verify/CounterClass3v2.v, verify/CounterCmp_v1.v. - Caution: 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF (Counter Class 4) is the machine in atlas/tooling-notes.md on which Quick_Sim finds 0 rules. It may be genuinely irregular.
6. Side quest (halting), not proofs: the not-simulated-to-10¹⁴ backlog sits in the chaotic classes (Chaotic Bell Class 1 19/19, Chaotic 1dCA-like 23/23, Spaghetti 16/18, Unknown 40/93). Recent halting kills came from accelerators, not this backlog. The backlog is still unsimulated, which makes it a cheap lottery for our sim tools.

6.4 Recurring proof templates worth reusing

6.5 Tarpits

• Bell-like nonhalting (80 left):
• 15 of 18 sheet CRYPTIDs, 18 on the "worked on extensively" level-1 tab, 9 on category tabs.
• 1 proof kill in 3 months, and that one was a halt.
• Treat it as the cryptid frontier (PLAN §8), not Track B.
• Category-1 tab ("bounded inductive rules, or it halts", 16 left: Quadratic Mess 8, Cubic Mess 4, Bell-like 4): the sheet itself says most cryptids live here.
• Chaotic classes with no proof kill since Dec:
• Chaotic Bell Class 3 (22; FAR killed 9 of 24 in 2025, nothing since)
• Chaotic Bell Class 1 (19, equivalence only)
• Spaghetti (18)
• Chaotic 1dCA-like in bouncer (14) and in bell (9)
• Chaotic Ack-like Bell (11)
• Chaotic Bell Class 4 (5)

Nobody, human or AI-assisted, has found a mechanism here. Expect STUCK. - Claimed-but-wrong proofs. Four of the 778 carry "NONHALT (?)… unlikely to be correct" on the Unverified tab: - 1RB1LB_1LC0RD_0LE1LA_0RF1RA_1LE0LA_---0RB - 1RB0RE_0RC---_1LD1LE_1LE1LD_1RF0LC_1RA1RF - 1RB0RE_1LC0RA_0LD0LB_1RE0LB_1RF---_0RB0RC - 1RB1RB_0LC0LD_0LE1LD_1LB0RE_1RA0RF_1RD---

Earlier informal arguments failed on these. - 1RB1LA_1RC0RF_1RD---_0LE1RB_---0LA_1LD1RF (Cubic Mess, two ---): "analysed thoroughly using formal proofs from Claude Opus 4.6" and still open; the sheet lists it as a potential cryptid. Someone has already thrown an agent at it. - Cost blow-up families: the recent kills in BLEC (BLECv3z.v, 772 KB for 2 machines), TranslatedBell (117 KB per machine), SOBC (SOBCv10.v, 152 KB for 1) and Loop4 (26 KB per machine) needed enormous bespoke proofs. The cheap members of these families are gone. - Mirror-form templates: 220 of 563 upstream proofs state the machine mirrored (1LB…). Copying one gives a file that fails our byte-exact gate until the string and every rule are mirrored back.

Appendix: files

Reproduce (about 30 s; read-only on vendor, no __pycache__):

cd [local working file]
python3 -B tools/analysis/forensics_git.py -j 24
python3 -B tools/analysis/forensics_attrib.py
python3 -B tools/analysis/forensics_style.py
python3 -B tools/analysis/forensics_report.py