/reports/wave5/ranking.md · raw

Wave 5 ranking (2026-10-13)

These are the 8 picks to attack now. They come from merging the four Wave 5 scout tables in reports/wave5/ (templates, families, dynamics, claims).

Scout signals are evidence only. Only a tools/check_kill.sh PASS counts as a kill.

A completeness critic re-checked this ranking on 10-13. It kept all 8 picks, corrected the facts for W5-3 to W5-8, and set a launch order (see Critic near the end).

Universe: the 740-list machines with no machines/ directory, 688 of them. After the exclusions (mined and taken classes, BBi ties, #16's siblings 199/510, open PR #13's line 8, line 556 ≡ our #19), about 255 remain.

Checks on every pick and family member (re-run here): - each string is byte-exact at its 740 line; - none has a machines/ directory; - none is canon-equal to one of ours; - no two picks share an eqv-1590 group, and no group contains one of ours; - upstream HEAD 9cf9e88 mentions them only in Eqv_* files; - the open busycoq PRs are #3, #4 and #13 (none of these machines) plus our #15 and #16.

The lesson from Wave 4

Wave 4 had 8 picks. The ones with a live template were all killed: W4-1 (#30's table), W4-2 (1 transition from BECv5) and W4-3 (3 starts, SBCv6 TM21 shape).

The new proofs in Unknown classes all parked: W4-4, W4-6 and W4-8. So did W4-5 (a counter with no invariant) and W4-7 (hlin decider, wide digits).

So Wave 5 leans on templates on purpose. The strongest common signal is W4-2's own architecture: Bell eats counter, records (10)^a (01)^b 1^c, a binary-ruler transfer between the two fields, and a size invariant. 349, 134, 525 and 29 all show it, so four picks reuse it. This concentrates risk in one class, but the merged scores are not close: those four average 0.43-0.91, and the best non-BEC family 0.27.

Picks

label machine 740 line class why nearest template risk family (same proof)
W5-1 1RB1LD_1LC1RA_0LD0LC_0RE1RB_1RD0RF_0RB--- 349 Bell eats counter W4-2's table with F1 = 1RC (W4-2 has 1LF), mirrored, started in W4-2's F. Upstream Eqv_v3 TM518 proves it halting-equivalent to W4-2's exact table from F. W4-2's invariant I holds from F (proof.md §7.3, 999,999/999,999 states). Spans equal at 1e7/1e8/1e9. All four scouts rank it first. Unclaimed. Our kill W4-2 (1RB1LF_..._1LA1LF.v, 1,217 lines) Low to medium. The planned Eqv route is out (see Corrections). The direct route re-derives the rules that use F1, as W4-2 did from BECv5. F1 fires 751 times in 1e8 steps. none
W5-2 1RB0RF_1RC1LB_1LD1RE_1LB0LD_1RF0RC_1RA--- 409 Shift-overflow counter (mined; exception) 1 transition (A1) from SOC_2_5_v1.v TM10, a hand proof (ccz181078, 2025-07-30). A1 fires once, at step 10, then never again to 1e9 in either machine. The scout compiled TM10's module with 409's string and a new init (cfgL 3 6 1 at step 34). Every lemma passed except ROv3_0/ROv3_1, the RC3 right-overflow rules, which use A1. SOC_2_5_v1.v TM10; probe in scratchpad/w5t/p409/Probe409.v Medium-low on the maths: 409's RC3 overflow ends in an RC'-like [0;0;0;1;1] tail, so closed needs a new case, or P must exclude it. Race: the SOC batches (09-16, 09-30, 10-07) are weekly. Finish within a day. none (follow-ons with other tables: 70, 223, 323, 495, 648)
W5-3 1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC 134 Bell eats counter Records (01)^a (10)^b 1^c A>: W4-2's words. a+b is conserved per round. c rises by 2 per round while the transfer doubles (5, 16, 32, ..., 512), then resets: a binary ruler. Rulefit validates A1(a+64c+128, b+2, c+15) -> A1(a, b+64c+130, c+17) and A0(a+62n+4, b+1, 5n+6) -> A0(a, b+62n+5, 5n+8). Wave-4 reserve; dynamics rank 4. Unclaimed. W4-2's architecture (budget / round-length invariant); new proof Medium-high (critic). No template within 3 transitions. Rulefit's 2-3 validated rules explain only 16-22% of the A-hub transitions (critic's reruns, 60-90 s budgets; W4-2 itself scores 26%), and 6 more record shapes (10^a 01011^2 1^b, 10^a 110^2 1^b, ...) have no rule yet. none
W5-4 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB 525 Bell eats counter Exactly W4-2's mirrored record shape: (10)^a (01)^b 1^c B> on 260 of 400 records at 3e8, stable to 1e9. Smallest tape of the family (2,058 cells at 1e9). Unclaimed. W4-2's architecture; new proof Medium-high (critic). No rule table yet: the critic's rulefit rerun (90 s budget, time cap hit) validates 0 rules, and all 25 fitted rules failed validation, so fit the rules by hand first. The transfers follow a short cycle (c runs through 22, 25, 28, 30), so it may be a two-level counter rather than a pure binary ruler. none
W5-5 1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC--- 29 Bell eats counter Base-4 W4-2: records <A (100)^a 1 (010)^b (001)^c. b+c ≈ 680-686 is conserved, and the transfers grow ×4 per level (2, 8, 32, 128, ~512). Scout rules: A0(a+2, 24a+b+8, c) -> A0(a+3, b, 24a+c+8) and A0(4n, b+126n+2, c) -> A0(4n+1, b, c+126n+2). Dynamics rank 1. Wave 4 rejected it for the residue-indexed rule, but W4-2 itself has 3n/4n/5n-indexed rules. W4-2's architecture with 3-cell words; new proof Medium-high (critic). The scout's rules are not "closed": the critic's rulefit rerun validates the 24a rule only for a ≤ 1 and does not validate the 4n rule. At the D hub it finds 4 rules (2 of them thin) covering 42% of transitions, with 134 probed cases unexplained. The Results row says "Chaotic", and an unattributed Level-0 note says "chaotic bell eats counter". Its eqv group has 13 members, all off the list. Launch last. none
W5-6 1RB0LC_1LC0RE_1LA1LD_1LA1LB_0RF1RA_---0RE 88 Bell eats counter 88 and 280 are exact trajectory twins: identical tape at 1e9, 10^3 0^3 010001^2 011^450 <A 110^561 1^366. IndBECv1.v certifies 88's table started in 88's B (config_BEC 1000 3 B F [0] [0] [0;1]). I ran that start: at 3e8 and 1e9 it has the same tape grammar, junk (011)^a head (110)^b 1^c, and only the far-left junk differs. 280's table is certified from another start too (Eat1Digit nonhalt6). Never attempted. IndBECv1.v hlin certificate; W4-7's native hlinx driver Medium-high (critic). 7 mapped hlinx configs came back false (T 1000/3000, bsz 3/6). Rulefit has a /6 rescale, so take the Collatz-like caution. W4-7 is the direct precedent: its table is also hlin-certified from another start (IndBECv1.v nonhalt3), and 384 hlin + 178 CTL runs from its own start all failed. The critic's merge test finds no shared configuration between 88 and its certified start, or 280 and its certified start, in 3e7 steps each. Cap the hlinx grid at 1 h, then hand proof or park. 280 1RB0LC_1LC0RE_1LA1LD_1LA1LF_0RB1RA_1LC--- (different table, same orbit: one proof, two inits)
W5-7 (bold, HALT) 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE--- 700 Shift-overflow bouncer counter (mined; exception) Same table as SOBCv6.v TM3, a HALT proof (ccz181078, Jul 2025), started in TM3's B. Its eqv members are the TM2/TM4 tables from B, and TM2/TM3/TM4 all halt. I checked the tape at 1e8: 700's whole left side (209 cells) parses into TM3's counter digits (w0/w1, 3-cell words), with the same 11 far-left boundary as TM3. The right side is the same (001)^n bouncer. TM3 halts at its first counter overflow. It is on mxdys's UBRRBA_TODO (fair game), and no SOBC batch has taken it. mira-quine's PR #8 (closed 10-10, now upstream Eqv_RegularPairs.v TM101) proves 700 equivalent to another table: an equivalence, not a verdict. SOBCv6.v TM3 (step_rec, LIncs, LOv, then a finite tail) Medium-high. The halt after overflow depends on the low digits that the overflow leaves. 700's ~70-digit counter may not end in TM3's halting tail. First step (cheap): run TM3's digit model from 700's record to the first overflow. Stop if it does not halt. none on the list
W5-8 (bold, family of 3) 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF 214 Bouncer + Chaotic Edge One table with 3 listed starts; widths within 0.3% at 1e9; clean tapes (19-21 tokens), bulk (01)^16651. 214 and 418 carry the same right-edge blocks 1^34/1^216/1^396. Rulefit has several halt branches, so look at HALT first, but for at most ~20 min: all 3 are on mxdys's UBRRBA_TODO (a list for accelerated halting runs) and still listed on 10-07, and the dynamics scout's halting lens found no linear reservoir. Unclaimed. None within 4 transitions; our #8 bouncer work is the nearest experience High. 5 of our B+CE machines are stuck on the edge lemma. My 1e9 snapshot shows the right edge carrying nested fields, (10)^198 (01)^108 (011)^2 (10)^15 ..., that change from record to record. 418 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF, 636 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA

If all 8 work, they cover 11 list entries.

First step per pick

Corrections to the scouts

  1. 349's Eqv route cannot be used. Our W4-2 status.json and proof.md §8 plan TM518.eqv + flip_halts_c0 + perm_nonhalt. - Eqv_v3.v begins with From BusyCoq Require Import BBinf Individual62, and its solve_eqv runs through TMinf/Permute_inf over BBinf. - BBinf carries the unsound Admitted all_qs_spec (zero-context's PR #3). Our rule (targeting.md, landscape.md §4.4) is never to import it, and Print Assumptions would most likely show it, which fails check_kill. - So W5-1 is a direct proof, like W4-2's own step from BECv5. The Eqv lemma still tells us the change in F1 does not affect halting.
  2. 88/280: the certified start has the same three-field tape as 88 (direct simulation, 3e8 and 1e9). This is why 88 counts as a pick and not a decider lottery.
  3. 700: neither the templates scout nor the claims scout checked whether 700's tape fits TM3's counter. It does: every 3-cell word is 100 or 111, with the same leftover boundary as TM3.
  4. Eqv groups: 2026-10-07_eqv_1590.txt separates groups by blank lines (778 groups). Read that way, 29's group has 13 members, 280's and 700's 3, and 349's 2 (349 plus TM518's tm).

Notable rejections

machine (740 line) signal reason
299, 412, 602 (+ 338, 577, 730 through eqv members) Same table as ChaoticBell1Halt.v TM13/TM7 (certified HALT, 10-11) from other starts Chaotic Bell Class 1 went hot on 10-11. This is a direct race with ccz181078, who can port his own executor. Same verdict as the Wave 4 critic: a priority call for Dennis, not an automatic start.
70, 223 1 transition from SOC_2_5_v1 TM43/TM62 Mined SOC. The compile probes leave 6 open goals in the overflow rules, more rework than 409. 70 is also the sheet anomaly (its row is struck NONHALT, but it is still listed). Follow-ons if W5-2 works.
323, 495, 648 1 transition from SOC_2_3_v2/v3 (F0 fires only early) Mined SOC, not probed (the parser could not reproduce TM39's init). Follow-ons after W5-2.
about 70 more SOC / Skelet 1-like Class 1 lines 1-2 transitions from TCv3, Sk1like_TC and SOC_* proofs Mined classes. mxdys works through them in batches. One verified exception (409) is enough for now.
10 Same table as SOBCv10.v (hand proof) from D Mined SOBC. The template is 4,234 lines and tied to specific parameters.
9 Cleanest Unknown: 2 skeletons cover every record to 1e9; binary counter plus bouncer, #8-like The sheet credits nerdyjoe with "Code. Binary counting + bouncing" (2025-12-28). Ask Dennis whether that counts as a claim. If not, it is the first reserve.
147 / 493 Near-exact twins (width curves 0.07% apart) Unknown, 57 tokens, no template; an edge like B+CE. Alistaire simulated 493 to 3.35e20. Reserve after W5-8.
6 / 348 B+CE pair, clean Same class and the same edge-lemma risk as W5-8, with a smaller payoff. Reserve.
310 / 528 (+ 548) BEC with W4-2's words plus (10101)/(11010) fields The 4-field grammar of 693, where mxdys stalled (Level 1). Next BEC slot after the W4-2 family.
87 / 342 / 689, 312 / 337 BEC trios and pairs; 87's shape is like #30's hub On dyuan01's longitudinal-24 list (treated as claimed).
170 / 278 / 374 / 434 + 257 / 535 / 669 7 machines on two tables 1 transition apart Chaotic Bell Class 1 neighbourhood (hot); tapes messy beyond 170/374; 278 has others' "partial analysis".
51 / 74 / 154 Clean trio No template within 5. Alistaire deep-simulated 51 and 74, so someone has an accelerator.
239 Labelled BEC, closed rules Growth t^0.65, a fossil bouncer: W4-8's seam problem.
192, 692 Explicit parity halt boundary (halting lens) Tarpit classes (Chaotic Bell 3 and 2). A proof needs a parity invariant on fossils, which is the W4-8 problem again. 692's reservoirs have the safe parity so far.
458 / 635, 96 Closed rules Collatz-flagged parity rules: cryptid risk.
218 / 159 / 230 / 401, 716, 211 Regular epochs ×3/2 and ×4/3 epoch maps: cryptid protocol.
197 / 583 / 678, 388 1 transition from FractalBEC / BECv1 Exact trajectory twins of our CRYPTIDs 611/596/486 and of STUCK 633.
441 / 686, 470 / 575, 188, 61 / 704, 530 Same table or eqv tie as our parked machines These ride on our own stuck work (347, 191/202, W4-4, W4-8, W4-5).
45 / 52 3 transitions from #4 Chaotic Fractal Type 1 is taken; 52 is on dyuan01's list; 45 diverges from #4 at step 15.
199 / 510 Same table as FractalType4 TM5 Siblings of our #16 (same fatal gap).
556 Eqv_WordPairs TM83 makes it equivalent to our #19.
8 In mira-quine's open PR #13.
221 / 416 / 455 (critic) One table, 3 listed starts; top 40 on claims and families; 34-58 tokens Unknown class, no template within 5 (nearest ours d6). The wake is nested 8-cell words, e.g. 455's (10010101^2 01100101^2 01011001^2 01010110^2 01^4)^219. A new proof in an Unknown class, the W4-4/6/8 pattern. Alternate bold family if W5-8 parks early.
141 / 551 (critic) One table, 2 starts; top 40 on claims and families Unknown, 130-145 tokens, no template within 6.
56 / 592 (critic) Fractal in Bouncer pair, look-alikes (claims 0.458/0.415, the highest unlisted) Fractal tapes of 370-400 tokens; 592's rulefit rescales a parameter by m/k (Collatz-like). No template within 4.
318 / 483 (critic) CTLv1.v certifies the table from 3 other starts Chaotic tapes (900-1,100 tokens). The critic's merge test finds no shared configuration with any certified start in 3e7 steps, so only a decider parameter sweep from start A is left, which upstream has very likely run.
406 / 509, 198 / 248 / 582 (critic) Families on two scouts Bell-like t^0.29 with 400-token tapes; 680-token tapes. No template.
707, 43, 162, 83, 653, 144, 246, 332, 384, 450, 463, 478, 519, 564, 599, 612, 638, 651, 657 (critic) Same table (any start) as one of our STUCK or CRYPTID machines Ride on our parked work (707 on W4-7, which has the same hlin situation as W5-6).
289, 291, 152, 98, 623, 543 (critic) Dynamics top 50, Unknown Collatz-flagged rules (289, 291, 152, 98), or no stable skeleton (623: 193 skeletons at 1e9; 543 degrades by 1e9).

Critic (2026-10-13)

Verdict. The 8 picks stand. None is claimed, proved upstream, or tied to work we already did, beyond what the table says. Six statements in the ranking were wrong or overstated; they are corrected in the table above and listed below. The launch order changes.

What was re-checked today

Corrections

  1. W5-6 (88/280): the W4-7 argument was backwards. The ranking said W4-7's obstacle does not apply because hlin already handles this table. But W4-7's table is also hlin-certified from another start (IndBECv1.v nonhalt3), and 384 hlin runs and 178 CTL runs from W4-7's own start all failed. That is exactly W5-6's situation. - New check (merge test, C, 3e7 steps per run): 88 never reaches a configuration that its certified start reaches, and neither does 280. So there is no free transfer from the certificate. - Risk raised to medium-high, and the hlinx grid is capped at 1 h.
  2. W5-5 (29): the "closed" rules do not hold up. - The critic's rulefit rerun (60-90 s budget) validates the 24a rule only for a ≤ 1, and does not validate the 4n rule. - At the D hub it finds 4 rules (2 of them thin) covering 42% of the transitions, and 134 probed cases with no rule. - The Results row says "Chaotic". Risk raised to medium-high; launch it last.
  3. W5-3 (134): "closed" is not "complete". Rulefit labels its rules "closed", but its 2-3 validated rules explain only 16-22% of the transitions at the A hub (9% at the B hub), depending on the budget. 6 more record shapes have no rule yet.
  4. Calibration for 2 and 3. On our kill W4-2, the same rulefit run explains only 26% of its hub transitions. So low coverage is normal for this architecture and is not a reason to drop 134 or 29. It is a reason not to call their rule tables closed.
  5. W5-4 (525): no validated rules at all. Within a 90 s budget (the time cap was hit), rulefit fits 25 candidate rules and all fail validation. This matches the ranking's "fit first", but it puts 525 behind 134.
  6. W5-8 (214 family): HALT-first is a long shot. All 3 are on mxdys's UBRRBA_TODO, a list he posted for accelerated halting runs (q64 offered 500 cores). They were still listed on 10-07, and our halting lens found no linear reservoir. Cap the HALT check at about 20 minutes.

Signals that were under-used

Fall-throughs

These machines were in the top 40 of two or more scouts but were missing from the ranking: 455, 221, 416, 141, 551, 56, 592, 318, 406, 509 and 248. None is better than a current pick. Each now has a row in the rejections table, along with the 19 machines that share a table with our parked work.

There is no exact sibling of a kill anywhere in the universe.

Launch order

  1. W5-1, W5-2. They take the coqc slots and are closest to a kill.
  2. W5-7. The Python go/no-go takes about 30 min. Stop if the counter does not halt.
  3. W5-3, then W5-4. Python first: rules, then the invariant.
  4. W5-6. Native hlinx, capped at 1 h, then a hand proof or park.
  5. W5-8, W5-5. The riskiest picks go last.

First reserve: line 9. It needs Dennis's call on nerdyjoe's note. The sheet has a precedent: another row reads "Incomplete analysis by nerdyjoe; solution ... by mxdys", which suggests an analysis note does not reserve a machine. 9 is not clearly better than 29, though: rulefit explains 1% of its transitions.

Critic's scratch is in /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/critic5/: - merge/merge.c: the trajectory-merge test; - upchk.py: matching against upstream strings; - killsib.py: same-table checks against our machines; - near.py: picks within 2 transitions of ours; - two.py: machines high on two or more scouts; - rf_*.txt: the rulefit reruns.

Resource plan