C2-552 1RB0RD_1LC0RA_---1RD_1RA1LE_1RC0LF_1LE0LB

740 list line 552 (778 list line 587), sheet class "Skelet 1-like Class 2". Singleton: no other holdout in the 740 list or the 1590 equivalence file is this table from another start state, mirrored or renamed.

Class 2 close-out, stage 1 (2026-10-12)

Stage 1 = PLAN §6 "Observe". Outcome: progress. The bottom level is an exact binary counter (rule M, exact step formula). The full machine is a multi-level structure whose fossil zone is Pascal's triangle. Neither #3's nor #11's architecture covers it as is.

Checks

• Byte-exact: tools/holdouts.py contains data/holdouts/BB6_holdouts_740.txt finds it at line 552. It is in all 26 snapshots and in the newest 778 list (line 587). holdouts.py solved: absent from verify/, with no equivalent proof.
• Claims: none. The results sheet row has empty Status / Notes / Sources / Done By. Nothing in data/discord/.
• No halt to 10¹¹ (direct C sim: span −3,671..552,893, 283,762 ones). Left edge −676 at 3·10⁹.

Halting condition (from the table alone)

• Only B0 and E0 enter C, and C reads 0 = halt.
• E0 → 1RC moves onto the cell that D1 or F0 just wrote as 1, so it is safe.
• B0 → 1LC after A0 is safe too (A just wrote the cell C reads).
• B0 → 1LC after F1 (0LB, moving left) halts iff that cell is 0.
• So the machine halts iff the head in F reads a 1 whose two left neighbours are 0 0.
• F is entered only from E1. Inside an alternating stretch a left sweep in F/E never meets this, so the danger is a 00 wall with gap 0 before 1s (0011).

Wall view (the representation that works)

Read the tape left of the head at a right record (state A on the blank cell). - A wall is a run of ≥ 2 equal symbols: 00, 11, 1111, 1^5, 1^n. - A gap is the number of cells between two walls; those cells alternate. - The 11 walls cut the tape into units. A unit is 11 x M m_1 P m_2 … P y: - lead marker M ∈ {00, 1111} (the bit: 00 = 0, 1111 = 1); - k − 1 passive walls P = 1111, so k markers in all; - gaps x (left), m_i (inside), y (right, the fuel). - The tail is 11 t (t = 2a − 1 odd, a = number of increments since the last reset). - Left of the first 11 is the prefix (the fossil zone). - In pair notation a k = 1 unit is (10)^p [1111] (01)^q, #11's digit shape with marker 1111 instead of 00. - Tools: work/walls.py, work/unitlib.py, work/build.py (builds a tape from wall tokens).

Rule M (one increment = one right record in state A): exact

The carry runs from the right. Every unit with lead 1111 is passed; the first unit with lead 00 stops it. - Passed unit: 1111 → 00, x += 3. - Stopping unit: 00 → 1111, x −= 1. - Every touched unit, k = 1: y −= 1. - Every touched unit, k ≥ 2: m_1 += 1, y −= 2. - Untouched units and the prefix are unchanged; t += 2. - Steps (old values; for k = 1 there are no m terms): - 2t; - plus, per passed unit, 20 + 16(k−1) + 2(x + Σm + y); - plus, for the stopping unit, 16 + 16(k−1) + 2(Σm + y).

Validated: - 27,033 / 27,033 orbit increments to 1e9 whose shape M covers: exact wall lists, 0 mismatches (work/unitcheck.py; 14,702/14,702 to 3e8, 4,530/4,530 to 3e7). - 3,000 / 3,000 random constructed instances (work/randM.py): 1–6 units, up to 3 markers each, random leads, random stop unit, a fossil-like prefix. - The step formula fits all 3,000 exactly (work/fitsteps.py, exact rational fit, max error 0).

So level 0 is #11's per-carry M macro with a different encoding. Every touch burns fuel, and the bit sense matches #11 (00 = 0).

The other events (785 of 27,818 increments to 1e9)

• Overflow O (437 to 1e9): the carry passes every unit and enters the prefix.
• Clean form: every unit as in M; the prefix's leading block 1^n → 1^(n+3); the prefix's last gap −2.
• Exact on 73 of the 285 prefix-entering increments to 3e8 (work/ocheck.py).
• The rest stop inside glued units in the prefix or exhaust the prefix's last gap. Not modelled yet.
• At 2e8 the prefix's last gap is 13, 11, 9, …, 1: the prefix is itself a unit with fuel.
• Glue G (72 multi-marker fuel-outs, k = 2..10): a k ≥ 2 unit touched at y = 1 gets y = −1. Its last P overlaps the next 11, giving a 1^5 wall.
• Split S (237 glued-unit events): a glued pair [x M m P]⊕[x' M' y'] acts as two units while the right one is touched with lead 00.
• When the carry passes it, the passive wall moves across. Example: 8 00 16 1^5 21 1111 13 → 7 1111 15 | 2 00 22 1111 11.
• Exact rule not written yet.
• Reset R (39 increments with the tail glued; 17 resets to 3e9): the multi-marker unit next to the tail glues to the tail, then splits.
• End shape on 17/17 resets to 3e9: … [x, M, a−1] [1, 1111, 2a−1] [1]. The old tail becomes the fuel of a new LSB unit, and the new tail is 1.
• a at the resets: 2, 4, 7, 11, 17, 28, 50, 93, 173, 317, 574, 1036, 1875, 3407, 6205, 11304, 20577 (ratio → 1.82; steps ×3.3).
• k = 1 fuel-outs: 0 to 1e9.
• A k = 1 unit that does run out halts the machine, as the halting condition predicts.
• Constructed: LSB [3 1111 5] → [10 00 0] → halt within the next increment (work/runincs.py).
• Any invariant must keep every single-marker unit's fuel ≥ 1.

Fossil zone = Pascal's triangle

The prefix is a list of rows. Row k is a block 1^{n_k}, then k passive walls, with inner gaps 2·C(k,i) − 1 (i = 1..k−1).

At 2.73e9 the prefix reads:

1^690 | 1^526 P | 1^283 P 3 P | 1^151 P 5 P 5 P | 1^82 P 7 P 11 P 7 P | 1^46 P 9 P 19 P 19 P 9 P | 1^25 P 11 P 29 P 7 …

• Rows 1–5 are exact.
• Row 6 (11, 29, 39, 29, 11) is complete inside unit 1 at 2.49e8.
• Row 7 is forming at 2.73e9 (15 55 111 139 111 57 vs 2C(8,i)−1 = 15 55 111 139 111 55 15).
• The leading blocks grow by 3 per overflow; n_k ≈ ×1.85 per row.
• One new row per ~1 reset generation, so the number of walls grows like log t: 28 → 46 walls, 8 → 9 units between 2e6 and 2.5e8.

Cryptid check

Not cryptid-like. - All updates are linear with exact formulas (M; the clean O; the R end shape). - The fossil zone is binomial (Pascal), not pseudo-random. No parity- or mod-driven branching was seen beyond binary carries. - The irregular part is when glue/split events happen (which unit's fuel runs out first). That is fuel arithmetic, the same kind as #11's drops.

Comparison with #3 / #11 / TM21

• #3 (down-counter, per-step J with ghost phase): does not fit; this counter increments.
• #11 / TM21: level 0 is #11's per-carry M (one macro step per carry, fuel burned per touch), so the per-step INV approach is the right shape for the active units. But: 1. There is no global re-pairing O. New digits enter at the right (R: the tail becomes a new LSB unit's fuel), and old units fossilize at the left. 2. Units carry passive markers (k up to 10 by 1e9). Their fuel burns 2 per touch, and they glue and split (G, S). 3. The fossil zone is an unbounded Pascal triangle, i.e. a multi-level structure whose depth grows like log t. #11's INV (three phases, 2^j bounds over one digit list) cannot express it.
• R4 / #32 (fossil-K walls): a similar level of difficulty, but a different mechanism and encoding. No shared rules.

Open (stages 2–3)

1. Exact rules for G, S, the prefix-entering carries and R (rule closure). Then validate them all on the orbit, aiming at 27,818/27,818 to 1e9.
2. An invariant: - every k = 1 fuel ≥ 1; - glue happens only for k ≥ 2; - an inductive description of the rows, with fuel bounds per row derived from the binomial gaps.

Natural route: a per-step INV over the unit list as in #11, plus a recursive row predicate for the prefix. Feasibility is unknown; it is far beyond a delta of #11.

Files

• img/:
• default_site.png (Fig 1);
• units_constructed.png (constructed 5-unit tape, every 4 steps);
• records_3e5.png;
• lrec_3e9.png (left records to 3e9, window −699..2300);
• records_1e8.png (unused, 5000 rows to 7.9e6);
• viewer.html.
• work/: lrec_3e9.jsonl, resets_3e9.jsonl (pair-view parse at each reset), unitcheck_1e9.txt, randM_steps.json, constructed.txt, scripts.

Class 2 close-out, stage 2 (2026-10-12)

Outcome: progress. The rules close: one rule set reproduces every increment from step 342 on. No invariant yet; the open problem is now one precise question, the fuel race of single-marker units.

Result: rule closure

The executable spec is work/rules3.py (parse, step, unparse). One call of step = one increment (A right record to the next). - Orbit: 27,813 / 27,813 consecutive increments from step 342 to step 999,928,220 predicted exactly (full wall lists, 0 mismatches). Only the 5 bootstrap increments before step 342 are outside the rules. - Macro run from step 342 reproduces the orbit configuration at step 999,928,220 exactly (work/macro.py). - Past the dump: 3,000,000 more macro increments, no rule failure: no fuel-out, no unknown shape (work/macrolong.py, log in work/macrolong_3M_log.txt). That covers at least 4.88·10¹² TM steps (lower bound Σ2t, work/steplb.py); the tape is then 6.09M cells. - Independent TM checks past 1e9 (build the tape, run the C simulator to the next A right record, compare walls): - 200 evenly spaced increments up to 600,000 increments past the dump, tapes up to 1.26M cells (work/valfar.py, work/valfar_log.txt); - 400 targeted increments in the first 277,096: every increment that used a rare rule (absorb, stack edge, U₀ rules, resets, unglue with g up to 576, stack glue) plus every 50th overflow (work/valfar2.py, work/valfar2_log.txt). - 600 / 600 match.

Representation

Read the wall tokens left of the head at an A right record (as in stage 1). Every 1-block is classified by its length mod 3:

The tape is

E U_0 b_1 U_1 b_2 … b_N U_N b_T [t] A>

• U₀ (left boundary E): leadless [x, Q, m, …, Q, y], empty [y], or a digit.
• U_j, j ≥ 1: a digit [x, M, m_1, Q, m_2, …, Q, y] with k − 1 passive walls; y is the fuel.
• The tail [t]. For one increment after a reset there is no tail.

The stage-1 "prefix" is not special: it is E, U₀ and the units whose boundaries are glued blocks (1^5, 1^11, …), and its big blocks are passive stacks.

The rules

The carry runs from the right and treats one unit at a time.

Unglue S (the left unit's glued walls enter this unit; the first one becomes the lead and is passed at once; the old lead 1111 turns passive; the boundary becomes 11):

g = 1:  [x, 1111, m_1, …, y]  ->  [2, 00, x+1, 1111, m_1, …, y-2]
g ≥ 2:  [x, 1111, m_1, …, y]  ->  [2, 00, 0, 1^(3g-2), x, 1111, m_1, …, y-2]

Glue G: whenever a last gap reaches −1, the last passive wall 1^q merges with the boundary 1^r on its right into 1^(q+r−1). If U₀ is empty and its gap reaches −1, E absorbs b₁ instead (e += r − 1; U₁ becomes U₀).

Reset R (two increments):

… 1^5 [t]          ->  … 11 [2, 00, t+2]            (no tail; the carry continues left)
… 11 [2, 00, t+2]  ->  … 11 [1, 1111, t] 11 [1]     (the digit stops the carry; new tail)

Event counts on the orbit (27,813 increments, step 342 → 1e9): - plain M: 27,255; - overflows: 373 with e ≡ 0, 10 with e ≡ 1; - absorptions: 10; - resets: 17 (16 first halves in the window); - unglue: 202 with g = 1, 47 with g ≥ 2 (g up to 52); - glue: 98 for k ≥ 2 units, 106 for leadless units, 3 in U₀, 22 right after an unglue.

What the rules say

• Binary counter. Every touch flips a digit's bit. U_j is touched exactly once per two touches of U_{j+1}.
• Markers flow right.
• A lead moves 1 cell per touch on average (x: −1, +3 alternately).
• A passive wall moves 2 cells per touch.
• When the last passive wall reaches the boundary it glues. At the next touch of its unit it becomes the right neighbour's lead, and that neighbour's old lead turns passive.
• Edge and fossils.
• The edge grows by 3 per overflow.
• When U₀ runs empty, E absorbs b₁ (e ≡ 1 mod 3). At the next overflow it fossilizes as a passive stack, and a fresh 111 starts.
• On the orbit the edge fossilized 10 times, at sizes 10, 10, 13, 19, 28, 40, 58, 91, 157, 286 (steps 884 … 365,107,435).
• The stacks 1^286, 1^154, 1^85, 1^49, 1^25, 1^10 seen at 1e9 descend from these blocks, less the walls they have shed.
• Stacks make the Pascal rows. A stack of g walls leaves one wall behind (the new lead) in each unit it enters, and travels on as a stack of g − 1.
• Bounded width. The unit count stays at 8–9: one absorption per reset on average (8 resets and 8 absorptions in the 3M-increment run).

The only danger: the k = 1 fuel race

Under the rules, the machine halts only if a single-marker unit (k = 1) runs out of fuel. Every other precondition held in all 3,000,000 macro increments, for example: - odd last gaps for k ≥ 2; - x ≥ 0; - only 1^5 ever glues to the tail.

A k = 1 unit j waits for its left neighbour i to hand it a wall (the rescue). Write T for the number of touches of i until the rescue, and bit for j's bit. Then: - j gets n_r = 2T − bit touches up to and including the rescue; - its fuel just before the rescue is y − n_r + 1.

So μ = y − n_r must stay ≥ 0. It is constant under ordinary touches: - a stop touch lowers y by 1 and raises bit, so n_r drops by 1; - a pass touch lowers y by 1, T by 1 and bit from 1 to 0, so n_r drops by 1.

T is local:

neighbour i with k ≥ 2 (or leadless), boundary b_j unglued:  T = (y_i + 1)/2 + 1
boundary b_j glued:                                           T = 1
neighbour i with k = 1:                                       T = (y_i + n_r(i))/2 + 1

• Check (work/margin.py, work/margin_epochs.py; 400k increments from step 54,043; 66 episodes):
• between resets the prediction is constant and equals the fuel left before the rescue, in all 66;
• a reset (its no-tail touch takes one extra cell) lowers it by 1 in 12 episodes and leaves it unchanged in 28;
• 26 episodes see no reset.
• Started at step 342 instead (1.5M increments, 93 episodes): the prediction is exact within the last reset epoch in all 93. Across a reset it drops by 1 in 20 episodes; in the first bootstrap episodes it can also rise (e.g. 1 → 3 at increment 9).
• Slack (work/fuelrace.py, 94 episodes over 1.5M increments from step 342): the fraction of the starting fuel left at rescue is:
• 0.178–0.197 at depth 1 (next to the tail);
• 0.36–0.41 at depth 2;
• 0.54–0.80 at depth 3;
• 0.71–0.99 at depth 4.
• The minimum fuel at rescue past 1e9 is 2,383. It grows about ×1.8 per reset generation.
• The depth-1 race is the reset race. The LSB unit born at reset n gets fuel 2a_n − 1 and must survive until reset n+1, a_{n+1} increments later. So non-halting needs a_{n+1} < 2a_n for every n.
• a_n (25 resets: 17 on the orbit, 8 in the macro run): 1, 2, 4, 7, 11, 17, 28, 50, 93, 173, 317, 574, 1036, 1875, 3407, 6205, 11304, 20577, 37419, 67969, 123257, 222949, 401914, 721916, 1292815.
• Ratios from the 8th reset on: 1.79–1.86, slowly oscillating (latest 1.809, 1.803, 1.796, 1.791). The first two are exactly 2 (bootstrap, before step 342).

Comparison with the templates (updated)

• Level 0 is still #11's per-carry M.
• New compared with #11: walls migrate between digits (glue/unglue), digits are created at the right (R) and absorbed at the left (edge), and an unbounded, Pascal-structured fossil zone feeds the digits.
• An #11-style INV would have to bound μ for every future k = 1 episode. Those episodes start at glue events (k: 2 → 1, y := m₁) and at resets, whose timing is set by the arrival schedule from U₀/U₁.

Open (stage 3)

1. Invariant. Turn "μ ≥ 0 for every episode" into a condition on the current configuration that all rules preserve. That needs: - a bound on m₁ at the coming glue of each k = 2 unit relative to its neighbour's T; - the reset ratio a_{n+1}/a_n < 2, which depends on the arrival schedule from U₀/U₁ (the Pascal rows).
2. Feasibility. This is a renormalization-type statement over an unbounded structure, far beyond #11's three-phase INV. A realistic stage-3 target is an exact invariant candidate, closed under all the rules and tested on the macro simulator, not a Coq proof.

Files (stage 2)

• work/rules3.py: the closed rules.
• Checks: work/macro.py, work/macrolong.py, work/valfar.py, work/valfar2.py, work/steplb.py, work/fuelrace.py, work/margin.py.
• Orbit dump: work/dumpinc.py.
• Data: work/anchors.json (configs at steps 342 and 999,928,220); logs *_log.txt, steplb.txt, fuelrace.json.
• Superseded: work/rules2.py (intermediate), and work/s2lib.py (a builder with 1^n support).

Class 2 close-out, stage 3 (2026-10-12)

Outcome: halt predicted. There is no invariant to find: run far enough, the closed rules of stage 2 reach a single-marker fuel-out, and the TM halts two increments later. This is a prediction from validated rules, not a simulated halt and not a kill.

How we got past 3M increments

work/fast.py is an exact accelerated form of rules3.step. - Between structural events every unit changes linearly in its touch count. - The touch counts follow binary-counter arithmetic: a unit with q digits to its right is touched ((C mod 2^q) + d) >> q times in d increments, where C is the counter value of those digits. - So the simulator jumps to one increment before the next structural event and runs that increment with rules3.step. - Structural events: glue, unglue, k = 1 fuel-out, resets, absorption, and any carry that reaches U₀ while U₀ is a digit or the edge is not ≡ 0 mod 3.

Checks of fast.py against plain rules3.step (work/xval.py, work/xval_log.txt):

The run from step 342 to the fuel-out takes 91 s (work/longrun.py; every reset is logged in work/resets_long.jsonl).

What the long run shows

Stage 2 saw reset ratios a_{n+1}/a_n of 1.79–1.86 and 8–9 units. That window was too short. The ratio oscillates, and the swings grow:

• The period is about 17–20 resets.
• The unit count grows slowly: 9 at reset 29, 12 at reset 40, 19 at reset 62, 25 at reset 82.
• Non-halting needs every ratio below 2 (stage 2's depth-1 race). The third swing crosses that line.

The fuel-out

• It comes 5,712,816,071,814,019,770,034 increments after reset 82, with a_82 = 2,856,408,035,907,009,885,019.
• The configuration just before it is in work/fuelout_config.json. Its right end reads: … 11 [x₂₀, 1111, 4.81e18] 11 [x₂₁, 1111, 1] 11 [x₂₂, 1111, 3] 11 [t] with t = 2·5,712,816,071,814,019,770,034 + 1.
• Units 20, 21 and 22 all have a single marker (k = 1). Unit 21 sits at depth 1, and its left neighbour (unit 20) has no passive wall to hand on, so no rescue can come.
• The next increment passes unit 21 with fuel 1, which gives [x₂₁+3, 00, 0]: a lead 00 right against the boundary 11.
• Two increments later the LSB (fuel 3) runs out as well, and the carry reaches unit 21.

What the real TM does with this shape (work/runincs.py, a constructed tape with the same right end at small sizes):

['111', 5, '11', 6, '00', 8, '11', 5, '1111', 7, '11', 3, '1111', 1, '11', 3, '1111', 3, '11', 7]
  increment 1 (step 150): unit 3 -> [6, 00, 0], exactly as the rules say
  increment 2 (step 188): LSB stop
  increment 3: HALT at step 228

This matches the halting condition from stage 1: F reads a 1 whose two left neighbours are 0 0.

So, if the rules hold, the TM halts during increment 11,631,266,794,472,450,654,093 counted from the step-342 configuration. Step count (work/stepest.py, which reruns the batched loop with accounting and reaches the same fuel-out increment): - Lower bound: 87,364,406,466,050,439,442,427,007,228,199,699,615,332,500 ≈ 8.74·10⁴³. This is 342 plus the sum of 2t over all increments; each increment sweeps the tail twice. - Estimate: ≈ 2.06·10⁴⁴. This adds 2 × the width of every unit the carry touches, and ignores the O(k) constants per touched unit. - The exact count is not computed: stage 1's exact step formula covers only rule M.

Are the rules still trusted that far out?

• Event-class coverage (work/evcover.py, work/evcover_log.txt). Event labels are bucketed by their parameters (k, g, q, r small or big).
• Every class on the run to the fuel-out also occurs in the stage-2 window, where each rare label was TM-checked, except two: a stack glue (1^7 or bigger) from a digit with k ≥ 4.
• Those two classes occur 9 times in all, first at increment 1.97·10²⁰.
• Constructed TM checks (work/ctest.py, work/ctests.txt). Four constructed tapes with stack glues from k = 5 and 6 digits (q = 10, 13, 31), each followed for 40 increments: 160 / 160 increments match rules3.step.
• These runs also exercise unglue with g up to 10, resets, absorption, U₀-1111 and edge fossilization.
• Earlier evidence:
• 27,813 / 27,813 orbit increments to 10⁹;
• 600 / 600 far TM checks;
• 3,000 random rule-M instances.
• Not checked on the TM: any configuration from the new regime (more than 10 units). The tape there has more than 10⁹ cells. The rules are local and linear in the gap sizes, but they are an empirical rule set, not a proof.

Corrections to stage 2

• "Bounded width, 8–9 units": wrong in the long run. The unit count grows, about one unit per 3–4 resets.
• "Ratios 1.79–1.86": that was one phase of a growing oscillation. It does not show a uniform bound below 2, and the rules predict there is none.
• The stage-3 goal (an invariant, μ ≥ 0 forever) is moot: under the rules, μ reaches 0 at reset 83.

Open

1. Certify the halt. This needs: - the rules as lemmas about the TM: parametric shift/sweep lemmas, one per rule of rules3.py; - an exact step count: extend stage 1's M formula to every rule, then sum it in fast.py; - a checked computation of the macro run: about 60k structural events plus closed-form batches.

The busycoq-style route for a halting kill would be a Coq development that replays the macro run. 2. An independent confirmation. sligocki's accelerated simulator (tools/qsim.py, recursive prover on) ran about 5 minutes in stage 3 and printed nothing: fewer than 2M loops, and its RSS grew past 1.7 GB. It is not a practical route to 10⁴⁴ steps. - A better independent check is a second implementation of the macro rules, written from the TM rather than from rules3.py. - Or the Coq replay itself.

Files (stage 3)

• Scripts: work/fast.py (accelerated exact rules), work/longrun.py, work/xval.py, work/evcover.py, work/ctest.py, work/stepest.py.
• Data and logs: work/resets_long.jsonl (all 82 resets with full unit lists), work/fuelout_config.json, work/xval_log.txt, work/evcover_log.txt, work/ctests.txt.

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

Outcome: exact step count computed. Assuming the closed rules hold, the TM halts after exactly

N = 176,522,930,997,643,289,094,015,905,898,381,767,890,130,463  ≈ 1.765·10⁴⁴ steps

N counts the halting transition, as tools/sim does (BB(5) = 47,176,870). In busycoq's convention (halts_in tm c0 n: n defined steps, then a halted configuration) this is n = N − 1 = …130,462.

This is still a prediction from validated rules, not a kill. No Coq was run.

Step formulas (work/steps_exact/costs.py)

An increment costs the sum of its carry actions' costs, computed from the old values. Notation: - Σm is the sum of a unit's inner gaps. - Qc sums (14L − 8)/3 over the unit's passive walls 1^L: 16 for a 1111, 14j + 2 for a stack of j walls.

Stage 1's M formula is the case g = 0 with the tail's 11 added to the stop constant: 5 + 11 = 16.

• How the formulas were found. An exact rational fit over all orbit increments, with constants per action. The constants were then fixed by per-region step attribution on the TM (work/steps_exact/attrib.py).
• Which constants matter. Only sums of constants are identified by the orbit. Every action pattern on the long run lies in the span of the orbit patterns, so the split between them cannot change N.
• The one class absent from the orbit: an empty-U₀ overflow without absorption. It fixed the empty-U₀ constant at 3 (constructed tapes).

Batches (work/steps_exact/stepsexact.py). A batch adds closed-form sums over the touches of each unit: - Tail: 2dt + 2d(d − 1) + 11d. - Digit with m touches: p passes and s stops alternate from its current bit. Σm + y drops by 1 per touch, and x rises by 2 per pass/stop pair. The sum is m·Qc + 2m·S₀ − m(m − 1) + 20p + 2p·x_first + 2p(p − 1) + 5s. - Leadless U₀: every overflow leaves x unchanged and lowers y by 2, so the sum is m·(const) − 2m(m − 1). - Edge: e rises by 3 per overflow, so the sum is m(14e₀/3) + 7m(m − 1).

Last three increments (work/steps_exact/final3.py, certify.py): - 091: unit 21 is passed with fuel 1 → [x+3, 00, 0], and the carry stops at unit 17. The table above applies. - 092: the LSB stops. - 093: the carry passes the LSB and halts in unit 21. It costs t + x₂₂ + 24 (start-of-093 values; the halting step included).

Result

The run reaches the stored fuel-out configuration (work/fuelout_config.json) exactly, at the same increment. The halt is in increment 11,631,266,794,472,450,654,093, as stage 3 predicted.

Cross-checks (all pass)

Per increment on the orbit. A direct 10¹¹ run logged every A right record (work/steps_exact/arec_1e11.jsonl). All 276,427 / 276,427 increments from step 342 to step 99,999,963,828 have exactly the formula's step count.

Cumulative anchors. The batched count from step 342 equals the TM step at the last increment ≤ 10⁹ / 10¹⁰ / 10¹¹:

The 10⁹ value matches work/anchors.json, and the 10¹¹ end matches work/sim_1e11.txt (hi 552,893).

Every structural increment of the run, on the TM (surrogate.py, surrogate_log.txt). There are 53,973 single-stepped increments from step 342 to the fuel-out. - Each was replayed on a reduced copy: gaps > 64 become random 40–79 of the same parity; 1-blocks > 64 become random 40–79 of the same residue mod 3. - All took the same rule path, and 53,973 / 53,973 gave exactly the predicted tokens and step count (44 classes). - Large-size version (bigsur.py, every 200th, sizes up to about 1,560): 270 / 270.

Constructed tapes. - The stack-glue tapes (k = 5, 6) of work/ctests.txt: 160 / 160 increments exact in tokens and steps. - The real fuel-out configuration, reduced 60 times: increments 091 and 092 exact, and 093 halts. - H = t + x₂₂ + 24 was fitted on 30 reductions and holds on the 30 others. - It also holds on 12 minimal tapes with t and x₂₂ up to 4·10⁵.

Batched against plain stepping. Identical step totals and configurations: - 4,027,813 increments from step 342; - 2M increments from each of the reset 40 / 62 / 80 snapshots; - 150k increments from each of the 82 reset snapshots.

Bookkeeping. The run's Σ2t plus stepest's end terms reproduces stage 3's lower bound to the digit: 87,364,406,466,050,439,442,427,007,228,199,699,615,332,500.

Bounds. - N / lower bound = 2.02. - N is below stage 3's estimate of 2.06·10⁴⁴, which charged every stopping digit its full width. A stop never crosses its x. - N plus that overcount (Σ 2(x + b) over stop touches, 2.86·10⁴³) gives 2.05·10⁴⁴ (recon.py), which accounts for the estimate.

What is still not proven

• Empirical rules. The rules (rules3.py) and these step formulas are an empirical, TM-validated rule set. Linearity in the gap and block sizes was checked up to about 10³–10⁵ cells; the real values reach 10²².
• Certification. A kill still needs the rule lemmas in Coq and a checked replay of the batched run, with this N (or n = N − 1) as the halts_in count.

Files (work/steps_exact/)

• Model: costs.py (formulas and constants), actions.py (carry-path classifier), stepsexact.py (batched exact counter, from a copy of fast.py's loop).
• Runs: longsteps.py (the run to the fuel-out, 333 s; fuelout_steps.json), final3.py and certify.py (last three increments; exact_steps.json, halt_inc_formula.json).
• Checks:
• orbitdata.py and exactsolve.py (orbit fit);
• xcheck_plain.py (logs xcheck_plain_*.log, xcheck_resets_log.txt);
• tmcheck.py, surrogate.py and bigsur.py (logs surrogate_log.txt, bigsur_log.txt);
• tailsum.py and recon.py.

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

Outcome: the predicted halt is confirmed by a second implementation. It was written from the TM table only; work/rules3.py, fast.py, longrun.py and stepest.py were not read or imported. It halts during increment 11,631,266,794,472,450,654,093 after the step-342 record, the same increment as stage 3. The configuration 3 increments earlier, all 82 resets and the reset increments are identical to work/fuelout_config.json and work/resets_long.jsonl. This is still a simulation with validated rules, not a proof.

Representation

• Wall list (work/indep/walls.py): the tape left of the head at a right record in state A is written 0^inf g1 W1 g2 W2 … Wn g.
• W = a maximal run of ≥ 2 equal symbols.
• g = the number of alternating cells between two walls.
• The encoding is lossless and covers every tape, so events need no special shapes.
• L1 (work/indep/l1.py): an exact TM simulator on run-length pieces.
• It moves through an alternating piece in one go when the table has a pair q/q2 that flips cells in the same direction. For this table the pairs are E/F going left, A/D and A/B going right.
• It has no unit rules.
• Long 1-walls (> 40) are shrunk to a short wall of the same length mod 3, and restored afterwards. A long wall is crossed by a 3-periodic process (1^3 B1 001 → B1 001 011, 9 steps). Each shrunk run is done twice, with two replacement lengths, and the restored results must agree.

Rule G: one rule for a carry (work/indep/rule_g.py)

Classify the walls:

• An increment carries through the leads with bit 1 and stops at the first 0. Every wall right of the stop is passed, and the head moves +2.
• A wall with r leads to its right is passed floor((V+N)/2^r) − floor(V/2^r) times in N increments from counter value V.
• Domain:
• the carry never reaches an irr wall;
• shrinking gaps stay valid (P to sep ≥ 1, lead to sep ≥ 0);
• a stopping lead has x ≥ 2.
• Rule M of stage 1 is the special case with no long walls. The fossil-zone overflow, the transparent 1^n 0 1111 passes and the units bounded by long walls are also rule G.
• Everything outside the domain is one exact L1 increment: glue, unglue, resets, P migration, fossilisation, fuel-outs, and the halt itself.

Checks

Logs: work/indep/checks_log.txt, tm_checkpoints_log.txt, tm_resets_compare_log.txt, halt_constructed_log.txt, compare_theirs_log.txt.

The run (work/indep/run_to_halt.py, 43 min)

• Start: the step-342 record (7th right A-record from blank), obtained by direct simulation.
• The run has 82 resets, 81,884 closed-form batches and 82,216 exact L1 increments. A rerun without self-checks is identical.
• Last configurations (right end; increment counted after the step-342 record): …090 11 1495536819214692213317 1111 4812803520428781749 11 2901296570081134732223 1111 1 11 5712816071814019770035 1111 3 11 11425632143628039540069 …091 11 1495536819214692213320 00 4812803520428781748 11 2901296570081134732226 00 0 11 5712816071814019770038 00 2 11 11425632143628039540071 …092 11 1495536819214692213320 00 4812803520428781748 11 2901296570081134732226 00 0 11 5712816071814019770037 1111 1 11 11425632143628039540073
• Increment …093 passes the LSB and reaches 00 0 11: F reads a 1 after 0 0, and the machine halts (L1, exact).
• Constructed tapes with this right end on the real TM (3 to 12 units kept, gaps shrunk to 40/41): rule G predicts the next 2 increments, and the 3rd halts at step 112 of that increment.

Comparison with stage 3

• Differences in method:
• One geometric rule plus exact accelerated TM increments, instead of a catalogue of event rules.
• Step counts were not computed.
• The halt is found by simulating the halting increment, not by extrapolating a fuel-out.
• Still open:
• L1's long-wall shrink is justified by a 3-periodic crossing, checked numerically but not proved.
• Inside a batch only the first and last increment are re-simulated.

Files

work/indep/: tm.py, l1.py, walls.py, units.py, rulem.py, engine.py (rules M and O, L1 wrapper with long-wall shrinking), rule_g.py, engine2.py, run_to_halt.py, the check scripts named above, run_resets.jsonl, halt.json and halt_nospot.json. Regenerate the TM record log with tools/sim/tmsim '<tm>' --max-steps 1e11 --on-record.

Kill (halting) (2026-10-12)

Outcome: KILLED_HALT. Lemma halt: halts tm c0. is proved and passes tools/check_kill.sh --halt. This is the first halting kill of the hunt.

The check

• Fresh run on the unchanged .v (sha256 95335b4984c87480b39f1399238df6f85637235879f381bfdd09303a392d515c, 1,142 lines): RESULT: PASS, exit 0, all 17 checks. Full output: submission/check_kill.txt.
• compile 69.7 s with -native-compiler yes;
• coqchk finished and passed in 509.7 s (cap 600 s), so the 22 vm_cast_no_check chunks were re-checked by the independent kernel (not a policy-A timeout);
• Print Assumptions halt = functional_extensionality_dep only (from flip_halts_iff), the baseline.
• Independent audit (a separate run of the same checker plus a full read of the .v): PASS. String byte-exact at line 552 of the 740 list; final theorem halt via flip_halts_iff and halt_tmf; no missing or circular soundness lemma; propose untrusted (it only picks d); IFail is a sound self-loop.
• Earlier runs: rocq/check_kill_r2.log (single cast: coqchk out of memory), rocq/check_kill_r2b.log (22 chunks: PASS).

What is and is not proved

• Proved: halting. The .v replays the run from the step-342 record (init, 342 steps by solve_init) through 107,781 checker moves to the halting touch during increment 11,631,266,794,472,450,654,093.
• Not proved: the step count. N = 176,522,930,997,643,289,094,015,905,898,381,767,890,130,463 (halting step included; busycoq halts_in n = N − 1) is computed from the per-rule step formulas (section "Halt certification: exact step count" above). status.json records it as halt_steps with proven_in_coq: false.

Package

• submission/: the .v (same hash), proof.md (public write-up; writeup_lint 0 errors, 0 warnings), check_kill.txt, README.md. No Discord draft (not requested).
• proof.md (working copy) = the public write-up plus an internal evidence appendix.
• how_proved.md written; tools/card.py now shows the how-proved box for KILLED_HALT too, headed "How we proved it halts" (how_title; killreview.py uses the same heading). test_card.py updated and passing (26 tests).
• Rebuilt: card.html, kill.html (auto 7/7), machines/kills.html (19 kills), dashboard (kill 19, bucket claimed).
• Checkpoint B is pending (non-blocking); there are no notes to fold in yet. Nothing posted.