1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---: never halts

This machine never halts. Its tape holds a marker on the left, followed by a list of pairs: each pair is two blocks of cells plus one binary digit. Read together, the digits form a binary counter, and the machine counts it down by one at a time.

Each decrement updates the pairs up to the lowest digit 1. In every updated pair, one block grows by one unit and the other shrinks by one. When the shrinking block of the last updated pair runs out, that pair fuses with the next one.

When the counter reaches zero, the machine adds a short tail. When it reaches zero again, it regroups the blocks into new pairs, adds one more pair and starts the next countdown.

A few rare shapes of the tape are not covered by these rules, and some of them halt. The proof tracks how much room every block has left, and shows that the run never reaches such a shape.

Machine and status

• Machine: 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, viewer https://bbchallenge.org/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---
• Holdout: on the current BB(6) holdout list (class "Skelet 1-like Class 2").
• Written for: the string itself. There is no mirror or state permutation.
• Status: formalized. The accompanying verify/Skelet1LikeC2_1RB0LD.v (1,303 lines) proves Lemma nonhalt : ~ halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c).
• Print Assumptions nonhalt is closed, and coqchk passes.
• It compiles in about 71 s with the flags of verify/_CoqProject (-native-compiler yes). About 30 s of that is the 78,710-step init.

Template

The template is verify/SBCv6.v, Module TM21 (1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE), as a loose template only. TM21 is a different machine; apart from A0 = 1RB no transition is shared.

What carries over is the architecture:

• the configuration is a Fixpoint over a list of pairs;
• a countdown sweeps over that list;
• an overflow re-pairs the list;
• multistep_nonhalt + progress_nonhalt_cond conclude.

It differs from TM21 in four ways:

1. The macro step is one decrement, not a whole countdown (TM21's LIncs).
2. A pair whose q-block runs out mid-countdown fuses with the next pair. Here that is routine; TM21's LWF (q ≥ 2^len) rules it out.
3. Every pair carries a binary digit.
4. A second tail shape gives a detour (the rules X1 and X2).

TM21's LWF is replaced by the invariant J (§4).

Where each section lives in the .v

The full map is in §4.

Overview

Summary

The tape is a binary down-counter over a list of pairs, behind a left marker (§1). Write (10)^p for p copies of 10, and s(d) for the digit block of the digit d (defined in §1). A pair and the left marker are

pair [p,q,d] = (10)^p (01)^q s(d)
left marker  = (10)^h 11001

The p-block of a pair is its (10)^p part, and its q-block is its (01)^q part.

Each decrement (a step of the Dec family) subtracts 1 from the counter. It touches the pairs up to the borrow pair; a touch turns (p, q, d) into (p+1, q−1, digit flipped). A borrow pair whose q-block runs out fuses with the next pair.

At counter 0 an End sweep adds a tail. At the next 0 an overflow re-pairs the blocks as (q_j, p_{j+1}), adds a pair and resets h to 2.

When the top two pairs both reach q = 1 at counter 0 (rare), the run detours through a second tail shape (X1, X2).

Nine macro rules (§2) cover every configuration of the family except a few outside shapes, some of which halt. The proof shows that the run never reaches one.

The proof idea

1. The run alternates between two kinds of cycle: an E-cycle, which contains End, and an L-slot, which contains EndLast or ends with X1.

A re-pairing swaps the roles of p-blocks and q-blocks, so every block has a fixed class:

• Eq blocks (q-blocks in E-cycles) never shrink in scaled terms.
• Ep blocks (p-blocks in E-cycles) shrink, but they always have the good parity, so when one runs out the merge is a legal rule.

2. The far end of the list reduces to a four-way case split on one number x ≥ 3 (§3.4).

3. Both facts are packaged as a threshold invariant, INV+(e), on the configuration at the start of each E-cycle (§3.3, §3.8.1). Its constants are explicit: 5, 4, 3 and powers of two.

From a start that satisfies it, one cycle pair stays inside the rules and reaches a start that satisfies it again (§3.8). It holds at the E-start reached after 78,710 steps.

4. The .v proves this in a per-step form. A ghost-phase invariant J, stated on projected values that a touch leaves unchanged, is preserved by every macro rule (Jstep).

At every E-start, J implies clauses (b)–(e) of INV+(e) and a weaker form of (a) (§3.8.5, §4).

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 (the head in state B, reading the 0).

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 is of one of two kinds:

• an end touch flips the digit 1→0 (pair j is the borrow pair of that decrement);
• a pass touch flips the digit 0→1.

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

Notation used in the rules:

• Π_{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.

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 (direct simulation):

In random samples, 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, and let

K0 := K(2; (11,11,0); -)

Suppose every K reached from K0 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

This subsection states six lemmas, L1–L6. Below, v₂(x) is the exponent of the largest power of 2 that divides x.

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 a merge at pair k from counter x, with H = ⌊x/2^k⌋, the counter is V' instead of x − 1:

V'    = 2^(k−1) − 1 + H·2^(k−1)      (after the merge)
x − 1 = 2^(k−1) − 1 + H·2^k          (after a plain decrement)

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. With e the depth defined in §3.3, write

τ_j := 3·2^(e) − 1      for j ≥ 2
τ_1 := 3·2^(e) − 2

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. They are defined 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). Take a countdown that starts at counter V₀ on n₀ pairs and ends at V = 0 on N pairs after m merges. Its 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. There are two types:

• 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. So no q-defect ever runs out on the orbit (§3.6).

Depth and scaled value at an E-start. Let L be the number of pairs. Pair j has a depth e_j and a scaled value r_j:

L*  := L + 1  if T = T2  (X2 will append a pair),   L* := L  otherwise
e_j := L* − j
r_j := q_j / 2^(e_j)           for j ≥ 2
r_1 := (q_1 + 1) / 2^(e_1)

With this convention, pair j runs out in the E-cycle only if 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). We write INV for clauses (a)–(d), and INV+(e) for all five. §3.8.1 restates them 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, d_1 = d_L = 0 and d_j = 1 for 1 < j < L.
• (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*).

Clause (e) is needed: INV alone is not inductive (examples in §3.8.1). 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:

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 table agrees with the abstract run (the exact macro rules) for x = 1..15 (§5).

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. 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. Clause (e) bounds them, and their survival follows 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 rather than L*' = M, because interior merges can lower it; 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 Consequences: defects, the far end, and why this is not a cryptid

• 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). In particular, pair L−1 of an E-cycle is interior, so INV(b) covers it.
• The far end is always covered.
• 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 overflow 3. From overflow 6 on this is INV(d). Before that, it holds by exact computation.
• Clause (c) is essential.
• A q-defect in an Ep position would erode by 3 per cycle pair and would eventually run out at an outside case. INV(c) says the orbit never has such a defect.
• In simulation, configurations with a planted Ep defect do leave D, while configurations with a planted good Ep block stay in D, as 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). Three earlier configurations parse as K:

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 these steps:

Every transition from step 956 to 3·10^7 is the one the rules predict (§5). The base E-start, after overflow 6, satisfies INV+(e) (§3.3, §3.8.1).

In the .v, two lemmas cover this segment, and each is one esx run:

init0 : c0 -->* K 2 [(11,11,false)] TN      (K0, 956 steps)
init  : c0 -->* K 2 base TN                 (the base E-start above, 78,710 steps)

nonhalt uses init, so no chain of rule applications from K0 to the base is needed.

3.8 INV+(e): statement, lemmas and preservation proof

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]          ([T = T2] is 1 if T = T2, and 0 otherwise)
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, d_1 = d_L = 0 and d_j = 1 for 1 < j < L.
• (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.

Clause (e) is needed. Each configuration below satisfies (a)–(d) and has no empty block, but violates (e). Within one cycle pair, the run leaves D or reaches an E-start where INV+(e) fails.

None of them is reachable from the blank tape (there p_1 ≥ 2^(L*+2) − 1), and the machine runs on past each of these failures. They are failures of the argument under (a)–(d) alone, not halting configurations.

1. L* = 3; violates (e1) and (e2).

start: K(2; (7,19,0),(2,10,1),(1,6,1); −) L-start: 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).

2. L* = 4; violates (e1) and (e2).

start: K(2; (7,39,0),(2,20,1),(2,10,1),(2,6,1); −)

DecMerges at k = 2, 2 and 1 give K(114; (183,1,0),(5,1,0); −): the X1 shape with L = 2, (o4).

3. Violates (e1).

start: K(2; (7,15,0),(8,8,0); T2(4))

After one cycle pair it reaches K(2; (83,80,0),(2,18,1); −), with L* = 2, so (d) fails.

4. At threshold with L* = 20; violates (e1) and (e2).

p = (7, 2, …, 2, 1) q = (5·2^19 − 1, 5·2^18, …, 10, 6)

One cycle pair later the run reaches (o7).

5. Both halves of (e) are needed:

• K(2; (31,19,0),(2,10,1),(1,6,1); −) satisfies (e1) but not (e2), and one cycle pair later L* = 2;
• K(2; (7,19,0),(8,10,1),(1,6,1); −) satisfies (e2) but not (e1), and one cycle pair later L* = 2;
• K(2; (15,41,0),(8,17,1),(1,9,1); −) satisfies (e2) but not (e1), and its next E-start has p_2 = 6 < 8, so (e2) fails there.

Theorem (cycle pair). 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;
• 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 on the current n pairs:

V = Σ d_j 2^(j−1),      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),      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. 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

1. A plain Dec leaves Φ unchanged.
2. 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).
3. Because x ≤ 2^n − 1, we have H ≤ 2^(n−k) − 1, so the change is at least 2^(k−1) ≥ 1.
4. 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; exact form of L5). 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. So they also make sense in 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 and after it:

before: R_i = 2^(k−i) + H·2^(k−i+1) + c·2^(n−i) after: p_i has risen by 1, R'_i = 2^(k−i) − 1 + H·2^(k−i) + c·2^(n−1−i), 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; this is the bound quoted in §3.5.) 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)
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
 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 d_1 = d_L = 0, d_j = 1 in between, 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. ∎

Every displayed equality and inequality of §3.8.2–3.8.4 was also checked numerically, step by step, with exact rationals for s and exact integers for Φ (§5).

3.8.5 Integer form, and the per-step form proved in the .v

• Every clause of §3.8.1 is an integer inequality. A bound s_i ≥ σ becomes p_i + R_i ≥ σ·2^(e_i), with R_i written with division and powers of two.
• R_i and e_i are formulas in (n, V, phase, slot type), so the x = 3 and x = 5 slots need no special case.
• The .v proves the Theorem in a per-step form. Its invariant J is stated for every K of the run (with a ghost phase), not only for E-starts. Every macro rule preserves it (Jstep).
• For each pair, J bounds the projected values p + Rt and q − Rt. Here Rt is the number of touches the pair still gets before the next re-pairing if no further merge happens; in an L-slot it is the R_i of L5'. A touch leaves both projected values unchanged, so only merges and re-pairings need arithmetic.
• At an E-start, J implies clauses (b)–(e) of INV+(e). Of (a) it keeps only weaker bounds, which are all the per-step proof needs:
• p, q ≥ 1;
• h even and h ≥ 2;
• T = − at a regular start, with far pair q ≥ 3 and p + Rt ≥ 3;
• T2(k) with k ≥ 3 at a T2 start.
• p_1 ≥ 7 follows from (e1). J does not state h = 2 or the digit pattern; at an E-start these hold because the rules Ov and X1 produce them.
• Within an L-slot, J carries:
• the pair-1/pair-2 budget of §3.8.3, as lower bounds on q − Rt for pairs 1 and 2;
• a projected bound on h that does the work of L6;
• bounds p + Rt ≥ c·2^f, c ∈ {4, 5}, that do the work of L5' and C2;
• the goodness of the q-blocks below the x-pair;
• the far-end state.
• Inside E-cycles, the touch counts are exact (L3).

§4 gives the clauses in detail.

4. Mapping to busycoq

TM21 in verify/SBCv6.v (1RB1LB_0LC1RD_0RA1LC_0RB1RE_0RD0LF_---1LE) 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.

So the .v keeps TM21's architecture:

• a Fixpoint over the pair list as the configuration;
• the overflow as a list re-pairing;
• multistep_nonhalt + progress_nonhalt_cond (TM.v) at the end.

Each macro rule is one decrement, one End-type sweep or one re-pairing, proved from plain es sweep lemmas and list inductions, and LWF is replaced by the invariant J.

New compared with TM21:

• routine merges (DecMerge*, EndLast);
• binary digit tags;
• the X1/X2 detour through a second tail shape;
• the invariant J, a per-step form of clauses (b)–(e) of INV+(e), which replaces TM21's LWF.

How the .v file is organized

The .v imports Individual62 and the stdlib Arith, Lia, List, String and ZifyNat. Every lemma is top level (no Section, Module or Hypothesis).

The invariant J

• Per-step. 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: E-cycle after End;
• T0: T2 start, before X2;
• L1: L-slot before EndLast;
• L2: L-slot after EndLast;
• 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. Here 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.
• Every clause of J is a nat inequality on these projected values. For example, q >= tv + 3 * 2 ^ n + 1 for an Eq block in E1 is INV(b) projected. Only merges and re-pairings need arithmetic.
• At a regular E-start (phase E1, digits (0,1,…,1)), the clauses of J give (b)–(e) of INV+(e):
  • (b) is the Eq bound;
  • (c) is the parity (p + tv) mod 2 = 1;
  • (d) is 2 <= n for pair 1;
  • (e1) is 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);
  • (e2) is the corresponding clause for pair 2.
• Of (a), J gives only weaker bounds. The far pair (n = 0) has q >= tv + 2 ^ n + 1, which at the E-start (tv = 1) is q_L ≥ 3, not q_L ≥ 6. J does not state h = 2 or the digit pattern; at an E-start these hold because Ov and X1 produce them.
• T2 starts (phase T0) have their own scaled forms of (b)–(e). Of (a), TC gives only T = T2(k) with k ≥ 3, not k ≥ 4.
• L6 and L5' in projected form. The .v does not state L6 or L5' as separate lemmas.
• In place of L6 (pair 1 gets at least 2^(L*') − 2 touches in an L-slot), J carries a projected bound on h: h + 4 * Rt_1 + 6 >= 2^(L'+2), where L' is the L* that the next E-start would have if no further merge happened.
• With it comes the phase-L1 clause q + 2^n >= tv + 2, which says that merges in phase L1 happen only in its second half.
• In place of L5''s potentials s_i, J carries the bounds p + Rt >= c * 2^f with c = 4 or 5.
• The bounds r' > 2r − 3 and r' > 2r − 4 (C3) and the fusion bound of §3.5 are not used.
• Far end and parity.
• In E phases, the far pair also satisfies p + Rt >= 3, so x ≥ 3 at the Ov.
• In L phases, q-blocks at n ≥ 2 (phases L1 and LX) or n ≥ 1 (phase L2) have good parity, (q + tv) mod 2 = 0. The alternative q ≥ Rt + 1 is allowed only for the x-pair and the top pair.
• Start. init reaches the base E-start by direct execution (§3.7), and J_base checks J there.

5. Numerical checks

These checks use direct simulation of the transition table and an exact implementation of the macro rules (the abstract run). They are evidence only; the result rests on the .v file alone.

• Rules. Each of the nine rules matches direct simulation on 45 random instances (405 in all), with exact equality of (h, P, T) at the next canonical configuration.
• 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.
• Also exhaustively for L ≤ 3, p, q ∈ {1,2,3}, both digits, h = 0..3 and 5 tails (95,832 instances), and on 900 random instances up to size 300: 0 mismatches.
• Outside cases. The (o1), (o3) and (o6) examples of §2 halt after 1,480, 1,554 and 1,684 steps; the random-sample rates quoted in §2 are also by direct simulation.
• Initial segment. K0 is reached at step 956.
• From the blank tape.
• To 3·10^7 steps: 1,534 consecutive canonical transitions, all as the rules predict (Dec 1,496, End 9, EndLast 9, Ov 18, DecMerge 1, DecMergeTail 1).
• To 10^9 steps: 8,374 of 8,374 transitions, including X1 and X2.
• 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 an overflow: 24.
• The far-end table of §3.4 agrees with the abstract run (exact macro rules) for x = 1..15.
• The invariant along the abstract run, from overflow 5 to L = 600 (2,209 overflows, 1,102 cycle pairs, 3 X1 detours):
• 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;
• r never drops over an EndLast slot and drops by at most 1 over 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;
• every L-slot run-out is an interior Ep block or x.
• INV+(e), step by step. Every identity and inequality of §3.8 is 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.

These checks pass on:

• the orbit from the base (overflow 6) to L* = 300: 542 cycle pairs (539 EndLast slots, 3 X1 slots, 245 L-slot merges). Min p_1'/(2^(L*'+2) − 1) = 1.000 (tight, after X1 slots), and min p_2'/2^(L*') = 2.23;
• exhaustive boxes of 1,027,584 starts:
  • 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;
  • they give 1,027,584 cycle pairs, 96,768 X1 slots and 605,952 L-slot merges, and x = 3, 4, 5 and ≥ 6 all occur;
  • min p_1'/(2^(L*'+2) − 1) = 1.000, min p_2'/2^(L*') = 1.125 and min T1/(2^(L*') − 2) = 1.000, so (e) and L6 are tight;
• random chains: 20,000 chains of 6 cycle pairs, L* = 3..40, each value at its threshold with probability 1/2. That is 120,000 cycle pairs, 6,963 X1 slots and 254,112 merges.
• Necessity of (e). Each configuration listed in §3.8.1 satisfies INV(a)–(d), violates (e), and behaves as stated there within one cycle pair.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).