1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---: informal proof

Submission copy of the working proof.md, made 2026-10-10 after the kill. The mathematics is unchanged. Only these parts were updated: the title, the header (holdout line, status, AI line), the last paragraph of §3.7 (how the .v starts), and §4 (a new subsection on how the .v is organized and where it departs from the plan). Scripts it cites (check_proof.py and its helper scripts and Rocq scratch files) and the review files (review-invariant*.md) live in the working directory and are not in this folder. The two notes below are kept as review history; they were written for a per-cycle period lemma, which the .v replaced by a per-step invariant (§4).

Second skeptic (2026-10-10, review-invariant-2.md): INV+(e) is inductive; no fatal/major gap. Minor items for the Rocq period lemma: m2 — state the pair-1/pair-2 budget as a quantity of the current state (q_j >= R_j + 1 with L5's R_j); m3 — write the sigma phase and the tail-block test as conditions on the current state; m5 — §3.4 far-end table x=3 entry: use +6 when reading with L-start values; m6 — 'runs out iff r_j < 3' should be 'only if'; m7 — state the T2 digit pattern so it also covers L=2.

Repaired 2026-10-10 (revision 3). The skeptic found that INV (revision 2) was not inductive: it did not record lower bounds on the two newest Ep blocks p_1 and p_2. INV now has a clause (e): p_1 ≥ 2^(L*+2) − 1 and p_2 ≥ 2^(L*). Its preservation rests on a new lemma, L6: an L-slot that ends with L*' touches pair 1 at least 2^(L*') − 2 times. The proof is a potential-function argument. The three minor items (G2–G4) are fixed too. For the Rocq period lemma, the invariant is INV+(e). Its statement, the lemmas and the full preservation proof are in §3.8. The counterexamples to revision 2 are kept in the review log (§6.2). check_proof.py §G checks (e), L6 and the L5 potential identities on the orbit, on 1,027,584 exhaustive starts and on random chains.

• Machine: 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, viewer https://bbchallenge.org/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---
• Holdout lists: on every holdout-list snapshot we have, from 2024-06-14 (12,091) to 2026-10-07 (778; line 53). Sheet: "Skelet 1-like Class 2", Results row 1278, no notes. No Discord thread found (our notes).
• Written for: the string itself (no mirror, no relabelling).
• State of the argument (revision 3, 2026-10-10). Sections 1–2 (family and rules) are unchanged, and every rule passes the random-instance checks.
• Revision 2 replaced the two open lemmas of revision 1 (O1, O2) with one invariant, INV, and a proof that INV carries over from one cycle pair to the next (§3.3–§3.5). The idea: every block of the tape has a fixed class. Blocks of one class never shrink in scaled terms. Blocks of the other class shrink, but always have the good parity, so when they run out the merge is legal. The far end then reduces to a four-way case split on one number x ≥ 3.
• Revision 3 adds clause (e) to INV and the lemma L6 that preserves it. It also replaces L5's "merge-free continuation" with an explicit potential, and collects the whole preservation proof in §3.8, which is the reference for formalization.
• check_proof.py §F checks every clause of INV, and every identity the proof uses, at every cycle to L = 600. §G checks INV+(e), L6 and the L5 identities step by step: on the orbit, on 1,027,584 exhaustive small starts, and on random chains.
• Status: fully formalized, killed. 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.v (1,303 lines) proves Lemma nonhalt : ~ halts tm c0. in Coq 8.20.1 against unmodified busycoq (commit 0940bb9c). check_kill (our checker) PASS on 2026-10-10: compile 71.1 s with -native-compiler yes (about 30 s of it is the 78,710-step init), Print Assumptions nonhalt closed, coqchk pass in 24.7 s (check_kill.txt). The review log is at the end.
• The .v does not formalize §3.8's per-cycle argument line by line. It proves a per-step invariant J that contains INV+(e) in projected form at every E-start (§4, "How the .v file is organized"). So the kill does not depend on the prose of §3.3–3.8 being right; that prose is the explanation, and the second skeptic review (header note above) found no fatal or major gap in it.
• AI assistance: this text and the Coq formalization were produced with the help of Claude (Anthropic). The kill rests on the .v file, checked by our checker, check_kill.

0. Machine and the halting transition

Only C1 enters F, and only B0 enters C. So the machine halts exactly when it reaches B> 0 1 1.

1. Family

A pair block and a digit block are

[p,q,d] := (10)^p (01)^q s(d)        s(1) := 0001,  s(0) := 0010

The family is

K(h; P; T) := 0^inf <A (10)^h 11001 [p_1,q_1,d_1] [p_2,q_2,d_2] ... [p_L,q_L,d_L] T 0^inf

  P = ((p_j,q_j,d_j))_{j=1..L},  L >= 1,  p_j >= 1,  q_j >= 1,  d_j in {0,1},  h >= 0
  T in { -,  T1(t) := (10)^t 1  (t >= 1),  T2(k) := (101)^2 (01)^k  (k >= 1) }
  V := sum_j d_j 2^(j-1)        (binary number; d_1, next to the head, is the least significant digit)

The head is in state A on the blank cell just left of the word. Every K reached from the blank tape has h ≡ 2 (mod 4), but the rules hold for every h ≥ 0.

A touch of pair j is the update (p_j, q_j, d_j) -> (p_j+1, q_j-1, 1-d_j). On the tape, the (10)|(01) split moves 2 cells to the right and the digit block flips. A touch that flips the digit 1→0 is an end touch (pair j is the borrow pair of that decrement); one that flips 0→1 is a pass touch.

2. Rules (macro steps; each is an exact run of at least 1 step from one K to the next)

Notation: Π_{j<k}[...] is a product over pairs; R is everything to the right of the touched pairs, tail included, and it is unchanged. The rules cover every K, except the "outside" cases listed after the table.

Let k := least j with d_j = 1 (when V > 0).

Dec_k          q_1..q_{k-1} >= 2, q_k >= 2:
  0^inf <A (10)^h 11001 Π_{j<k}[p_j,q_j,0] [p_k,q_k,1] R 0^inf
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<k}[p_j+1,q_j-1,1] [p_k+1,q_k-1,0] R 0^inf

DecMerge_k     q_1..q_{k-1} >= 2, q_k = 1, k < L:
  ... Π_{j<k}[p_j,q_j,0] [p_k,1,1] [p',q',d'] R
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<k}[p_j+1,q_j-1,1] [p_k+p'+3, q', d'] R

DecMergeTail   q_1..q_{L-1} >= 2, k = L, q_L = 1, T = T1(t):
  ... Π_{j<L}[p_j,q_j,0] [p_L,1,1] (10)^t 1 0^inf
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<L}[p_j+1,q_j-1,1] (10)^(p_L+t+3) 1 0^inf

DecMergeEmpty  as DecMergeTail but T = -:          ... [p_L,1,1] 0^inf --> ... (10)^(p_L+2) 1 0^inf

End            V = 0, T = -, all q_j >= 2:
  0^inf <A (10)^h 11001 Π_{j<L}[p_j,q_j,0] [p_L,q_L,0] 0^inf
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<L}[p_j+1,q_j-1,1] [p_L+1,q_L-1,0] (10)^1 1 0^inf

EndLast        V = 0, T = -, q_1..q_{L-1} >= 2, q_L = 1:
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<L}[p_j+1,q_j-1,1] (10)^(p_L+4) 1 0^inf

Ov             V = 0, T = T1(t), p_1 >= 2:
  0^inf <A (10)^h 11001 Π_{j<=L}[p_j,q_j,0] (10)^t 1 0^inf
  --> 0^inf <A (10)^2 11001 [h+5, p_1-1, 0] Π_{j=1..L-1}[q_j, p_{j+1}, 1] [q_L, t+1, 1] 0^inf

X1             V = 0, T = -, L >= 3, q_1..q_{L-2} >= 2, q_{L-1} = q_L = 1, p_1 >= 2:
  0^inf <A (10)^h 11001 Π_{j<=L}[p_j,q_j,0] 0^inf
  --> 0^inf <A (10)^2 11001 [h+5, p_1-1, 0] Π_{j=1..L-3}[q_j, p_{j+1}, 1] [q_{L-2}, p_{L-1}, 0] (101)^2 (01)^(p_L+3) 0^inf

X2             V = 0, T = T2(k), all q_j >= 2:
  0^inf <A (10)^h 11001 Π_{j<=L}[p_j,q_j,0] (101)^2 (01)^k 0^inf
  --> 0^inf <A (10)^(h+4) 11001 Π_{j<L}[p_j+1,q_j-1,1] [p_L+1,q_L-1,0] [3, k, 1] 0^inf

In words, each Dec* subtracts 1 from V: pairs 1..k are touched. End* and X2 touch every pair; they behave like a decrement from 0 that the tail absorbs. Ov and X1 re-pair the blocks, so that the old splits become the new digit blocks, and they reset h to 2. Physically, a decrement is three short bounces at the left end followed by one sweep to the borrow pair and back (diagrams in img/).

Outside cases are the K for which no rule above applies: - (o1) Some pass-through pair j < k has q_j = 1. - (o2) k = L, q_L = 1 and T = T2. - (o3) V = 0, T = -, and some q_j = 1 with j ≤ L−1, but the shape is not X1. - (o4) The X1 shape with L ≤ 2 or p_1 = 1. - (o5) Ov with p_1 = 1. - (o6) X2 with some q_j = 1. - (o7) L = 0.

At least (o1), (o3) and (o6) can halt (check_proof.py §B, informational): - (o1) K(6; (5,1,0),(7,4,1); −) halts after 1,480 steps. - (o3) K(2; (6,1,0),(5,8,0),(11,2,0),(12,3,0); −) halts after 1,554 steps. - (o6) K(6; (9,1,0),(5,4,0); T2(5)) halts after 1,684 steps.

In the reviewer's random sampling, 45 of 56 (o1) instances, 24 of 35 (o3) and 27 of 44 (o6) halted. The others jump to an unrelated K. Either way, the proof must keep the orbit out of (o1)–(o7), and it does so without using what the machine does there.

3. Argument

3.1 Reduction

Let D be the set of K that some rule covers. Suppose every K reached from K0 := K(2; (11,11,0); -) is in D. Then the run is an infinite chain of rule applications, each taking at least 1 step, so the machine never halts. This is multistep_nonhalt + progress_nonhalt_cond (§4). The halting cell B> 0 1 1 is never presented: each rule is an exact computation from K to K, and the machine halts only on reading F1.

Two facts hold at all times: - p_1 ≥ 7. Each Ov or X1 creates a new pair 1 with p = h+5 ≥ 7; touches only increase p, and so does a merge into pair 1. This rules out (o5) and the p_1 condition of (o4). - No block is ever empty. A q that reaches 0 is merged away in the same rule, and p values start at 1 or more and never decrease.

Everything else, including L ≥ 3 (which rules out (o7) and the L condition of (o4)), is part of the invariant INV+(e) below (§3.3, stated in full in §3.8).

3.2 Counter lemmas

• L1 (touch counts). In a countdown from V, the decrement x → x−1 touches pairs 1..v₂(x)+1. Pair j is touched ⌊V/2^(j−1)⌋ times, and its touches alternate between end and pass. A merge at pair k leaves the touch counts of the pairs to its right unchanged, and it can only lower those of pairs j < k. (After the merge the counter is V' = 2^(k−1) − 1 + H·2^(k−1), where H = ⌊x/2^k⌋, instead of x − 1 = 2^(k−1) − 1 + H·2^k.)
• L2 (parity). A touch preserves q+d mod 2, p+d mod 2 and p+q. A pair runs out (q: 1 → 0) on an end touch exactly when q+d is even. Call a pair with q+d even good. When a good pair runs out, the DecMerge family applies. A good pair is never a pass-through with q = 1, because q = 1 and d = 0 would make q+d odd. A pair with q+d odd is a q-defect; if it ever ran out, that would be (o1), (o3) or (o6).
• L3 (cycle touches). Define the two cycle types as in §3.3. Within each type, the touch counts are exact as long as no merge occurs. Write τ_j := 3·2^(e) − 1 for j ≥ 2 and τ_1 := 3·2^(e) − 2, with e the depth defined in §3.3:

At the closing Ov of an E-cycle, h + 5 = 2 + 4τ_1 + 5 = 3·2^(L+1) − 1. Each row is a sum of ⌊V/2^(j−1)⌋ terms from L1. For example, the first row for j ≥ 2 is (2^(L−j+1) − 1) + 1 + (2^(L−j) − 1). - L4 (parity across a re-pairing).* At an Ov all d_j = 0. The Ov sends p_j to q_j and q_j to p_{j+1}, and its new pairs j ≥ 2 get d = 1. Therefore: - A p-block with p+d odd becomes a good q-block, and a good q-block becomes a p-block with p+d odd. - The new pair 1 has p = h+5, which is odd, with d = 0. Its q = p_1 − 1 is good when p_1+d was odd.

X1 acts the same way, except on its top pair [q_{L−2}, p_{L−1}, 0]. There d = 0, so a good q-block arrives as a p-block with p+d even. The following X2 adds 1 to that p and leaves d = 0, which makes p+d odd again. - L5 (merges never hurt a p-block, in scaled terms). Let pair i hold a p-block during an L-slot, with current value A, depth e and remaining touches R. Here R and e are what the block would get if no further merge happened; revision 3 defines them by an explicit formula (the potential s_i of §3.8.2), which also makes sense in x = 3 and x = 5 slots, where every real run merges at the far end. Let a DecMerge or DecMergeTail occur at a pair k > i. - By the counter formula in L1, the remaining touches afterwards satisfy R' = R/2 + 2^(k−i−1) − 1 ≥ R/2. Here R counts the touch of the merge step itself. This holds for both countdowns: the EndLast touch plus the second countdown, 2^(M−i) touches, becomes 2^(M−1−i). - The block gains the touch of the merge step, and its depth becomes e − 1. So its end-of-slot scaled value satisfies (A + 1 + R')/2^(e−1) = (A + R)/2^e + (A + 2^(k−i))/2^e, which is more than (A + R)/2^e + A/2^e. - By induction over the merges, a merge to the right never lowers a p-block's end-of-slot scaled value, and it adds more than A/2^e. The exact statement and proof are L5' in §3.8.2. - L6 (pair-1 touches in an L-slot; new in revision 3). In a countdown that starts at counter V₀ on n₀ pairs and ends at V = 0 on N pairs after m merges, the number of steps D satisfies D ≥ V₀ − 2^(n₀) + 2^N + m. So an L-slot that ends with L*' touches pair 1 at least 2^(L*') − 2 times (3·2^(L*'−1) − 2 if it is an EndLast slot). The proof is in §3.8.2. This lemma preserves clause (e).

3.3 Cycles, classes and the invariant

A cycle is the run of macro steps from one re-pairing (Ov or X1) to the next. Its start is the K right after the re-pairing. An E-cycle is a cycle that contains End (it may begin with X2). An L-slot is a cycle that contains EndLast or ends with X1. §3.4 shows that every cycle is exactly one of these and that the two types alternate.

Classes. A re-pairing swaps roles (p_j → q_j, q_j → p_{j+1}). Merges keep roles: two p-blocks fuse into a p-block. So, given the alternation, every block has a fixed role in all E-cycles: - Eq blocks are q-blocks in E-cycles and p-blocks in L-slots. In scaled terms they do not change: what they lose in an E-cycle they get back in the next L-slot (§3.5). - Ep blocks are p-blocks in E-cycles and q-blocks in L-slots. They lose 3·2^e per cycle pair, so they run out, and every merge is the run-out of an Ep block.

All parity defects sit in Eq blocks (INV(c)). Merges are run-outs of Ep blocks, which are good. This is why the "race" of revision 1 does not occur on the orbit (§3.6).

Depth and scaled value at an E-start. Let L be the number of pairs. Set L := L + 1 if T = T2 (X2 will append a pair), and L := L otherwise. Pair j has depth e_j := L − j. Its scaled value is r_j := q_j / 2^(e_j) for j ≥ 2, and r_1 := (q_1 + 1)/2^(e_1). With this convention, pair j runs out in the E-cycle iff r_j < 3 (L3). The interior pairs are j ≤ L − 1: all pairs but the last at a regular start, and all L pairs at a T2 start. The last pair at a regular start is the far pair.

INV+(e) (at an E-start). Clauses (a)–(d) are revision 2's INV; clause (e) is new in revision 3. §3.8.1 restates all five as integer inequalities. - (a) shape. h = 2 and p_1 ≥ 7. Then either - regular: T = −, digits (0,1,…,1), and a far pair (p_L, q_L, 1) with p_L ≥ 1 and q_L ≥ 6; or - T2 start: T = T2(k) with k ≥ 4 and digits (0,1,…,1,0). - (b) Eq bound. Every interior pair has r_j ≥ 5, or r_j ≥ 4 at a T2 start. - (c) Ep parity. Every interior pair has p_j + d_j odd. The one exception is the top pair at a T2 start, which has d = 0 and p even. - (d) size. L ≥ 3. - (e) newest Ep blocks. p_1 ≥ 2^(L+2) − 1 and p_2 ≥ 2^(L*).

Without (e), the invariant is not inductive: §6.2 lists starts that satisfy (a)–(d) and leave D within one cycle pair. Clause (e) is what makes pairs 1 and 2 survive the L-slot (§3.8.3).

Theorem. If INV+(e) holds at an E-start, then every K up to the next E-start is in D, and INV+(e) holds again there (proof: §3.4–3.5, collected and completed in §3.8.4). INV+(e) holds at the E-start after overflow 6 (step 78,710): K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); −). There r = 8.625, 8.25, 7.5, L* = 4, p_1 = 95 ≥ 63 and p_2 = 34 ≥ 16. Every K from K0 to that point is in D by exact computation (§3.7). So every reachable K is in D, and the machine never halts (§3.1).

3.4 One cycle pair, given INV+(e)

S1 (the E-cycle). This part uses only (a) and (b). - Nothing runs out. The q-blocks are the interior Eq blocks, which have q_j ≥ 4·2^(e_j) > τ_j, and the far pair's q (≥ 6, losing 2) or the appended pair's q (k ≥ 4, losing 2). p-blocks only grow. So no rule of the DecMerge family occurs, and L3's touch counts are exact. - Every side condition holds. At every moment, an interior q is at least q_j − τ_j ≥ (r_j − 3)·2^(e_j) + 1 ≥ 3, and pair 1's q is at least 2^(L−1) + 1. That covers every pass-through condition (no (o1)), End's "all q ≥ 2" (no (o3)) and X2's "all q ≥ 2" (no (o6)). The top pair at a T2 start is interior, so its q is at least 3 too. - The T2 countdown runs 2^(L−1) − 2 decrements, which never touch the top pair. Its digit 0 is the top bit, and V < 2^(L−1). So (o2) cannot occur. T2 is created only by X1 and removed only by X2, so it exists for exactly this one countdown. - The cycle ends with Ov on T1(1), because End creates T1(1) and nothing touches the last pair afterwards. - x := the p of the last pair at that Ov. At a regular start, x = p_L + 2 ≥ 3, since the far pair gets exactly 2 touches. At a T2 start, x = 3 + 2 = 5. So x ≥ 3 always.*

S2 (the L-slot). It starts with M = L + 1 ≥ 4 pairs, digits (0,1,…,1) and T = −. The blocks are: - the q-blocks q_1..q_{M−2}: interior Ep blocks, good by INV(c) and L4. q_1 and q_2 never run out* (§3.8.3, which uses (e)), so every merge of the slot is at a pair k ≥ 3; - q_{M−1} = x; - the last pair (t₀, 2, 1), where t₀ is the old far q.

The first countdown runs from 2^M − 2: - Interior Ep run-outs are legal. An interior Ep block that runs out does so on an end touch (L2). The x-pair and the last pair are above it, so DecMerge applies at some k ≥ 3 below the x-pair. Pass-throughs have q ≥ 2 (L2). By L1, these merges do not change the touch counts of the x-pair and the last pair. - The far end follows a fixed schedule. The last pair gets one end touch (q = 1, d = 0). Pair M−1 gets three touches: end, pass, end. Then:

This is the endgame table of revision 1 (check_proof.py §E2 replays it), now with x ≥ 3 proved. Indices M−1 and M are those at the L-start. Earlier interior merges shift both pairs down by one index each, but by L1 they change nothing else, so the table is stated relative to the current top two pairs.

The second countdown (after EndLast, all digits 1) touches each pair at most as often as L3 says (L1): - Interior run-outs are legal DecMerges. - A run-out of the current last pair is an end touch by a good block, or by x = 5, so DecMergeTail applies. Such run-outs may cascade, and every link is legal. DecMergeEmpty never occurs, because T = T1 after EndLast.

The slot ends with V = 0 and T = T1(t), t ≥ 5 (EndLast gives t = p+4 ≥ 5, and DecMergeTail only adds). So Ov applies (p_1 ≥ 7), and the next start is regular, with far pair (q, t+1, 1), where q ≥ 1 and t+1 ≥ 6.

This proves INV(a), and the alternation: after an E-cycle the last pair has q = 2, so the next cycle is an L-slot; after an L-slot the far q is ≥ 6 (or the T2 shape), so End, not EndLast, ends the next countdown.

3.5 INV(b)–(e) carry over (narrative; the complete proof is §3.8.4)

Persisting Eq block, at interior pair j of an E-start with value Q and depth e: - EndLast slot, no merges. The E-cycle takes exactly τ_j. The Ov moves the block to p_{j+1} at the same depth (M − (j+1) = e). The merge-free EndLast slot gives back 3·2^(M−j−1) − 1 = τ_j (for j = 1, τ_1 + 1, which is the +1 in r_1). The next Ov moves it to q_{j+1}, again at depth e. So r' = r exactly. - X1 slot. It gives back only 2^(e+1) − 1, so r' = r − 1. - With merges to the right (L5): r' ≥ r, or ≥ r − 1 in an X1 slot. With at least one such merge, r' > r + (r − 3) = 2r − 3 in an EndLast slot. In an X1 slot, L5 gives only r' > (r − 1) + (r − 3) = 2r − 4 (corrected in revision 3). The T2-start threshold needs only r − 1 ≥ 4, so 2r − 4 is enough.

The thresholds then work out as follows: - After a regular start, an EndLast slot keeps r ≥ 5. - An X1 slot follows only a regular start, because a T2 start gives x = 5. It leads to a T2 start, with r ≥ 4. - The slot after a T2 start has x = 5, so its second countdown contains a DecMergeTail, a merge to the right of every interior block. That gives r ≥ 2·4 − 3 = 5.

New Eq block from the head. - The p_1 = 3·2^M − 1 created at an L-start becomes q_1 at the next E-start. - After a merge-free EndLast slot: q_1 = 9·2^(M−1) − 4 with L* = M, so r_1 = 9 − 3/2^(M−1) ≥ 8.6. - After an X1 slot: q_1 = 2^(M+2) − 4, so r_1 = 8 − 3/2^(M−1) ≥ 7.6. - Merges only raise these values (L5).

New Eq block from a fusion. - A DecMerge at interior k in an L-slot fuses p_k and p_{k+1}. These are Eq blocks that were q_{k−1} and q_k at the E-start, with scaled values r_a and r_b. Since q_1 and q_2 never run out (§3.8.3, which uses (e)), k ≥ 3, and so k−1 ≥ 2. - The fused block inherits pair k+1's remaining touches (L1), and at the next Ov it lands at q_k's old depth. - At the merge, p_k ≥ Q_a − τ_a, and p_{k+1} plus its remaining touches gives back Q_b. So the fused value is at least (Q_a − τ_a) + Q_b + 3, and r_F ≥ 2(r_a − 3) + r_b. In an X1 slot it is r_F ≥ 2(r_a − 3) + r_b − 1. - After a regular start this is ≥ 9 (or ≥ 8 in an X1 slot). After a T2 start it is ≥ 2·1 + 4 = 6. - Fusing a block that was itself fused in the same slot only adds non-negative terms. Eq blocks taken into the far end (DecMerge at M−1, DecMergeTail, EndLast) become tail blocks. Tail blocks never become interior, so INV(a) is the only thing asked of them.

This proves INV(b) at the next E-start.

INV(c). An interior p-block at an E-start is an Ep block. Only the head creates new ones, as the p_1 = h+5 of a regular start, which is odd with d = 0: - E-cycles have no fusions (S1). - Fusions in L-slots join p-blocks of the L-slot, which are Eq blocks. - X2's block 3 is the far pair's p, not an interior block. - The old x never becomes interior. It is consumed (x ∈ {3, 4, 5}) or stays the far p.

L4 carries goodness across every Ov and X1, with the T2-start exception already in the statement of INV(c).

INV(d) and (e). At an L-start, q_1 and q_2 are the two newest Ep blocks. Revision 2 bounded them using values left by earlier cycles, which INV did not record; that was the gap (§6.2). Clause (e) now records them, and the bounds follow from (e) alone (§3.8.3): - q_1 = p_1 + τ_1 − 1 ≥ 11·2^(L−1) − 4 against at most 3·2^(L) − 2 touches; - q_2 = p_2 + τ_2 ≥ 7·2^(L−2) − 1 against at most 3·2^(L−1) − 1 touches.

Neither runs out, so pairs 1 and 2 survive every slot. Because M ≥ 4, these pairs are distinct from the far pairs, and the next start has L ≥ 3. After X1, the bound is L ≥ 4, not L* = M: interior merges can lower it (revision 3). Pairs 1 and 2, the x-pair and the last pair are all present at X1. Clause (e) carries over by L6 (§3.8.4).

3.6 What this replaces, and why the reviewer's races do not apply

• Old O1 (interior defects never run out). Every q-defect is an Eq block (INV(c)), and Eq blocks never run out (S1: q_j ≥ 4·2^e > τ_j in E-cycles; in L-slots they are p-blocks). The pair L−1 of an "odd" cycle, which is an E-cycle, is interior, so INV(b) covers it.
• Old O2 (far-end eras).
• x ≥ 3, because x = p_L + 2 and blocks are never empty, and S2 is exhaustive for x ≥ 3.
• The T2 clauses follow from the top-digit argument in S1.
• The last pair's q at X2 is the X1-time p_{L−1}. At the T2 start it is the top pair's q, an interior Eq block at depth 1, so INV(b) gives q ≥ 4·2 = 8. The T2 countdown does not touch it, so it is still ≥ 8 at X2.
• L ≥ 2 after Ov 3. Covered by INV(d) from overflow 6 on. Before that, by exact computation.
• The reviewer's perturbation runs planted defects into reachable configurations. A defect planted in an Ep position erodes by 3 per cycle pair and loses the race, as observed. INV(c) says the real orbit never has such a defect. Planted good segments, which are legal Ep blocks, never exited, which is also what the proof predicts.
• Not a cryptid. INV+(e) is a threshold invariant with explicit constants (5, 4, 3, and the powers of two in (e)). It is preserved by affine bookkeeping and the binary-counter lemmas L1, L5 and L6. No pseudo-random arithmetic enters.

3.7 Initial segment and base case

0^inf A> 0^inf reaches K0 = K(2; (11,11,0); −) after exactly 956 steps (direct simulation, check_proof.py §C). Three earlier configurations parse as K: - step 8 is K(0; −; −), with L = 0; - step 275 is K(2; (7,1,0); −). It is in D: EndLast applies and predicts the next configuration exactly. That successor, step 451's K(6; −; T1(11)), has L = 0 and is outside D; - step 451 is that successor.

So the machine passes through L = 0 before K0, and the argument starts at K0. From K0 the rules apply at once: End at step 1240, then Ov at step 1845.

Overflows 1–6 follow at steps 1845, 4610, 8319, 19436, 34137 and 78710. All transitions from step 956 to 3·10^7 are rule-predicted (§D), which covers the base. The base E-start, after overflow 6, satisfies INV+(e) (§3.3, §3.8.1). In the .v, init0 : c0 -->* K 2 [(11,11,false)] TN (K0, 956 steps) and init : c0 -->* K 2 base TN (the base E-start above, 78,710 steps) are each one esx run. nonhalt uses init, so the finite chain of rule applications from K0 to the base is not needed; the rule-by-rule path is a cross-check only.

3.8 INV+(e): statement, lemmas and preservation proof (revision 3; reference for the Rocq period lemma)

This subsection is self-contained. It restates the invariant and proves the lemmas it needs. It then gives the complete argument that one cycle pair stays in D and re-establishes the invariant. §3.4–3.5 are the narrative version; where they differ, this subsection is authoritative.

3.8.1 Statement

The setting is an E-start K(h; P; T) with L pairs. Let L* := L + [T = T2] and e_j := L* − j. The interior pairs are j = 1..L*−1. INV+(e)(K) is the conjunction of: - (a) h = 2; p_j ≥ 1 and q_j ≥ 1 for all j; p_1 ≥ 7. Then either - regular: T = −, digits d = (0,1,…,1), p_L ≥ 1 and q_L ≥ 6; or - T2 start: T = T2(k), k ≥ 4, L ≥ 2 and d = (0,1,…,1,0). - (b) The bound uses θ := 5 at a regular start and θ := 4 at a T2 start: - for interior j ≥ 2: q_j ≥ θ·2^(e_j); - for j = 1: q_1 + 1 ≥ θ·2^(e_1).

In scaled terms, r_j ≥ θ. - (c) For interior j, p_j + d_j is odd. The exception is j = L at a T2 start, where d_L = 0 and p_L is even. - (d) L* ≥ 3. - (e) (e1) p_1 + 1 ≥ 2^(L*+2), and (e2) p_2 ≥ 2^(L*).

At the base E-start K(2; (95,68,0),(34,33,1),(10,15,1),(1,24,1); −), L* = 4, and every clause holds: - (b): 69 ≥ 40, 33 ≥ 20 and 15 ≥ 10; - (c): 95, 35 and 11 are odd; - (e): 96 ≥ 64 and 34 ≥ 16.

At regular starts the proof actually gives p_1 ≥ 3·2^(L*+1) − 1, which is tight at the base (95). The uniform (e1) is all the proof needs, and it is what check_proof.py §G checks.

Theorem (period). Suppose INV+(e)(K) holds at an E-start K. Follow the macro steps from K through the next two re-pairings. Then every configuration on the way is in D, and the configuration K' right after the second re-pairing satisfies INV+(e)(K'). There are at least two macro steps, and each one takes at least one machine step.

3.8.2 Counter facts, and the lemmas L6 and L5'

A countdown is a maximal run of Dec-family steps (Dec, DecMerge, DecMergeTail). During a countdown, the digits form a counter V = Σ d_j 2^(j−1) on the current n pairs, so 0 ≤ V ≤ 2^n − 1. A step at counter value x > 0 has borrow pair k = v₂(x) + 1 and touches pairs 1..k. Write x = H·2^k + 2^(k−1), with H := ⌊x/2^k⌋; H = 0 when k = n. - A plain Dec sets V := x − 1. - A merge at k (DecMerge_k with k < n, or DecMergeTail with k = n) sets n := n − 1 and V := V' := (2^(k−1) − 1) + H·2^(k−1). Pairs 1..k−1 get digit 1, pair k disappears, and the digits above it move down one index unchanged.

Three facts follow: - (F1) Every step touches pair 1. - (F2) V' ≤ x − 1, because H·2^(k−1) ≤ H·2^k. Take a pair j < k: the step touches it, and ⌊V'/2^(j−1)⌋ ≤ ⌊(x−1)/2^(j−1)⌋. So (touches of pair j so far) + ⌊V/2^(j−1)⌋ never increases while pair j exists. Hence in a countdown from V₀, pair j is touched at most ⌊V₀/2^(j−1)⌋ times. - (F3) The pairs above k keep their digits, and the counter restricted to them counts down exactly as before. So pairs above every merge get exactly their merge-free touches, in the same order (L1).

Lemma L6 (new). Let a countdown start at V₀ on n₀ pairs and end at V = 0 on N pairs, after m merges and D steps in all. Then D ≥ V₀ − 2^(n₀) + 2^N + m.

Proof. Let Φ := (steps so far) + V − 2^n. A plain Dec leaves Φ unchanged. A merge at k from x = H·2^k + 2^(k−1) changes Φ by 1 + V' − x + 2^(n−1) = 2^(n−1) − H·2^(k−1). Because x ≤ 2^n − 1, we have H ≤ 2^(n−k) − 1, so the change is at least 2^(k−1) ≥ 1. Hence Φ_end ≥ Φ_start + m, that is, D − 2^N ≥ V₀ − 2^(n₀) + m. ∎

Corollary (pair-1 touches in an L-slot). Take an L-slot that starts on M pairs at counter 2^M − 2. Let N₁ be the number of pairs when its first countdown ends. In an EndLast slot, let N_f be the number of pairs at the closing Ov. The slot is a first countdown followed either by X1, or by EndLast, a second countdown and Ov, and pair 1 is never merged (§3.8.4 Step 2 and §3.8.3).

Let T1 be the number of macro steps of the slot before its closing re-pairing. Every such step is a Dec-family step or EndLast, and each touches pair 1 once, so T1 is also the number of touches of pair 1. Then: - the first countdown has D₁ ≥ 2^(N₁) − 2 steps (L6 with V₀ = 2^M − 2 and n₀ = M); - X1 slot: T1 = D₁ and L*' = N₁, so T1 ≥ 2^(L*') − 2; - EndLast slot: EndLast leaves N₁ − 1 pairs, all with digit 1, at counter 2^(N₁−1) − 1. So the second countdown has D₂ ≥ 2^(N_f) − 1 steps, and T1 = D₁ + 1 + D₂ ≥ 2^(N₁) + 2^(N_f) − 2. Since L*' = N_f + 1 ≤ N₁, this gives T1 ≥ 3·2^(L*'−1) − 2 ≥ 2^(L*') − 2.

Lemma L5' (the potential s; replaces L5's "merge-free continuation"). Fix an L-slot. The x-block at the L-start fixes its type: it is X1 type if x = 4 and EndLast type otherwise (§3.4 S2).

At any moment, with n pairs and counter V, assign to the p-block of pair i:

R_i := ⌊V/2^(i−1)⌋ + c·2^(n−i), e_i := n − i + δ, s_i := (p_i + R_i)/2^(e_i),

where (c, δ) is: - (1, 0) before EndLast in an EndLast-type slot; - (0, 1) after EndLast; - (0, 0) in an X1-type slot.

R_i is the number of touches the block would still get if no merge happened from now on, and e_i is the depth it would then have at the next E-start. Both are defined by the formula, whether or not the real run merges. This answers the x = 3 and x = 5 slots, where every real run merges at the far end.

1. A plain Dec leaves every s_i unchanged, and so does EndLast.
2. A merge at k changes s_i as follows (values before the step): - for i < k, s_i rises by exactly (p_i + 2^(k−i))/2^(e_i); - the fused block of DecMerge_k, the new pair k, has s_F = s_(k+1) + (p_k + 3)/2^(e_(k+1)); - a block at i > k + 1 keeps its s and moves to index i − 1.
3. At the end of the slot (V = 0 after EndLast, or at X1), s_i = r'_i. This is the scaled value of pair i at the next E-start, with r'_1 = (q'_1 + 1)/2^(e'_1).
4. At the L-start, M = L* + 1 and the head block is p_1 = 3·2^M − 1: - s_1 = 9 − 3/2^(M−1) in an EndLast-type slot, or 8 − 3/2^(M−1) in an X1-type slot; - for 2 ≤ i ≤ M − 1, pair i holds the Eq block of interior pair i − 1 of the E-start, and s_i = r_(i−1) (EndLast type) or r_(i−1) − 1 (X1 type).

Proof. 1. A plain step at x touches pair i iff 2^(i−1) | x. When it does, ⌊V/2^(i−1)⌋ drops by exactly 1 and p_i rises by 1; n and the phase do not change. Now take EndLast at V = 0 on n pairs. Before it, R_i = 2^(n−i) and e_i = n − i. After it there are n − 1 pairs, V = 2^(n−1) − 1 and δ = 1, so p_i has risen by 1, R_i = 2^(n−i) − 1 and e_i = n − i. 2. Take i < k. Before the step, R_i = 2^(k−i) + H·2^(k−i+1) + c·2^(n−i). After it, p_i has risen by 1, R'i = 2^(k−i) − 1 + H·2^(k−i) + c·2^(n−1−i) and e'_i = e_i − 1. Then 2(p_i + 1 + R'_i) − (p_i + R_i) = p_i + 2^(k−i), which gives the stated rise. - The fused block has p = p_k + p(k+1) + 3. Its R after the step is H + c·2^(n−1−k). That equals R_(k+1) before the step, because the step does not touch pair k+1 and ⌊x/2^k⌋ = H. Its e equals e_(k+1). - For i > k + 1, use F3: the shift leaves n − i unchanged. 3. At the end, R_i = 0. - Ov on n pairs sends p_i to q'_i, and p_1 to q'_1 = p_1 − 1. It makes L*' = n + 1, so e'_i = n + 1 − i = e_i (here δ = 1). - X1 on n pairs does the same for i ≤ n − 1, with L*' = n (here δ = 0). 4. By S1, the Eq block of interior pair j = i − 1 enters the slot as p_i = Q − τ_j, at depth M − i = L* − j. At the L-start its R is ⌊(2^M − 2)/2^(i−1)⌋ + c·2^(M−i): 3·2^(M−i) − 1 in an EndLast-type slot, 2^(M−i+1) − 1 in an X1-type slot. Compare τ_j = 3·2^e − 1, or 3·2^e − 2 for j = 1, which is where the +1 in r_1 comes from. The head block p_1 = 3·2^M − 1 is h + 5 at the E-cycle's Ov (L3). Its R_1 is 3·2^(M−1) − 2 (EndLast type) or 2^M − 2 (X1 type), at depth M − 1. ∎

Corollaries. These hold as long as no merge happens at k ≤ 2 (§3.8.3), given INV(b) at the E-start. A tail block is the last pair's p-block t₀, or any block fused with it (only the x = 3 far merge does that). Tail blocks are absorbed by EndLast or X1 and are never interior. - (C1) s_i never decreases while its block exists, and a fused block starts above its right part: s_F > s_(k+1). - (C2) A-bound. Every non-tail p-block of a pair i ≥ 2 has p_i ≥ 2^(e_i) + 1 throughout the slot. - For a block of the E-start: p_i ≥ Q − τ = (r − 3)·2^(e₀) + 1 ≥ 2^(e₀) + 1, since r ≥ 4 by INV(b). Also e_i ≤ e₀, because e drops by 1 at a merge to the block's right and no other step changes it. - For a fused block: p_F > p_k ≥ 2^(e_k) + 1 = 2^(e_F + 1) + 1, and e_F can only drop afterwards.

So, for i ≥ 2, a merge to the right of pair i raises s_i by more than 1, and a fusion gives s_F ≥ s_(k+1) + 2. - (C3) (Informational: the corrected "2r − 3".) Suppose a block of the E-start, with value r, sees at least one merge to its right. The first such merge happens at depth e₀, when p ≥ (r − 3)·2^(e₀) + 1, so r' > s_start + r − 3. That gives r' > 2r − 3 in an EndLast slot and r' > 2r − 4 in an X1 slot.

3.8.3 Pairs 1 and 2 survive the L-slot (uses (e))

At the L-start (M = L* + 1), Ov has made pair 1 = (h+5, p_1^Ov − 1, 0) and pair 2 = (q_1^Ov, p_2^Ov, 1), with p_j^Ov = p_j + τ_j (S1). So, by (e):

q_1^L = p_1 + τ_1 − 1 ≥ (2^(L*+2) − 1) + (3·2^(L*−1) − 2) − 1 = 11·2^(L*−1) − 4, q_2^L = p_2 + τ_2 ≥ 2^(L*) + 3·2^(L*−2) − 1 = 7·2^(L*−2) − 1.

As long as neither has run out, they stay pairs 1 and 2, because merges at k ≥ 3 do not move them. By F2, their touches in the slot are at most: - pair 1: (2^M − 2) + 1 + (2^(M−1) − 1) = 3·2^(L*) − 2 in an EndLast-type slot, or 2^M − 2 in an X1-type slot; - pair 2: (2^(M−1) − 1) + 1 + (2^(M−2) − 1) = 3·2^(L*−1) − 1.

These use the fact that the second countdown starts at 2^(N₁−1) − 1 ≤ 2^(M−1) − 1. For L* ≥ 2, 11·2^(L*−1) − 4 ≥ (3·2^(L*) − 2) + 1 and 7·2^(L*−2) − 1 ≥ (3·2^(L*−1) − 1) + 1. So each of q_1 and q_2 is ≥ 2 before each of its touches and ≥ 1 after the last one. By induction over the steps of the slot, neither runs out, neither is a pass-through with q = 1, and every merge of the slot is at k ≥ 3.

3.8.4 Proof of the Theorem

Assume INV+(e) at an E-start with L*.

Step 1: the E-cycle (§3.4 S1; uses (a) and (b)). - No merge occurs, and the touch counts are exactly τ_j (L3). - The cycle is [X2,] End, Ov, and it ends at Ov on T1(1). - At that Ov, h + 5 = 3·2^(L*+1) − 1. - x ≥ 3: x = p_L + 2, or 5 after X2.

Every K is in D.

Step 2: the L-slot is in D (§3.4 S2 together with §3.8.3). The L-start has M = L* + 1 ≥ 4 pairs, digits (0,1,…,1) and T = −. - Pairs 1..M−2 hold good q-blocks (INV(c) and L4). Pair 1's q = p_1^Ov − 1 is even with d = 0. The T2 top pair has odd p at its Ov, thanks to X2's non-flipping touch. - Pair M−1 holds x with d = 1, and pair M is (t₀, 2, 1).

In both countdowns: - Pairs 1 and 2 never run out, and are never a pass-through with q = 1 (§3.8.3). - Every other q-block below the x-pair is good. So it is never a pass-through with q = 1 (q is even at a pass touch), and it runs out only on an end touch (L2). - If a pair lies above it, DecMerge applies. - If it is the top pair, DecMergeTail applies. That happens only after EndLast, when T = T1. - DecMergeEmpty never occurs. Before EndLast, the x-pair and the last pair lie above every other pair. The last pair gets a single end touch, which leaves q = 1 and digit 0. - The x-pair and the last pair follow the S2 table (F3). - The x-pair's only pass touch meets q = x − 1 ≥ 2. - The x-pair runs out on an end touch: legally as a DecMerge into the last pair (x = 3), or as DecMergeTail (x = 5). - Each countdown ends at V = 0. There every pair below the far pairs is good with d = 0, so its q is even and ≥ 2. - After the first countdown, EndLast applies (x = 3, x = 5 or x ≥ 6), or X1 applies (x = 4, n ≥ 4, p_1 ≥ 7). - The second countdown ends with Ov (T = T1(t), p_1 ≥ 7).

So every K of the slot is in D. Formally, Step 2 and §3.8.3 are one induction over the steps of the slot. As long as every step so far was a rule application and pairs 1 and 2 are intact, the next step is a rule application (the bullets above), and pairs 1 and 2 stay intact (the budget of §3.8.3).

Step 3: INV+(e) at the next E-start K'. Let m be the number of merges in the slot. Then L*' = M − m ≤ L* + 1. In an EndLast slot, EndLast and Ov cancel. In an X1 slot, X1 turns N₁ pairs into N₁ − 1 pairs plus T2, so L*' = N₁. - (a) Ov and X1 set h = 2, and p_1' = h + 5 ≥ 7. - Regular K': Ov gives digits (0,1,…,1). The far pair is (q of the top pair at the end, t + 1, 1), with that q ≥ 1 and t ≥ 5 (EndLast gives t = p + 4, and DecMergeTail only adds). So q_L' ≥ 6. - T2 start K': X1 gives digits (0,1,…,1,0) and T2(p_M + 3). The last pair's p is t₀ + 1, and t₀ = q_L − 2 ≥ 4, because an X1 slot follows a regular start (a T2 start gives x = 5). So k ≥ 8. - (d) Pairs 1 and 2 survive (§3.8.3), so a regular K' has N_f + 1 ≥ 3 pairs. A T2 start K' comes from X1 on N₁ pairs. Pairs 1 and 2, the x-pair (q = 1, not run out) and the last pair are distinct, because M ≥ 4. So N₁ ≥ 4 and L*' = N₁ ≥ 4. - (e1) h starts at 2, and every step of the slot adds 4, so p_1' = h + 5 = 4·T1 + 7. By the L6 corollary, this is ≥ 4·(2^(L*') − 2) + 7 = 2^(L*'+2) − 1. At a regular K', p_1' ≥ 3·2^(L*'+1) − 1. - (e2) Ov, and X1 with N₁ ≥ 4, both send q_1 at the end of the slot to p_2'. So p_2' = q_1^L − T1 ≥ (11·2^(L*−1) − 4) − (3·2^(L*) − 2) = 5·2^(L*−1) − 2 ≥ 2^(L*+1) ≥ 2^(L*'), since L* ≥ 2 and L*' ≤ L* + 1. In an X1 slot, T1 ≤ 2^M − 2, so the margin is even larger. - (b) The interior q-blocks of K' are exactly the p-blocks of pairs 1..L*'−1 at the end of the slot. Their scaled values are their s (L5'.3). - These blocks are the head block, blocks of the E-start, and fused blocks. Tail blocks are absorbed by EndLast, X1 or DecMergeTail: t₀, and the x-block's p in slots with x ∈ {3, 5}. - Let θ' be the threshold that K' needs: 5 for a regular K', 4 for a T2 start K'. - By L5'.4 and C1, every non-tail block has s ≥ σ throughout the slot, where: - after a regular start (r ≥ 5): σ = 5 in an EndLast slot (the head has 9 − 3/8), and σ = 4 in an X1 slot (the head has 8 − 3/8). An X1 slot leads to a T2 start, so σ ≥ θ' in both cases; - after a T2 start (r ≥ 4): x = 5, so the slot is EndLast type and σ = 4. In its second countdown the x-block runs out by DecMergeTail at the top pair. That is a merge to the right of every block then present. By C2 it adds more than 1 to each block at i ≥ 2, and the head has s ≥ 8.6 anyway. A block fused later has s_F > s_(k+1) ≥ 5. So every block left at the end has s ≥ 5 = θ'. - Hence r'i ≥ θ' for every interior pair of K'. - (c) The interior p-blocks of K': - Pair 1's p is h + 5, odd, with d = 0. - For 2 ≤ i ≤ L*' − 1, pair i's p is q(i−1) at the end of the slot, a q-block below the top pair. Every q-block below the x-pair is good, and so is the q-block of a fused pair, which is that of pair k+1. At the end V = 0, so d = 0 and q is even. Ov or X1 gives the new pair d = 1, so p + d is odd. - At a T2 start K', X1's top pair [q_(N₁−2), p_(N₁−1), 0] has p = q_(N₁−2), which is even (good with d = 0), and d = 0. This is the exception in (c). - The top q-block at an Ov becomes the far pair's p, which is not interior. It is the x-pair for x ≥ 6, and a good block otherwise.

So INV+(e)(K') holds. ∎

check_proof.py §G checks every displayed equality and inequality of §3.8.2–3.8.4, step by step. It uses exact rationals for s and exact integers for Φ. The checks run on the orbit, on 1,027,584 exhaustive starts and on 120,000 random chained cycle pairs (§5).

3.8.5 Notes for the Rocq period lemma

• Invariant: INV+(e) of §3.8.1, in the integer forms given there.
• Loop invariant J inside a slot:
• the pair-1/pair-2 budget: q_j ≥ (remaining touch bound) + 1, from §3.8.3;
• Φ ≥ Φ_start + (merges so far), from L6;
• s_i ≥ σ, and the A-bound p_i ≥ 2^(e_i) + 1 for i ≥ 2, from L5' and C2;
• every q-block below the x-pair is good;
• the far end is in one of the S2 rows.

Inside E-cycles, J is the exact touch counts. - Integer forms: all of these are integer inequalities. Multiply s_i by 2^(e_i), and write R_i with div and pow. - No special case for x = 3 and x = 5: these rows need no "merge-free continuation". R_i and e_i are formulas in (n, V, phase, slot type).

4. Mapping to busycoq, and what is new

TM21 in verify/SBCv6.v is a loose template only: - Its LIncs packages a whole countdown, k = 2^len − 1 head visits, as one sideRLs over hLR2^^k, built per pair with segRLs. - It has no per-decrement rule and no borrow-chain relation. - Its Ov/Ov_S is the re-pairing at overflow. - Its LWF (q ≥ 2^len) forbids merges, and LIncs's uniform k-visit composition breaks when a segment runs out mid-countdown. Here that happens routinely.

Route chosen: (a), per-decrement macro lemmas plus progress_nonhalt_cond over E-starts.

Option (b) was also considered: extend TM21's segRLs/LIncs with a lemma for a segment that runs out at visit i and fuses with the next segment. It was not chosen, because fusions can cascade within one countdown and (a) reuses one per-decrement lemma for all of them. segRLs_sideRLs_concat (Individual.v) is not needed under (a).

New compared with TM21: routine merges (DecMerge*, EndLast); binary digit tags; the X1/X2 detour through a second tail shape; the class invariant INV+(e), whose clauses (b), (c) and (e) replace TM21's LWF.

How the .v file is organized

The table above is the plan as written before the .v. The .v follows route (a), with one change: there is no per-cycle period lemma. It imports Individual62 and the stdlib Arith, Lia, List, String and ZifyNat. Every lemma is top level (no Section, Module or Hypothesis).

Where it departs from the plan: - Per-step, not per-cycle. The state is (h, P, T, phase, c4), and every macro rule is one step of progress_nonhalt_cond. The ghost phase records where the run is in the two-cycle period: E1/E1t (E-cycle before End, after a regular or a T2 start), E2/E2t (after End), T0 (T2 start, before X2), L1 (L-slot before EndLast), L2 (after EndLast) and LX (an L-slot that ends with X1). c4 marks an L-slot after a T2 start, before its DecMergeTail. - Projected values. For pair j, Rt_j = tv_j + (phase term) is the number of touches it still gets before the next re-pairing, where tv_j is the digit value from pair j up (dv) and the phase term is 2^n, 5·2^n or 0. A touch keeps p + Rt and q − Rt fixed. So every clause of J is stated on these projected values as a nat inequality (for example q >= tv + 3 * 2 ^ n + 1 for an Eq block in E1, which is INV(b) projected), and only merges and re-pairings need arithmetic. At a regular E-start (phase E1, digits (0,1,…,1)) J's clauses give INV+(e): (b) the Eq bound, (c) the parity (p + tv) mod 2 = 1, (e1) p + tv + 2 ^ n + 3 >= 11 * 2 ^ n for pair 1, which at tv = V = 2^L − 2 and n = L − 1 is p_1 + 1 ≥ 2^(L+2), and (e2) for pair 2. T2 starts (phase T0) have their own scaled forms. - No L6 or L5'. L6 (pair 1 gets at least 2^(L') − 2 touches in an L-slot) is replaced by a projected bound on h (h + 4 * Rt_1 + 6 >= 2^(Lproj+2)) together with the L1 clause q + 2^n >= tv + 2, which says merges in L1 happen only in its second half. L5''s potentials s_i are replaced by the bounds p + Rt >= c * 2^f with c = 4 or 5. The bounds r' ≥ 2r − 3 / 2r − 4 (G3) and the fusion bound are not used. - Two clauses the plan did not have. The far pair in E phases also has p + Rt >= 3, so x ≥ 3 at the Ov. L-phase q-blocks at n ≥ 2 (L1, LX) or n ≥ 1 (L2) must have good parity; the "Qhat ≥ 1" alternative is allowed only for the x-pair and the top pair. - No finite chain from K0. init reaches the base by direct execution (§3.7).

5. Evidence (python3 check_proof.py, defaults; about 5 min)

check_proof.py is self-contained: its own simulator, parser and abstract map, independent of our other scripts and tools. The SUMMARY line is PASS only if A, C+D, E, E2, F and G all pass. B is informational. --only-g runs section G alone; --sweep full runs G3 on the full 1,027,584-start boxes.

• §A, rules. Every rule passes 45/45 random instances, 405 in all: Dec, DecMerge, DecMergeTail, DecMergeEmpty, End, EndLast, Ov, X1 and X2.
• Sizes 2–4, 2–30 and 60–300; L = 1–5 (X1: L = 3–5); all h mod 4; all three tails for the Dec family.
• Each instance is checked by direct simulation to the next canonical configuration, with exact equality of (h, P, T).
• The reviewer also checked independently: exhaustive for L ≤ 3, p, q ∈ {1,2,3}, both digits, h = 0..3 and 5 tails (95,832 instances), plus 900 random instances up to size 300, with 0 mismatches.
• §B, outside cases (informational). The (o1), (o3) and (o6) examples halt after 1,480, 1,554 and 1,684 steps. The others land on unrelated K.
• §C, initial segment. K0 is reached at step 956.
• §D, cross-check from the blank tape.
• To 3·10^7 steps: 1,534 consecutive canonical transitions, all predicted by the abstract map (Dec 1,496, End 9, EndLast 9, Ov 18, DecMerge 1, DecMergeTail 1).
• Observe stage, to 10^9 steps: 8,374 of 8,374 transitions, including X1 and X2 (notes.md). The reviewer counted 8,375 of 8,375.
• §E, abstract run to L = 300.
• No configuration outside D; 1,086 Ovs, about 2^304 decrements. Rule counts: End 545, EndLast 541, DecMerge 240, DecMergeTail 5, X1 3, X2 3. DecMergeEmpty never occurs.
• L2 holds on every plain decrement batch.
• Minimum scaled q of a q-defect at overflow: 24.
• §E2 replays the endgame table for x = 1..15 and now returns FAIL on any mismatch.
• §F, the invariant (new). Segment tracking along the abstract run, from overflow 5 to L = 300 by default. The same check was run separately to L = 600 (2,209 overflows, 1,102 cycle pairs, 3 X1 detours). It checks:
• the alternation, and that E-cycles are exactly [X2,] End, Ov;
• L3's exact touch counts τ_j for every interior pair;
• INV(b): min r = 7.5 at regular starts and 7.906 at T2 starts. New head blocks have r ≥ 7.99 and new fused blocks r ≥ 27;
• that r never drops after an EndLast slot and drops by at most 1 after an X1 slot;
• INV(c), and INV(d) (min M = 4);
• x = p_L + 2 (or 5), so x ≥ 3, with all three residues of x mod 3 seen;
• that every L-slot run-out is an interior Ep block or x.
• §G, INV+(e) (revision 3). Every check is an exact identity or inequality from §3.8, evaluated at every step of every cycle pair:
• E-cycle events and τ_j; h+5 = 3·2^(L*+1) − 1; x ≥ 3;
• the L-start shape and goodness; q_1, q_2 against their touch bounds; no merge at k ≤ 2;
• L6's Φ: unchanged by plain Dec, rising by exactly 2^(n−1) − H·2^(k−1) ≥ 2^(k−1) at each merge; D₁ ≥ 2^(N₁) − 2 + m₁, D₂ ≥ 2^(N_f) − 1 + m₂, T1 ≥ 2^(L*') − 2;
• L5': s_i unchanged by plain Dec and EndLast, the exact merge and fusion increments, the L-start values (r, r − 1, 9 − 3/2^(M−1), 8 − 3/2^(M−1)), s = r' at the end; the A-bound;
• the run-out bookkeeping: only interior Ep blocks or the x-block run out, and the x-block only for x ∈ {3, 5}, with the S2 outcome for each x;
• p_1' = 4·T1 + 7, p_2' = q_1 at the end, L' = M − merges ≤ L + 1, L*' ≥ 4 after X1, and INV+(e) at the next E-start.
• G1: the skeptic's starts (§6.2) satisfy INV(a)–(d), violate (e), and leave D or break INV within one cycle pair under INV alone. The checker also flags them when they are fed to it directly.
• G2: the orbit from the base (overflow 6) to L = 300: 542 cycle pairs (539 EndLast slots, 3 X1 slots, 245 L-slot merges), all checks pass; min p_1'/(2^(L'+2) − 1) = 1.000 (tight, after X1 slots), min p_2'/2^(L*') = 2.23.
• G3, exhaustive boxes (L = 3, 4; regular and T2 starts; every value at its threshold or a few steps above, p_1 and p_2 at their (e) minima; far p_L = 1..10 or 1..8, so x = 3..12 or 3..10): default 9,936 starts. --sweep full runs the skeptic's boxes, 1,027,584 starts: all pass (2026-10-10: 1,027,584 cycle pairs, 96,768 X1 slots, 605,952 L-slot merges; x = 3, 4, 5 and ≥ 6 all exercised; min p_1'/(2^(L'+2) − 1) = 1.000, min p_2'/2^(L') = 1.125, min T1/(2^(L') − 2) = 1.000, so (e) and L6 are tight).
• G4, random chains: default 2,000 chains × 6 cycle pairs, L* = 3..40, each value at its threshold with probability 1/2: 12,000 cycle pairs, 25,635 merges, all pass. A separate run of 20,000 chains × 6 (--nrand 20000): 120,000 cycle pairs, 6,963 X1 slots, 254,112 merges, all pass.
• Necessity of both halves (G1):
  • K(2; (31,19,0),(2,10,1),(1,6,1); −) satisfies INV + (e1), and one cycle pair later L* = 2.
  • K(2; (7,19,0),(8,10,1),(1,6,1); −) satisfies INV + (e2), and one cycle pair later L* = 2.
  • The review's K(2; (15,41,0),(8,17,1),(1,9,1); −) satisfies INV + (e2), and the next start has p_2 = 6 < 8, so (e2) fails there.
• Not done: low-level step formulas, which are not needed for progress_nonhalt_cond.

6. Review log

6.1 Skeptic review of revision 1 (2026-10-10)

6.2 Skeptic review of revision 2: INV not inductive (2026-10-10; review-invariant.md)

The reviewer wrote independent code: a simulator, a parser, the abstract map, an accelerated countdown and block tracking. It found one fatal gap and three minor ones. Everything else in §3.3–3.5 was attacked and held: L1, L3, L5, the fusion bound, the head block, X1/X2, the far-end table, INV(a)–(c) and the base.

Counterexamples to revision 2's INV, kept for the record. Each satisfies INV(a)–(d), p_1 ≥ 7 and non-empty blocks. None is reachable from the blank tape (on the orbit p_1 ≥ 2^(L*+2) − 1), and the machine itself runs on through each. They are gaps in the proof, not halting witnesses. 1. K(2; (7,19,0),(2,10,1),(1,6,1); −), L* = 3. The L-start is K(2; (47,16,0),(9,7,1),(5,3,1),(4,2,1); −), with x = 3. DecMerges at k = 3 and then k = 2 lead to EndLast with L = 1, then DecMergeTail, then K(66; −; T1(102)): L = 0, (o7). Violates (e1) and (e2). 2. K(2; (7,39,0),(2,20,1),(2,10,1),(2,6,1); −), L* = 4. DecMerges at k = 2, 2 and 1 give K(114; (183,1,0),(5,1,0); −): X1 shape with L = 2, (o4). Violates (e1) and (e2). 3. K(2; (7,15,0),(8,8,0); T2(4)). After one cycle pair, K(2; (83,80,0),(2,18,1); −), with L* = 2. Violates (e1). 4. At threshold with L* = 20: p = (7,2,…,2,1), q = (5·2^19 − 1, 5·2^18, …, 10, 6). One cycle pair later it reaches (o7). Violates (e1) and (e2). 5. Both halves of (e) are needed: - K(2; (31,19,0),(2,10,1),(1,6,1); −) satisfies (e1) but not (e2), and reaches L* = 2; - K(2; (7,19,0),(8,10,1),(1,6,1); −) satisfies (e2) but not (e1), and reaches L* = 2; - K(2; (15,41,0),(8,17,1),(1,9,1); −) satisfies (e2) but not (e1), and its next start has p_2 = 6 < 8.

Scale of the failure under revision 2's INV (the reviewer's exhaustive boxes, at the same values check_proof.py --sweep full now passes with (e)):