1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE--- halts

This machine halts. An informal growth estimate puts its step count on the scale of a power tower of height about 195. The count is not computed, and the formal proof establishes only halting.

The left part of the tape is a binary counter, written with two words of three cells each. The right part is a unary register. Each increment of the counter is one bounce of the head, and every bounce makes the register one unit longer.

When the counter is full, an overflow turns the register into new low digits of the counter. It also re-reads the old counter, shifted by one word. From the blank tape the machine runs 194 of these cycles.

In the 195th overflow, an increment inside the re-read carries off the far end of the counter. A short run near the far end then reaches F reading 1, the only undefined transition.

The table is that of busycoq's verify/SOBCv6.v, Module TM3, with the states renamed. So TM3's rules hold unchanged. The new parts are bookkeeping for astronomically long blocks of digits, a checked computation of 192 cycles, and a halting argument at the far end of the counter.

Machine and status

• Machine: 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---, viewer https://bbchallenge.org/1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
• Holdout: line 700 of the 740-machine BB(6) holdout list (line 738 of the 778 list). Class "Shift-overflow bouncer counter".
• Statement: Lemma halt: halts tm c0. with tm := TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---". The proof is written for the string itself, with no mirror and no renaming of the machine.
• Status: formalized in the accompanying .v (838 lines).
• It compiles in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9) in about 26 s with -native-compiler yes.
• coqchk re-checks it, the computed chain included, in about 43 s.
• Print Assumptions halt: functional_extensionality_dep only. The file declares no axiom of its own.
• Template: busycoq verify/SOBCv6.v, Module TM3, which proves that 1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD--- halts.
• Same table under the state map ours A B C D E F = TM3 B C A E D F, with no mirror. TM3 starts in its state A, which is our C. This machine starts in TM3's state B.
• Kept: TM3's words, counter and rules (LInc, LOv, Incs, Ov and the block lemmas), with only the two head notations renamed. Also kept: its abstract-list checker (LInc_rec, LIncs_rec, LOv_rec, step_rec, P).
• Changed: a new start (38,573 steps to the first abstract configuration), and 192 abstract cycles instead of 2.
• Changed: every block carries a lower bound on its length, so an increment can stop inside a block of W1 W0 pairs (§5.2).
• Changed: the explicit pair on the far side of a block is split off when it is needed (the peel, §5.4). The bound on the count is kept in binary and saturates at 256.
• Changed: the halt is a far-end predicate, Doomed (§4.7, §8), in place of TM3's short direct run next to the head.
• Step count: informally estimated on the scale of a power tower of height about 195 (§8.3); neither computed nor proved.

Where each part lives in the .v

A comment at the end of the .v restates the rules in busycoq's closing-comment style.

Summary

The proof has six pieces.

1. The rules at a glance

This block is in the style of a busycoq closing comment, in this machine's state names. Each item is defined and argued in §2–§8.

1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
  = SOBCv6.v TM3 "1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD---" with ours A B C D E F = TM3 B C A E D F

      0     1
  A   1RB   0RD
  B   1LC   1RE
  C   1LA   0LD
  D   0RE   0RF
  E   1LC   1RA
  F   0LE   ---

words (paper order)  W0 = 001   W1 = 111
lists                head first: x = x_0 x_1 ... x_(k-1), x_0 next to the head
Lmp(x)               0^inf w(x_(k-1)) ... w(x_1) w(x_0)
RC(n)                1 (011)^n 01 0^inf
P(x)                 Lmp(x) <D 010 RC(1)
TM3 notation         l <| r  =  l <D 010 r          l |> r  =  l A> r
digits               W1 W0 = digit 0,  W1 W1 = digit 1,  a lone W0 = separator;  lowest digit next to the head
count(x)             sum over digit pairs p (p = 0 next to the head) of (1 - b_p) 2^p
ones(x)              x with every digit pair set to W1 W1

LInc     Lmp(x) <D 010 r         -->*    Lmp(LInc x) 001 A> r              r never read
LOv      Lmp(x) <D 010 1 r       -->*    Lmp(LOv x) A> r                   x in {W0, W1 W1}*, r never read
Incs     Lmp(x) <D 010 RC(1)     -->*    Lmp(ones x) <D 010 RC(c+1)        c = count(x), c odd
Ov       Lmp(x) <D 010 RC(2m+2)  -->*    Lmp((W1 W0)^m W1 W1 x') <D 010 RC(1)     LOv(x) = W0 x'
cycle    P(x)                    -->+    P((W1 W0)^((c-1)/2) W1 W1 x')     c = count(x) odd, LOv(ones x) = W0 x'
walk0    Lmp(x) 001 <D 010 1 r     -->(19)  Lmp(x) <D 010 1 011 r          Lmp(x) and r never read
walk1    Lmp(x) 111 111 <D 010 1 r -->(12)  Lmp(x) <D 010 1 010101 r       Lmp(x) and r never read
far      Lmp(x_far) <D 010 1 r   -->(1368)  F reads 1 (halt)               x_far = (W1 W1 W0)^5 (W1 W1)^3, r never read

LInc(W0 t) = W0 LInc(t)      LInc(W1 W0 t) = W1 W1 t      LInc(W1 W1 t) = W1 W0 LInc(t)      LInc([]) undefined
LOv([]) = W0 W1              LOv(W0 t) = W1 LOv(t)
LOv(W1 W1 t) = W0 W0 W1 v'          if LOv(t) = W0 v'
LOv(W1 W1 t) = W0 W0 W0 LInc(v')    if LOv(t) = W1 v'

blocks (abstract)    W10(l) = (W1 W0)^(1+l+n)    W11(l) = (W1 W1)^(1+l+n)    n >= 0 free for each block
step_rec             x -> W10(n-1) W1 W1 x2    where LIncs_rec(x) = (x0, n, 1), n >= 1, LOv_rec(x0) = W0 x2

init     c0 -->(847) P(x0) -->(1289) P(x1) -->(36437) P(x2)    x0 = 1000111011, count 5, then count 51
chain    x2 --(192 step_rec, maxv = 256)--> x194    (all succeed; smallest block bound 62)
halt     P(x194) --Incs--> Lmp(z) <D 010 RC(2N+2),  z = prefix ++ x_far,  prefix in {W0, W1 W1, (W1 W1)^k}*
         walk0 / walk1 through the prefix, then far: halts

2. The machine and TM3

2.1 The table and the state map

The transition table is in §1. The only undefined transition is F reading 1.

verify/SOBCv6.v, Module TM3 (lines 1164–1736) proves that 1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD--- halts. This machine's table is TM3's under the following state map:

No mirror is involved. A brute-force search over all renamings of the states finds this map.

2.2 What this means for the proof

TM3 starts in its state A, which is our C. This machine starts in A, which is TM3's B. So the run from the blank tape is a different run.

Still, every TM3 lemma that does not mention c0 is a statement about the table alone. Those lemmas hold for this machine once the two state names in TM3's notations are renamed:

• TM3's E becomes our D: Notation "l <| r" := (l <{{D}} [0;1;0] *> r), and hL := (D,[0;1;0]).
• TM3's B becomes our A: Notation "l |> r" := (l {{A}}> r), and hR := (A,<[0;0;1]).

The .v does not use the renaming as a formal step. It proves TM3's lemmas again on this table, with TM3's proof scripts. Those scripts are es, er, follow and solve_segRLs runs, and they replay unchanged because the renamed table makes the same moves.

3. Words, counters and configurations

3.1 Words and lists

There are two words of three cells each, in paper order (left to right):

W0 = 0 0 1
W1 = 1 1 1

A counter is a list of words. Lists are written head first: x_0 is the word next to the head.

Lmp(x) = 0^inf  w(x_(k-1)) ... w(x_1) w(x_0)

This is TM3's Lmp. The far end of the counter is the end next to 0^inf.

3.2 Digits

Read a list from the head. A W0 on its own is a separator. A W1 and the word after it form a digit pair:

The lowest digit is the pair nearest the head. A list parses if reading it this way never leaves a W1 without a partner.

For a list with D digit pairs b_0, b_1, … (b_0 nearest the head), the count is the number of increments that fill the counter:

count(x) = sum over p of (1 - b_p) 2^p  =  2^D - 1 - value(x)

ones(x) is x with every pair set to W1 W1. A ones-list is a list of separators and W1 W1 pairs only.

The count is odd exactly when the lowest digit is 0. That is, the first digit pair read from the head is W1 W0.

3.3 The right part and P-configurations

RC(n) = 1 (011)^n 01 0^inf
P(x)  = 0^inf Lmp(x) <D 010 RC(1)

In l <D r the head is on the last cell of l, in state D. TM3 writes l <| r for l <D 010 r, and l |> r for l A> r (in our state names).

4. Rules on explicit lists

§4.1–§4.5 and the block lemmas L1–L3 are TM3's rules, proved in the .v with TM3's scripts (§2.2). L4, L5 and the walk-in rules of §4.7 are new. All are stated here in this machine's notation, with their exact domains.

4.1 LInc: one increment from the head end

LInc is a partial function on lists (TM3's inductive LInc):

LInc([]) undefined is the case that matters at the end: the carry runs off the far end of the counter.

Rule (LInc_spec). If LInc(x) is defined, then for every r:

Lmp(x) <D 010 r   -->*   Lmp(LInc x) 001 A> r

The head never reads r.

4.2 LOv: re-reading a full counter

LOv is a partial function on ones-lists (TM3's inductive LOv). Let v = LOv(t).

The output is two words longer than the input. In each W1 W1 case the word boundary moves by one word. This is the "shift" in shift-overflow.

Rule (LOv_spec). If LOv(x) is defined, then for every r:

Lmp(x) <D 010 1 r   -->*   Lmp(LOv x) A> r

The head never reads r.

How the machine runs LOv. It first walks left through the whole counter (§4.7) and turns at the far end. On the way back it rewrites one token at a time, using the first word of the deeper result. In the W1 W1 case with deeper result W1 v', it makes an LInc excursion back into the deeper part.

4.3 Incs: filling the counter

Rule (Incs). If x parses and c = count(x) is odd, then:

Lmp(x) <D 010 RC(1)   -->*   Lmp(ones x) <D 010 RC(c+1)

Each of the c increments is one bounce: LInc on the left, one more 011 on the right. TM3 proves it with LIncs_spec and RIncs, combined by sideRLs_concat_1L.

TM3's LIncs x x' c is the relation x' = ones(x), c = count(x).

4.4 Ov: the overflow

Rule (Ov). If x is a ones-list and LOv(x) = W0 x', then for every m ≥ 0:

Lmp(x) <D 010 RC(2m+2)   -->*   Lmp((W1 W0)^m W1 W1 x') <D 010 RC(1)

LOv runs first (§4.2). Then the leading W0 of LOv's result and the register RC(2m+2) turn into m new digit pairs W1 W0, one pair W1 W1, and a fresh RC(1).

This is TM3's Ov, proved by LOv_spec and es.

4.5 One cycle

Incs followed by Ov, with 2m + 2 = c + 1, gives one cycle:

P(x)   -->+   P((W1 W0)^((c-1)/2) W1 W1 x')
         where c = count(x), LOv(ones x) = W0 x'

The cycle is defined exactly when all of the following hold. Each failing item is a way the chain could stop:

Every cycle contains c ≥ 1 bounces, so it takes at least one step. After a cycle the lowest digit is 0 whenever (c − 1)/2 ≥ 1, so the next count is odd again.

4.6 Block lemmas

Long runs of equal pairs are handled by these lemmas on explicit lists. In each, n ≥ 0, and x is any list for which the left-hand side is defined.

Proof of L4. Split off the far pair:

(W1 W1)^(1+n) x  =  (W1 W1)^n (W1 W1 x)

One LOv step on W1 W1 x gives W0 W0 W0 LInc(v). That starts with W0 W0, so L3 applies to the remaining n pairs. In the .v the split is lpow_shift from the framework plus app_assoc. ∎

The same split with deeper result W0 v would give a second lemma. The chain never needs it, so the proof leaves it out (§5.4).

4.7 Walk-in rules and the halting predicate

LOv starts by walking left through the counter. The walk past one token does not depend on anything else on the tape.

walk0. For every left part Lmp(x) and every r:

Lmp(x) 001 <D 010 1 r   -->(19)   Lmp(x) <D 010 1 011 r

walk1. For every left part Lmp(x) and every r:

Lmp(x) 111 111 <D 010 1 r   -->(12)   Lmp(x) <D 010 1 010101 r

In both, the head reads neither Lmp(x) nor r. By induction on k:

Lmp((W1 W1)^k x) <D 010 1 r   -->(12k)   Lmp(x) <D 010 1 (010101)^k r

The halting predicate. Call a list x doomed if, for every r, the machine started in the following configuration halts:

Lmp(x) <D 010 1 r

By walk0 and walk1:

• if x is doomed, so is W0 x;
• if x is doomed, so is W1 W1 x;
• if x is doomed, so is (W1 W1)^k x, for every k.

So a ones-list is doomed as soon as some suffix of it, at a token boundary, is doomed.

The base case is the far rule (§8.2): x_far = (W1 W1 W0)^5 (W1 W1)^3 is doomed. This is the far-end halting predicate. It replaces TM3's short direct run next to the head.

5. Abstract lists

From cycle 2 on, every new block of W1 W0 pairs is huge. Cycle 2's block has 654,311,423 pairs, and each later block is about 2 to the power of the one before.

The proof does not track block lengths. It tracks a lower bound for each block.

5.1 Tokens

An abstract list is a list of tokens:

Each block has its own free n. The number l is the block's bound. TM3's W10 and W11 are the case l = 0.

An abstract list X denotes an explicit list x, written Lmp'(X, x), when x is obtained by choosing an n for every block. This is TM3's Lmp' with the extra l.

The abstract P-predicate is TM3's P:

P'(X)  :=  there is x with Lmp'(X, x) and c0 -->* P(x)

5.2 LInc_rec

The rows cover every list. The last row rejects misaligned pairs such as W1 W10(l). They never occur in the chain: LIncs_rec (§5.3) rejects them too, and it succeeds on every list of the chain.

Spec. If LInc_rec(X) = Y and Lmp'(X, x), then LInc(x) is defined and Lmp'(Y, LInc x).

The new case is where the bound is needed. After the first pair of a W10 block becomes W1 W1, the rest of the block must still be non-empty to be a block.

5.3 LIncs_rec

LIncs_rec(X) = (X0, n, m). Here X0 is X with every pair set to W1 W1 and every W10(l) changed to W11(l). The count of every denoted list is 2N + m with N ≥ n.

Let (T0, n, m) = LIncs_rec(T):

This is TM3's LIncs_rec with l carried along. A block counts as one pair for the lower bound, which is enough. The cap is maxv = 256 instead of TM3's 4.

Spec (TM3's LIncs_rec_spec). If LIncs_rec(X) = (X0, n, m) and Lmp'(X, x), then ones(x) is denoted by X0, count(x) = 2N + m, and N ≥ n.

The proof is TM3's. Its block cases use L1 and L2 with exponent 1 + l + n instead of 1 + n.

5.4 LOv_rec and the explicit pair on the far side

Let V = LOv_rec(T):

"Anything else" means one of these:

• a W10 token or a W1 W0 pair (X is not a ones-list);
• a W1 not followed by an explicit W1;
• W11(0) T with V = W1 V' (no bound left to peel);
• W11(l) T with V = W0 V', where V' does not start with W0 (the case left out, below);
• a failing LInc_rec(V'), or a failing V.

The explicit pair on the far side. TM3's LOv_rec has only the keep case. It needs the deeper result to start with W0 W0, which is what an explicit W1 W1 pair just beyond the block produces.

In this run the deeper result usually starts with W1. TM3's function fails there, at cycle 4. The peel case splits the far-most pair off the block as an explicit W1 W1 pair:

(W1 W1)^(1+(l+1)+n) t  =  (W1 W1)^(1+l+n) (W1 W1 t)

The explicit pair is then processed by the plain W1 W1 case. Its result starts with W0 W0, and the rest of the block is TM3's keep case. The cost is one unit of bound.

The same could be done statically, by storing explicit pairs on the far side of every block when it is made. A block made in cycle k would need 192 − k of them, about 18,000 pairs in all, which roughly doubles the list. The peel does it on demand and keeps x194 at 38,120 tokens.

The case left out. A deeper result W0 V' with V' not starting with W0 could be peeled the same way. The chain never meets it: of the 18,336 W11 cases in the 192 cycles, 191 are keep and 18,145 are peel.

A missing case only makes LOv_rec fail, and a failure proves nothing. So leaving it out is sound, and it saves one lemma and one case.

Spec. If LOv_rec(X) = Y and Lmp'(X, x), then LOv(x) is defined and Lmp'(Y, LOv x).

Each case looks at V once, so LOv_rec is linear in the list length plus the LInc excursions. A peel that called LOv_rec again on the peeled list would recompute the deeper part, and it would be exponential in the number of blocks.

5.5 step_rec

step_rec(X):
  (X0, n, m) := LIncs_rec(X)        require m = 1 and n >= 1
  LOv_rec(X0) = W0 X2               require it is defined and starts with W0
  result:  W10(n-1) W1 W1 X2

Spec (step_rec_spec). If step_rec(X) = Y and P'(X), then P'(Y).

Proof. Take x with Lmp'(X, x) and c0 →* P(x). By §5.3, count(x) = 2N + 1 with N ≥ n. Incs gives:

Lmp(ones x) <D 010 RC(2N+2)

By §5.4, LOv(ones x) = W0 x2 with Lmp'(X2, x2). Ov with m = N gives P((W1 W0)^N W1 W1 x2).

Finally (W1 W0)^N = (W1 W0)^(1+(n-1)+(N-n)) is denoted by W10(n-1). ∎

Unlike TM3's step_rec, the new block is a single abstract token, with no explicit pairs around it.

6. The start

Direct simulation from the blank tape gives three P-configurations:

Here 1 = W1 and 0 = W0, head first. The x column is grouped into tokens for x2.

The first two cycles are exact and small. count(x0) = 5 and count(x1) = 51, and the cycle rule of §4.5 maps x0 to x1 and x1 to x2. This agrees with the simulation.

The blocks made in these two cycles are short: 2 and 25 pairs. Each loses about one pair per cycle, so as abstract blocks their bounds would run out. Started at x0 or at x1, the abstract chain fails in cycle 2 or cycle 25. That is why the abstract chain starts at x2.

In the .v, init proves P'(x2) with x2 written out as 70 explicit tokens. The 38,573 steps are one solve_init run.

count(x2) = 1,308,622,847. So cycle 2 makes a block of 654,311,423 pairs, and from then on every new block is far beyond any bound used here.

7. The chain: 192 abstract cycles

7.1 The computation

Start from x2, written with tokens W0 and W1 only (no blocks). Apply step_rec 192 times with maxv = 256:

x2  --step_rec-->  x3  --step_rec-->  ...  --step_rec-->  x194

Every call succeeds. These facts come out of the computation:

The smallest maxv that works is 194; maxv = 193 fails in cycle 193. So 256 leaves a margin of 62.

7.2 Why the bounds last

Each block is kept in its first cycle: right after it is made, the pair W1 W1 that follows it gives the deeper result W0 W0. In every later cycle it is peeled once. Now and then an LInc stops on it, at most three times over its life.

A block made in cycle k is processed in cycles k+1 … 193: one keep and 192 − k peels. So its bound at x194 is at least:

255 − (192 − k) − 3  =  60 + k  ≥  62

This explanation is descriptive. The proof only needs the computation to succeed.

7.3 Shape of the run

Near the head the list settles into segments separated by blocks. x194 starts:

W10(255) 1 1 0  W10(255) 0 0 0 1 1  W10(253) 0 1 0 0 0 1 1  W10(252) 0 0 0 0 1 0 0 1 1  W10(251) ...

Each segment is two words longer than the one before. The far end, about 100–200 words, keeps changing and looks irregular.

This does not matter. The run is a finite computation, and the proof executes it.

8. The halt

8.1 From P(x194) to the far end

Incs. By §5.3, LIncs_rec(x194) = (z, 256, 1). So for the explicit list x194' that the run reaches, count(x194') = 2N + 1 with N ≥ 256. Incs gives:

c0  -->*  P(x194')  -->*  Lmp(z') <D 010 RC(2N+2)

Here z' = ones(x194'), and z denotes z'.

The overflow fails. LOv_rec(z) fails, so §4.5 does not give a 195th cycle. Instead z splits as follows:

z = prefix ++ x_far
x_far  = (W1 W1 W0)^5 (W1 W1)^3          21 words, 13 tokens
prefix = 16,971 W0 + 10,468 pairs W1 W1 + 192 blocks W11(l)

Every denoted z' has the same shape, with each block a run of W1 W1 pairs.

Walk in. RC(2N+2) begins with 1, so the configuration has the form Lmp(z') <D 010 1 r. By walk0, walk1 and the block form of walk1, the head walks through the whole prefix. It arrives at Lmp(x_far) <D 010 1 r' for some r'.

8.2 The far tail halts

For every r, direct execution gives:

0^inf Lmp(x_far) <D 010 1 r
   -->(191)    0^inf <D 010 1 (010101)^3 (011 010101)^5 r
   -->(856)    0^inf <D 010 101010101010101010101101101101101101101101101101101101101011010101 r
   -->(321)    0^inf 1^6 0^2 1^4 0^2 1^4 0^2 1^7 0^2 1^4 0^2 1^4 0^2 1^4 0^2 1^4 0^2 1^4 0^2 1 0^4 1 <F 010101 r

The last configuration has F reading 1: the machine halts after 1,368 steps. The head stays between 4 cells beyond the far end and the first cell after x_far, so it never reads r.

In LOv terms:

1. Steps 0–191. walk0 and walk1 through the 13 tokens of x_far.

2. The return pass. LOv of the far three pairs is W0 W0 W1 W0 W1 W0 W1 W1. As a counter, that is the value 4 on three digits.

3. Three increments. Each following W0, W1 W1 token pair (going toward the head) adds W0 W0 W0 and increments that counter: 5, 6, 7. The value 7 is W0^11 (W1 W1)^3.

4. The carry runs off (step 1,047). At the fourth pair the deeper result is W1 W0^11 (W1 W1)^3, so LOv must increment W0^11 (W1 W1)^3. The carry passes the eleven separators and the three ones and runs off the far end: 0^inf <D 010 ….

5. The halt (step 1,368). The machine moves back and forth over the partly rewritten tokens, between 4 cells beyond the far end and cell 63. It halts in the image of the nearest token of x_far, 60 cells from the far end.

x_far is the shortest token suffix that works. With 12 tokens or fewer, the head reaches r before any halt.

8.3 Conclusion

The pieces fit together in this order:

1. c0 →* P(x2), by the start (§6).
2. P'(x194), by 192 applications of step_rec_spec (§7).
3. The Incs run and the walk-in of §8.1.
4. The 1,368-step run of §8.2.

So halts tm c0.

Why --- is not read earlier. The returning rules Incs, Ov, LInc, LOv, walk0 and walk1 are exact runs that finish before reaching F reading 1. The final far run first reaches F reading 1 at its endpoint, after 1,368 transitions.

The step count. It is not needed for the proof. The informal growth estimate treats each cycle's count as roughly 2 to the power of the previous one, suggesting a tower scale of height about 195. The formal proof does not establish this quantitative estimate.

9. How the .v states it

9.1 From TM3, with only the notations renamed

These need only the notation change of §2.2. Their proofs are TM3's. Line numbers are those of verify/SOBCv6.v.

9.2 Changed from TM3

The peel's 1+S l0+n is convertible to 1+(1+l0+n), so LOv_peel applies without rewriting.

9.3 The computation and the theorem

The chain is a plain iteration of step_rec, by recursion on the number of cycles:

Fixpoint iter (k:nat) (x:list LD') : option (list LD') :=
  match k with O => Some x | S k0 => step_rec x &&& (fun y => iter k0 y) end.
Lemma iter_spec k x y: iter k x = Some y -> P x -> P y.        (induction on k, step_rec_spec)

x194 is never written in the source. The whole check is one boolean, with k as a parameter:

final_check k :=  match iter k x2' with
                  | Some y => match LIncs_rec y (S (length y)) with
                              | Some (z, n, m) => if m =? 1 then doom_rec z else false
                              | None => false end
                  | None => false end

final_check_ok : final_check 192 = true             (vm_compute; reflexivity)
halt_from k    : final_check k = true -> halts tm c0
halt           := halt_from 192 final_check_ok

halt_from is proved for an arbitrary k, so no tactic reduces the 192-cycle term. Only final_check_ok evaluates it.

The proof of halt_from follows §8.3:

1. final_check_spec unpacks the boolean into iter k x2' = Some y, LIncs_rec y _ = Some (z, n, 1) and doom_rec z = true.

2. iter_spec with init gives P'(y): an explicit x with Lmp'(y, x) and c0 -->* Lmp x <| RC 1.

3. LIncs_rec_spec gives LIncs x z' (n'*2+1) and Lmp'(z, z').

4. doom_rec_spec gives Doomed z'.

5. Incs takes the configuration from P(x) to the one below. RC begins with [1], so Doomed z' applies, and halts_evstep closes the goal.

Lmp x <| RC 1   -->*   Lmp z' <| RC ((n'+1)*2)

9.4 The halt in the .v

Because Doomed quantifies over every r, doomed_pow needs no walk rule for k pairs at once. Each pair is one doomed_w1.

doom_rec. It is recursive, and it tests for the far tail before it strips anything:

Fixpoint doom_rec (X: list LD') : bool :=
  if ltok_eqb X x_far' then true else
  match X with
  | W0' :: t        => doom_rec t
  | W1' :: W1' :: t => doom_rec t
  | W11 _ :: t      => doom_rec t
  | _               => false
  end.

Here x_far' is x_far with W0' for W0 and W1' for W1.

ltok_eqb is token-wise equality on W0' and W1', false on blocks, with ltok_eqb_spec : ltok_eqb a b = true -> a = b.

The order matters. x_far' itself starts with W1' W1'. A version that stripped a token before testing would strip that pair too, never see x_far' whole, and return false. Testing equality first stops exactly at the split of §8.1.

doom_rec_spec. The induction is on a bound n for length X, since the W1' :: W1' :: t case recurses two elements down.

• If X = x_far', then inversion of Lmp' x_far' x gives x = x_far, and far_halt applies.
• If X = W0' :: t or W1' :: W1' :: t, then inversion gives x = W0 :: x' or W1 :: W1 :: x' with Lmp' t x'. Use the induction hypothesis, then doomed_w0 or doomed_w1.
• If X = W11 l :: t, then inversion of Lmp'_W11 gives x = [W1;W1]^^(1+l+n) ++ x' with Lmp' t x'. Use the induction hypothesis, then doomed_pow.

This needs only one-token inversions of Lmp'. No inversion lemma for Lmp' over ++ is needed, because doom_rec never splits the list.

9.5 Fuel, cost and trust

Fuel. As in TM3, LIncs_rec and LOv_rec get S (length x), and LOv_rec loses one unit per token level. Each LInc_rec call inside LOv_rec gets the fuel of its level, and it needs one unit per token it visits, the stopping token included.

Fuel can only make a function return None, so it affects whether the check succeeds, never soundness. Over the whole chain there are 422,885 LInc_rec calls inside LOv_rec. The smallest slack (fuel minus depth) is 35, and the deepest call is 41 levels.

Cost. The count bound is a binary number (N), so each upd is cheap in the VM. final_check_ok is a single vm_compute; reflexivity lemma.

Trust. coqc checks final_check_ok with the VM. coqchk re-checks the whole file, this lemma included, by plain conversion in about 43 s. So the VM and the native code are not in the trusted base.

10. Numerical sanity checks

These are evidence only; the result rests on the .v file alone. Every claim of §2–§8 was also tested numerically, with simulators that are independent of the .v.

The tape tests use a simulator with unknown cells. A run that reads an unknown cell fails, so a pass shows the rule for every content of the unknown part.

The full-scale run halts with F reading 1, 60 cells from the far end, after 815,565 steps for minimal blocks. That is exactly 19 steps per separator plus 12 per pair of the prefix plus 1,368.

Direct runs on instantiated tapes, with long blocks cut to 1–3 pairs, halt the same way. Measured from the leftmost cell the run visits, 4 cells beyond the far end, the halt is at cell 64.

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).