Halting hunt: ranking (2026-10-13)

None of the four scouts (deep, margins, parked, hints) saw an in-scope machine halt. So no pick has a halt to replay; nothing here is a kill. Only tools/check_kill.sh --halt PASS counts.

The ranking follows the brief:

1. a halt seen in simulation (none this round);
2. a shrinking margin with a model route;
3. machines whose exact models can run much further.

Picks are deduplicated by table family. Table identity was checked here by relabeling and mirroring states.

Scout tables: scout-deep.tsv, scout-margins.tsv, scout-parked.tsv, scout-hints.tsv (same folder).

Picks

All four are outside Astra's claims: lines 443/533/615 and the class 'Bouncer + Chaotic Edge'. None is in an open busycoq PR (#3, #4, #13, #17, #18 checked today) or in an excluded mined class.

Claims still needed before anyone creates machines/<tm>/: 686, 244, 216, 701, 362, 433 and 43. Only 269 is already ours.

H-1: line 686 (347's table, Bell eats counter)

Signal.

• On 686's own orbit the margin reached k_align/(M-1) = 0.9755 at phase 1572 (M = 13,204, k_align = 12,879).
• 347's own orbit never went above 0.467 (to phase 16,800), and 441's stayed at or below 0.42.
• The fast map has run 686 to phase 15,304 (M = 153,097, about 2e14 steps) without a halt.
• The only other phase above 0.5 is phase 725 (0.73).
• In this table halting comes only from margin breaks. From 347's notes: 3 halts in 380 phases with M-1 < k_align, and 7 in 3,293 with M forced below k_align.

Model route.

1. Resume reports/halting-hunt/margins/scripts/t347fam.py, which drives the fast map in machines/1RB1RF_1RC0RA_1LD1RE_1LE0LE_0RA0LD_0RB---/scripts/deepen3_fast.py, from phase 15,304 on 686's start. reports/halting-hunt/parked/l347_resume.py shows how to resume from a full-counter dump.
2. Log every phase with a ratio above 0.9.
3. Whenever the ratio reaches 1 or more, save that phase start and run that one phase by direct simulation (tools/sim C core: about 2M² steps, roughly 1 to 3 minutes at M ≈ 1e5).
4. Cost: about 0.3 s per phase at M ≈ 1.6e5 (347's extension). The cost per phase grows with M, so 5e4 phases take about 6 h and 1e5 phases about a day.
5. Cheaper extension: derive a J-rule-level phase map from 347's rule table (J-rule, aligned walk, k_align as a sum of carries over chain heads). It runs in O(digits) per phase instead of O(M).

Certification if it halts.

• First choice: RWLAcc62_BigUint solve_halt' with raised budgets (the RWLAccHaltv6.v route). The bell (10)^M and the counter blocks are run-length friendly.
• Fallback: a W5-5-style chunk replay of the phase model (machines/1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC---/*.v).

Risks.

• 347's tests show that mild breaks do not halt: 0 of 1,100 with M in [3k/4, k]. 6 of the 7 forced halts had M < k_align/3, so a halt needs a severe break.
• The 0.9755 spike may be a one-off: only 2 of 15,000 phases went above 0.5.
• 686 is not ours. It falls under our 'Bell eats counter' class claim, but it still needs its own claims line.

H-2: line 244, with 216 and 701 (Counter Class 3, CounterClass3v1 halter tables)

Signal.

• 244 is 1 transition from both CounterClass3v1 halting tables (the TM4 table, and the TM5/TM6 table, which are one table from two starts). 216 and 701 are 1 transition from the TM4 table. Checked here.
• Per the hints scout, the differing transition fires only during startup: 4 to 6 times, all before step 787,288. After that each machine runs a halter's table from its own configuration.
• The upstream accelerator (astep/skip_lr, P0_n) checks out empirically on our tables.
• The Python port reproduces TM4's own halt at 1.016e7 msteps.
• Ours run to 5.9e8 to 6.9e8 msteps without halting.
• Halting needs a consumption wave to leave the last tail block at 1. TM4 halted with tail [..,118,16,1]. Our tails cycle through [..,23,12], [..,74,11] (244) and [..,40,14,5] (216/701).

Model route.

1. Reuse reports/halting-hunt/hints/cc3acc.py and cc3trace.py.
2. Derive one consumption wave as one macro step: the tail-rebuild map.
3. Validate it wave by wave against cc3acc.py for every wave up to 6.9e8 msteps.
4. Run all three machines in one driver and log the tail at every wave.
5. Keep a guard that the differing transition never fires again after startup. If it does, the model is no longer our machine.

Certification if it halts.

• Copy the CounterClass3v1 module (P0_n, astep_spec, msteps_halt) with our TM string, a startup init and a larger msteps budget.
• This works while the halt is within roughly 1e9 msteps of vm_compute. Beyond that, the wave step needs its own Rocq lemma.

Risks.

• Already 70x past TM4's halting point, and the tails are not trending toward 1.
• reports/targeting.md marks Counter Class 3 as taken. Upstream's CounterClass3v2.v (10-07, "M1") is a macro-inductive nonhalting proof. Its machine is 7 transitions from ours and is not on the 740 list, but someone may be preparing nonhalting proofs for these three.
• Upstream had this accelerator (with an msteps budget of 10^10) and did not certify these three. Either they were never tried or they did not halt within that budget.
• These three are kept despite the "taken" note for three reasons: the brief's exclusion list does not name Counter Class 3, the upstream work there is on the nonhalting side, and the signal is exceptional.

H-3: line 269, with 43 (R5, SO structural counter, ours STUCK)

Signal.

• The first counter overflow, at 4.391e15, did not halt. It reset the machine to an almost blank new epoch.
• Halting is decided at overflows. The halting path there is 0 <A 101, which halts in 4 steps (machines/1RB1LA_1RC1RE_1RD0RD_1LA1RC_1RF0LE_1RA---/work/r5_followup.md).
• 43 is the same table from D, mirrored (checked here).

Model route.

1. The seeded qsim (reports/halting-hunt/parked/r5/r5q.py, from work/r5_post_ckpt.bin) matches direct simulation on the full 1.0066e8-cell tape.
2. Its 4 h run (r5q_long.jsonl) is at 4.615e15 steps (loop 62M) with 0 prover rules, so it only does chain moves and cannot reach the next overflow.
3. Derive an epoch model: the counter's per-cycle consumption, the reservoir size and the overflow trigger. Fit it on epoch 1 (blank to 4.391e15) and on the start of epoch 2.
4. Validate it against the r5q dumps and scripts/r5run (direct C).
5. Fast-forward to the next overflow and apply the overflow rule, then repeat. Run 43 on the same model.

Certification if it halts. No template reaches that depth. It would need an epoch-level certified replay (in the style of C2-552's Sk1Auto certificate runner) or solve_halt', if run-length acceleration happens to suffice.

Risks.

• The next overflow is probably exponentially later than the first.
• If the epochs are self-similar, R5 is probably nonhalting.
• r5_followup.md lists the epoch-map stage as Dennis's call. Today's hunt approval covers exact models, but this should be stated when it is launched.

H-4: line 362, with 433 (Chaotic Bell Class 2)

Signal.

• The k=4 qsim run reached 10^145.8 steps in 180 s.
• It found 1,885 Collatz rules, each used once (one fresh epoch per rule). The log-steps gain per time doubling held at about 39, so the run is keeping up.
• 433 is the same table from C (checked here). Its run reached 10^135.7.
• RWLAccHaltv6.v certifies a halt of this table from 362's start B, so the halting branch is reachable from these dynamics.

Model route.

1. Run tools/qsim.py (.venv/bin/python -B, k=4, backsymbol + prover + recursive) as in the deep scout's worker.py: 1 to 2 h per start, with progress lines, nice -n 10 and ulimit -v 6000000.
2. Add a k=2 run as a cross-check.
3. On a HALT, re-derive the halt with an independent run-length simulator before any proof work.

Certification if it halts. RWLAcc62_BigUint solve_halt', the generic certified run-length executor already used on this exact table.

Risks.

• A lottery with no trend to watch.
• Upstream's RWLAcc sweep has probably already run these starts to some budget.
• qsim's prover rules reach further than run-length shifts. A halt at about 10^300 steps may therefore be out of solve_halt''s reach, and there is no template for replaying qsim's rules in Rocq.
• qsim can blow its memory limit (518's k=2 run died at the cap).

Notable rejections

Running processes (when the next stage starts)

Both of our heavy slots are taken:

• R5 seeded qsim (r5slot.sh, 4 h cap from 17:36). This is H-3's validation baseline.
• Chain B. The 239 qsim run until about 19:01, then R2 to 3e10 (up to 3 h), then R3 to 1e10 (up to 2 h).

The W4-6 hybx (pid 509176) is paused with SIGSTOP and resumes when R5's run ends.

Recommendation: end chain B after the 239 run, since the R2/R3 extensions were rejected as picks above. That frees a slot for H-1 or H-2. Keep hybx paused or end it.

Critic (2026-10-13, 19:15)

The critic re-checked every pick for claims, ownership, cryptid status and settlement, and re-read the four scout tables for signals that fell through. Nothing here is a kill.

Verdict. All four picks stay, but the order changes and each one gets corrections:

• H-1 stays 686, with a corrected signal: the near-miss was an early transient.
• 362 moves up to H-2. The frame labels in its write-up were wrong.
• The Counter Class 3 family moves down to H-3. Upstream works this class for halting, 216 is on the sheet's Level 1 tab, and the cheap certificate's reach is nearly used up.
• R5 moves down to H-4. Both of its starts are on mxdys's UBRRBA to-do list, and its epoch-map stage was left for Dennis to decide.

No strong signal fell through.

Checks run (table level: any start state, mirror and renaming)

Corrections per pick

H-1, line 686: keep, with the signal restated.

• Both phases above 0.5 are early: phase 725 (0.73) and phase 1572 (0.9755).
• Over the 10,300 phases from 5,000 to 15,304, the maximum is 0.424. That is the level of 347's own orbit (0.467) and 441's (0.42).
• Tail counts over 15,000 phases:

ratio > 0.2: 102 > 0.3: 24 > 0.4: 5 > 0.5: 2

• An exponential fit to that tail gives a mild break (ratio above 1) about once per 10^6 to 10^7 phases. The 0.9755 outlier itself sits above that fit, so the true tail may be heavier. A halt needs a severe break.
• It is still H-1 for two reasons: it has the only validated exact model whose halting mechanism (a margin break) is known, and resuming costs one existing driver and no new code. Expect a low yield per day of compute.

H-2 (was H-4), line 362 with 433: move up, and fix the start labels.

• In 362's own labels, the upstream halter (RWLAccHaltv6.v tm128, halting at (F,1)) is this table started from F, not B. (B is 362's start in the halter's labels.)
• 433 is this table started from 362's E. (C is 362's start in 433's labels.) Eqv_v2.v's partner of 433 starts from 362's D.
• Only one start of this table halts upstream. The deep scout's "433 @D;@F" counts the same halter twice.
• It moves up because it is the cheapest pick: existing qsim, 1 to 2 h per start, no new model. It is also the only pick whose certificate route (solve_halt') has already been used on this exact table.
• Optional: run 428 (Chaotic Bell Class 2, 10^115.8 at k=2 in 180 s) in the same slot.

H-3 (was H-2), line 244 with 216 and 701: move down.

• Counter Class 3 is a class worked by others for halting. CounterClass3v1.v (mxdys, 08-15) holds three halting certificates built with exactly this accelerator, and reports/targeting.md §2.2 lists the class as taken. The brief's "exceptional signal" bar applies, and the class's own author had these machines and this tool.
• 216 is on the Level 1 tab (nickdrozd).
• The cheap certificate (copy CounterClass3v1 with a bigger msteps budget) reaches about 1e9 msteps. Our runs already sit at 5.9e8 to 6.9e8. So nearly any halt found from here on needs a new Rocq lemma for the wave step.
• Run the wave map only as a short first stage, with an exit rule: if the last tail block (11 to 12 for 244, 5 for 216/701) is invariant under the wave map, stop and write it up. That is nonhalting evidence, and nonhalting is the side upstream is working on (CounterClass3v2.v).

H-4 (was H-3), line 269 with 43 (R5): move down.

• mxdys listed both starts for UBRRBA halting runs in August.
• Upstream proves the table nonhalting from three other starts (RWL_mod_v3.v).
• The epoch-map stage was the 10-10 option Dennis did not pick (he picked watch). work/r5_followup.md line 100 still lists it "for Dennis to decide". Launching it under the 10-13 hunt approval is defensible because it is simulation of our own STUCK machine, but tell Dennis in one line when it starts.
• The seeded qsim run continues to its 4 h cap (about 21:36). At 19:14 it was at 4.629e15 steps, still with 0 prover rules.

Fell through the record (none displaces a pick)

Processes (19:14)

• Slot 1: r5q (H-4's baseline) runs to about 21:36. Then r5slot.sh resumes the W4-6 hybx.
• Slot 2: chain B has moved on. The 239 qsim ended at 18:58 (1.08e14 steps, 12 rules, 0 Collatz rules, no halt), and R2 to 3e10 has been running since 18:58 (cap 3 h), with R3 next (cap 2 h). The ranking's advice to end chain B after the 239 run is overtaken. It stays as is.
• Orphan, a third heavy process on our side (the limit is 2): a tmsim on line 469 (W4-5) with --max-steps inf, started at about 18:07 by the margins scout (cwd scratchpad/mh). Its parent is gone, and nothing holds the other end of its stdin/stdout/stderr pipes. Its output cannot be read, and a halt would kill it with SIGPIPE before anything is recorded. Not stopped by the critic. It is the orchestrator's call: stop it, or rerun it with a log file.
• Load is 3.0 and MemAvailable is 21 GB, so the per-agent slot rule is the limit, not the machine. No pick can start until a slot frees.