/reports/wave4/ranking.md · raw

Wave 4 ranking (2026-10-10)

These are the 8 picks to attack now. They come from merging the four scout tables in reports/wave4/ (templates, families, dynamics, claims). Scout signals are evidence only; only a tools/check_kill.sh PASS counts as a kill.

Universe: the 740-list machines with no machines/ directory, 699 of them. Every pick and every family member below was re-checked: each is on the 740 list byte for byte, none has a directory, and none is canon-equal to one of ours.

Picks

label machine 740 line class why nearest template risk family (covered by the same proof)
W4-1 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB 590 Bell eats counter Kill #30's transition table, renamed EABCDF with no mirror, started in #30's state B (confirmed: identical table key). Two scouts independently ran #30's own check_proof section D (Lemma D, FIN, H3) from this start: ALL PASS to N = 400,035 (11,074 epochs). The model also reproduces 71/71 later left records to 1e8 steps. Unclaimed. #30's .v with a state rename, a new init (42 steps to L(2,0001)) and a new vm_compute finite part from K 3 t1 to N ≥ 17,705, with Inv there. inv_step, LP and Phi are reused verbatim. Low. The finite part has to be recomputed, and its size and compile time are unknown. Timing (critic): #30 is claimed but not submitted; once #30 is public, ccz181078 can port it to this table's other starts himself, so finish W4-1 (and #7) before posting #30 and submit the three as one family. No other universe entry. Our STUCK #7 (line 381) has the same table and takes the same route (mirror plus #24's flip_halts/perm_halts recipe). Run the two together.
W4-2 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF 224 Bell eats counter 1 transition (F1) from two hand proofs, BECv5.v TM1 (F1=0RB) and TM2 (F1=1LB). F1 fires only during the left-counter carry (811 times in 1e8 steps). Record configurations have the same shape as both neighbours, 0^inf <A 1^(2j+1) (10)^x (01)^(2^j-1). Dynamics rank 5, closed rule table, unclaimed. BECv5.v TM1/TM2 (about 140 lines each). Keep LC0, R, LInc0, LIncs and RIncs; re-derive ROv, LIncs' and BigStep for F1=1LF, then choose the invariant. Medium. The F1=1LF carry may need more low-bit case splits: rulefit shows a parity-mixing reset A0(4n+13,4m+3,2k+1). mxdys left this variant for about 14 months. No same-table entry. 349 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- is the same BECv5 table with F1=1RC, run from another start (look-alike skeleton). It needs its own proof but the same method. Critic: upstream Eqv_v3.v makes F1 ∈ {1LF, 1RC} irrelevant for both starts. TM493 proves 224 ≡ 224 with F1=1RC (1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC, its eqv member), and TM518 proves 349 ≡ 1RB1RA_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB---, which is 224's exact table started in 349's start. That twin is also 1 transition from BECv5 TM1/TM2. So 349 is a second start of the same table up to a proved equivalence, and a start-independent epoch invariant for 224 should carry over.
W4-3 1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA--- 341 Skelet 1-like Class 2 Our strongest class (8 kills). One table, 3 listed starts (confirmed). 341 and 512 are exact twins and 588 is the mirror view; they are different orbits of one macro map, like the #3 and #11 families. The tape is (10)^a (01)^b pairs with 0^2 separators. Claims score 0.91: the only mentions are Level-0 rows and an Eqv tm'. Our Sk1C2 kills (#3 and #11, with SBCv6 TM21's architecture). The trio is 4-5 transitions from #11/#33, so it needs a new proof first. After that, the other two are ports (the #25/#33b recipe). Medium to high, because the first proof is new. Our open PR #15 may draw mxdys to the rest of this class, so move fast. 512 1RB0RA_1LC0RE_1LD0LC_1RA0LB_1RA0RF_1LE---, 588 1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD
W4-4 (bold) 1RB0RA_1LC0RE_0LD0LB_1LA1LF_1RA0LF_1LC--- 156 Unknown 4 kills from one proof: one table with 4 listed starts (confirmed), exact trajectory twins (76,681-76,685 cells, nonzeros 38,337-38,339 at 1e9). It is a Skelet-like run counter on 10^a/01^b blocks and a look-alike of #11 (width within 7%). Rulefit closed (156 and 564), skeleton stable from 1e8 to 1e9. Unknown class, so not mined; unclaimed. #11's architecture (counter over (10)^u [00] (01)^v digits). It is 6 transitions away, so this is a new proof. High. The far tape has irregular block lengths, and 450's rule fit has a /k guard (Collatz-like caution). Critic: the four orbits are near-twins, not merged. They share no record configuration in 3e6 steps, and their record times differ by 0.005-0.07% at 1e8. So expect one architecture with four inits and bases, not one proof with four one-line inits. 188 1RB1RF_1LC0LB_1RE0LD_1LB0RF_0RA0RC_1RE---, 450 1RB0LE_0RC0RA_1RD1RF_1LA0LD_1LD0RF_1RB---, 564 1RB0LF_1RC0RB_1LD0RA_0LE0LC_1LB1LF_1LD---
W4-5 1RB0LF_1RC0LB_1RD1RB_1RE1RF_1LA---_0RC1LA 469 Counter Class 2 Tiny clean counters (462-511 cells at 1e9, growth exponent about 0.1), unclaimed. Targeting gated them out only for an Eqv tm' mention. The class has been cooling since 07-29. None has been simulated to 1e14, so a HALT proof is possible and would also count. CounterClass2v1.v (599 is 1 transition away, but in C0, a bulk slot) and CounterClass2v1..v4; our #12 (Counter Class 4) for recursive counter work. Medium. Rulefit and compress do not handle counters, so the digit rules need fitting by hand. Run an accelerated halting search first. 599 1RB1RD_1LC---_1RF0LD_0RE1LC_1RA1RF_1RE0LF (same table); 530 1RB0LA_1RC1RA_1RD1RE_1LC---_0RB1LF_1RA0LE (its eqv member has this table, 1 transition from 530's own string, so it needs its own init or an Eqv bridge). Critic: the eqv members of 469, 599 and 530 are each 1 transition from all four CounterClass2v1-v4 files (always the same slot, where the proven files have 0LF/1LA/1LE/1LB and ours have 1RF/1RA). Upstream Eqv_v2 TM359/TM1380 and Eqv_v3 TM306/TM540/TM627 tie the three tables together.
W4-6 1RB---_0RC0RF_0RD0RA_1RE0LB_1LF0LE_1RC0LE 99 Unknown (Skelet-like) An exact twin pair (44,247/44,255 cells, identical skeleton). The tape is a chain 10^a 01^b 0^2 10^c 01^d 0^2 ..., the same grammar as #3's (10)^p (01)^q pairs, so our Sk1C2 pipeline applies. Labelled Unknown, so not mined; unclaimed. #3's down-counter (TM21 architecture, the J invariant). Compare the macro steps first. Medium. No rule table yet (rulefit none), and qsim flags its rules as Collatz-like. 612 1RB0RA_1LC0RA_0LF0LD_1LE---_0LC0LB_1LA0RE
W4-7 (cheap) 1RB0RA_1RC0RD_1RD0LC_1LE1RA_---1LF_1RB0LC 317 Bell eats counter IndBECv1.v (a verified hlin decider with per-machine configs) certifies this exact table from another start: _3ary nonhalt3, 1LB0LC_1LC0RB_1RD1LF_---1RE_1LA0RB_1LA0LF, using config_T_bsz 745 3 plus side_3ary_Pos_inc_rule (confirmed by table key). 317 and 707 are trajectory twins. Batch with them the twin pair 88/280, whose tables IndBECv1 also certifies from other starts (88: Others nonhalt17 config_BEC 1000 3 B F [0] [0] [0;1]; 280: Eat1Digit nonhalt6 config_BEC 1000 3 B E [] [] [0;1]. Critic correction: nonhalt6 is in Module Eat1Digit, line 526, not Others). IndBECv1.v configs. Try a small config grid per machine (state pair, T, digit words) through solve_hlin_nonhalt, one coqc at a time. If that fails, write a hand proof from the certified sibling's dynamics. Low cost, low to medium odds. mxdys's own sweep probably already failed on these starts. 707 1RB0LA_1LC1RF_---1LD_1RE0LA_1RA0RB_1RE0RF. Same method, separate families: 88 1RB0LC_1LC0RE_1LA1LD_1LA1LB_0RF1RA_---0RE and 280 1RB0LC_1LC0RE_1LA1LD_1LA1LF_0RB1RA_1LC--- (trajectory twins, tables 3 transitions apart)
W4-8 (bold) 1RB1RA_1LC0RE_1LE0LD_0LB1LB_1RA0LF_1LD--- 644 Unknown (fossil bouncer) One table with 3 listed starts (confirmed). Dynamics rank 3 of 256: 3 skeletons cover every snapshot at 1e8, and 644 and 61 stay stable to 1e9. The bouncer rule is C0(a,-a+407,3a-32) -> C0(a+1,-a+406,3a-29): per visit a goes +1, b −1, c +3, over 10100111 words. Different class from W4-1..7; unclaimed. None within 3 transitions. Nearest experience: our #8 (sync bouncer counter) and R4's fossil walls. High. The reservoir b runs out, which leads to hierarchical epochs (R4/R5 territory). 61 is on mxdys's Category-2 random-50 tab. 61 1RB0LF_1RC1RB_1LD0RA_1LA0LE_0LC1LC_1LE---, 704 1RB---_0RC1RC_1RD0LE_1RE0RB_1LF0RA_1LC1LF

If all 8 work, they cover 21 list entries: 1 + 1 + 3 + 4 + 3 + 2 + 2 (+2 for 88/280) + 3, plus our #7 alongside W4-1.

Action outside the universe (worth more than most picks)

#16 / pool #39 / R7 share one table with an upstream hand proof. #16 is line 440 (ours, CHECKPOINT_A, hub_invariant). Lines 199 and 510 have the same table, and so does FractalType4.v Module TM5 1RB0RE_1RC0RF_0LD---_1LA1LE_1RA0LB_1LC1RE (confirmed by table key; ccz181078, 2025-06-17, about 140 lines). TM5 starts in E in 440's naming; 199 starts in TM5's B and 510 in TM5's F (mirror).

I simulated the orbits. TM5's own orbit has a clean two-block outer tape, for example 110^683 10^597 110^82 1^2. The three holdouts carry a staircase of extra walls: 440 10^745 110^58 10^15 110^679 ..., 199 10^141 110^272 10^206 110^180 10^44 110^338 ..., 510 similar. So TM5 is not a port. But its inner engine (Inc1/Incs1, and P_S/P_S' for P a, all stated for an arbitrary left tape l) should carry over directly. Hand this to #16's owner; it was not mentioned anywhere in our files.

199 and 510 are not picks: they are #16's siblings, and #16 is in flight.

Notable rejections

machine (740 line) signal reason
381 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA (our #7) #30's table; #30's section D passes to N = 400,004 Ours (STUCK), so outside the universe. Do it with W4-1.
199, 510 Same table as FractalType4.v TM5 (a hand proof) Siblings of our in-flight #16 (duplicate risk). TM5 only covers the wall-free orbit (see above).
552 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB Sk1C2 singleton, no mentions anywhere (claims 0.85) Same class as W4-3 and 7-8 transitions from every kill. Reserve after W4-3.
134 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC Bell eats counter, dynamics rank 4, closed rules No template within 3 transitions. Three BEC picks already, and we have 5 STUCK/CRYPTID machines in this class. Reserve.
29 1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC--- Dynamics rank 1, closed rules, eqv group 13 Level-0 note "chaotic bell eats counter"; two residue-dependent rules (A0(4n,…)).
458 / 635 Closed rules (635 coverage 0.92), Block_Finder accelerates to 1e12 Fossil blocks (-7n+630) and a parity-halving rule B1(4n,2m+1) -> B1(2m+2n+2,4n+1); sligocki flags them as Collatz. Cryptid risk.
197 / 583 / 678 1 transition from FractalBEC/BECv1 instances Exact trajectory twins of our CRYPTID 611/486 and CHECKPOINT_A 596.
239 Labelled BEC, closed rules Growth exponent 0.646, not a bell; fossil rule E1(2n,-n+632).
87 / 342 / 689, 312 / 337, 118 BEC trios and pairs; 118 is Bouncer + Chaotic Edge On dyuan01's longitudinal-24 list (118 is also on UBRRBA-86): claim risk.
129, 411 (Sk1 Class 1); 409, 70, 223 (SOC) Startup-only differences from hand proofs (TCv3, SOC_2_5_v1) Mined classes; mxdys is working through Sk1 Class 1, and the sibling files are 7-14 months old, so the leftovers probably differ for a real reason.
701, 244, 216 Near CounterClass3v1 HALT proofs Counter Class 3 is taken (CounterClass3v2, 10-07), and these need an accelerated-simulator port.
716, 211 Regular-looking bouncers D0(2n) -> D0(3n+16) (×3/2, Antihydra-like) and a ×4/3 map: cryptid protocol.
159 / 218 / 230 qsim reaches 10^129-10^204 Ack-like Bell: tarpit, no hand proof ever.
90 Structural counter + counter M-Abozaid's public Lean proof (claimed).
556 Upstream Eqv_WordPairs TM83 makes it equivalent to our #19.
53/307/398/663, 344/426/600/706 4-start families Chaotic tapes, no rule table.
652 Tiny counter mxdys: "strange shift overflow counter probably" (SO heat).

Exclusions applied

Resource notes for the attack

Critic (completeness pass, 2026-10-10)

Verdict: the 8 picks stand, with the same labels. Nothing I found beats the weakest pick (W4-8) once claim and heat risk are counted. The changes are corrections and extra facts inside the table, each marked "Critic": W4-1 timing, W4-2 Eqv tie to 349, W4-4 near-twins, W4-5 Eqv/CounterClass2 ties, W4-7 module name for 280. Scratch: /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/w4crit/ (upidx.py, near.py, d0scan.py, d2scan.py, ours2.py, merge.py, twin.py and their .txt outputs).

Signals that were not run or were under-used, and what re-running them showed

signal gap in the scouts re-run here result
Templates at upstream HEAD Template scout used vendor 0940bb9 only. It missed the 6 files new in 9cf9e88 (BellEatsCounter_1RB0RF, ChaoticBell1Halt, Cubic50, CubicMachines_v2, Eqv_RegularPairs, Eqv_WordPairs) and our PR #15 files (feeffa1). It had only 3 rows from our own .v files, and no dist-0 rows at all (same table, other start). (a) Distance ≤ 1 at HEAD, all 240,415 TM strings in verify/*.v, for every pick, family member and reserve. (b) Same table, any start, for all 699 universe machines against all upstream strings. (c) Distance ≤ 2 for all 699 against our 43 machines (any status) plus the 10 new files. No pick or family member is proved or certified upstream, beyond the IndBECv1 entries the ranker already found. Our kills have no universe neighbour within 2 transitions except 590 (W4-1). The only new cluster is Chaotic Bell Class 1 around ChaoticBell1Halt.v (see the rejections below).
Eqv members as alternative start points Templates were measured from the list strings only. near.py on the 35 eqv-1590 members of the picks. 349's eqv twin is 224's exact table, 1 transition from BECv5 TM1/TM2. The eqv members of 469/599/530 are 1 transition from CounterClass2v1, v2, v3 and v4. 317's and 280's members have the IndBECv1 tables (already known). There is nothing new for W4-3, W4-4, W4-6 or W4-8.
Same table as an upstream decider certificate from another start (FAR, CTL, RWL, NG, CPS, TCv1, Indv3/5) Not listed by any scout. Part of scan (b): about 60 universe machines. These are parameterised decider runs (e.g. RWL_mod_FAR 20000 10000 ...), not fixed certificates, and mxdys sweeps them over all holdouts. Not a lead. The 83/653 hits are siblings of our CHECKPOINT_A 534.
Orbit merging inside multi-start families The families scout used span/nonzero closeness. merge.py (exact record-configuration match) and twin.py (record times). W4-4 quartet: near-twins, not merged (see W4-4). W4-3 trio: no merge in 3e6 steps (expected: different orbits of one macro map).
Claims beyond the sheet Sheet, local Discord exports and verify mentions only. gh search code for 31 strings (picks, families, reserves); every upstream PR (#1-#15, all states); sheet strikethrough and links. GitHub: only yongyi781/fiery collections.ts, a holdout list, not a claim. PRs: mira-quine #6-#13 and the rest touch none of these machines. No strikethrough or link on any pick. Live Discord is still unreadable: search #bb6 for each string before posting.
Deep-simulation notes as a negative halting signal Not used by the dynamics scout. Claims-table hints. 291 and 152 were simulated by Alistaire to 10^73975 and 10^160394 steps without halting, and 543 to 10^15.6. Someone has an accelerator for them. No HALT route there, and their fitted rules are Collatz-flagged.
Halting search for small counters Planned for W4-5 but not run. Not run (out of scope for the critic). Still the first step of W4-5.

Fell through: high on two signals, missing from picks and rejections

machine (740 line) signals verdict
299 1RB0LE_1RC1RA_1LD0RE_1LA1LD_1LD0RF_0RA---, 412 1RB0LE_1RC1RB_1LD0RE_1LA1LC_1RB0LF_0LC---, 602 1RB1RD_1LC0RE_1LD1LC_1RA0LE_1LC0RF_0RD--- Same table as ChaoticBell1Halt.v TM13 (a HALT proof by certified RLE execution, commit d3c52f5, today): TM13 started in B (mirrored), D and C. Also 338 and 577 are 1 transition from TM7, and 303, 545, 662 and 730 are 2 away. That is 9 of the 17 Chaotic Bell Class 1 machines on the 740 list. None is on the 1e14 simulation list and none is claimed. Rejected: hot, and the signal is against them. targeting.md filed this class as a tarpit on 10-09; ccz181078 changed that today with a generic engine (CB1.Core macro lemmas plus CBSim.check_spec, fuel 100000). He had these same-table siblings in front of him and shipped only TM7 and TM13, so they probably failed his budget. Porting is not mechanical: CB1.R/L/J hard-code states A/B/C and CBSim starts from c0, so a sibling start needs a modified copy of the engine. The orbits of 299/412/602 share no record configuration with TM13's in 2e6 steps (no merge), and qsim finds no rules on TM13 (n = 2/4/6), so our tools cannot predict halting. This is a priority call for Dennis (possible HALT kills, but a direct race with the maintainer); do not start it automatically.
686, 441 (siblings of our STUCK 347); 470, 575 (STUCK 191/202); 384, 651 (STUCK 659); 83, 653 (CHECKPOINT_A 534); 463, 638 (STUCK 443); 144 (STUCK 628); 332 (STUCK 633); 657 (STUCK line 11); 43 (R5's table, STUCK line 269); 162 (our STUCK #19's table, off-list) Same table as one of our parked machines; several rank 22-60 on dynamics (686 is rank 22, 470 rank 28) Not picks: they ride on our own stuck work, and our attempts on that table are what got stuck. They should go in the rejections. 83/653 vs 534: their widths are far from 534's (a different orbit phase), so they cannot ride on 534's conditional proof.
525 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB and 310 1RB0LF_1LC0RE_0LD1LC_1LA---_0RB1RA_0LE1LF Bell eats counter, dynamics rank 16 and 43, claims score 0.6, small tapes (2,058 and 3,202 cells at 1e9). 525's skeleton is 0^inf 10^a 01^b 1^c B> 0^inf, stable to 1e9. Reserve (next BEC slot after W4-2). There is no rule table (rulefit none) and no template within 3 transitions.
291 (rank 14, eqv group 13), 152 (rank 46, eqv group 21) Stable skeletons; Alistaire deep-simulated both Rejected: Collatz-flagged rules (32 of 53 for 291), and someone else holds the accelerator.
289, 96, 543, 623, 9, 374, 455, 278 Dynamics rank 21-59 only Single-signal: Collatz flags (289, 96), a skeleton that degrades by 1e9 (543), or no rules (623, 9, 374, 455, 278).
227/387/699, 242, 395, 220/610 Upstream has 2024 ccz181078 files named after 227, 242, 395, 220 and 610 These are reductions to Collatz-like maps with halting conditions (cryptid-type), and the machines are in mined classes anyway. 387 and 699 share 227's table. Not picks.

Claimed or hot, per pick

Sibling or equivalent of something already worked or proved