W5-4 · 1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB (740 line 525)

Status: CHECKPOINT_B, informal_proof stage, proof.md revised after skeptic round 1 (confidence: high) Class guess (agent): Bell eats counter, two-level (decrementing binary counter on a spacing-3 lattice, bitten from its low end). Sheet: Bell eats counter. Spreadsheet notes / Discord thread: results.csv row 1044 has only the class (no status, no notes, no "done by"); no hit in data/discord/*.txt. Viewer: https://bbchallenge.org/1RB0RC_1LC1RB_0RE1LD_0LC1LA_1RF1RA_---0RB

Observe stage, 2026-10-13.

Checks

• Byte-exact entry of data/holdouts/BB6_holdouts_740.txt, line 525 (holdouts.py contains: exit 0). On all 26 snapshots since 2024-06-14.
• Not proved upstream: holdouts.py solved finds no byte-exact, notation-only or equivalent entry in verify/.
• No claim: sheet results.csv row 1044 = class "Bell eats counter" only; classifications.csv lists it under that column; no Discord hit.
• Siblings: none.
• canon (renaming + mirror) from every start: only start A is on the 778/740 lists; starts B..F halt within 44 steps.
• No 740 entry is within 2 transitions of any renamed/mirrored form of this table.
• Its equivalence group in data/holdouts/2026-10-07_eqv_1590.txt (line 1445) is a singleton.

The configuration family

R(p, q, Z) = 0^inf (10)^p 1 C> 0 0 (10)^q Z 0^inf      (p >= 0)
R(-1, q, Z) = 0^inf C> 0 0 (10)^q Z 0^inf              (cycle start; q = n)

• C reads the first 0 of a "wall" 00. Left of it is the bell part already passed, right of it the bell (10)^q, then the zone Z.
• The bell takes every leading 10 pair (greedy parse); Z never starts with 10.
• Zone grammar from blank: Z = 1^f 0 (1^(3k+2) 0)* 1^(3m), f >= 2, m >= 1, or Z = 1^w. No 00 inside Z (checked on every event to 1e9).
• Counter. Zeros sit on a lattice anchored at the right end: positions j = w-1-3i (i >= 1), only j >= 2 count. A zero is a set bit. The LSB is the leftmost lattice position. Value v, L bits.
• Blank start: R(-1,0,11) at step 4. Left records are exactly the cycle starts R(-1,n,Z) (821 of 822 left records to 1e9, tape for tape).

Rules (scripts/rules.py; validated by scripts/validate_rules.py against tools/sim.py)

• dec Z: clear the leftmost zero j, set j-3, j-6, ... while >= 2 (= v-1). allset(u): every lattice position >= 2 set. O2 gives v = 2^L-1, O0 gives 2^L-2.
• "re-parsed": leading 10 pairs of the new zone move into the bell (q grows).
• Validation: seed 3, 150 instances per kind, random p in -1..25, q up to 30, zones up to ~40 cells (work/validate_rules.json); seeds 1 and 2 earlier (10-12 per kind) also all pass.
• Not closed: B2'' = the f=2 bite at q=2 with k >= 2 low bits set. A second wall forms inside the zone and the round machinery runs again on the low part (nested eating), leaving R(p+2, q', Z[cut:]) with q' = 5..15 (img/nested_bite_explore.png). 49 of 204,953 transitions to 1e9.

Coverage from blank (scripts/coverage.py on work/direct_all_events_1e9.txt)

• 204,953 transitions to 1e9: R1 202,502 · O0 881 · B1 808 · B2 312 · O2 294 · B2'(k=1) 71 · R2 18 · B0 9 · O1 6, all equal to the rule's prediction.
• Uncovered: 49 nested bites (B2'') and 3 tiny-zone events before step 30.

Two levels

• Fast level (one cycle). From R(-1,n,Z): about n/2 rounds; each moves the wall 2 pairs right and decrements Z. Overflows refill Z (and widen it by 1 or 3 cells). When q <= 2 the wall reaches Z and bites its low end (B0/B1/B2/B2'), then a new cycle starts with n' = n+1..3.
• Slow level (calm phase). Cycles alternate between w = 3L+3 and w = 3L+2 (for example 27/29 at L = 8). Per two cycles n grows by 2 and the start value v drops by 1. The counter overflows early in each cycle, and the bite drops one bit (v -> v>>1).
• Level-up. When v reaches 0 near n = 2^(L+1), a second overflow per cycle widens Z for good: L -> L+1, v jumps to about 2^L. Fig levels_fill shows the sawtooth, one tooth per level.
• Transitions. Some level-ups pass through an irregular phase: nested bites eat Z deep, w drops to 5..17 and rebuilds.
• n = 258..810 (about 550 cycles), n = 2050..2110 (60 cycles).
• Deep eats (w = 8) recur at n near 2^13, 2^17, 2^19, 2^21, 2^23, with the same margin-1 zone 110110110111111 at cycles 8,477 and 2,096,322.

Abstract run (scripts/absim.py)

• Accelerated runs of R1; every other step by the rules above; B2'' and tiny zones by direct TM simulation (scripts/macro.py) from a shrunken p.
• Matches the direct run at all 4,200 cycle starts to 1e11 steps (work/direct_events_1e11.txt; C event logger scripts/direct_events.c, whose cycle starts equal tools/sim.py's left records).
• Ran 3e7 cycles (n = 30,001,809, L = 23 bits, about 1.2·n^3 = 3e22 TM steps): no halt (work/absim_3e7.txt, work/absim_near_3e7.txt).
• Rule uses: B1 29,999,979 · O0 24,412,335 · B2 14,999,552 · O2 5,591,100 · B2' 481 · B2''/tiny (direct fallback) 469 · R2 242 · B0 18 · O1 9.

Where halting could come from

• Random search over q <= 3 and zones up to 40 cells (6,000 instances): the only halts are H, R(p,2,(110)^k 111) (and the degenerate Z = 11).
• dec never produces an all-set zone. So H needs O2 at q = 4 (all-set zone at q = 2 next round), or a bite that leaves an all-set zone exactly at q = 2.
• Of the closed bite rules only B2 with f = 3 ends at q = 2, and its zone Z[4:] is all set only if its input was an all-set w = 1 zone at q = 2, which again only a bite can make. B2'' is the open case.
• Parity separation (empirical). After cycle 24 every O2 overflow with q <= 8 has odd q (q = 1, 3, 5, 7: 4, 11, 5 and 4 events to 3e7 cycles). After cycle 24 no even-q O2 overflow has q <= 8 (3e7 cycles); in the first 1.1M cycles the smallest even q is 12 (cycle 74).
• Smallest even q per active octave of n: 16, 20, 130, 84, 246, 246, 368 (2^8 .. 2^19). Large q (all even) are the calm-phase overflows.
• Near misses:
• O2 at q = 3 and q = 5 (one or two rounds from q = 4, but on the wrong parity);
• q=2, f=2 zones one bit short of all set (k = 8 of 9 at cycle 595; 110110110111111 at three level-ups). These are harmless: the conversion stops at the clear top bit.

Template comparison (nearest proved neighbour: our W4-2 kill)

• W4-2 = 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF, built from BECv5 TM1/TM2.
• Its K(w,n,m) = w <A 1 (10)^(1+n) 0 (10)^m is the mirror of our R(p,q,Z): a bell with one defect, plus a counter word.
• Rules there: R1 bounce (n -> n-1, counter +1 by phi), overflow with a bite (R2/R3), halting R4, nested eating R5 (no closed form at Observe), invariant I on (type, N, m) with parity classes.
• Same: a bell with a moving defect, a counter bumped once per pass, a bite of the counter's low end at overflow, rare nested eating, a halting configuration that needs a coincidence.
• Different:
• our counter counts down, not up;
• our bits sit 3 cells apart on a lattice anchored at the zone's far end, not as pairs next to the head;
• the defect moves 2 pairs per round, not 1;
• the bell grows about 1 pair per cycle, and the counter's capacity doubles per level (a slow two-level counter, v -1 per 2 cycles).
• W4-2's .v reuse: the shape of progress_nonhalt_cond with an invariant, BigStep per rule, RS/OV-style low-level lemmas. Its phi/Sweep lemmas do not carry over (different counter).
• Rulefit's 25 fitted rules failed (stage note) because they fit records, whose shape (10)^a 0 (10)^b 1^c B> is a mid-cycle snapshot. The family above is aligned to the wall.

Cryptid check (ground rule 6)

• The rules are plain counter arithmetic: decrement, overflow refill, bites that drop 1..3 low cells. No Collatz-style branching, and no parity of a growing number decides a branch.
• What looks irregular: the transitional phases at level-ups (nested bites, deep eats), whose length is not self-similar (550 / 0 / 60 cycles at L = 7-8 / 9 / 10).
• The halting route is narrow (O2 at q = 4) and the data show a clean parity split, not a shrinking gap. Small-q O2 overflows are odd, even ones stay >= 12.
• Verdict: not cryptid-like on current evidence, but the invariant behind the parity split is unknown and B2'' has no closed form. Risk: medium-high.

Files

• scripts/rules.py (rules), scripts/validate_rules.py (tools/sim.py check), scripts/coverage.py, scripts/macro.py (direct macro step), scripts/absim.py (abstract run), scripts/plot_levels.py (Fig levels_fill), scripts/direct_events.c (C event logger).
• work/validate_rules.json, work/direct_all_events_1e9.txt, work/direct_events_1e11.txt, work/absim_3e7.txt, work/absim_near_3e7.txt, work/records_1e9.jsonl, work/compress_track_1e8.txt, work/qsim_2e5.jsonl.

Checkpoint A (Dennis)

(pending)

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

Outcome: progress (confidence: med). B2'' is closed, the run's global structure is mapped, and an inequality invariant is the candidate. No proof yet.

1. The nested bite B2'' has a closed form: a stack of the same rules

• Input: R(p, 2, (110)^k Y) with k >= 2 and Y starting 111.
• The wall turns the k low set bits into k nested walls (blocks 1 00). The innermost level starts at R(0, 1, Y[2:]).
• Each level runs the ordinary rules from R(0, q, Z) until its own bite brings it to a cycle start R(-1, q', Z'). That tape is the next level's R(0, q', Z') (a "pop").
• The k-th pop lands in the original level as R(p+2, q', Z'). A nested bite inside a level recurses the same way.
• Inner levels have even p; the outer level has odd p.
• H is exactly the case Y = 111: the innermost R(0, 1, "1") has no move.
• New small rule B0c (needed inside nested levels, after R2 at q = 3 with v = 1):
• R(p, 0, 1^w), w = 0 mod 3, w >= 6 -> R(-1, p+2, 11·allset(w-2));
• R(p, 0, 111) -> R(-1, p+1, 1^6).
• 180/180 against the TM (p = -1..13, w = 6..39).
• Validation (scripts/nested.py, scripts/absim2.py; no TM simulation anywhere in absim2):
• 256 brute-force nested bites (k = 2..5, every Y of width <= 21 with clear LSB, work/b2pp_bruteforce.txt): 252 exact, 4 halts, all with Y = 111.
• Larger brute force (k = 2..8, p = 3 and 4): only Y = 111 halts; outputs with w' = 1 or 2 mod 3 always have odd q'.
• Direct run to 1e9: 204,951 of 204,953 transitions exact. Only the 2 tiny-zone events before step 30 are uncovered.
• Closed-rule abstract run = direct run at all 4,197 cycle starts to 1e11 (work/cycle_starts_1e11.txt). Nesting depth reaches 8.

2. Global structure: calm 2-cycles, clean and messy level-ups

• Calm phase at level L is an exact 2-cycle with a fixed C = n + 2v.
• Even L: w alternates 3L+3 / 3L+5, with C = 2^(L+2)+4 / 2^(L+2)+2.
• Odd L: w = 3L+3 always, C = 2^(L+2)+2 / 2^(L+2)+1.
• It contracts: an offset delta = C - 2^(L+2) goes to about delta/2 (+3) per cycle, so errors die out.
• Entering an odd level is clean: cycle starts with E = 6, 9, 10, 13, 14, ...
• Entering an even level L starts a transient from the fixed state T(L) = R(-1, 2^(L+1)+3, zone(3L+3, 2^L-2)) (E = 7)
• Nested bites eat the zone down to w = 5..12, it rebuilds, and the run falls back and climbs again until the calm 2-cycle of level L locks.
• The T(L) model equals the real run (L = 12 from cycle 7,979; L = 14 from cycle 32,243).
• So the machine runs forever iff every transient T(L), L even >= 10, locks without halting.
• Transient sweep (scripts/transient.py; work/transients_closed_rules.txt, L = 10..38; work/transients_fallback_L10-56.txt, L = 10..56): all lock, none halts.
• Lock lengths (cycles), L = 10, 12, ..., 56: 37, 523, 191, 87, 579, 815, 193, 2,977, 171, 245, 253, 2,483, 22,839, 19,581, 114,157, 55,385, 37,795, 400,211, 132,843, 30,913, 45,287, 1,799, 47,525, 124,485.
• Erratic, not uniform in L. A proof cannot just compute each transient; it needs an invariant that covers them.

3. Invariant search

• Parity part (holds on all data):
• At the outer level, configurations with q even and w = 2 mod 3 occur only in cycles that start with w = 2 mod 3 and n even, and right after O1 (checked on every configuration of the transients L = 10..32).
• Reason: a B1 bite gives n' = p+3+r with p odd, and r = 0 whenever the new w is 1 or 2 mod 3, so those starts have n' even (a B0 bite with f = 2 gives w' = 2 mod 3 with n' odd, which is harmless). Nested-bite outputs with w' = 2 mod 3 have odd q'.
• So H (an O2 overflow at q = 4) needs E = n - 2v = 4 at a w = 2 cycle start, or n - 2^(L+1) = 4 at a w = 1, v = 0 start.
• No congruence obstruction. At w = 2 starts inside transients, E mod 16 is spread evenly over the even residues (2,570 starts, L = 10..32).
• Bell-capacity window. Let cap(w) = number of counted bits, +1 when w = 1 mod 3 (an R2 round adds a bit) d = n - 2^(cap+1)
• Since v <= 2^LL - 1, E >= d + 2. So d >= 3 at a w = 2 start rules out E = 4.
• J := d >= 2, minus (d = 2 with an all-set zone, w = 0 or 2) and (d = 2, w = 1, v = 0).
• Exhaustive test (w <= 21, every v, n from 2^(cap+1)+2 to 2^(cap+2)+100): no cycle from J halts. The only J states that leave J are (w = 0 mod 3, v = 0, n = 2^(cap+2)+3), one per width.
• With larger n (up to 2^(cap+6) for w <= 15): their predecessors (n = 2^(cap+2)+2, v = 2) and (n = 2^(cap+2)+1, w = 2 mod 3, v = 1) appear, the backward orbit of the calm map.
• Backward closure of all halting starts (scripts/closure.py, w <= 18, n < 2^(cap+3)): 113 bad starts, 20 of them in J, all on one line at the top of the window. Either n = 2^(cap+2)+3-j with v = 2j (w = 0), or n = 2^(cap+2)+1-j with v = 1+2j (w = 2). In both cases C - 2^(cap+2) = 3+3j. One outlier: w = 11, n = 31, v = 3.
• The calm phases have C - 2^(cap+2) in {1, 2, 4}, never 0 mod 3.
• Real run: inside transients (after the entry cycle) d >= L+3 (13 at L = 10, 39 at L = 38), and d >= 44 at w = 2 starts. The tight states (d = 2..6) are only at the clean, parametric level-ups.
• Candidate invariant for proof.md: J minus the top line {C - 2^(cap+2) = 3+3j, n near 2^(cap+2)}. It is an inequality invariant like W4-2's, so the chaotic transients need no exact tracking.

Cryptid check (update)

• The transients are chaotic: erratic lengths, zones eaten to 5..12 cells, nesting depth up to 24.
• But every halting start found sits on one thin line at the top of the bell-capacity window, and the run keeps a growing margin from it inside transients.
• Verdict: not cryptid on current evidence; risk medium.

Open

1. The bad line in closed form for every cap, and a check that J minus that line is closed for all n, including n >> 2^(cap+2) (tiny zones, where one cycle overflows many times). Then a proof sketch of closure from the cycle arithmetic: overflow chain q_(i+1) = q_i + 1 - 2^(L+i+1), bite parity.
2. Nested levels: an inner invariant (a push never meets Y = 111) for the Coq B2'' lemma.
3. Coq shape: a stack family (outer block (10)^p 1, inner blocks 1 00), one BigStep per rule, progress_nonhalt_cond over the invariant.

Files (new)

• scripts/nested.py (B2'' recursion + B0c), scripts/absim2.py (closed-rule abstract run; checked against work/cycle_starts_1e11.txt), scripts/transient.py (T(L) sweep), scripts/closure.py (backward closure of halting starts).
• work/b2pp_bruteforce.txt, work/cycle_starts_1e11.txt, work/transients_closed_rules.txt, work/transients_fallback_L10-56.txt.

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

Outcome: progress (confidence: high on non-halting). A simple invariant is found and checked; two of its three lemmas have a paper argument. No proof.md yet.

1. The invariant

Work on outer cycle starts s = (n, w, v), i.e. R(-1, n, encode(w, v)).

cap(w) = counted lattice bits, +1 when w = 1 mod 3
d(s)   = n - 2^(cap+1)
M(s)   = n + 2v - 2^(cap+2)  (mod 3)     w = 0, 2 mod 3
         n +  v - 2^(cap+2)  (mod 3)     w = 1 mod 3
K      = { w >= 3, d >= 2 }
I      = { s in K : M(s) != 0 },  minus the one state (6, 4, 0)
T_c    = (2^(c+1)+2, 3c+5, 2^c-1)        (d = 2, w = 2 mod 3, zone all set)

• The blank run enters I at step 327: R(-1, 6, 11111) = (6, 5, 0), with d = 4 and M = 2 (scripts/entry_check.py).
• It stays in I at every later cycle start checked: 304,194 of them (the direct run's cycle starts to 1e11, then 300,000 closed-rule cycles).
• T_c (the start of an O2 overflow at q = 4, then H) has M = 0. The exceptional state (6, 4, 0) has no predecessor in K.
• So the old "bad line" (C - 2^(cap+2) = 3+3j) and the w = 11, n = 31 outlier are just M = 0 states.

2. Lemma M (sign law): proved on paper

Extend M to every configuration of the family:

Q(p, q, Z) = q - (p+1) - v - (-1)^cap   (mod 3)      (+v instead of -v when w = 1 mod 3)

At a cycle start (p = -1), Q = M because 2^(cap+2) = (-1)^cap mod 3. - Rounds, overflows and q = 2 bites keep Q: R1, R2, O0, O1, O2, B2, B2'. - Bites that end a cycle negate Q: B1 (all three cases), B0 (f = 2 and f >= 5), B0c. - Each case is a two-line computation from the rule table, using 1/2 = -1 (mod 3). - The nested bite B2'' keeps Q. Proof by induction on depth: - inner level i starts with X_i and ends with -X_i; the pop shifts p by 1, so X_(i+1) = -X_i - 1; - after k levels, X_k + 2 = (-1)^(k-1) (X_1 + 2), and that gives Q_out = Q_in. - So M(F(s)) = +-M(s): M = 0 is preserved both ways. - Checks: - TM level (scripts/signlaw.py): 7,977 of 7,977 random family configurations obey the law after one direct-simulation macro step (seeds 1, 2; 23 others halt). - Rule level: every rule application in the cycles from K, w <= 21: 7.3M, 0 failures (work/signlaw_seed2.txt).

3. Lemma K (inequality): checked exhaustively; plain cycles proved on paper

Statement: if s is in K, then the cycle from s halts only when s = T_c or s = (6,4,0). Otherwise F(s) is in K.

Checks with scripts/invariant.py (closed rules, nested bite included, no TM simulation):

• F itself was checked against direct TM simulation on 300 random states of I (n <= 700): 300 agree (work/check_F_vs_tm_seed1.txt).

Paper argument for plain cycles (no B2'/B2'' inside the cycle): - From K, E = n - 2v >= d + 2 >= 4, so level 0 always overflows. E = 4 at w = 2 mod 3 is exactly T_c. - The overflow chain gives q_m = E - e - 4 + m - (2^(c+m+1) - 2^(c+2)) at level m >= 2, where e = 1 if the first overflow is O2. - A w = 1 mod 3 start reduces to this after its first round (R2 or O1); then E >= 7. - Say the chain stops at level f. Then: - f = 1: d' >= d; - f >= 3: d' >= 2^f - 2f + 2 >= 4; - f = 2, ending in B1: d' >= 2 + 2e + r + 2v (r = reparse). Equality only at n = 2^(c+2)+3, v = 0, w = 0 mod 3, which maps to T_(c+1) and has M = 0; - f = 2, ending in B2 or B0: d' >= 4 or d' >= 2, and the output is not all set.

Open: - (a) Continuation cycles. A B2' or B2'' at level f lets the cycle go on. Data: the final cap is always <= (cap at the first continuation) - 1, and min d' = 5 (cont1) or 105 (cont2) against 2 for plain cycles (work/continuation_w21_X4.txt). This needs a bound on the nested output (q', Z'). - (b) No halt inside nested levels from K (no push meets Y = 111). It holds in every check above, but has no argument yet.

4. Consequence

• With Lemmas M and K, I is closed and no cycle from I halts, so the machine never halts.
• The level-up transients T(L) are in I (d = 3, M = 2), so their lengths no longer matter.

Cryptid check (update)

• Not cryptid. Halting is ruled out by a mod-3 quantity plus an inequality. The chaotic transients are inside I.

Next

1. Close (a) and (b) on paper: the nested output bound, and an inner-level version of the sign law or of the inequality.
2. Write proof.md.
3. Formalize: one lemma per rule (the nested bite by induction on depth), a cycle lemma for K, and progress_nonhalt_cond over I.

Files (new)

• scripts/invariant.py (definitions + Lemma K/M window check), scripts/signlaw.py (sign law, TM and rule level), scripts/check_F_vs_tm.py, scripts/continuation.py.
• scripts/entry_check.py (blank run vs I).
• work/invariant_w3-31_X3.txt, work/invariant_w3-16_X10.txt, work/invariant_w3-12_X14.txt, work/signlaw_seed1.txt, work/signlaw_seed2.txt, work/check_F_vs_tm_seed1.txt, work/continuation_w21_X4.txt, work/entry_check_300k.txt.

Funded stage (2026-10-10, proof)

Run 2026-10-13 (Dennis: "go with recommendations"). Outcome: proof_ready (confidence: high). Both open sub-lemmas are closed on paper and checked; Lemma K now covers every cycle from K. proof.md is the next stage.

1. Shift law and the G-form of the nested bite

• The rules read q and Z only; p just moves along. So a level started at R(p0, q, Z) runs the same rule sequence as the cycle from R(-1, q, Z), and pops p0 + 1 later. Write G(t) = F(t) + (1, 0, 0) (t = (n, w, v): the pop of a level started at R(0, n, Z))
• Nested bite (B2', k = 1, and B2'', k >= 2) is k - 1 G-steps: R(p, 2, (110)^k Y) -> R(p+2, G^(k-1)(3, Y[3:])) (Y starts 111, Y != 111; Y = 111 is H)
• Level 1 (innermost) is a single B1: R(0, 1, Y[2:]) -> pop (3, Y[3:]). Each later level is one G-step.
• Y[3:] = Z >> (k+1): width w - 3k - 3, value v >> (k+1).
• Check: 20,000/20,000 random nested bites (k = 1..7, Y up to 30 cells) equal scripts/nested.py, Y = 111 always H (work/contlemmas_gform_seed7.txt).
• Composite form of a continuation cycle. Let the first continuation of the cycle from s be at R(p_c, 2, Z_c), with k low set bits and L_c bits. The rest of the outer level is one more G-step, shifted by p_c + 2: F(s) = (p_c + 2) + t_(k+2), t_2 = (3, Z_c[3k+3:]), t_(i+1) = G(t_i) d(F s) = p_c + 2 + d(t_(k+2))
• Later continuations of the outer level sit inside the last G-step.
• Check: 533,148 continuation cycles from K (w <= 27) and 151,880 (w <= 15, n < 2^(cap+10)), 0 mismatches (below).

2. Gap (b) closed: no halt and no gap inside nested levels

• Phase lemma. Call a phase start a level start or the output of a continuation. Inside a phase:
• a w = 2 zone with q >= 3 exists only from the phase start (w = 2) or right after an O1 at the phase start (w = 1, v = 0); R1 and O1 keep the parity of q;
• after the first overflow the zone has w = 0 mod 3 for the rest of the phase, so only O0 follows;
• H = R(p, 2, (110)^j 111) is produced only by O2 at q = 4 (dec never gives an all-set zone; R2 and O0 leave the LSB clear; B2 with a reparse would need an all-set w = 1 zone at q = 2, i.e. a phase start with q = 2, and every phase start has q >= 3).
• So H needs a phase start with w = 2 mod 3, q = 2v + 4, or w = 1 mod 3, v = 0, q = 2^(L+1) + 4. That set is H. Check: the cycle from t (w >= 3, n >= 3) halts iff t is in H, on 610,121 states (w <= 24) and 606,121 (w <= 12, n < 2^(cap+12)).
• Parity of pops. A pop with w' = 1 or 2 mod 3 has n' = p + 3 (B1, no reparse) or p + 5 (B2 then B1), so n' = p + 1 mod 2. B0 with f = 2 never occurs inside a cycle: q = 0 only follows R2 or O0 at q = 3, and both leave the LSB clear. Inner levels have p even, so their pops have n' odd when w' = 1, 2.
• Lemma J. J = { w >= 3, n >= 3, n odd when w = 1 or 2 mod 3 }. For t in J the level from t never halts, never meets a configuration without a rule, and pops into J.
• Proof: q stays odd in its w = 1, 2 part, so q = 2 occurs only with w = 0 mod 3, w >= 6, zone not all set (B2, or a continuation with Y != 111 and |Y| >= 6, so t_2 is in J). Pops have w' >= 3, n' >= 3 and the parity above. Continuations recurse (induction on the length of the computation).
• The innermost level is R(0, 1, Y[2:]) -> (3, Y[3:]), in J.
• Consequence: every phase start except the outer cycle start is in J, so a cycle from s halts iff s is in H. In K, H = {T_c} u {(6,4,0)} (w = 2: n = 2v + 4 >= 2^(c+1) + 2 forces v = 2^c - 1; w = 1: d >= 2 forces L = 0, n = 6).
• Check: J1 holds on all 1,920,333 J states with w <= 27, n < 2^(cap+4), and 479,621 with w <= 15, n < 2^(cap+10).

3. Gap (a) closed: Lemma K for continuation cycles

• A1 (bell at the continuation). From K, level 0 always overflows (E >= 4), so the first continuation is at a level m >= 1 with L_c = c + m bits, and p_c >= 2^(L_c) - 3
• m = 1: p_c = n - 3 (w = 2 start), n - 4 (w = 0), n - 5 (w = 1, v >= 1, via the R2 equivalence (n, w, v) ~ (n-1, w+2, 2v-1)); d >= 2 gives the bound. w = 1, v = 0: the O1 level has c - 1 bits, the next one c bits and p_c = n - 3.
• m >= 2: p_c = n - 3 - j with j = m - e (the O0 overflows before; e = 1 if the first overflow is O2), and reaching level m needs q_m = E - e - 4 + m - 2^(c+m+1) + 2^(c+2) >= 2. With n >= E this gives p_c - 2^(c+m) + 3 >= 2^(c+m) - 2^(c+2) + 6 - 2m + 2e >= 0.
• Check: min slack 0 (it is tight at w = 1 mod 3, d = 2).
• Lemma Z' (zone-dominated step). If t is in J and d(t) <= 1, then d(G t) >= 2 or cap(G t) <= cap(t) + 1.
• With n <= 2^(c+1) + 1 the top level of the step makes at most one overflow after its first (the next one would need E >= 2^(c+2) + 2 > n).
• Cases: w = 0, no overflow: bite, cap - 1; w = 0, one O0: bite at c + 1 bits, cap c (L = 0: B0c gives cap 1); w = 2 (n odd): B1 to w = 1 gives cap + 1, or O2 then a bite at odd q gives cap c; w = 1 (n odd): v >= 1 reduces to the w = 0 case by the R2 equivalence (d - 1 <= 1), v = 0 is O1 then the w = 2 case.
• A continuation inside the step: its inner run is again G-steps from (3, Z_c[3k+3:]) with L_c <= c + 1. If the last inner state is K-like (d >= 2), then d(G t) >= p_c + 3 + 2 >= 2. Otherwise every inner state is zone-dominated and, by induction, the inner cap grows by at most 1 per step: cap <= (L_c - k - 1) + k <= c.
• K-likeness persists. If t is in J and d(t) >= 2, then t is not T_c or (6,4,0) (both have even n and w = 2 / w = 1), so Lemma K gives d(G t) = d(F t) + 1 >= 3.
• Lemma K, continuation case. With F(s) = (p_c + 2) + t_(k+2):
• if some inner state is K-like, so is t_(k+2), and d(F s) >= p_c + 4 >= 4;
• otherwise t_2, ..., t_(k+2) are all zone-dominated, cap(t_2) = L_c - k - 1, and Z' gives cap(t_(k+2)) <= L_c - 1. Then, with n(t_(k+2)) >= 3 (Lemma J) and A1, d(F s) >= (2^(L_c) - 3) + 2 + 3 - 2^(L_c) = 2.
• Lemma K, Lemma Z' and K-persistence are proved together by induction on the length of the cycle computation (inner G-steps are strictly shorter).
• Data: min d(F s) on continuation cycles is 5 (slack 3 over the bound).
• (6,4,0) has no predecessor in K (needed for the closure of I): plain cycles give n' >= n - 1 - f + 2 with f <= log2(n) - c overflows, continuation cycles give n' >= p_c + 5 >= 2^(L_c) + 2; so n' = 6 forces n <= 9 and c <= 1 (w <= 8), inside the exhaustive window (0 predecessors, work/invariant_w3-31_X3.txt).

4. Checks (scripts/contlemmas.py, closed rules, no TM simulation unless stated)

• Z' in numbers (w <= 27): when G(t) stays zone-dominated, cap(G t) - cap(t) is +1 in 10,796 cases and <= 0 in 159,188; 69,802 steps become K-like.
• Every check is on the closed-rule model; the model itself was checked against the TM before (rules 150 per kind, nested bite 252/252, F = TM on 300/300 states of I).

5. The non-halting argument, end to end

1. The blank run reaches R(-1, 6, 11111) = (6, 5, 0) at step 327, a state of I (d = 4, M = 2).
2. Lemma K (now for every cycle) and Lemma M: for s in I the cycle from s does not halt (s is not in H*), F(s) is in K, M(F s) = -+M(s) != 0, and F(s) != (6,4,0). So F(s) is in I.
3. Inside a cycle nothing halts: the outer phase start s is not in H*, and every other phase start is in J (Lemma J).
4. So the machine never halts.

Still open

• proof.md (next stage): write out the plain-cycle part of Lemma K in full (stage 2 sketch: f = 1, f = 2 with B1/B2/B0, f >= 3), and Lemmas P, J, A1, Z' above, the shift law, and the TM-level justification of the nested-bite stack (stage 1 structure, validated 252/252 by brute force).
• Rocq: one lemma per rule; the nested bite and the shift law by induction on depth; the cycle lemma by strong induction on steps; progress_nonhalt_cond over I.

Files (new)

• scripts/contlemmas.py (hstar, jwin, kwin, random, gform, tm).
• work/contlemmas_*.txt.

Informal proof (2026-10-13, informal_proof stage)

proof.md is written; checks in check_proof.py (self-contained). Outcome: informal_proof_written (confidence: high).

New this stage

• Tape-level rules. Every macro rule is now a chain of 11 low-level rules, each an exact TM run that reads only its pattern:
• BR B> 1^k, S (01)^k <C (C1 D0), T (111)^j <C -> <C (011)^j (C1 D1 A1 C1 D0), W (wall entry, 10 steps), PS (pair step, 12 steps);
• ZA (zone arrival) in three cases by f mod 3, f = the first 0 of the zone;
• PUSH k (14+3k), B1 (2p+15), B0, B0c, and the 9-step halting tail Ht.
• One round lemma. R1, R2, O0, O1, O2 are all W, PS^(q-3), ZA. Split by f mod 3: f = 2 gives q-2 and (110)^((f-2)/3) 111 r; f = 1 gives q-2 and 1111 (011)^((f-4)/3) 1 r; f = 0 gives q-3 and 11111 (011)^((f-3)/3) 1 r. The w mod 3 table is its counter form.
• Stack and shift law. An ending bite's sweep reads exactly the two cells 00 left of its left part. For an inner level they are the 00 of its 001 block, so a pop is the next level's R(0, ..) tape. TM check: the level starts occur in order (NEST).
• Lemma K, plain cycles, in full. E_m = E_0 + m - e - (2^(c+m+2) - 2^(c+2)); p_b = n - 1 - q_b - (f - e); d' >= X_f + 2e + 2v + ... with X_f = 2^(c+f) - 2^(c+2) - 2f + 6. The w = 1 cases reduce by EQ1 (v >= 1) and EQ2 (v = 0); E1 with f = 1 needs a parity step (d odd).
• Safety vs termination. Lemma J and the halting part of K hold at every configuration. Lemma K's bound is used only on completed cycles (induction on run length). Termination of levels is not claimed and not needed informally. It matters for the Rocq route (proof.md section 9): a stack invariant carrying the outer cycle's partial derivation, or a termination lemma.
• Corrections found by check_proof.py: NB needs 2^(f-1) <= n, not 2^f (w = 1, v = 0 counts O1). The predecessor check of (6,4,0) is now done up to n = 12. The B2 counter form for w = 1 with bit 0 clear is enc(w-2, v/2); that case never occurs.

Files (new)

• proof.md, check_proof.py; work/check_proof_quick_seed1.log, work/check_proof_seed1.log, work/check_proof_seed2.log.

Skeptic round 1 (2026-10-13, informal_proof stage)

Verdict: sound; five minor gaps, all fixed in proof.md and check_proof.py (Review log has the details). No lemma changed. Status: CHECKPOINT_B. - Round at p = -1. L C> 00 (10)^q Z -> L 0101 C> 00 ... for every L: this is R_L'(1, ..) only when L = L'0 (blank left side included), one cell short of R_L(1, ..) when L ends in 1. Rules are now stated for p >= 0 with any L, and at p = -1 only with the blank left side; R_L(-1, ..) is only the name of a pop tape. New check MAC.round at p = -1. - NB. 2^(m-1) <= n derived from the overflow chain (m >= 2: n >= E_0 >= 2^(c+m+1) - 2^(c+2) + 4 - m + e >= 2^m; w = 1 via EQ1/EQ2); first half sharpened to n(F s) >= n - m, so a predecessor of (6,4,0) needs n <= 10 (checked to 12). - Route. proof.md section 6 is now one bounded statement U(N) (Lemmas J, K, Z', M for one level; Kp a case), by strong induction on the number of steps; non-halting is a second strong induction over cycles. Recommended Rocq route 3: forall N, ~ halts_in, lemma form "no halt within N, or a pop within N with (U1)-(U4)" (no abstract F, no pop uniqueness); TM.v has preceeds_halt / exceeds_halt / progress_nonhalt' (strong induction). - Notation. Bite level renamed m (f = first zero only); lattice bit b = b-th smallest cell; Z' composite form in the level's own frame (new check CF-J). - Omissions. B2 row: reparse, w >= 6, w = 1 bit-0-set case; Z = 111 at q = 2 halts (k = 0 form of H), never occurs; w = 1, v >= 1: E0 at m = 1 impossible (E_0~ >= 7). New ABS bite-width check (>= 6 at q = 0, 2; >= 5 at a phase bite; >= 4 for B1 after B2). - check_proof.py: default seed 1 81/81 PASS (107 s), quick seeds 1, 2 80/80; --full seed 1 partial: T..CH 74/74 and INV window w <= 24 PASS; its second INV window (w <= 14, n < 2^(cap+11)), random states and Z stopped unfinished after 35 min (overflow_count/outer_trace do not batch R1 rounds).

Kill

2026-10-13: KILLED_NONHALT, independently re-verified and packaged. - Audit (independent agent): check_kill --json PASS, exit 0 (2026-10-13T20:01:12Z; 17/17 sub-checks, compile 35.3 s native, coqchk -norec pass 4.6 s, busycoq 0940bb9 = pin); string byte-exact at 740 line 525 (778 line 558); .v read end to end (1039 lines, sha256 f61649bd...74fc), only Individual62 + stdlib, no Section/Module/Opaque/Hint/attributes, house-style header OK; Print Assumptions nonhalt closed. - Fresh check_kill for the package (2026-10-13T20:03:57Z): PASS, exit 0, compile 34.7 s native, coqchk pass 4.6 s, 0 assumptions. The .v is unchanged (same sha256 as rocq/W54.v and rocq/check_kill_round2.log). - Route of the .v (differs from proof.md §4-5 in organisation, not in substance): phase invariants Saf (Lemma P), KI (Lemmas K, A1), ZI (Lemma Z') kept by every round via phase; U(N) in CPS form with Post = U1-U4 plus U5 (a pop into w = 4, v = 0 has n' = 4 or n' >= 8), which replaces NB and its finite n <= 12 computation; no EQ1/EQ2; stack by STK/compose. - submission/: the .v (verbatim copy), proof.md (public write-up: plain opening, header with template and a .v map, sections 0-8 with the mathematics of the working proof.md minus check names and process notes, overflow "levels" renamed "stages", a new section 9 on the finished Rocq proof; writeup_lint 0 errors, 0 warnings), check_kill.txt (fresh run, local paths replaced by placeholders), README.md, discord.md (1,679 characters without the link; not posted; fill in , search #bb6 first). - Checkpoints A and B had no notes from Dennis on file at packaging; none to fold in. No siblings.