1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF: never halts

Submission copy of the working proof.md, made 2026-10-10 after the kill. The mathematics is unchanged. Only these parts were updated: the header (holdout line, status, AI line), a new subsection 7.1 that maps the proof to the lemmas of the .v and says where the .v departs from the plan, and the first two items under Gaps in §8. The scripts and notes it cites (check_proof.py, edge_scan.c, epc.c, inv_scan.py, their outputs, notes.md, deepen.json, observe.json) live in the working directory and are not in this folder. The Review log at the end is kept as history.

• Machine: 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF, viewer https://bbchallenge.org/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF
• Holdout list and sheet: on every holdout-list snapshot we have, from 2024-06-14 (12,091) to 2026-10-07 (778; line 2). Results tab row 832, class "Counter Class 4", no notes, no links. There is no local Discord thread. Twin 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB (row 833) appears only as tm' of Eqv.v TM113, and it is unsolved. TM113.tm is this machine with its states renamed, started in our state B, so the same Theorem also settles row 833 (§6.1).
• Written for: the string itself (the twin needs a separate formal file, §6.1, and is not covered by the .v).
• Status: fully formalized, killed. 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v (876 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 3.9 s with -native-compiler yes, Print Assumptions nonhalt closed (no axioms), coqchk pass in 1.3 s (check_kill.txt). The informal proof was written 2026-10-10 and revised the same night after an independent skeptic review (six minor gaps, all closed; see the Review log at the end). Every claim below is also checked by simulation in check_proof.py (section labels A–H match). No Checkpoint B notes from Dennis were on file when this copy was made.
• AI assistance: this text and the Coq formalization were produced with the help of Claude (Anthropic), working from the deepen passes in notes.md and deepen.json. The kill rests on the .v file, checked by our checker, check_kill.

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. This is the number of internal markers, the ones the next replay will absorb.

1. TM-level rules

The --- is E0. Shift rules (ind, one IH use each):

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). Evidence: A in check_proof.py (n, m, x, k, j up to 25, random l and r, exact tape, head, state and step count).

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. Evidence: B1, the model equals the TM at every macro step for 40,000 macro steps from step 50. B2: the TM C core agrees at the edge returns up to TM step 4·10^8.

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. Evidence: D.

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. ∎ (The Coq form of this argument is in §7, step 3.)

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 model lemma (the Coq form), 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. Evidence: D7, 1,200/1,200 (a, b in 1..20, half marker tails, half arbitrary tails).

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.

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) I_aff(N) <= a-2. The aff internal markers are within reach. - (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 Coq, state the step as a lemma over arbitrary W ∈ Inv(M, n). Evidence E2 tests exactly this step on words that are not orbit words.

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 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: I_{aff_T}([2,1]+N) = 1 + I_{aff_S}(N) <= (a+1)-2. When aff_S = 0 this is 1 <= a-1. - 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*}): 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. 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. 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. The next one is a-3+I_{j*+1}-n >= a-2. 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: I_{aff''}(N''+) = I_{aff''}(N'')+2 <= a'' ✓. - 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. ∎

4. Coverage

• Edge level. The run reaches Edge(O_0([])) (§5). By the Theorem with M = [], every epoch from Edge(O_n([])) exists and costs 2, because I([]) is empty. The epoch ends at conf([], [5-2, 2] + O_{n+1}([])) = Edge(O_{n+1}([])). Every O_n([]) is a U-word (n = 0), a T-word or an S-word, and each epoch is covered by U0, T or S. For M = [] no absorption step ever occurs, so rule X is never used at the top.
• Inside epochs. Rules U0–U2, TR, TL, TF and X are exact macro-step runs, and each macro step is a TM rule from §1. RM covers every in-domain configuration, so nothing is left uncovered.
• Case splits used. These are: p = 0 / a_p >= 2 / a_p = 1 with p >= 2 / p = 1; g_1 = 2 / g_1 >= 3 / r = 1; for words, U (with the three forms) / S / T, and T as "not an absorption step" / "absorption step"; and inside the Theorem, aff = -1 versus aff >= 0 and α = m versus α < m.

Evidence: - E1: Inv and AL on 2,500 random even-gap marker words (m <= 6, gaps 2..14, n up to 28), plus every word with gaps in {2,4,6,8} and m <= 3. Every word along each orbit is checked against every clause. - E2: the induction step tested by itself. The step uses only "W satisfies Inv(M, n)" plus the IH on the inner orbits of W's marker tail. So E2 builds words directly from the Inv(M, n) clauses (orbit words or not) and checks that Ep(W) costs 2 + [n ∈ I(M)] and lands in Inv(M, n+1). It runs every such word with a <= 14 for all 85 M with gaps in {2,4,6,8} and m <= 3, then random words (a <= 26, m <= 6), then extreme placements (internal markers packed at the bottom or top of their range, and the within-reach marker at its lowest or highest position; a <= 22, m <= 7). A sensitivity run moves one clause's bound by 2 and shows that the step then fails on the words this adds. Counts are in §8. - F: O_n([]) for n <= 37: all costs 2 and Inv holds. The S-words reproduce the observer's history Fs(4,2,6), Fs(5,6,4), Fs(6,4,8), ....

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. Evidence: C (check_proof.py simulates the 50 steps and parses the tape).

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. Evidence: G, E is entered about 10^5 times in the first 2·10^6 steps, always reading 1. A5: the HALT pattern halts in exactly 3 steps reading E0.

6.1 Twin: Eqv.v TM113 and row 833

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 (row 833). The twin is in the current holdout list (2026-10-07_778). TM113.tm itself left the list after 2025-08-30. Our index of solved machines has a busycoq proof for neither.

Claim. TM113.tm never halts. Hence, by TM113.eqv, neither does row 833. - 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. - 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. A separate file whose TM_from_str is the row-833 string, so that the kill criteria hold byte for byte. It proves ~halts TM113.tm c0 and transfers it through TM113.eqv, either imported or as a copy of its solve_eqv call. The model layer and the Theorem (§7 steps 2–4) are shared. 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 Edge). - Evidence: H. The relabeling is checked symbolically, along with the 44-step init and the budget-2 edge lemma (orbit words, marker orbits and arbitrary words). A raw-TM scan from blank in state B to step 4·10^8 finds exactly conf([],[1]) at step 8 and conf([],[2,2]+O_n([])) for n = 0..39, at the model's exact step counts, and no other left-edge configuration.

7. busycoq lemma plan

• Nearest template: verify/CounterClass2v1.v. It has an abstract Inductive Side, a to_side translation, a measure, one-step lemmas lifted to the TM, and progress_nonhalt_cond. BinaryCounter.v shows Fixpoint-built sides. No repo file has this machine's word recursion, so the model layer below is new.
• Size: larger than the CounterClass examples. Most of it is the model-level combinatorics, which is pure list nat + lia with no TM execution.

1. TM layer. Definition tm := Eval compute in (TM_from_str "1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF"). - Shift lemmas CW, DW and FW, by ind n with es. - R1, R3, R2 and R2e, for all sides l and r, by es and follow CW/DW/FW in the order listed in §1.

2. Sides. Store L with its top first. - Fixpoint lside : list nat -> side (single 0 between runs, const 0 at the bottom). - Fixpoint rside : list nat -> side (alternating runs and gaps). - Definition conf L R := lside L <{{A}} [0] *> rside R. - Lemma RM_sound : wf L R -> mstep (L,R) = Push/Pop (L',R') -> conf L R -->+ conf L' R'. This is a case split on g_1 = 2 / >= 3 / r = 1. The 0 0 1^x 0 reshaping needs rside rewriting lemmas.

3. Model layer. Pure Coq, no TM. - mstep is a Fixpoint-free function on (list nat * list nat), with mrun k its k-fold iterate. - Ep W c W' is defined as mrun k ([], [3;2]++W) = ([], [5-c;2]++W'), with no intermediate empty L. - Lemmas U0, U1, U2, TR, TF and X are reflexivity/simpl after destruct on the list shapes. - TL needs a simulation relation: the edge state ([4-i]++S, R) against (L0++[y-1; z-i]++S, R), both written bottom-first here. Prove it by induction on the remaining step count, generalized over (i, S, R). Put these into the invariant explicitly: - i <= c; - if S = [] then i < c, so the bottom frame, when it is top, has value >= 2 in both runs (4-i >= 2 and z-i >= 2). Derive this from "the edge run does not halt and the bottom value only decreases". - Before the last step, every pop has |S| >= 2, so the frame it reads sits in S. The |S| = 1 pop is the step that empties the edge stack, which is the epoch's last step and the base case of the induction. The "no intermediate L = []" clause in the definition of Ep is what identifies the |S| = 1 pop as the last step. This is the one non-trivial model lemma. The twin's budget-2 edge lemma (§6.1) is the same proof with L0 empty and [3-i] in place of [y-1; z-i]. - Rule T and rule X follow by induction on a, using follow-style transitivity of mrun. State them for tails, not for marker words. Rule S is then T at a = 2 with tail [2;b]++N, or a standalone 18-step computation.

4. Theorem (§3). - orbit M n W is an inductive relation. - Inv M n W is a Prop over list nat, with Ivec as a Fixpoint prefix-sum. - Prove forall Λ M n W, n + markers M <= Λ -> orbit M n W -> AL M n /\ Inv M n W by induction on Λ. Factor out the step as its own lemma over arbitrary words: Inv M n W -> (IH for all (N, i) with i + markers N <= n + markers M) -> exists W', Ep W (2 + [n ∈ I M]) W' /\ Inv M (S n) W'. This is the statement E2 tests. - The parity facts and the EXT arithmetic are lia with Nat.even/Nat.odd lemmas. - Expect the EXT index bookkeeping (nth on prefix sums under [2;1]++ and "first gap +2") to be most of the work. Write helper lemmas Ivec_cons21 and Ivec_bump2 first.

5. Top. - Lemma init : c0 -->* conf [] [3;2;1] by solve_init/es (50 steps). - Lemma nonhalt : ~halts tm c0. Apply multistep_nonhalt (TM.v:584) with init. That leaves ~halts tm (conf [] [3;2;1]). Close it with progress_nonhalt_cond (TM.v:632), whose arguments are an index type A, a start index i0, a map C : A -> Q * tape and a predicate P : A -> Prop (not a predicate on configurations, which is progress_nonhalt's shape). Take: - A := nat * list nat, - C '(n, W) := conf [] (3 :: 2 :: W), - P '(n, W) := orbit [] n W, - i0 := (0, [1]), so that C i0 = conf [] [3;2;1] and P i0 is the base case of orbit. The step obligation is forall i, P i -> exists i', C i -->+ C i' /\ P i'. Take i' := (S n, W'), where W' comes from the Theorem (AL([], n+1): epoch n exists and costs 2), lifted to the TM by RM_sound. This avoids having to define W_n as a function. - Twin (§6.1): the same with C '(n, W) := conf [] (2 :: 2 :: W), a 44-step init from c0 of TM113.tm, and the budget-2 edge lemma in the step. Then TM113.eqv gives row 833.

7.1 How the .v file is organized

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

Where it departs from the plan: - No small-step model. There is no mstep/mrun and no TL simulation relation (step 3's invariant with i <= c and S = [] -> i < c). The big-step relation Life reads the run model frame by frame, as in §1.1's frame reading. TL becomes Life_shape: a Pop c outcome depends on the frame's value only through z >= c+1. It is 15 lines by induction on Life, with no case split on |S|. - Ep is a Life of the edge frame, not an mrun with "no intermediate L = []". Ep_tm lifts it to conf [] (3::2::W) -->+ conf [] ((5-c)::2::W'). - AL is built into Orb. Each step of Orb Q n W is an Ep at cost 2 + [n ∈ Q], so an orbit word exists only if every earlier epoch exists at the cost AL predicts. - One predicate for both word types. Core P k a b Q takes k = n for a T-word T(a, n+α) and k = n+1 for an S-word S(a, n+α-1). It says Q = Qi ++ Qe, |Qi| + a = b + 1 + ind P k, every q in Qi has q + 2 + ind P k <= a (INT, plus the absorption exception), and Sh (k+3) a Qe (filter (k <?) P) (EXT, as an exact shifted copy of the unabsorbed indices). The merged case aff = -1 and the case α = m need no separate branch. - Measure. Claim Lm (every (Q, k) with k + |Q| <= Lm has an orbit word in Inv) is proved by plain induction on Lm. It is the same measure Λ = n + m as §3. - The twin of §6.1 is not in this file.

8. Evidence and gaps

ulimit -v 6000000; python3 -B check_proof.py runs the full checks, and --quick runs a 30-second subset. It needs a C compiler (B2, H and the long epochs of E2 compile edge_scan.c and epc.c into a temporary directory). The script exits 0 iff everything passes. After the review the full run (seed 2026, 1,570 s) printed ALL CHECKS PASSED. Its output is in check_proof_out_review1.txt. The pre-review run is still in check_proof_out.txt. A second E2 run with seed 11 is in e2_seed11_out.txt, with 0 failures.

Gaps. - (Closed by the .v.) §3 was a hand proof that Rocq had not checked, and the EXT index bookkeeping was the step most likely to hide an off-by-one. Simulation (E1 along orbits, and E2 for the induction step by itself) checked every clause exactly, including the absorption-step exceptions and the merged case aff = -1, but that was evidence, not proof. The .v now proves §3 (main, §7.1). - (Closed by the .v.) Lemma RM's bridge between 0 0 1^x 0 r and the R-list cases is routine but fiddly in Rocq (rside rewriting). In the .v the reshaping is one lemma, updt_shape. - 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. - deepen.json described a third exhaustion kind, "BETA" (ζ = 3 at the last replay). It never arises: at an absorption step the absorbed marker sits at <= a-3, never at a-2 (the exception clause), so ζ_{a-2} = 2 exactly.

Review log

2026-10-10, skeptic review 1 (independent). Verdict "sound", with six gaps, all minor and none fatal or major. Each gap and what was done:

1. §2, proof of TL. The proof said "a macro step reads only the top value, R, and whether the depth is 1", which is false for pops: a pop also reads a_(p-1). Fixed. The proof is rewritten by cases on |S|: push; pop with |S| >= 2 (reads inside S); B on top (only "value >= 2" matters, and it holds in both runs); and the |S| = 1 pop, which is the epoch's final step. §7 step 3 now lists the Coq invariant clauses: i <= c, S = [] -> i < c (a bottom frame on top has value >= 2), and the rule that every non-final pop has |S| >= 2.
2. §2, Rule S did not type-check. Rule T and O_i were defined only for marker words, while S applies T to the tail [2,b]+N. Fixed. Tails are defined in §0 and W_i(N) in §2. U2, TR, Rule T and Rule X are now stated for tails (the traces read only g_1 >= 2). Rule S is derived as Rule T at (2, a, [2,b]+N) plus U2, and is also given as a standalone 18-step model lemma with its step list. Checks: D2 (TR) and D6 (T/X) now include arbitrary tails, and D7 (S) runs 1,200 cases with a, b in 1..20, half of them on arbitrary tails.
3. §7 step 5. The plan used the wrong progress_nonhalt_cond shape, and one sentence was garbled. Fixed: A := nat * list nat, C '(n,W) := conf [] (3::2::W), P '(n,W) := orbit [] n W, i0 := (0,[1]), applied after multistep_nonhalt (TM.v:584) with init. The sentence is rewritten.
4. §8 B2 undercounted the evidence. Fixed, and the check is stronger. B2 now scans the raw TM at every step up to 4·10^8 (edge_scan.c) for left-edge configurations: state A with every cell at or left of the head blank. It finds exactly three kinds: blank (step 0), conf([],[2]) (step 10), and Edge(O_n([])) for n = 0..39, each at the model's exact TM step and with nothing else. This matches the skeptic's independent count of 40. The old comparison against our simulator is kept as B3 spot checks.
5. E never tested Inv as inductive on its own. Fixed with the new section E2: words built from the Inv(M, n) clauses, whether or not they lie on an orbit. Exhaustive at a <= 14 (93,113 words), random at a <= 26 (2,000), and extreme placements at a <= 22 (3,000): every word costs 2 + [n ∈ I(M)] and lands in Inv(M, n+1), with 0 failures. A sensitivity run moves one clause's bound by 2 and checks that the step then fails on the words this adds. §3 now says that the step is a lemma over arbitrary W ∈ Inv(M, n), and §7 step 4 factors it out. The stale "section 5" comment in check_proof.py now says "section 3". For comparison, at a <= 12 E2 counts 262 merged (aff = -1) words, the same as the skeptic's own a <= 12 run. Other totals differ because the enumeration ranges differ.
6. Twin. Added §6.1: Eqv.v TM113.tm is this machine relabeled and started in state B. Its 44-step init reaches conf([],[2,2,1]). With the budget-2 edge lemma and the Theorem at M = [], every top epoch spends exactly its budget of 2, so it never halts, and TM113.eqv then gives row 833. §7 step 5 gives the twin's formal route, and new evidence H checks the relabeling, the init, the edge lemma, and a raw-TM scan from state B.

Validation after the revision: the full check_proof.py run (seed 2026, 1,570 s, sections A–H) printed ALL CHECKS PASSED (check_proof_out_review1.txt), and E2 alone with seed 11 also had 0 failures (e2_seed11_out.txt). No fatal or major gap remains. The open items are the ones listed under Gaps in §8, which are the formalization risks: the hand proof of §3 is not yet machine-checked, and the rside bridge in RM is fiddly. Status: CHECKPOINT_B, proof.md ready, and formalization may start.