/machines/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF/submission/proof.md · raw

1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF: never halts

Summary. The tape is a stack of runs of 1s, and the machine is a recursive counter. One "epoch" starts and ends with the head at the left edge, and the leftmost frame has a budget of 3 child creations per epoch. The machine halts exactly when that budget runs out. An epoch on a word T(a,b)+N replays the machine's own history one level down, on the marker word N, for a-1 epochs. Each inner epoch costs 2, or 3 when it absorbs a marker. The absorption law (§3) says exactly when the cost is 3. Its proof is an induction on (epoch index + number of markers), carried by an invariant on the shape and positions of the markers. The top level is the marker-free orbit, so every top-level epoch costs 2 and the budget never runs out.

0. Notation

Tape notation: l <A r means A is reading the last cell of l.

Run configurations. For L = [a_1..a_p] (a stack, top = a_p) and R = [c_1, g_1, c_2, g_2, ..., c_r]:

conf(L, R) := 0^inf 1^a_1 0 1^a_2 0 ... 0 1^a_p <A 0 1^c_1 0^g_1 1^c_2 0^g_2 ... 1^c_r 0^inf
domain:  every a_i >= 1, c_i >= 1, g_i >= 1, and g_1 >= 2.   (p = 0 means 0^inf <A 0 1^c_1 ...)

R always has odd length and ends with a run. I call the entries of L frames and a_p the top frame.

Words. A word is an R-shaped list. The edge configuration of a word is Edge(W) := conf([], [3,2]+W). - Marker word: M = [g_1,1, g_2,1, ..., g_m,1] (lone 1s), with every g_i >= 2 even. Write #M = m. - Absorption indices: I_j(M) := sum_{i<=j} (g_i - 1) for j = 1..m, and I_0 := 0. They are strictly increasing, and I_j ≡ j (mod 2) because each g_i - 1 is odd. Write I(M) = {I_1..I_m}. - Tail: N = [], or an even-length list N = [g_1, c_2, g_2, c_3, ..., g_k, c_(k+1)] (a gap first, then run and gap alternating) with every entry >= 1 and g_1 >= 2. For every x >= 1, [x]+N is then a word in the domain. Every marker word is a tail. The epoch rules of §2 are stated for tails; the invariant of §3 uses marker words. - T(a,b)+N := [a,2,b]+N, a T-word. S(a,b)+N := [2,2,a,2,b]+N, an S-word. In §3, N is a marker word; in §2's rules it may be any tail. S(a,b)+N is also T(2,a)+[2,b]+N, where [2,b]+N is a tail but not a marker word when b >= 2. On orbit words the invariant says which reading is meant, and Rule S (§2) handles the S reading directly. - For a T- or S-word, aff := b + 1 - a. For aff >= 0, this counts the internal markers the next replay will absorb; aff = -1 denotes the merged-marker case.

1. TM-level rules

The --- is E0. Shift rules (each by induction on n):

CW   C> 1^n 1        -->  1^n C> 1        3n steps   [C1 B1 B0 per cell: 0RB, 1LB, 1RC]
DW   D> 1^n          -->  1^n D>          n steps    [D1]
FW   1^n <F          -->  <F 1^n          n steps    [F1]

Macro rules. l and r are arbitrary. All parameters are >= 0.

R1   l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r  -->  l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r      3m+2x+15
     = A1 C1 B1 B0 C1 B0 · CW(m) · C1 B0 C0 · DW(x+2) · D0 E1 · FW(x+1) · F0
R3   0^inf <A 0 1^(k+1) 0 0 1^m 0 r       -->  0^inf 1^(k+2) <A 0 1^(m+1) 0 0 r           3k+2m+11
     = A0 B0 · CW(k) · C1 B0 C0 · DW(m+2) · D0 E1 · FW(m+1) · F0
R2   l 1^(j+1) 0 1^(k+1) 0 1 <A 0 r       -->  l 1^(j+1) <A 0 1^(k+2) 0 0 r               k+10
     = A1 C0 · DW(3) · D0 E1 · FW(k+2) · F0
R2e  0^inf 1^(k+1) 0 1 <A 0 r             -->  0^inf <A 0 1^(k+2) 0 0 r                   k+10   (same transitions)
HALT 0^inf 1 <A 0 r                       -->  A1 C0 D0, then E reads 0: halt (3 steps)

Inside R1 and R3: after C1 B0 C0 the tape reads ... 0 1^(m+1) 0 D> 1 1 1^x 0 r. DW walks over the x+2 ones, D0 writes 0 and turns, E1 erases the last 1, FW walks back, and F0 lands A on the last 1 of 1^(m+1). In the .v these are tR1, tR3 and tR2, each proved by one es, and tR3c (R3 at the left edge), proved by one const_unfold rewrite of const 0 followed by es; R2e is tR2 with l = const 0.

1.1 The run model (Lemma RM)

Every conf(L,R) in the domain moves by exactly one rule below. The result is again in the domain.

push   (p = 0, or a_p >= 2):   R3 if p = 0, pushing c_1+1;  R1 if p >= 1, setting a_p := a_p - 1 and pushing c_1.
       In both cases R becomes:  g_1 = 2:  [c_2+1, g_2+1, c_3, ...]   (just [c_2+1] if r = 2)
                                 g_1 >= 3: [1, g_1-1, c_2, g_2, ...]  (just [1] if r = 1)
pop    (a_p = 1, p >= 2):      L := [a_1..a_(p-2)],  R := [a_(p-1)+1, 2] + R      (R2, or R2e when p = 2)
halt   (a_p = 1, p = 1):       HALT

Matching against §1: with g_1 = 2, R1/R3 take x = c_2, and the 0 after 1^x is the first cell of 0^g_2. With g_1 >= 3 they take x = 0, so 0 0 1^0 0 = 0^3 is the start of 0^g_1. With r = 1, the rest is 0^inf. The pop rule needs a single 0 between frames, which the domain gives. The constraints are preserved: a new first gap is g_1-1 >= 2, g_2+1 >= 2 or 2.

Frame reading. A push decrements the top frame (its payment) and creates a child frame. A frame is top only when it has just been created, or right after its child and grandchild were popped together (the grandchild finished). In both cases it then pays for one child (re)creation. When a frame is top with value 1, it finishes: it is popped together with its parent, and the parent goes back into R with value +1. The grandparent then pays to re-create the parent. HALT is a depth-1 frame that has to pay with value 1.

2. Epoch rules

Epoch. Run from Edge(W) until L = [] again. The run ends at conf([], [5-c, 2]+W'). Write Ep(W) = (c, W'), with cost c ∈ {1,2,3}. The first step R3 creates the edge frame E with value 4. E pays once for each child it creates, and the epoch ends when E's current child finishes (the R2e step). So c is the number of children E created, and HALT happens exactly when an epoch would need a 4th. For a tail N, put W_0(N) := [1]+N and, as long as the epochs exist, (c_i, W_(i+1)(N)) := Ep(W_i(N)). The orbit of a marker word M is O_n(M) := W_n(M) = Ep^n([1]+M) (the cost is dropped).

Every rule below is an exact run of the run model. Macro-step lists are in order.

U0   Ep([1])           = (2, [2,2,1])                    R3 R1 R1 R2 R1 R1 R1 R2 R2e      (9)
U1   Ep([1,g]+rest)    = (2, [2,2,1,g-2]+rest)           g >= 4, rest arbitrary           (9)
U2   Ep([1,2,b]+N)     = (2, [b+2,2,1]+N)                b >= 1, N a tail                 (9)
TR   Edge(T(a,b)+N)  -->  conf([2,a], [b+2,2,1]+N)       a >= 2, b >= 1, N a tail         (8: R3 R1 R1 R2 R1 R1 R1 R2)
TL   conf(L0+[y], [z,2]+W)  -->  conf(L0+[y-1], [z-c+1,2]+W')
         if Ep(W) = (c,W') in k macro steps, y >= 2, z >= c+1, L0 arbitrary                  (k)
TF   conf([2,1], [z,2]+W)  -->  conf([], [3,2,z,2]+W)                                        (1: R2e)
X    conf([2,2], [2,2,a'',2,b'']+rest)  -->  conf([], [2,2,a''+2,2,b''+2]+rest+)
         a'' >= 2, b'' >= 1, rest arbitrary; rest+ = rest with its first gap +2               (10)

U1 trace (rest = [c_2, ...]): ([4],[2,g+1,..]), ([3,2],[1,g,..]), ([3,1,1],[1,g-1,..]), ([3],[2,2,1,g-1,..]), ([2,2],[2,g,..]), ([2,1,2],[1,g-1,..]), ([2,1,1,1],[1,g-2,..]), ([2,1],[2,2,1,g-2,..]), ([],[3,2,2,2,1,g-2,..]). U0 is the same with R = [2], [1], .... U2 goes ([4],[2,3,b,..]), ([3,2],[1,2,b,..]), ([3,1,1],[b+1,g_1+1,..]), ([3],[2,2,b+1,..]), ([2,2],[b+2,g_1+2,..]), ([2,1,b+2],[1,g_1+1,..]), ([2,1,b+1,1],[1,g_1,..]), ([2,1],[b+2,2,1,g_1,..]), ([],[3,2,b+2,2,1,g_1,..]).

TR trace (N = [g_1, ...]): ([4],[a+1,3,b,g_1,..]), ([3,a+1],[1,2,b,g_1,..]), ([3,a,1],[b+1,g_1+1,..]), ([3],[a+1,2,b+1,g_1+1,..]), ([2,a+1],[b+2,g_1+2,..]), ([2,a,b+2],[1,g_1+1,..]), ([2,a,b+1,1],[1,g_1,..]), ([2,a],[b+2,2,1,g_1,..]). The frame Y with value a now sits on E = 2, and the word right of the head is [b+2,2] + W_0(N). The trace reads nothing of N beyond g_1, and it needs g_1 >= 2 only at the seventh step (the g_1+1 >= 3 push case). So N can be any tail. The same holds for U2 (its seventh step), and U1 and X allow an arbitrary rest.

X trace (rest = [g'', ...]): ([2,1,2],[a''+1,3,b'',g'',..]), ([2,1,1,a''+1],[1,2,b'',g'',..]), ([2,1,1,a'',1],[b''+1,g''+1,..]), ([2,1,1],[a''+1,2,b''+1,g''+1,..]), ([2],[2,2,a''+1,2,b''+1,g''+1,..]), ([1,2],[a''+2,3,b''+1,g''+1,..]), ([1,1,a''+2],[1,2,b''+1,g''+1,..]), ([1,1,a''+1,1],[b''+2,g''+2,..]), ([1,1],[a''+2,2,b''+2,g''+2,..]), ([],[2,2,a''+2,2,b''+2,g''+2,..]). In frame terms: Y = 2 creates Z = 2. Z's first child finishes at once, but Z has value 1 and cannot pay, so Z finishes too. E re-creates Y with value 2, Y's child finishes, and the epoch ends with E = 1. That is cost 3.

Proof of TL (translation). Run both sides one macro step. Edge(W) does R3 and pushes 4. conf(L0+[y], [z,2]+W) does R1 (y >= 2): it sets y := y-1 and pushes z. Both leave the same R = [W_0+1, W_1+1, W_2, ...], because the R-update of a push depends only on R. Call the pushed frame the bottom frame B, and let i be the number of children B has created so far. Claim: until the edge run's last step, the edge run is at ([4-i] + S, R) and the other run is at (L0 + [y-1, z-i] + S, R), with the same S and R.

What a macro step reads (Lemma RM): - A push reads the top value and R, and whether the depth p is 0 (R3 or R1). Here p >= 1 in both runs before the end. - A pop (a_p = 1, p >= 2) also reads the frame beneath the top, a_(p-1), which goes back into R as [a_(p-1)+1, 2]. Whether p = 2 (R2e) or not (R2) changes only the TM step count, not the model. - HALT is a_p = 1 with p = 1. The other run has p >= |L0| + 2 >= 2 throughout, so it never halts.

Cases, by the length of S: 1. S non-empty, top of S >= 2: both runs push the same value with the same R-update, so S grows. 2. |S| >= 2, top of S = 1: both runs pop. The frame beneath the top is inside S, so it is the same in both runs, and so is the new R. 3. S = [], so B is top. In the edge run its value is 4-i, and 4-i >= 2 because the epoch does not halt. So B pushes (R1), and i grows by 1. B creates c children in all, so i <= c-1 before this push. Then z-i >= z-(c-1) >= 2, and the other run pushes too (R1), with the same R-update. 4. |S| = 1, top of S = 1: the pop reads B's value. In the edge run this is R2e: [4-c, 1] -> [], R := [5-c, 2]+W'. It is the epoch's final step, because L = [] for the first time, and i = c here. The other run does R2: L0+[y-1, z-c, 1] -> L0+[y-1], R := [z-c+1, 2]+W', and z-c >= 1.

So before the last step every pop has |S| >= 2 and reads only frames inside S. Case 3 depends on B's value only through ">= 2", which holds in both runs. The single pop with |S| = 1 is the epoch's final step (case 4). Both runs take the same k macro steps. ∎ In the .v, TL is frame_step. Its core is Life_shape, which proves the same fact in big-step form, by induction on the frame semantics Life (§7).

Rule T (replay). Let a >= 2, b >= 1, and N a tail. Put ζ_0 := b+2, (c_i, W_{i+1}(N)) = Ep(W_i(N)) and ζ_{i+1} := ζ_i - c_i + 1. For a marker word, W_i(N) = O_i(N). - If the epochs Ep(W_i(N)) exist and ζ_i >= c_i + 1 for i = 0..a-2, then Ep(T(a,b)+N) = (2, [ζ_{a-1}, 2] + W_{a-1}(N)). Proof: TR, then TL a-1 times, then TF. The i-th TL use has y = a-i, z = ζ_i and W = W_i(N). None of TR, TL or TF uses marker structure. - Rule X (exhaustion). Suppose the epochs exist, ζ_i >= c_i + 1 for i = 0..a-3, ζ_{a-2} = 2, and W_{a-2}(N) = [a'',2,b'']+N'' with a'' >= 2, b'' >= 1, and N'' arbitrary. Then Ep(T(a,b)+N) = (3, T(a''+2, b''+2) + N''+), where N''+ is N'' with its first entry increased by 2 ([] stays []). Proof: TR, then TL a-2 times (Y goes from a to 2), which gives conf([2,2], [2,2]+W_{a-2}(N)), then X. - Rule S. For a, b >= 1 and N a tail: Ep(S(a,b)+N) = (2, T(a+1, b+2) + [2,1] + N), in 18 macro steps. Proof: S(a,b)+N = T(2,a)+N_S with N_S := [2,b]+N, a tail with first gap 2. Rule T at (2, a, N_S) needs one inner epoch. W_0(N_S) = [1,2,b]+N, and U2 gives Ep(W_0(N_S)) = (2, [b+2,2,1]+N). Then ζ_0 = a+2 >= 3 = c_0+1, and Rule T gives (2, [a+1,2] + [b+2,2,1]+N). The count is TR (8) + U2 replayed by TL (9) + TF (1) = 18. As a standalone computation (the form ruleS proves in the .v), the macro steps are R3 R1 R1 R2 R1 R1 R1 R2 | R1 R1 R1 R2 R1 R1 R1 R2 R2 | R2e. The middle block is U2 with its first R3 read as R1 and its last R2e read as R2. Every case split in it is decided by the literal entries 2, a+1 >= 2 and so on, and by N's first gap >= 2.

Unrolled to the tape, ζ_i is the value of the [ζ,2] run right of the head when the replay frame Y creates its i-th child. "Cost 3" at an inner level means "ζ drops by 2" at the level above. Since ζ_{i+1} = ζ_i - c_i + 1, the condition ζ_i >= c_i + 1 is the same as ζ_{i+1} >= 2, and ζ is non-increasing (every cost is >= 1). So, given that the inner epochs exist, the conditions of Rule T for all i follow from ζ_{a-1} >= 2, and those of Rule X from ζ_{a-2} = 2. These are the hypotheses of ruleT and ruleX in the .v.

3. The orbit invariant and the absorption law

Fix an even-gap marker word M with m markers and n >= 1. Let α := #{j >= 1 : I_j(M) < n} (markers already absorbed), and let j* := α+1 be the first unabsorbed marker if α < m. Call n an absorption step when α < m and I_{j*} = n.

Inv(M, n). W := O_n(M) has one of the following two forms. The type rule decides which: T when n - I_α is odd, S when it is even.

T case. W = T(a,b)+N with a >= 2, b = n + α, and N an even-gap marker word. Let aff := b+1-a. Then: - (count) #N = aff + (m - α), and aff >= -1. aff = -1 happens only at an absorption step (the marker has merged into the head). - (INT) If aff>=0, I_aff(N)<=a-2 (I_0=0); vacuous for aff=-1. - (EXT) For every j with j* <= j <= m, put t := aff + 1 + (j - j*), the index in N of original marker j. If t >= 1 then I_t(N) = a - 3 + I_j(M) - n. There is one exception: at an absorption step, for j = j*, the claim is only I_t(N) <= a-3 (within strict reach).

S case. W = S(a,b)+N with a >= 2, b = n - 1 + α, aff := b+1-a. Everything is as in the T case with a-3 replaced by a-4 in EXT. The exception now applies when n+1 = I_{j*}: the claim is then I_t(N) <= a-3, and aff = -1 is allowed only then.

When α = m there are no external markers: N has exactly aff markers, all within reach.

Read with an arbitrary word W in place of O_n(M), the clauses define a predicate "W ∈ Inv(M, n)". The induction step below uses nothing about W = O_n(M) except these clauses and the IH on the inner orbits O_i(N) of W's own marker tail. In the .v the step lemmas stepS, stepT_nabs and stepT_abs are stated this way, for any word whose marker tail satisfies the clauses (Core, §7).

AL(M, n). Epochs 0..n-1 of the orbit exist (no halt), and epoch i costs 3 iff i ∈ I(M). Otherwise it costs 2.

Theorem. For every even-gap marker word M and every n >= 0, AL(M, n) holds, and so does Inv(M, n) when n >= 1.

Parity facts. (P1) I_i ≡ i (mod 2). (P2) At a T-word, b = n+α is odd: n - I_α is odd and I_α ≡ α. At an S-word, b = n-1+α is also odd.

Proof. Strong induction on Λ := n + m. For Λ = 0 (M = [], n = 0) there is nothing to prove. Assume the claim for every (M', n') with n' + #M' < n + 1 + m, and in particular for (M, n). We prove it for (M, n+1) by cases on O_n(M).

Case n = 0 (U-words). O_0 = [1]+M. - M = []: by U0, O_1 = T(2,1) with α = 0 and aff = 0. - M = [g_1,1]+M' with g_1 >= 4: by U1, O_1 = T(2,1)+[g_1-2,1]+M'. Here aff = 0 and I_t(N) = I_t(M) - 2 = a-3+I_t-1 (EXT with n = 1 < I_1). - M = [2,1]+M': by U2, O_1 = T(3,1)+M'. Here aff = -1 and n = 1 = I_1 is an absorption step; the marker merged into the head. EXT holds for j >= 2: I_{j-1}(M') = I_j - 1 = a-3+I_j-1.

The epoch costs 2, and 0 ∉ I(M) because every I_j >= 1. The type is T since 1 - I_0 = 1 is odd, and b = 1 = n + α.

Case S-word, O_n = S(a,b)+N. Rule S needs a >= 2, b >= 1 (S-words occur only at n >= 2) and N's first gap >= 2. It gives O_{n+1} = T(a+1, b+2) + [2,1] + N at cost 2. Here n ∉ I(M): I_α < n, and, when α < m, I_{j*} - n is odd (because n ≡ I_α ≡ α and I_{j*} ≡ α+1), so n+1 <= I_{j*}. - α is unchanged, the type is T (n+1-I_α is odd), and b+2 = (n+1)+α. - The new aff_T = aff_S + 1 >= 0, and the marker count goes up by 1 (the new [2,1]) ✓. - INT: For aff_S >= 0, I_{aff_S+1}([2,1]+N) = 1 + I_{aff_S}(N) <= (a+1)-2. For aff_S=-1, aff_T=0, so I_0=0 <= (a+1)-2. - EXT: indices shift by 1 and positions by +1, so 1 + (a-4+I_j-n) = (a+1)-3+I_j-(n+1) ✓. - Absorption exception (n+1 = I_{j*}): for a marker already present in N (t >= 1), 1 + I_t(N) <= (a+1)-3. If aff_S = -1, the new [2,1] at position 1 is the (aff_T+1)-th marker, and 1 <= a-2 because a merged S-word has b = a-2 >= 1.

Case T-word, not an absorption step (n < I_{j*}, or α = m), O_n = T(a,b)+N. 1. Inner costs. I_1(N) .. I_aff(N) <= a-2 by INT. If α < m, the next one is I_{aff+1}(N) = a-3 + I_{j*} - n >= a-1, because I_{j*} - n is even and positive. This uses the type rule, the P1 parity of I_{j*}, and n - I_α odd. If α=m, all markers are internal. Take the IH AL(N, a-1). Its measure is Λ = (a-1) + #N = (a-1) + aff + m - α = b + m - α = n + m, which is smaller. It gives c_i = 2 + [i ∈ I(N)] for i <= a-2, with exactly aff threes. 2. ζ-accounting. ζ_i = b+2-i-#(I(N)∩[0,i-1]), so ζ_i - (c_i+1) = b-1-i-#(I(N)∩[0,i]) >= b-1-(a-2)-aff = 0. Also ζ_{a-1} = b+2-(a-1)-aff = 2. Rule T gives Ep(O_n) = (2, [2,2] + O_{a-1}(N)). The cost is 2, and n ∉ I(M) ✓. 3. Shape. By the IH Inv(N, a-1), α_N = aff (the same count as in step 1), and (a-1) - I_aff(N) ≡ a-1-aff ≡ b ≡ 1, so the inner word is a T-word: O_{a-1}(N) = T(a',b')+N' with b' = (a-1)+aff = b. Therefore O_{n+1} = S(a', b) + N'. Check the S clauses at n+1: - b = (n+1)-1+α ✓. - #N' = aff' + (#N - aff) = aff' + m - α ✓. - INT is inherited. - EXT: original marker j = j*+s is N-marker aff+1+s, at a-3+I_j-n. Inner EXT puts it at a'-3 + (a-3+I_j-n) - (a-1) = a'-4+I_j-(n+1) in N' ✓. - If I_{j*} = n+2, the inner word is at its own absorption step, so the inner exception gives <= a'-3 (or aff' = -1). This is exactly the S exception at n+1. - The type is S because n+1-I_α is even ✓.

Case T-word at an absorption step (n = I_{j*}). Here a >= 3: if aff >= 0 then 1 <= I_{aff+1}(N) <= a-3, and if aff = -1 then a = b+2 >= 3. 1. Inner costs. The first aff+1 markers of N are <= a-3; when aff = -1 there are none. If j* < m, the next one is a-3+I_{j*+1}-n >= a-2; otherwise no markers remain beyond those first aff+1. The IH AL(N, a-2) has measure n+m-1. It gives exactly aff+1 threes among c_0..c_{a-3}. 2. ζ-accounting. For i <= a-3: ζ_i-(c_i+1) >= b-1-(a-3)-(aff+1) = 0. Then ζ_{a-2} = b+2-(a-2)-(aff+1) = 2. 3. Shape for rule X. By Inv(N, a-2): α_N = aff+1, and (a-2) - I_{aff+1}(N) ≡ a-3-aff ≡ b ≡ 1 (when aff = -1: a-2 = b, odd). So O_{a-2}(N) = T(a'',b'')+N'' with b'' = (a-2)+(aff+1) = b >= 1 and a'' >= 2. Rule X gives Ep(O_n) = (3, T(a''+2, b+2)+N''+). The cost is 3 at n = I_{j*} ✓. 4. Clauses at n+1. Now α' = α+1, the type is T (n+1-I_{j*} = 1), b+2 = (n+1)+α' and a''+2 >= 4. - aff_new = aff'', and #N''+ = aff'' + (#N-aff-1) = aff'' + m - α' ✓. - INT: For aff'' >= 1, I_{aff''}(N''+) = I_{aff''}(N'')+2 <= a'' = (a''+2)-2. For aff''=0, the bound is I_0=0 <= a''. For aff''=-1, INT is vacuous. - EXT for j >= j*+1: inner EXT gives a''-3 + (a-3+I_j-n) - (a-2) = a''-4+I_j-n. Adding 2 gives (a''+2)-3+I_j-(n+1) ✓. - If I_{j*+1} = n+1, the inner exception carries over: <= a''-3, plus 2, gives <= a_new-3, or the marker has merged (aff'' = -1).

Measure. Every inner call uses (N, i) with i <= a-1 and #N = aff + m - α, so i + #N <= n + m < (n+1) + m. The outer call uses (M, n). So the induction is well-founded. Epochs are finite because each is a finite composition of rules. ∎

Remarks. - Odd gaps never occur: every gap the rules create is 2, g+2 or g-2 starting from even values. The Theorem is stated only for even gaps, and that is all the proof needs. - A T-word epoch ends in one of exactly two ways: ζ_{a-1} = 2 with Rule T (not an absorption step), or ζ_{a-2} = 2 with Rule X (absorption step). A third ending with ζ = 3 at the last replay does not arise: at an absorption step the absorbed marker sits at <= a-3, never at a-2 (the exception clause), so ζ_{a-2} = 2 exactly.

4. Coverage

5. Initial segment

c0 = 0^inf A> 0^inf
 --10-->   0^inf <A 0 1^2 0^inf          = conf([], [2])        A0 B0 C0 D1 D1 D0 E1 F1 F1 F0
 --14-->   0^inf 1^3 <A 0 1 0^inf        = conf([3], [1])       R3 (k=1, m=0)
 --15-->   0^inf 1^2 0 1 <A 0 1 0^inf    = conf([2,1], [1])     R1 (n=1, m=0, x=0)
 --11-->   0^inf <A 0 1^3 0^2 1 0^inf    = conf([], [3,2,1]) = Edge([1]) = Edge(O_0([]))   R2e (k=1)

That is 50 steps in total. In the .v this is init : c0 -->* conf [] [3; 2; 1], by solve_init.

6. Conclusion

Every top-level epoch costs 2, so the edge frame E creates exactly 2 children per epoch. It is never asked for a 4th, which is the only way HALT can happen (§2). Each epoch takes at least 9 macro steps, and so at least 9 TM steps. The run therefore passes through Edge(O_n([])) for every n and never halts.

Why --- (E0) is never read. E is entered only by D0 (0LE). In R1 and R3, D0 fires just right of the 1^(x+2) block, so E reads a 1. In R2 and R2e, D0 fires just right of the lone 1, so E reads that 1. E reads 0 only in the HALT pattern 0^inf 1 <A 0, where C0, D0 run off the left edge. That pattern is a depth-1 frame with value 1 on top, which the cost-2 argument excludes.

6.1 The twin: Eqv.v TM113

verify/Eqv.v Module TM113 has tm = 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RA1LB. That is this machine with the states renamed: TM113's A..F are our B, C, D, E, F, A. So TM113.tm from c0 is our machine on a blank tape started in state B. TM113.eqv proves halts tm c0 <-> halts tm' c0 for tm' = 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB, the twin, which is on the current BB(6) holdout list.

Claim. TM113.tm never halts. Hence, by TM113.eqv, neither does the twin. - Initial segment. From blank in our state B: B0 C0 D1 D1 D0 E1 F1 F0 (8 steps) gives conf([], [1]). Then R3 (k=0, m=0; 11 steps) gives conf([2],[1]), R1 (n=0, m=0, x=0; 15 steps) gives conf([1,1],[1]), and R2e (k=0; 10 steps) gives conf([], [2,2,1]) = conf([], [2,2]+O_0([])) at step 44. - Budget-2 edge lemma. If Ep(W) = (c, W') with c <= 2, then conf([], [2,2]+W) --> conf([], [4-c, 2]+W') in the same k macro steps, with L ≠ [] in between. The proof is TL's argument with an empty context. R3 pushes 2+1 = 3 instead of 4, so the stacks are [3-i]+S and [4-i]+S with the same S and R. The bottom frame is top only to create child i+1 <= c <= 2, so its value is 3-i >= 2. The final step is R2e: [3-c, 1] -> [], R := [4-c, 2]+W', with 3-c >= 1. In terms of the .v's lemmas, it is Life_shape applied to the edge frame with value 3 in place of 4 (c <= 2 gives c + 1 <= 3), followed by push0_ok and Life_tm. - Top level. With M = [], the Theorem says every Ep(O_n([])) costs exactly 2. So conf([], [2,2]+O_n([])) --> conf([], [2,2]+O_{n+1}([])) for every n, with at least 9 TM steps each. The edge frame starts each epoch at 3, a budget of 2 children, and every epoch spends exactly 2. There is zero slack: a single cost-3 top epoch would halt the twin, and the Theorem rules that out. - Formal route (not in the accompanying .v). A separate file whose TM_from_str is the twin's string proves ~halts TM113.tm c0 and transfers it through TM113.eqv, either imported or as a copy of its solve_eqv call. It shares the model layer and the Theorem (Life and its lemmas, the epoch rules, main; §7). Only these differ: the TM-level rules (the same R1/R2/R2e/R3 with renamed states), the 44-step init, and the top-level step (the budget-2 edge lemma in place of Ep_tm).

7. The .v file

The .v proves Lemma nonhalt: ~halts tm c0. for tm := TM_from_str "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF". It imports Individual62 and the stdlib Lia, String, List and Arith. Every lemma is top level (no Section, Module or Hypothesis). It follows §1–§6 with the choices below.

The constructors are L_fin (value 1: the frame finishes), L_cf (the frame pays and creates a child that finishes, so the frame is popped with it: Pop 1), and L_cpf, L_cpp (the frame pays and creates a child whose own life ends in Pop, then lives on with its value reduced by 1; the outcome is that of the rest of its life, Fin for L_cpf, and Pop with one more child for L_cpp). Life_tm lifts Life to the TM for every stack L below the frame: Fin Rf gives conf (x::L) R -->* conf (1::L) Rf, and Pop c Rf gives conf (x::L) R -->+ conf L Rf. - Epochs (§2). Ep W c W' := exists R0, updt (2::W) = Some R0 /\ Life 4 R0 (Pop c ((5-c)::2::W')) is the life of the edge frame, which R3 creates with value 4. Ep_tm gives conf [] (3::2::W) -->+ conf [] ((5-c)::2::W'). - Translation (TL). Life_shape: if Life x R (Pop c Rf), then c + 1 <= x, Rf = (x-c+1)::2::W' for some W', and Life z R (Pop c ((z-c+1)::2::W')) for every z >= c + 1. So a Pop outcome depends on the frame's value only through z >= c + 1, which is case 3 of the proof of TL; the proof is by induction on Life, with no case split on |S|. frame_step combines it with Ep: a frame of value y >= 2 over [z,2]+W, with Ep W c W' and z >= c + 1, creates a child of value z whose life is the translated epoch, and then continues with value y-1 over [z-c+1,2]+W'. - Concrete rules. U0, U1, U2, ruleS (the standalone 18-step form of Rule S), TRF (TR, then a given life of the replay frame Y that ends in Fin, then TF), Xin0/Xin1 (the inner part of X, with rest empty or not) and TRX0/TRX1 (TR, then a given life of Y that ends in Pop, then the rest of X) are closed by the tactics ep and lf; lf searches the four Life constructors, with each updt computed by reflexivity. The tail hypothesis is tail_ok N: N = [] or its first gap is >= 2. - Marker words and orbits (§0, §3). A marker word is stored by its absorption indices: mw P for P = [I_1; ..; I_m], with gaps g_j = I_j - I_(j-1) + 1, each followed by a lone 1. valid P says every gap is even (each index is odd above the previous one). cnt P n = #{p ∈ P : p < n} is α, ind P n = [n ∈ P], and cost P n = 2 + ind P n. Orb Q n W is the orbit with AL built in: O0 : Orb Q 0 (1 :: mw Q), and OS extends Orb Q n W by an epoch Ep W (cost Q n) W'. So an orbit word exists only if every earlier epoch exists at the cost AL predicts. - Rules T and X. replay iterates frame_step along an orbit, by induction on Orb. ruleT is Rule T for a marker tail, with hypothesis a - 1 + cnt Q (a-1) <= b, which is ζ_{a-1} >= 2, and result ζ_{a-1} = b + 3 - a - cnt Q (a-1). ruleX is Rule X for a marker tail, with b = a - 2 + cnt Q (a-2) (that is, ζ_{a-2} = 2); N''+ is mw (map (+2) Q''), since adding 2 to every index adds 2 to the first gap only. The .v uses Rule T and Rule X only on marker tails, and Rule S in its standalone form. - Invariant. Core P k a b Q holds when valid Q, a >= 2, and Q = Qi ++ Qe with - |Qi| + a = b + 1 + ind P k (count), - every q in Qi has q + 2 + ind P k <= a (INT, together with the absorption exception), and - Sh (k+3) a Qe (filter (k <?) P), that is, Qe lists the indices of P above k, each shifted by a - k - 3 (EXT, as an exact shifted copy).

Inv P n W, with α = cnt P n: either n + α is odd and W = T(a, n+α) + mw Q with Core P n a (n+α) Q, or n + α is even and W = S(a, n+α-1) + mw Q with Core P (n+1) a (n+α-1) Q. The parity of n + α is the type rule of §3, since I_α ≡ α. The merged case aff = -1 and the case α = m need no separate branch. - Theorem. stepU (n = 0), stepS, stepT_nabs and stepT_abs (rule X) are the four cases of §3, and step_lemma dispatches on the word's shape and on n ∈ P. Claim Lm says that every (Q, k) with k + |Q| <= Lm and valid Q has an orbit word W (Orb Q k W) that is in Inv Q k when k >= 1. main : forall Lm, Claim Lm is proved by induction on Lm, which is the measure Λ = n + m of §3. The EXT bookkeeping is the shifted-copy relation Sh and its lemmas, and the parity facts are parity_in. - Top level. nonhalt applies multistep_nonhalt with init, then progress_nonhalt_cond with - index type nat * list nat and start (0, [1]), - configuration map (n, W) ↦ conf [] (3 :: 2 :: W), so that the start is conf [] [3; 2; 1], - predicate Orb [] n W /\ (1 <= n -> Inv [] n W).

The step obligation is step_lemma at P = [], where cost [] n = 2, lifted to the TM by Ep_tm.

7.1 Where each part lives in the .v

section lemma(s) in the .v
§0 conf(L,R) lsep, lside, rside, conf (L stored top first), lsep_eq
§1 R1, R3, R2, R2e tR1, tR3, tR2 (each one plain es, so CW/DW/FW are not separate lemmas), tR3c (R3 at the left edge: one const_unfold rewrite of const 0, then es). R2e is tR2 with l = const 0 (through lsep_eq)
§1.1 Lemma RM updt (the push R-update, None outside the domain), updt_shape, push_ok, push0_ok, pop_ok
§1.1 frame reading Inductive Life x R o with constructors L_fin, L_cf, L_cpf, L_cpp; Life_tm lifts it to the TM
§2 epoch Ep Ep W c W' (the life of the edge frame, value 4), Ep_tm
§2 U0, U1, U2, Rule S U0, U1, U2, ruleS (the standalone 18-step form), each closed by ep (the search tactic lf)
§2 TR, TF TRF (the TR prefix, then a finishing continuation)
§2 TL Life_shape, frame_step
§2 Rule T replay (induction on Orb), ruleT
§2 X, Rule X Xin0, Xin1, TRX0, TRX1, ruleX
§0 marker words, I_j, tails mw/mwf (the word built from its index list P = [I_1; ..; I_m]), valid/valid_from (even gaps), tail_ok
§3 α, [n ∈ I(M)], cost, orbit, AL cnt P n, ind P n, cost P n = 2 + ind P n, Inductive Orb
§3 Inv(M, n) Inv, Core
§3 parity facts parity_in
§3 cases stepU (n = 0), stepS, stepT_nabs, stepT_abs (rule X); step_lemma dispatches
§3 Theorem main : forall Lm, Claim Lm
§3 EXT bookkeeping Sh, Sh_filter, Sh_in, Sh_trans, Sh_map, Sh_ge, sh_compose, in_transfer, filter_cnt_len
§5 initial segment init : c0 -->* conf [] [3; 2; 1] (50 steps, solve_init)
§6 nonhalt

The twin of §6.1 is not in this file.

8. Numerical sanity checks

These were checked by direct simulation of the transition table and of the run model. They are independent of the .v, and the result rests on the .v alone.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic); corrections from an independent audit by GPT-6 Astra (OpenAI).