/reports/bec-sweep/ranking.md · raw

Bell eats counter sweep: ranking (2026-10-13)

This ranks the untouched Bell eats counter machines on the 740 list for an attack now. The per-machine data is in reports/bec-sweep/universe.tsv.

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

Corrected by the Critic section at the end: B-1 to B-3 run the dynamics of 693 (mxdys, "Chaotic"), so they now need Dennis's go. B-7 (707) is withdrawn because it was parked with W4-7. Only B-4 can be launched now.

In short

The class is thinner than its size suggests. Of the 21 untouched machines:

6 are excluded as claimed by others;
4 are exact trajectory twins of our own parked machines (identical tape at step 1e9);
7 share a transition table with one of our parked machines, so they inherit its open lemma;
only 4 are genuinely fresh: 528, 310, 548 and 239.

No universe machine is within 4 transitions of any of our 9 BEC kills (the nearest is 5). So no pick is a cheap sibling or a one-transition port, as W4-1, W4-2 and W5-1 were.

Recommendation: launch B-1 and B-2 now (one mechanism, two machines). B-3 follows once B-1 has a round map, after Dennis says whether its link to 693 counts as a claim. B-4 is the bold pick. B-5 to B-8 restart families that we parked under a stop rule, so each needs Dennis's go and a new idea first.

Universe and exclusions

The universe is every 740-list machine in sheet class Bell eats counter (data/sheet/2026-10-09_classifications.csv) with no directory under machines/: 21 machines.

Checks run on all 21:

claims.tsv: the class is claimed by claude. No machine line has another owner, and Astra holds no claims.
Upstream (vendor 0940bb9, and the clone's origin/BB6, now d026880 after PRs #15 and #16 merged): no proof of any of the 21. Eight appear only in Eqv_v2.v / Eqv_v3.v (equivalences, not verdicts).
Open busycoq PRs (#3, #4, #13, #17, #18): none touches them.
dyuan01's longitudinal-24 list: 87, 312, 337, 342, 689. Excluded as claimed.
Sheet: 693 is on the Level-1 tab, analysed by mxdys as "Chaotic bell eats counter" (Results: Chaotic). Excluded. No other sheet claim.

Picks

label	machine	740 line	why	nearest template	risk	family (same table, other listed starts)
B-1	`1RB0LF_1LC0RE_0LD1LC_1LA---_0RB1RA_1LC1LF`	528	Fresh, never attempted, no parked relative. Four fields, one bell. The counter is the head field `(01)^a (10)^b` (W4-2's two 2-cell words, a+b about 20-22 at 1e9). The bell is two 5-cell fields c, d that trade each round (c up 1-5, d down), with c+d about 607-665 at 1e9, growing by 1-2 per round. The 5-cell words switch encoding every round, `10101/11010` <-> `10110/01011`, like W4-2's two encodings. When the head counter fills, a reset moves a block of units from c back to d. Bell-like growth t^0.326; 73 record skeletons at 1e9. No halt branch in rulefit.	W4-2's architecture (size invariant tying the counter to the round length) and W5-3's conserved-sum transfer; no table within 4 transitions (nearest BEC kill #2 at d=7, nearest upstream proof `IndBECv1.v` at d=5)	Medium-high. Rulefit validates only 1 rule (9% of hub transitions; W4-2 itself scores 26%). The same 4-field grammar is in 693, which mxdys labelled chaotic. The reset amounts vary (95, 11, 23, 11 and 47 units in the last five resets before 1e9), so the reset rule needs care.	none (310 is a 1-transition neighbour, B-2)
B-2	`1RB0LF_1LC0RE_0LD1LC_1LA---_0RB1RA_0LE1LF`	310	528 with F0 = 0LE instead of 1LC. The two machines carry the same field values at their left-edge F visits (e.g. `(01)^14 (10)^2 1 (10)^4 (10101)^120 (11010)^71`), with 310 a few million steps behind, so one invariant should serve both, as #12's did for #12b. Checked to 1e9: all 641 left-edge F visits of 310 carry exactly the field values of 528's visits, index for index, and every record tape of 310 after step 1,008 is also a record tape of 528 (528 reaches it first, at step 858).	B-1's proof, plus 310's own left-edge rule	B-1's risk, plus a small one for the edge rule	none
B-3	`1RB0LF_1LC0RD_1LA1LC_---0RE_0RB1RA_1LC1LF`	548	The same 4-field mechanism in other words: a 3-cell head counter `(011)^a (101)^b` and two 4-cell fields (`1011`/`0111`, c+d about 214-221 at 3e7) that trade each round. 4 transitions from 528 (B1, C0, D0, D1).	B-1 once it has a round map	High. Rulefit validates no rule (time cap). Record twin of 693: a quarter of 693's record tapes (365 of the last 1,462) also occur in 548's run, all the way to 1e9, with 548 slightly ahead. So a proof of 548 is close to a proof of 693, which mxdys analysed as "Chaotic bell eats counter" (sheet Level-1). Ask Dennis whether that counts as claimed before starting.	none
B-4 (bold)	`1RB0RF_1RC0LD_1RD0RA_1LE0LC_1LB0LE_0RC---`	239	Fresh. Rulefit's only closed table in the class: a transfer `E1(2n, 632-n) -> E0(2n+1, 632-n) -> E1(2n+2, 631-n)` between two 6-cell word fields, fed by a 3-cell reservoir `(011)^n` on the left. Simulated to 2e10: no halt. The span doubles in spurts (7.8k cells at 1e8, 17k at 4e8, 35k at 1e9, flat at 37-38k until about 1.7e10, then 76k by 2e10). Between spurts the reservoir drains into the 6-cell fields and refills; it fell to 66 and to 7 words without halting.	none within 4 (nearest: our W4-3 family and `SOMDC_Class1.v`, both d=4)	High. Wave 5 read it as a fossil bouncer (W4-8's seam problem). Bold because a halt or a clean second regime would both be quick to see.	none
B-5	`1RB0RE_1LC1RD_1LD0LC_1RA0RF_1RD---_0RD0LA`	470	Same table as our parked #29 (line 191) and R3 (line 202). #29 is one lemma short: its generic size lemma is proved, and only the leading-spacer recovery is open (true on all 265,642 test words). Records use #30's grammar `110^a 0 011^b 1 110^c 1^d ...` with a = 2^k - 1. Not a twin: no late record tape of 470 or 575 occurs in 191's or 202's run (record-tape hashes to 1e9), so these are new orbits of the same table.	#29's proof.md and rules (`machines/1RB0RA_1LC0LF_1LE0LD_1LB---_1RA1LB_0LB0RC/`)	Very high. #29 was parked with "no further stages" (2026-10-11). R3 is stuck on a different lemma (Big-Y). Needs Dennis's go and a new idea for the recovery lemma.	575 `1RB---_1RC0RF_1RD0RA_1LE1RB_1LB0LE_0RB0LC` (plus ours: 191, 202)
B-6	`1RB---_1RC0RF_1RD0RA_1LE1RB_1LB0LE_0RA0LC`	651	Same table as our parked R2 (line 659), 1 transition (F0) from B-5's table. R2 reduces non-halting to one inequality (R1: T_k + 1 <= I_k) that holds at all 808,539 epochs to N = 1e7 but needs a crossing lemma. Not a twin of 659 or of each other (record-tape hashes to 1e9).	R2's notes; the joint R2/R3 crossing-lemma stage	Very high. Parked waiting for that joint stage.	384 `1RB0RF_1RC0RE_1LD1RA_1LA0LD_1RA---_0RE0LB` (plus ours: 659)
B-7	`1RB0LA_1LC1RF_---1LD_1RE0LA_1RA0RB_1RE0RF`	707	W4-7's table (line 317) from W4-7's start C. W4-7's abstract simulator is exact on 707 for 226,216/226,216 marker turns to 1e9, so 707 is already modelled. The table is certified from a third start by `IndBECv1.v` (hlin). Not a twin: no record tape shared with 317 or with the certified start to 1e9 (Wave 5's critic checked 3e7), so the certificate does not transfer.	W4-7's absim2 and notes; `IndBECv1.v` nonhalt3	Very high. W4-7 parked: halting tapes are word-level grammatical, so the proof needs a quantitative invariant. Not a cryptid.	none on the list besides ours (317)
B-8	`1RB0RE_1LC1RD_1LD0LD_0RE0LC_1RA1RF_0RA---`	441	W4-2's field pair `(10)^a (01)^b` (a+b = bell M, about 662 at 3e7) driven by a base-3 counter on domain walls. Same table as our parked line 347, whose rules (J-rule, Gap-Inc, J-crossing, walk) are validated. Not a twin: no record tape shared with 347, or between 441 and 686, to 1e9.	347's rules and fast phase map	Very high. 347 was parked as a cryptid-margin suspect: its margin depends on the exact bell (bell 102,051 instead of 102,052 changes the next ratio from 0 to 0.979).	686 `1RB0RB_0LC0RA_1LE1LD_0LE---_1LF0LC_1RA1LB` (mirrored; plus ours: 347)

If all 8 work, they cover 11 universe machines (528, 310, 548, 239, 470, 575, 651, 384, 707, 441, 686) and 5 of our parked machines (191, 202, 659, 317, 347).

First step per pick

B-1 (528):
Write the round map by hand from the left-edge F records: fields a, b, c, d and the encoding flag.
Pin the ordinary round, the encoding switch and the reset.
Look for a W4-2-style size invariant and test it with a check_proof.py before any Rocq.
Stop rule: if after the first hour the round or reset rules split on residues that look pseudo-random, apply the cryptid protocol.
B-2 (310): after B-1 has its rules, derive 310's left-edge rule (F0 = 0LE goes through E0 = 0RB) and check that it lands in the same field tape. Reuse B-1's invariant.
B-3 (548): ask Dennis about the 693 link first. Then map its words onto B-1's (3-cell head digits, 4-cell fields) and test B-1's invariant shape.
B-4 (239): pin one plateau first: the drain-and-refill round between the left 3-cell reservoir and the two 6-cell fields, and the spurt that ends it (around 1.7e10). If a round map with a size law exists, it is a counter proof; if the spurts depend on residues that look pseudo-random, park. Cap: 1 h.
B-5 to B-8: do not start without Dennis's go. Each restarts a family parked under a stop rule. The new starts are separate orbits (no shared record tape with the parked machine to 1e9), so they add test cases for the open lemma but do not remove it.

Rejected

machine (740 line)	signal	reason
87, 342, 689 (one table)	`110^a 0 011^b ...` like #30's grammar; rulefit finds halt branches (probes)	dyuan01's longitudinal-24 list (claimed)
312, 337 (one table)	W4-2's `(10)^a (01)^b`; 1 transition from a `BECv1_6x2_solved.v` machine (312 from A, D1)	dyuan01's longitudinal-24 list (claimed)
693	4-field grammar of B-1	Sheet Level-1: mxdys, "Chaotic bell eats counter"
197, 583 (one table)	1 transition from `BECv1_6x2_solved.v` (583 from A) and `FractalBEC.v`	Exact trajectory twins: 197 has the identical tape at 1e9 as our CRYPTID #10 (line 611), 583 as our CRYPTID #28 (line 596). A proof would settle a cryptid candidate.
678	1 transition from `BECv1_6x2_solved.v` and `FractalBEC.v`	Exact trajectory twin of our CRYPTID line 486 (identical tape at 1e9).
280	Same table as an `IndBECv1.v` certificate from start F	Exact trajectory twin of W5-6 (line 88, parked 10-13): identical tape at 1e9. Rulefit flags Collatz-like rules (cases on c mod 6, factor 3/2). No record tape shared with its certified start to 1e9 (88's certified start neither).

Method

Simulation: C engine from the blank tape to 1e7, 1e8 and 1e9 (span, nonzeros, growth exponent). No machine halts by 1e9.
Records: tools/compress.py, the last 300 records before 1e8 and 1e9 (dominant skeleton, number of fields and bell blocks).
Distances: transitions changed, minimised over all state renamings (any start) and the mirror, against our 9 BEC kills (#2, #30, #7, W4-1, W4-2, W5-1, W5-3, W5-4, W5-5), all our other machines, and 462 upstream BEC/Bell/SOMDC proofs (data/solved_index.tsv plus BellEatsCounter_1RB0RF.v and ChaoticBell1Halt.v from origin/BB6).
Families: same table up to renaming and mirror, over the whole 740 list.
rulefit: tools/rulefit.py fit --budget 75 --top 2.
Twins: the 1e9 tapes compared exactly, and every record tape to 1e9 hashed (with its mirror) to look for merges at different step counts.
Halting: no machine halts by 1e9, and 239 runs to 2e10 without halting (its reservoir emptied twice on the way). Rulefit found no halt branch on any pick. The Wave 5 jump lens found no linear reservoir except 239's.

Critic

Completeness check of this ranking, 2026-10-13. Scripts and dumps: /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/critic/.

Two findings change the picture:

B-1, B-2 and B-3 are not fresh. All three run the bell trajectory of 693, the machine mxdys analysed as "Chaotic bell eats counter" and that this sweep excluded for that reason.
B-7 (707) is already parked. Dennis parked it together with W4-7 on 2026-10-12.

So the only fresh orbit left in the universe is 239 (B-4), which Waves 4 and 5 both rejected. The corrected picks are below.

Claims and upstream: re-checked, no change

claims.tsv: no line has another owner. Astra holds no claims, and coord/mailbox/to-claude/ is empty.
Upstream: origin/BB6 is d026880 (2026-10-13 12:26 UTC, our #15 and #16). A git grep of all 21 strings finds only Eqv_v2.v / Eqv_v3.v, where the 740 string is always tm', the representative. No proof.
Open PRs: #3, #4, #13 (row9, 1RB0LA_0RC1LE_...), #17 and #18 (ours). None touches the 21.
Discord lists: all 5 dyuan01 exclusions confirmed. None of the 21 is on mxdys's UBRRBA list.
Sheet: 693 is still the only universe machine with an analysis row.

Finding 1: 528, 310 and 548 carry 693's bell values

The sweep's twin test hashed whole record tapes. That misses two kinds of twin:

the same field values written in other words (528 uses 5-cell words, 693 uses 4-cell words);
the same active part next to different fossil debris at the far end.

So I compared field values instead. At every left-edge record I read the two bell fields (c, d), meaning the runs of at least 40 words, and looked each pair up in 693's run to 1e9.

machine	late-half left visits	(c, d) pairs also in 693's run	step ratio to 693 (last 50)
548 (B-3)	232	232	0.998
528 (B-1)	206	196	1.248
310 (B-2)	186	177	1.497

The step ratio is constant, so each machine is a time-rescaled copy of the same abstract dynamics. Taking all records instead of left visits gives the same answer: 97% of 528's late records carry a (c, d) pair from 693's run. For example:

528 reaches (c, d) = (307, 359) at step 995,707,720
693 reaches (c, d) = (307, 359) at step 797,816,274

The reset sequences match too. A reset is a left visit at which c falls. To 1e9, 528 has 71 resets and 310 has 65. Each sequence equals the start of 693's sequence, except one reset early on (49 units instead of 50, near c + d = 321). 548's 80 resets equal 693's exactly.

What this means:

By the sweep's own rule (693 is excluded because mxdys analysed it on the sheet), B-1 to B-3 inherit 693's status. Only Dennis can say whether a 2024 sheet analysis ("Results: Chaotic", last Discord link 2024-11-03) counts as a claim.
The risk is not "medium-high". These machines run exactly the dynamics that mxdys already judged chaotic.
A proof would cover four machines (528, 310, 548 and 693), with one abstract argument and separate low-level rules for each encoding.

The structure is not obviously chaotic. 693 has 80 resets to 1e9:

69 follow a binary ruler: the cycle 1, 10, 4, X repeats, with X = 24·2^v − 2 (22, 46, 94, 190) and v following the ruler sequence 0, 1, 0, 2, 0, 1, 0, 3.
11 are irregular, in four bursts at c + d ≈ 91-153, 220-228, 321 and 475-537 (the last one moves 3, 59, 256, 431 and 8 units). The ruler restarts after each burst.

So this looks like a bell eating a binary counter, with the bursts as the "eat" events. The bursts are probably what mxdys called chaotic. If Dennis says go, the first hour should go to the bursts on 693's own run (the fastest encoding), under the cryptid stop rule.

Finding 2: B-7 (707) was parked by Dennis

W4-7's status.json says the park "covers W4-7 (line 317) and sibling 707", and every W4-7 decision question named both machines.
The brief for this sweep also lists "W4-7 + 707" among the parked machines.
Moved to Rejected. Restarting it needs a new idea and Dennis's go, like any parked machine.

Two side checks on 707. Comparing big-field values, it is still a separate orbit from 317 (9 of 1,458 late records shared). Wave 5 also called it a "width look-alike" of line 36 (Category 1, probviously halting), but that link does not hold up: no field values are shared.

Finding 3: B-4 (239) is a re-pick, and its "closed table" is a fossil rule

Wave 4 and Wave 5 both rejected 239: the growth exponent is 0.65, so it is not a bell, and it is a fossil bouncer with W4-8's seam problem.
Rulefit's "closed" table is the same rule Wave 4 already called a fossil rule. It has two rules with the constant 632 built in (E1(2n, 632-n) -> E0(2n+1, 632-n)), which describes one finite pass, not an unbounded law.
The only new evidence is the run to 2e10.
239 is not a twin of any machine checked. That covers the other 20 universe machines (693 included), line 36, and 24 of our 64 machines: every parked or cryptid BEC relative, W4-2, the W4-3 family and W4-8. The other 40 belong to other classes, and none is closer in table distance than W4-3 (d = 4). The runs went to 1e9, or to 3e8 for W4-2, W4-3 and W4-8.

It stays as the bold pick because it is the only fresh orbit that needs no question to Dennis. The 1-hour cap stays.

Finding 4: B-5, B-6 and B-8 hold

These machines share a table with our parked machines. A fossil-robust twin check (big-field values, with the mirror) confirms that they are separate orbits:

pick	compared with	late records shared
470, 575	191 (#29), 202 (R3)	about 1% or less
651, 384	659 (R2)	0
441, 686	347	0

The upstream proofs one transition away (tm108 in BECv1_6x2_solved.v, the IndBECv1.v certificate) were already used in #29's and R2's notes, so no template was missed.

Finding 5: rulefit and bell counts in the risk notes

528's one validated rule has a fitted coefficient of 112 per step of n (C1(6n+8, ...) -> C2(6n+11, b+d+3m-112n-12, ...)). That is a fit to the observed window, not a law, so rulefit gives B-1 nothing usable.
The W4-2 comparison: reports/rulefit-sweep.tsv records W4-2 as closed, with 4 rules and 32% coverage, not 26%.
310 and 548 got no rule because of the time cap (no exact affine fit ...; time cap). They were not refuted.
"One bell" for 528 is a reading (c + d as the bell), not a measurement: universe.tsv gives bell_blocks = 0, because the 5-cell words contain two 0s. The multi-bell picks are 470 (6 bell blocks), 651 (4) and 441 (1).

What fell through

312 and 337 are the strongest machines that fell through. They share one table, which is 1 transition (D1) from a BECv1_6x2_solved.v machine and has W4-2's field pair. They were excluded only by the dyuan01 rule. 312 uses the differing transition from step 24 onward, so the certificate does not carry over as it stands.

The repo holds two readings of dyuan01's list:

reports/targeting.md and the Wave 4/5 scouts treat it as claimed.
reports/family-sweep.md (Gate) records Dennis as saying that list membership "does not exclude a machine". reports/discord-drafts.md calls the list "a technique filter, not a claim". #4 was on the list, and we killed it.

If Dennis confirms the second reading, 312/337 should be ranked above B-4.

342 and 689 (also on dyuan01's list) overlap our cryptids.

About 70% of 342's late records match 611's mirrored (our CRYPTID #10, via 197).
689 matches 596 the same way (our CRYPTID #28, via 583).

If dyuan01 solves 342 or 689 by longitudinal analysis, his method probably applies to #10 and #28 too.

The cryptid and W5-6 twins are confirmed by the fossil-robust check: 197 = 611, 583 = 596, 678 = 486 and 280 = 88, each 100% of late records.

Corrected order

Launch now: B-4 (239) only, with a 1-hour cap.
Ask Dennis (one question): "B-1 to B-3 (528, 310, 548) run 693's dynamics (mxdys, Chaotic). Treat them as claimed, or spend 1 hour on the bursts of the binary-ruler structure?"
Ask Dennis (one question): "Is dyuan01's longitudinal list fair game (family-sweep ruling)? If yes, 312/337 go first."
Only with Dennis's go and a new idea: B-5 (470), B-6 (651) and B-8 (441). B-7 is withdrawn.