W5-5 · 1RB0RE_1RC0RA_0LD0RB_1LA0LE_1LC1LF_0LC--- (740 line 29)

Observe stage, 2026-10-13. Sheet class: Bell eats counter (results row 1007: "Chaotic"; level-0 note: "chaotic bell eats counter"). No claim, no Discord thread.

Checks

• Byte-exact on data/holdouts/BB6_holdouts_740.txt, line 29.
• No claim: results.csv row 1007 has only the class and "Chaotic", level-0.csv row 33 only the note, classifications.csv lists it under Bell eats counter. Nothing in data/discord/*.txt.
• holdouts.py solved: no completed proof. The string is tm' of Eqv_v2 TM291 (line 3030; also lines 4040 and 19250), and its mirror appears in Eqv_v3 (lines 10629, 11475). So a proof of this machine also covers those equivalence partners.
• Upstream busycoq 9cf9e88: not there.
• Siblings by canon (all 6 starts, renaming + mirror) on the 740 list: none.

Configuration family

Round start (the head has just turned right at the counter boundary):

K(w, b, c) = 0^inf w 0 E> 101 (001)^b 0001 (001)^c 0^inf

• w is the counter: 3-cell digits, most significant first. A clean digit is x0y with value e = 2x - y: 001 = -1, 000 = 0, 101 = 1, 100 = 2. Blank = 0, so leading zeros are free.
• Counter value C(w) = sum e_i 4^i. Every integer has exactly one such representation (base 4, digits -1..2).
• Read as cells from the boundary leftwards, the bits have weights -1, (0), +2, -4, (0), +8, ...: a negabinary number with every third cell kept at 0.
• Right of the boundary is the bell: 101 (the 1-gap), b blocks 001, the 3-gap defect 0001, then c blocks 001. L = b + c + 1 is the bell length in blocks.
• Real run: 243,388 round starts to 1e9 steps (scripts/eats.c, work/rounds_1e9.txt). The right side has this exact form at every one of them (c = 1 once, early). The counter uses only the codes 001/000/101/100 plus the dirty 010/011.

Rules

• ROUND (b >= 3, clean w): K(w,b,c) -> K(w+1, b-1, c+1) in 12b + 22 + 14t (+4) steps. Here t is the number of trailing 100 digits, and the +4 applies when the digit that absorbs the carry is 000 or blank.
• The head zigzags right (9 steps per block) carrying a defect to the 3-gap, which moves one block left. Then a straight left sweep comes back and adds 1 to the counter.
• c plays no part.
• Validated 300/300 random instances (k <= 6 digits, b 3..40, c 0..40; scripts/validate_round.py seed 11, work/validate_round_seed11.json). The step formula fitted 40/40.
• ROUND, dirty w: the shape is the same (b-1, c+1), but the counter map is not additive.
• Example: 010 -> 100 001; 001 010 -> 101 001; 100 010 -> 100 001 001.
• Exhaustive over every 1-3 digit word on the 6 codes with a dirty digit, 40-70 rounds each (scripts/inc_closure.py): 172/172, no halt, no other code ever appears, and every word is clean again after the carry passes through.
• EAT (b = 2): the next round reaches the counter itself.
• 1-7 sub-rounds follow (most: 1-2), each a full trip over the bell, until a round start with b' >= 3.
• Measured (random, scripts/eat_random.py, 3,000 instances clean + 30%-dirty, c 20..120): never halts, always returns to K-form with b' = c + delta, delta in 1..5, c' in 0..6.
• Real run to 1e9 (496 eats): the boundary moves left by d = 3j+2 cells (d = 2: 228, 5: 137, 8: 68, 11: 27, 14: 20, 17: 6, 20: 6; d = 0 four times, early). Bites of 5 or more cells leave every cell left of the new boundary unchanged (pure truncation of the low end). Bites of 2 cells rewrite 1-8 cells near the boundary (a carry or borrow).
• Since d = 2 (mod 3), every eat shifts the digit alignment by 2 cells. The surviving high cells are then re-read in the new alignment, which is where the dirty digits 010/011 come from (5.8% of round starts to 1e9).
• No closed form for w' yet. This is the open part.
• Halting routes (direct simulation from constructed K):
• A: a round on w ending in cells 1 110 (low block 110 with a 1 to its left) halts in 6 steps. All four 2-digit cases.
• B: an eat on a counter with top block 111 can halt (111001011, 111000001, 111000101, at c = 30, 31, 32).
• Feeding B: an eat on a top-011 counter that bites down to it leaves a 110/111 top (14 words of 3 digits, scripts/eat_closure.py, work/eat_closure_k3.txt, work/closure2_k3.txt). Such tops are harmless under rounds (they become clean high digits after 1-8 rounds), but another eat on them first can halt.

Long run

• tools/sim.py: no halt to 1e10 steps (span -5352..1095).
• scripts/eats.c (direct C, eats only): no halt to 3e10 steps. That is 1,597 eats, L = 3,072 blocks at the end, and a counter of 6-8 digits.
• A cycle (L rounds) costs about 12 L^2 steps, so L grows like step^(1/3), about 1-3 blocks per eat. The counter stays at about log4(L) + 2 digits: each cycle adds about L to it, then the next eat bites its low end.
• Pre-eat counters (the K(w,2,c) states, work/eats_3e10.txt): over all 1,597 there are only 8 dirty blocks, all 010, 7 of them the top block. The top block is never 011 or 111, so halting route B is never even set up.

Template comparison (W4-2 / BECv5)

• Same architecture as W4-2 (BECv5 TM1/TM2 plus an invariant). W4-2's K(w,n,m) = w <A 1 (10)^(1+n) 0 (10)^m, with:
• a bounce n-1, m+1, w -> phi(w) (binary +1);
• an overflow at n = 0 that bites q+1 cells;
• parity of q deciding safety;
• dirty words after the bite.
• Here the bounce is the ROUND rule with a signed base-4 counter on 3-cell digits.
• The overflow is a multi-sub-round EAT that bites 3j+2 cells, and the bite re-aligns the digits.
• The halting points are dirty top digits under a deep bite, rather than W4-2's q-odd landings.
• RIncs/LIncs-style lemmas carry over in shape (ROUND = RIncs + a left sweep). The eat and the dirty-digit bookkeeping are new.
• The table is not a near neighbour of any BECv5 machine (different transitions throughout).

Cryptid check (ground rule 6)

• The abstract system has halting branches (A, B), so non-halting rests on avoiding states, as in W4-2.
• Avoidance looks structural, not lucky:
• Halting needs a 011/111 top at an eat. That top is a dirty high digit that survived a whole cycle of about L >= 4^5 increments without a carry cleaning it, and then met a bite deep enough to reach it.
• In 1,597 eats the precondition never occurred once, not even as a near miss: the pre-eat counters hold 8 dirty blocks in all (010) and never a 011/111 top.
• A random-digit model would predict many hits: in the exhaustive 3-digit eat test, 51 of 777 cases (6.6%) leave a 110/111 top, and in the wider closure test 60 of 1,152 cases fail, some halting outright.
• Verdict: not cryptid-like on current evidence. The eat rule still has to be written exactly before an invariant can be stated.

Figures

• img/default_site.png: the site's default view.
• img/rounds_late.png: every 6th round start near 1e9, three cycles.
• img/eat_pairs.png: the counter before and after each of 120 eats to 1e9.
• img/state_ER_2e5.png: entries into E moving right, from blank.
• Renderer: scripts/fig_rounds.py (from the eats.c dumps).

Files

• scripts/rules.py: K, inc, parse_K, next_K.
• scripts/validate_round.py, scripts/inc_closure.py, scripts/eat_random.py, scripts/eat_closure.py, scripts/closure2.py.
• scripts/eats.c (direct C round/eat dumper; eats N prints every round start, eats N -e only the pre-eat round and the sub-rounds with a longer sweep).
• scripts/peek.py, scripts/peek2.py (3-block views).
• work/: rounds_1e9.txt, eats_3e10.txt, validate_round_seed11.json, eat_random_*.txt, eat_closure_k3.txt, closure2_k3.txt, history_rows.json.

Next

Derive the EAT exactly, then test an invariant (W4-2 style). Spelled out under next_goal in the stage report.

Wave 5, stage 1 (2026-10-12)

Result: the machine is predicted to HALT, at about 1.82e18 steps. Not certified. The last cycle is checked by direct simulation. The path to it rests on a cycle model that is TM-grounded and checked several ways (below).

Cycle model (exact on everything tested)

• Cycle start K0(w, c) = K(w, 0, c) = 0^inf w 0 E> 101 0001 (001)^c 0^inf. The blank run reaches K0('', 2) at step 288.
• Eat: from K0, run the TM until the first K(w', b', c') with b' >= 3. Then b' = c + delta, and (w', delta, c') do not depend on c.
• Rounds: b' rounds K(w, b, c) -> K(inc(w), b-1, c+1). inc does not depend on b or c. The next cycle starts at K0(inc^b'(w'), c + delta + c').
• inc on a clean word is +1 in base 4 with digits -1..2, at 12b + 22 + 14t + 4[absorbing digit 000] steps (9,000/9,000 at b = 3, 7, 20).
• scripts/fastabs2.c runs the model. The eat is a TM run at bell size 40. Clean stretches of increments are done arithmetically. Each carry into a dirty digit is one TM round at b = 3.
• It reproduces all 1,572 K0 states of the direct run to 3e10 (words, c and exact step counts; work/k0_3e10.txt, scripts/runk.c, scripts/steps.py).

What the observe stage missed

• Dirty digits are not values. An eat realigns the counter into 0my digits (000, 001, 010, 011). A carry into a 010 run converts the whole run at once and sends a large carry upward. Each realigned word has a well-defined effective value G (value after conversion minus increments, constant once converted). G(010^k) = 6, 42, 426, 2730, ..., about (4k - 16/3) 4^k.
• Excursions. The counter inflates through such conversions and grows long runs of 001 digits. Up to 121 digits more than log4(c) appear in the long run; 16 digits already at 1.5e10 in the direct run. Each excursion is then eaten back (img/excess_all.png).
• Dirty K0 words do occur after 3e10: 976 of 611,577 cycles (2nd digit 010, top 011, top 110, ...; work/abstract_dirty_k0.txt). Post-eat 111 tops: 37 in 1e5 cycles, always carried within the cycle (margin R / t >= 7.1; work/post_eat_111_1e5.txt).

The halt

• Cycle 611,577 (0-based), c = 1,218,828. K0 word 010 111 100 100 001 101 000 000 000 001 001 000 101, already dirty after an excursion. In cycle 611,575 a 14-digit counter left a 011 unconverted. The eat turned it into 111, and that 111 was not converted either (img/k0_last400.png).
• The eat gives 101 111 001 000 011 010 000 000: a 111 digit with y = 1 above it.
• The carries reach the 111 twice: 111 -> 110, then 1 110 -> F reads 1. The halt comes in round 7,435 of the cycle.
• Direct TM run from 0^inf w 0 E> 101 0001 (001)^1218828 0^inf: halts after 108,456,557,258 steps (halting transition counted), after 7,435 round starts (scripts/directk0.c).
• The model's step accounting for this cycle (scripts/steps_chunk.py: eat cost affine in c, rounds 12b + h, clean batches counted arithmetically) gives exactly 108,456,557,258, equal to the direct run.
• Total: the 6R(R+1) round cost alone sums to 1.8168e18. The exact total = 288 + PARTSUM(cycles 0..429,999) + PARTSUM(430,000..611,577), from steps_chunk.py fast2_all.txt a b. It reproduces the 3e10 run's K0 steps exactly. Chunks were still running at the end of the stage (scratchpad w55/indep/chunkA.txt, chunkB.txt); fast2_all.txt is regenerated by fastabs2 - 2 611578 40 1 in 8 s.

Checks of the path to the halting cycle

• Eat bell-size independence: bell 40 vs 300 give identical (d, w', delta, c') on all 611,577 eats. Bell 60/120 match too, and step counts are affine in c (bell 180 checked on every 97th eat).
• Round b-independence: about 2.0M oracle rounds (every carry into a dirty digit) give the same word at b = 1, 2, 3 and 9.
• Independent re-implementation (scripts/check_cycles.py): tools/sim.py Python engine, Python integers, bell 60, b = 4. It matches 22,905 cycles (20,000 random plus the last 3,000) and finds the same halt (after 7,434 rounds of cycle 611,577).
• Not checked: the full 1.8e18-step direct run (out of reach). The model is the only route to cycle 611,577.

Open

• Certify the halt (decision.json): a Rocq certificate in the C2-552 style. It needs parametric eat and round lemmas plus a checked replay of 611,577 cycles.
• An exact total step count.
• Equivalence partners: this string is tm' of Eqv_v2 TM291 (plus 2 more Eqv_v2 modules), and its mirror is in Eqv_v3, so a certified halt decides those too.

Halt certification: independent re-check (2026-10-13)

Result: agrees. I wrote a second implementation from the TM table alone. It does not read or import scripts/fastabs2.c, steps_chunk.py, check_cycles.py or runk.c. It reaches the same halt:

• cycle 611,577 (0-based; cycle 0 is K0('', 2) at step 288), c = 1,218,828;
• K0 word 010 111 100 100 001 101 000 000 000 001 001 000 101, reached at step 1,816,823,958,776,312,687;
• eat: K(101 111 001 000 011 010 000 000, b = 1,218,830, c = 3) after 58,503,988 steps;
• the halt comes in round 7,435 after the eat: 7,434 rounds complete, and the 7,435th round starts at K(101 110 100 100 100 100 100 100, 1,211,396, 7,437).
• In that round the carry runs through the six 100 digits into 110 (D reads m = 1). Then E reads x = 1, and F reads the y = 1 of the top 101: the halt. That is 36 steps into the round, at cell -23 from the boundary.
• 108,456,557,258 steps from K0 to the halt, with the halting transition counted. This is the same number scripts/directk0.c gives.
• Exact total: 1,816,824,067,232,869,945 steps (halting transition counted; busycoq's halts_in index is one less).

Everything is in work/indep/.

How the second model works

The rules below were derived from traces of constructed tapes, not taken from the stage-1 notes.

• Round = COUNTER + BELL. From w 0 E> 1..., the head goes left into the counter. It first comes back to the boundary cell in state C, with the cell left of the boundary now 1. In between it visits no bell cell except the boundary cell, which E rewrites as 1. So w' = COUNTER(w) depends on w alone, and it is computed by running the TM on the counter cells.
• BELL lemma (b >= 1). From 1 C> 101 (001)^b 0001 (001)^c, the head first returns left of the boundary in state A reading 1, after 12b + 17 steps. The bell is then 101 (001)^(b-1) 0001 (001)^(c+1). The rightmost cell visited is 3b + 5, inside the defect, so c plays no part. Then A1 = 0RE closes the round, so a round costs COUNTER + 12b + 18.
• Clean increments (the carry stays in clean digits): +1 in base 4 with digits -1..2, at a cost of 4 + 14t + 4[the absorbing digit is 000 or blank]. These are batched in closed form, up to the point where the clean low part would carry into the lowest dirty digit (m = 1). Step sums come from residue counts: the v with t(v) >= k are the v congruent to 2(4^k - 1)/3 mod 4^k.
• Carries into a dirty digit are run as one exact TM COUNTER run on the whole word. There were 2,096,688 of these and 2,234,206 arithmetic batches.
• The eat uses no rule at all. The TM is run exactly, at the true c, by a macro simulator on run-length blocks.
• Its only shortcut is a shift rule a P^j -> P' a P^(j-1) (and its mirror image), found by simulating the rule's window and checked there; the head never leaves the window.
• A period in which E reads a 1 is refused, so no K-form can hide inside an accelerated stretch.
• The eat ends at the first K-form, detected cell by cell.
• So the eat does not assume c-independence. There were 4,264,432 rule applications over all eats, and the eat at c = 1.2M takes about 0.3 ms.
• Run from blank to the halt: 503 s in Python (run.py; output k0_model_all.txt, one line per cycle start).

Validation against the real TM

• Method. Each case was checked two ways:
• tools/sim.py (reference engine) gives the configuration at the predicted step count, or confirms a halt at the predicted step;
• work/indep/direct.c (my own C simulator) confirms that the predicted K-form is the first one after the start.
• Results (validate.py, val_*.json). Words were random with dirty digits; 0 failures in every set:

• Real-run rounds and eats. Every round start of the direct run below 1.9e9 was replayed: 378,178 single rounds and 616 eats, all identical.
• Huge b (check_bigb.py). 400 rounds with b up to 2e6 and c up to 2e6 were run exactly with the macro simulator and compared with the ROUND rule: identical, including 16 halts.

Cross-checks of the path

• 3e10 run. direct.c from blank to 3e10 steps gives 1,573 K0 states (step-288 one included). The model reproduces every one: step, c and w.
• 10 whole cycles by direct.c, from the model's K0 (spot_cycles.txt, spot_results.txt). Five were random and five had a dirty K0 word not starting with 010; c ran from 18,422 to 87,349 and cycles were up to 4.6e10 steps long. The next K0 matched in step, c and w in all 10.
• Final cycle by direct.c, from the model's K0 of cycle 611,577 (direct_final_cycle.txt, compare_final_cycle.py). All 7,435 round starts are identical in w, b, c and step, and so is the halt at 108,456,557,258.

Comparison with the stage-1 outputs (read only at the end)

• work/k0_3e10.txt (1,573 K0 lines) is identical to my direct run and to my model.
• work/abstract_cycles_sampled.txt: all 3,608 rows match. Their row n gives the K0 that ends cycle n, which is my cycle n + 1.
• work/abstract_dirty_k0.txt: all 976 rows match on the same n + 1 offset.
• My model has 2,915 K0 words that contain any m = 1 digit.
• The extra 1,939 all have a dirty top 010, which that file leaves out. This is a difference of definition, not of data.
• status.json halt_prediction: the cycle, c, K0 word, post-eat word, round 7,435 and 108,456,557,258 all agree.
• Small wording differences:
• "1,572 K0 states" in stage 1 is 1,573 lines in both files.
• check_cycles.py's "after 7,434 rounds" means the halt in the 7,435th round.

What this does and does not show

• Two independent implementations now agree exactly on the path to cycle 611,577 and on the halt. The eat and every dirty carry are exact TM runs here, so the only parametric pieces are:
• the BELL lemma;
• the clean increment, with its cost.
• Both were validated on random instances against tools/sim.py and checked against every round of the direct run to 1.9e9.
• It is still simulation evidence, not a proof. The Rocq certificate (decision certify) remains to be written.

Halt certification: exact step count (2026-10-13)

Exact total: 1,816,824,067,232,869,945 steps from the blank tape (state A) to the halt, with the halting transition counted (tools/sim convention, as in BB(5) = 47,176,870). In busycoq terms this is halts_in tm c0 1816824067232869944.

This is still a prediction. It rests on the cycle model for cycles 0..611,576, which is not proved. Every formula used in the count is checked against the real TM (below). Everything is in work/steps_exact/.

The count

• Cycle n starts at K0(w, c). The eat runs to K(w', R, c') with R = c + delta. Then R rounds follow at b = R, R-1, ..., 1, each costing 12b + h.
• Total = 288 + (sum over cycles 0..611,576 of eat + 6R(R+1) + sum of h) + the halting cycle 611,577.

• The halting cycle 611,577 starts (K0) at step 1,816,823,958,776,312,687.
• It then runs 108,456,557,258 more steps: an eat of 58,503,988 steps (R = 1,218,830), 7,434 complete rounds, and a 36-step halting round (F reads 1).

Independent counts, same number

• Python (steps.py and steps_chunk.py, copied unchanged), in 16 parallel chunks (py_chunks/):
• eats at bells 60 and 120, extrapolated (also bell 180 on every 97th);
• each carry into a dirty digit is one TM round at b = 4 (also b = 7 on every 13th);
• clean stretches are counted by congruences.
• Same total as the stage-1 run, which used two chunks.
• C (stepsx.c, with its own simulator and its own table parsed from the machine string):
• cycles with c <= 250 are run whole on the TM;
• eats at bells 100 and 250, extrapolated (also bell 600 on every 61st, and the real c on every 307th);
• each carry into a dirty digit is one TM round at b = 5, c = 3. Of these 2,096,514 rounds, 462,866 are re-run at b = 1 or 2;
• clean stretches are counted by digit-count identities: sum of t = (k - dS)/3, and #(absorbing digit 0) = (k + dN1 - dN0)/3.
• It reproduces fast2_all.txt at all 611,578 cycles.
• The two counts agree at all 47 comparison points (chunk boundaries and 20,000-cycle marks) and on the total.
• They also agree cycle by cycle on 4,988 single cycles (3,000 random plus the last 2,000) recounted in Python (percycle_sample.py).
• A third count gives the same total: the independent re-check above (work/indep/), whose eats are exact TM runs at the true c by a run-length macro simulator.

Cross-checks (all pass)

• Direct run to 3e10. Both counts hit all 1,573 K0 states of work/k0_3e10.txt at the exact step, word and c. The last is at step 29,992,405,167.
• Whole cycles on the TM past 3e10 (directcyc.c, direct/).
• 14 cycles, at c = 4,399 to 229,443. 9 of them start from a dirty K0 word (an 011 or 110 top, or 010/011 digits), and 4 from 78- to 124-digit excursion words.
• The largest is cycle 115,284, with 315,886,109,619 steps.
• For each one, the step count and the next K0 equal the accounting.
• Halting cycle on the TM. From the cycle-611,577 K0, directcyc.c (written fresh, not directk0.c) halts after 108,456,557,258 steps, equal to both counts.
• Every eat at its real bell size (eatreal.c and eatreal_desc.c, eatreal_out/).
• All 611,445 eats with c > 250 (cycles 133..611,577, up to c = 1,218,828) were run on the TM at their real c.
• Each step count equals the extrapolated one, and each (w', delta, c') equals the bell-100 eat.
• Formulas on constructed tapes (validate.c, 8 seeds, 0 failures):
• 160,000 single clean rounds at b = 1..60, 56,916 of them at b = 1 or 2. Each goes K(w,b,c) -> K(inc w, b-1, c+1) in 12b + 22 + 14t + 4[absorbing digit 000] steps.
• 22,890 clean batches of k <= 400 rounds, each as one TM run K(w,k,c) -> K(w+k, 0, c+k) in 6k(k+1) + (batch sum) steps. In 10,890 of them the batch runs below a dirty digit.
• 1.6M batch sums: the identities equal the explicit per-increment sum.
• 37,133 carries into a dirty digit (real and random words) at b = 1, 2, 3, 5, 9, 17. Each gives the same word, b-1 and c+1, and steps - 12b is constant. The 2,943 halting ones halt at the same step for every b.
• 12,000 eats at c = 100..2,000 (2/3 of them real pre-eat words): the same (w', delta, c') at every c, and the step count is exactly affine in c.
• Lower bound. The total exceeds sum 12b = 1,816,798,040,775,616,704 by 26,026,457,253,241, a factor of 1.0000143.

Found on the way

• The eat's c-independence is not universal. In 4 of 4,000 random counters, the eat wipes the counter and ends at a fixed b' (3 or 4); c' - c and the step count are then constant.
• No real eat is of this kind: bells 100 and 250 agree on every eat, and so does the real c. A Rocq eat lemma has to exclude this case word by word.

Files (work/steps_exact/)

• stepsx.c, tm.h, stepsx_out.txt, stepsx_percycle.txt (columns: n, c after, R, eat, cycle steps, cumulative; small cycles marked direct).
• steps.py, steps_chunk.py, check_cycles.py (copies), run_py_chunks.sh, py_chunks/.
• steps_anchor.py, percycle_sample.py, compare_impl.py, compare_direct.py, compare_eatreal.py, breakdown.py.
• directcyc.c, run_direct.sh, direct/.
• eatreal.c, eatreal_desc.c, run_eatreal.sh, eatreal_watch.sh, eatreal_out/.
• validate.c, validate_seed1..8.txt.
• fast2_all.txt, regenerated by fastabs2 - 2 611578 40 1; same md5 as the stage-1 file.

Kill (halting)

KILLED_HALT (2026-10-13). Lemma halt: halts tm c0. in the 2,975-line .v: a checked certificate runner in the style of busycoq verify/Sk1Machines.v Module Sk1Auto. Rounds and the clean carry are es-lemmas (bellpart, round, absm/abs0/abs1/pass2, callw_inc), rounds applies n rounds in closed form (batch via split 16, untrusted propose, addn), and eats plus carries into dirty digits run on a verified run-length macro simulator (single steps + block rules found by window simulation, crossed by shift_rule_L/R). init (288 steps, solve_init) then 751 vm_check_eq chunks: 4,942,483 checker moves (611,578 eats, 2,234,211 batches, 2,096,694 simulated rounds; 300,612,334 macro steps), ending in the halt in round 7,435 of cycle 611,577 (F reads the y = 1 of the 101 above 110).

Checks

• Formalizer run rocq/check_kill_r1.log: PASS (compile 609.7 s, coqchk timeout at 600 s), sha256 851ca695…0ea92.
• Independent audit (same sha256): PASS, exit 0 (compile 615.9 s, coqchk timeout); holdout line 29 byte-exact; whole file read; soundness chain s1..s751 / h750..h0 / halt checked mechanically; Print Assumptions halt closed (in-file and isolated). One cosmetic finding: line 699's comment said "chunks of about 200,000 macro steps" (really ~400k).
• Packaging: fixed that comment (also in rocq/test/assemble.py); shipped sha256 866a5226…27f4, diff = that one line. Fresh tools/check_kill.sh --halt on the shipped file: PASS, exit 0, checked_at 2026-10-13T18:31:15Z, compile 613.1 s (-native-compiler yes), 0 assumptions, coqchk timeout at 600.2 s (policy A warning: the chunks rest on coqc's kernel check at Qed). Log: submission/check_kill.txt.
• killreview: 6/7; the only miss is "coqchk finished". A finishing coqchk would need several hours (3-chunk prefix took 31 s for 600k macro steps; 300.6M in all, roughly 4 h) with --coqchk-timeout; not run.

Step count (computed, not proved)

1,816,824,067,232,869,945 steps (halting step included; busycoq halts_in n = N − 1), from the three independent counts in "Halt certification: exact step count" and work/indep/. status.json halt_steps has proven_in_coq = false.

Package

• submission/: the .v (= the machine dir copy, same sha256), proof.md (public; writeup_lint 0 errors, 0 warnings), check_kill.txt (fresh run), README.md. No Discord message written; nothing posted.
• proof.md (working copy) = the public text + an internal appendix (written after the .v this time). how_proved.md in the house format.
• The §8 counts of the write-up (369 cycles with a post-eat 110/111 digit, only cycle 611,577 under a digit ending in 1; d ≡ 2 mod 3 in 610,646 of 611,445 eats with c > 250; b' = c − 1 and c' = 2 in half the eats) are from work/writeup_stats/ (scan.py, stats.py over work/indep/model.py's eat and work/indep/k0_model_all.txt).
• Equivalence partners settled with it: Eqv_v2 TM291, TM392, TM1913 (tm' = this string) and Eqv_v3 TM558, TM605 (tm' = its mirror); none on the 740 list.
• decision.json (answered: certify) moved to decisions/2026-10-13-certify.json; no new decision.