Family sweep: untouched holdouts related to our kills

2026-10-10. Inputs: data/holdouts/2026-10-07_778.txt (778 entries), data/holdouts/2026-10-07_eqv_1590.txt (778 groups, 1,590 machines), the 9 machines/*/status.json with KILLED_NONHALT (#2, #3, #4, #11, #12, #12-twin, #24, #25, #33), their proof.md/check_proof.py, reports/forensics/remaining_778.tsv (sheet fields), data/discord/, reports/landscape.md §7 (claims), data/solved_index.tsv.

Simulation and table matching are evidence, not proof. Only a tools/check_kill.sh PASS counts.

Bottom line

• Three new same-table relatives. Each is an untouched holdout that runs a killed machine's own transition table (up to renaming states) from a different start state. On each one, simulation shows the run entering the parent's proven invariant. If that holds, the parent's rules and invariant carry over as they are, and only the init changes, as with #24, #25 and #33. 1. line 388 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---: kill #33's table renamed (no mirror), started in #33's D. Equivalently, #11's table mirrored and started in #11's C. 2. line 604 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---: kill #3's table renamed (no mirror), started in #3's B. This is the 4th holdout with that table (A = #3, B = this, C = #25, D = #24). It is not mentioned anywhere in the project yet. 3. line 17 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA: kill #4's table renamed (no mirror), started in #4's F. Not mentioned in any machine notes yet.
• Excluded as claimed: line 541 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- (#11's table from B; Level 1 tab, "Done By: hipparcos", Discord thread). It would be as cheap as 388 if the duplicate-work question is resolved.
• Relation (2), 1–2 transitions after the best renaming + mirror: no untouched holdout. The only holdouts at distance 1 are already touched: #32 and R4 (from #11/#33), 1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- (from #2) and the #12 twin pair. Nothing is at distance 2. At distance 3–4 there are 16 untouched representatives, but every one first uses a differing transition within 31 steps, and most are in another sheet class (full table below).
• Relation (3), trajectories: the only exact twin of a kill that is untouched is 388, twin of #11 (77,691 / 77,685 cells and 38,839 / 38,836 nonzeros at 1e9). 541 is also a twin but is claimed. 604 and 17 are different orbits of the same macro map, not trajectory twins: at 1e9 they have 18% and 23% more cells than their parents.
• Relation (4), same class and similar growth: two weaker multi-start families. One is a Skelet 1-like Class 2 trio, a single table with 3 starts that is 5 transitions from #11. The other is an "Unknown" quartet, a single table with 4 starts that is 6 transitions from #11 and within 7% of its trajectory. Each would need a new proof, but one proof would cover all of its starts.

Method

1. Relabelling distance. For every kill and every one of the 1,590 machines (778 representatives plus their equivalence-group members), we took the minimum, over all 720 state permutations (the start state included) with and without the L/R mirror, of the number of differing transitions (out of 12, with --- compared as a symbol). Distance 0 with a permutation that moves A means the same table with a different start, i.e. relation (1).
2. Divergence. For each pair at distance 1–4, we ran the kill's relabelled table and the holdout in lockstep from the blank tape (a small C tool), and recorded the first step at which the holdout uses a transition where the two differ. A pair that never diverges would mean the differing transitions are unused. None qualified.
3. Trajectories. We ran all 778 holdouts with the C core (tools/sim/tmsim) to 1e9 steps, taking the width at every 1e7 checkpoint and the nonzero count at 1e8 and 1e9. 778/778 ran, and none halted. A twin is defined as in reports/targeting.md (width within 0.3% + 3 at every 1e7 checkpoint, and nonzeros at 1e9 within 0.5% + 3). Look-alikes have width within 8% at every checkpoint and nonzeros at 1e9 within 5%. The growth exponent is log10(w(1e9)/w(1e8)).
4. Parent-mechanism checks for the three relation-(1) machines, using each parent's own check_proof.py functions on the new start (details per candidate below).
5. Gate. Every candidate is a byte-exact entry of the 778 list (tools/holdouts.py contains, exit 0), has no machines/<tm>/ dir, and has no completed proof in solved_index.tsv in any tier. At most it has Eqv*.v tm' mentions with proves=-. None has a sheet status, "done by", Level 1 or Unverified-tab entry, or a §7 claim. Membership in the UBRRBA (mxdys) and longitudinal (dyuan01) lists is noted but does not exclude a machine, per Dennis.

Permutation notation: perm EDBCFA means the kill's A, B, C, D, E, F become the holdout's E, D, B, C, F, A. "kill start" is the kill state that becomes the holdout's A.

Ranked candidates

The three strong candidates in detail

1. Line 388 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- (parent #33 / #11)

• Relation. It is #33's table with states renamed A→B, B→C, C→D, D→A (E, F fixed), with no mirror, started in #33's D. Seen from #11, it is #11's table mirrored, started in #11's C. This is row D of #33's proof.md §0 and the "C-start twin" of #11's proof.md §4. Its equivalence group, 1RB1RF_1RC0RA_1LD0RA_1LE0LE_1RB0LD_1RB--- and 1RB---_1RC0RF_1LD0RF_1LE0LE_1RB0LD_1RB1RA (Eqv_v2.v TM688/TM2137), is #11's table started in E and in F. So all 6 starts of this table are now accounted for: A (#11, killed), B (541, hipparcos), C (388), D (#33, killed), and E/F (merged into 388).
• Evidence.

• 11's check_proof.py check 10 passes: 687 steps reach K((1,1,9); 8, 1), class A of INV.

• Our closure run of #11's table from C: 2,753/2,753 macro steps of the real run match #11's abstract mstep model to step 2.0e7. The INV class counts are A 983, B 876, C 894, with no failure.
• It is an exact trajectory twin of #11.
• Formal route. #33's .v (669 lines), every state letter renamed by BCDAEF, with no mirror (cheaper than #11 + mirror). The new init is 687 steps to K [d1 1 9] 8 1. The abstract part is unchanged. This is the cheapest kill on the list.
• Flags. Sheet: Skelet 1-like Class 2, no status or notes. It is named in the unposted reports/discord-drafts.md Message 2, group 2. Not on the Discord lists.

2. Line 604 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA--- (parent #3; #25 and #24 are siblings)

• Relation. It is #3's table renamed A→D, B→A, C→B, D→C (E, F fixed), with no mirror, started in #3's B. From #25 it is perm BCDAEF from #25's D; from #24 it is the mirror from #24's C. With this machine, the table has four holdouts, A = #3, B = 604, C = #25 and D = #24; the E and F starts are not on the list. No project file mentions 604 yet. It is absent from solved_index.tsv and is a singleton equivalence group.
• Evidence. The script imports #25's check_proof.py and, through it, #3's (cp.astep, cp.inv_violations, J_base). It simulates 604's own table, with the canonical head state D = π(A).
• From step 1,083 to 3e8, 5,323/5,323 consecutive canonical configurations follow #3's abstract map (Dec 5,266, Ov 26, End 13, EndLast 13, DecMerge 3, DecMergeTail 2).
• The base E-start after re-pairing 6, at step 38,732, is K(2; (47,32,0),(40,33,1),(13,34,1); −). There, INV+(e) has no violations and the Rocq J_base clauses (PC E1 per pair) all hold.
• All 11 E-starts at the even re-pairings 6–26 (to step 2.78e8) pass both checks, which matches the parent's own alternating pattern (the parent's base is at step 78,710).
• Formal route. #3's .v (1,301 lines) with the states renamed by DABCEF and no mirror. The new init is one esx of 38,732 steps to the 3-pair base. J, Jstep and J_base are reused, and J_base is re-proved by computation for the new base. This is the #25 recipe (a scripted σ-swap); the init is about half the parent's 78,710 steps.
• Caveat. The base has 3 pairs, where #3's and #25's bases have 4. INV+(e) and J accept it, but it is the one structural difference to watch.

3. Line 17 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA (parent #4)

• Relation. It is #4's table renamed A→E, B→D, C→B, D→C, E→F, F→A, with no mirror, started in #4's F. #4's F1 = --- becomes this machine's A1. Its equivalence-group member 1RB0LC_1LC0RB_0LD1LA_0RA1LE_0LA1LF_1LD--- is #4's table mirrored and started in #4's D. Eqv_v2.v TM7 proves halts ⟺ halts between that member (in its 1LB mirrored form) and line 17. Starts B, C and E are not on the list.
• Evidence. We simulated #4's table from 0^inf F> 0^inf and pattern-matched every right-edge C visit against #4's P/Q families.
• S(6,14,4) = Q(7,65,1,14,4) appears at step 16,590 (from D it is the same S(6,14,4), at step 16,585). In the .v's coordinates this is CfgF 5 0 14 4.
• Inv holds: 64 ≤ 112 ≤ 192; 12 ≤ 64; 0 ≤ 96; 64 ≤ 4·14 + 2·4 = 64 (tight); 344 ≤ 576.
• From there, the first S-config of each level k = 7..14 is exactly #4's cycle map F(k, Y, Z): (7,25,29), (8,68,2), (9,104,115), (10,271,186), (11,594,−31), (12,860,888), (13,2178,1485), (14,4752,2348) at step 1.27e9. That is 8/8 matches, all in the hexagon.
• The same script on #4 itself reproduces the proof's S(6,16,0) at step 17,215 and 8/8 cycles.
• Formal route. #4's .v (502 lines) with the states renamed by EDBCFA. The new init0 is an esx of 16,590 steps to CfgF 5 0 14 4; the final cbn; lia must close the tight facet, which it should because Inv uses ≤. cycle_step is unchanged.
• Flags. Sheet class Sync bouncer counter, no notes. It is on mxdys's UBRRBA_TODO list and dyuan01's longitudinal list. Per Dennis these lists are fair game, and #4 was on both too, but someone's pipeline may absorb it.

Excluded (relation found, but gated out)

Full table A: every structural relative at distance ≤ 4 (representatives and equivalence-group members)

Columns: dist, kill, holdout representative, 778 line, matched machine (the rep itself, or an equivalence-group member), the best permutation, the kill start, the differing transitions (kill transition → holdout transition), the first step at which the holdout uses a differing transition, the sheet class, and flags. Kill-to-kill pairs are omitted (#3/#24/#25 and #11/#33 are mutual distance 0, and #12/#12-twin distance 1).

Full table B: trajectory look-alikes of a kill (width within 8% at every 1e7 checkpoint and nonzeros within 5% at 1e9, or a twin)

Kill reference values at 1e9 (cells / nonzeros / exponent): - #2: 4,902 / 4,592 / 0.344 - #3: 67,343 / 33,665 / 0.484 - #4: 23,607 / 11,358 / 0.356 - #11: 77,685 / 38,836 / 0.510 - #12: 134 / 89 / 0.063 - #24: 67,345 / 33,665 - #25: 67,347 / 33,668 - #33: 76,245 / 38,119 / 0.523

Within each relation-(1) family the trajectories split as follows: - #11's table: 388 and 541 are exact twins of #11; #33 (D start) is 7% off. - #3's table: #24 and #25 are exact twins of #3; 604 is 18% wider at 1e9. - #4's table: 17 has the same width at 1e8 (10,453 vs 10,403) and is 23% wider at 1e9.

This happens because the start sets the orbit inside the same invariant. So for start-variant searches, trajectory matching is a weaker test than table matching.

Full table C: untouched members of the kills' sheet classes (relation 4)

• Skelet 1-like Class 2 (untouched, unclaimed):
• 388 and 604 (above);
• the trio 543 / 363 / 624 (one table; −20% width vs #11; exponent 0.503);
• 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB (587; 7–8 transitions from every kill; 56,062 cells at 1e9, 24% off #3; 0.05, not ranked).
• Sync bouncer counter: 17 only. The other two members are touched.
• Counter Class 4: none left.
• Bell eats counter (#2's class, 32 untouched representatives, one of them claimed): all but one share #2's exponent (0.31–0.36); the exception is 256, at 0.65. The closest by width (within 3–4%) are 364, 92, 727, 215, 687, 500 and 611, but every one has 30–56% fewer nonzeros at 1e9 than #2. That points to different mechanisms; growth alone does not separate this class.

Reproduction

The scratch scripts are in this session's scratchpad (/tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/) and are not kept in the project: - relabel_all.py: the 1440-relabelling distance; - lockstep.c + diverge.py: first use of a differing transition; - traj_one.sh + trajall.py: the 778 runs to 1e9 with tools/sim/tmsim, about 10 minutes on 6 niced processes; - chk388.py, chk604.py, chk17.py: the parent-mechanism checks, which import the parents' check_proof.py read-only.

Each relation-(1) claim is quick to re-check by hand: - 388: machines/1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---/check_proof.py check 10. - 604 and 17: the step counts and base configurations above are exact and deterministic.