1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---: halts

W5-7 halts. Its step count is a power tower of height about 195. It is not computed and not needed.

The machine has the same table as busycoq's SOBCv6.v Module TM3, with the states renamed. The left part of the tape is a binary counter written in two words. The right part is a unary register that grows by one with every increment.

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

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

The proof reuses TM3's rules unchanged. The only new ingredients are bookkeeping for the astronomically long blocks of digits and a halting argument at the far end.

• Machine: 1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---, viewer https://bbchallenge.org/1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---
• Holdout list: line 700 of data/holdouts/BB6_holdouts_740.txt (byte exact). Also line 738 of the 778 list.
• Sheet: class "Shift-overflow bouncer counter"; no status, no notes, no "done by". Discord: only on mxdys's UBRRBA to-do list (data/discord/2026-08-24_mxdys_ubrrba_86.txt), which is not a claim.
• Written for: the string itself. No mirror and no renaming of the machine is needed. The table is TM3's under the state map below, so TM3's Rocq lemmas hold for it once the notations are renamed.
• Statement to prove: Lemma halt: halts tm c0. with tm := TM_from_str "1RB0RD_1LC1RE_1LA0LD_0RE0RF_1LC1RA_0LE---".
• Status: informal proof (this file). All claims are checked by check_proof.py (46 checks, all PASS, §10). No .v yet.

1. The rules at a glance

This block is in the style of a busycoq closing comment. It is all in our state names. Every 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 its relation to TM3

2.1 The table and the state map

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

SOBCv6.v Module TM3 (vendor/busycoq/verify/SOBCv6.v, lines 1164–1736) proves that 1LB0LE_1RC0RE_1LA1RD_1LA1RB_0RD0RF_0LD--- halts. Our table is TM3's under this state map:

No mirror is involved. The map was found by brute force over all renamings in the observe stage; check T1 recomputes it.

2.2 What this means for the proof

TM3 starts in its state A, which is our C. Our machine starts in A, which is TM3's B. So the run from the blank tape is different, but every TM3 lemma that does not mention c0 is a statement about the table alone.

Those lemmas therefore hold for our machine after renaming the two state names that TM3's notations use:

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

The Rocq proofs of those lemmas are es, er, follow and solve_segRLs runs. They replay unchanged on the renamed table, because the renamed table makes the same moves.

3. Words, counters and configurations

3.1 Words and lists

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, when 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 L1–L3 are TM3's rules, proved in Rocq for this table (§2.2). L4–L5 and the walk-in rules of §4.7 are new. All are restated here with our notation and their exact domains. §10 lists the simulation checks.

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 (check W1).

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, which 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 (check W2).

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 word W0 at the head of LOv's result and the register 1 (011)^(2m+2) 01 turn into m new digit pairs W1 W0, one pair W1 W1 and a fresh RC(1) (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 these hold. Each failing item is a way the chain could stop:

Every cycle contains c ≥ 1 bounces, so it takes at least one step: there is progress. 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.

The split is lpow_shift from Helper.v plus app_assoc.

The same split with deeper result W0 v would give a second lemma, W0 W0 (W1 W0)^n W1 v. 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 (checks W5, W6). 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. Say a list x is doomed if, for every r, the machine started in Lmp(x) <D 010 1 r halts.

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 one 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. 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:

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

It is TM3's P.

5.2 LInc_rec

The rows cover every list. The last row rejects misaligned pairs such as W1 W10(l) (check A5). 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). X0 is X with pairs set to W1 W1 and 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. We take 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 our run the deeper result usually starts with W1. TM3's function fails there at cycle 4 (observe stage). 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)

Then the explicit pair is 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 second lemma mentioned under L4). The chain never meets it: of the 18,336 W11 cases in the 192 cycles, 191 are keep and 18,145 are peel (check C4).

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

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. Do not implement a peel by calling LOv_rec again on the peeled list: that recomputes the deeper part and is 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. There are no explicit pairs around it.

6. Initial segment

Direct simulation from the blank tape (check I2):

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 (check I1). 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 (check C8). That is why the abstract chain starts at x2.

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 (check C1):

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 (check C6). 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 (check C4b). In every later cycle it is peeled once, and now and then an LInc stops on it, at most three times over its life (check C5b).

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, notes.md) keeps changing and looks irregular. This does not matter: the run is a finite computation that the proof executes.

7.4 Cross-checks

The chain agrees, block for block, with the observe stage's independent stack model work/model/fast.py. That model keeps exact lengths for short blocks and marks a new block BIG when it has more than 10⁶ pairs. We compare after merging explicit pairs into an adjacent block of the same kind. They agree at cycles 2–11, 50, 100, 150, 190, 193 and 194 (check C7).

fast.py was itself checked against the exact list model and against direct simulation in the observe stage.

Instantiated cycles 2–9 (each block with its minimal length, and with one extra pair) were also run on the tape. The overflow phase reaches the exact next P-configuration, and step_rec's result denotes it (check D1).

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, and Incs gives:

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

Here z' = ones(x194'), denoted by z (check H1).

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

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)

This is check H3. 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 is 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 (checks W7, W7c):

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 (check H4):

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 (check W7b).

8.3 Conclusion

c0 →* P(x2) (§6). Then P'(x194) by 192 applications of step_rec_spec (§7). Then the Incs run and the walk-in of §8.1, and the 1,368-step run of §8.2. So halts tm c0.

Why --- is not read earlier. Every step before the last one belongs to an exact rule: Incs, Ov, LInc, LOv, walk0, walk1, or the first 1,368 steps of the far run. Each of these is an exact run that ends in a configuration other than F reading 1.

The step count is not needed. Each cycle's count is about 2 to the power of the previous one, so the total is a tower of height about 195.

8.4 Full-scale confirmation

The complete cycle-194 overflow was also run on an instantiated tape: every block at its minimal length 1 + l, and again with one extra pair (check H5). The tape has about 99,000 words.

The run halts with F reading 1, 60 cells from the far end, after 815,565 steps (minimal blocks). That is exactly 19 per separator plus 12 per pair of the prefix plus 1,368. The observe stage's direct runs agree: 64 cells from the moved far end, which is 4 cells further out.

9. Lemma plan against SOBCv6.v TM3

Copy Module TM3 (lines 1164–1736) into a new module for our string, and make the changes below. Line numbers are SOBCv6.v's.

9.1 Reused after renaming the two notations

These need only the notation change of §2.2. Their proofs replay unchanged.

9.2 Changed

9.3 New: the 192 iterations

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

Do not write x194 into the source. It has 38,120 tokens. State the final check as one boolean (§9.4) and prove it by vm_compute; reflexivity.

Alternatively start at x0 (step 847) as the plan in notes.md suggests. Then the first two cycles must be done with TM3's explicit Incs and Ov and concrete LIncs and LOv derivations (solve_L), because step_rec would turn their short blocks into abstract ones that run out. Starting at x2 avoids this.

9.4 New: the peel lemma and the halt

Because Doomed quantifies over every r, doomed_pow needs no walk rule for k pairs at once (the k-pair form of walk1 in §4.7, walkk in the earlier plan). Each pair is one doomed_w1.

RC k is [1] *> …, so the configuration after Incs has the form Lmp z' <| [1] *> r that Doomed needs.

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

Definition LD'_eq_dec (a b: LD'): {a = b} + {a <> b}.    (decide equality; Nat.eq_dec; Defined)

Fixpoint doom_rec (X: list LD'): bool :=
  if list_eq_dec LD'_eq_dec 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.

The order matters. x_far' itself starts with W1' W1'. A version that strips 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 (check H6).

doom_rec_spec. Strong induction on length X; the W1' :: W1' :: t case recurses two elements down.

• If X = x_far', then invs on Lmp' x_far' x gives x = x_far, and far_halt applies.
• If X = W0' :: t or W1' :: W1' :: t, then invs 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 Risks and costs

vm_compute time. The bounds are unary nat up to 256. Nat.min maxv (n*2+m) costs about 800 reductions per digit.

Over the chain that is roughly 7·10⁵ digit visits, so about 6·10⁸ reductions. If it is slow, switch the bound in LIncs_rec to N.

Fuel (measured). TM3 passes S (length x0) to LOv_rec, which loses one unit per token level. Each LInc_rec call inside LOv_rec gets the fuel of its level. It needs one unit per token it visits, the stopping token included.

Under this convention, over the whole chain (check C9):

LInc_rec calls inside LOv_rec    422,885
smallest slack (fuel - depth)    35
deepest call                     41 levels

So TM3's fuel suffices with room to spare. LIncs_rec gets S (length x) and visits at most length x + 1 levels, so it cannot run out either.

far_halt. TM3's own halt also ends with a symbolic direct run (repeat (step1 || sr) after unfolding Lmp). Here it is 1,368 steps with r symbolic. The head never reaches r, so no case split on r is needed.

Statement. The kill criteria want the final theorem Lemma halt: halts tm c0. (the halting form). Plan for check_kill.sh --halt as for C2-552.

10. Evidence

check_proof.py checks every claim above (python3 -B check_proof.py, about 9 s; --quick about 6 s). Latest run: 46 checks, 0 FAIL (work/check_proof.out).

The tape checks use a partial simulator. Cells marked unknown must never be read, so a pass shows a rule for every value of the unknown part.

The rules of §4 are already Rocq lemmas (TM3's, §2.2) except L4–L5 and walk0/walk1/far. The checks are there to catch transcription errors.

11. Gaps

• Not formalized yet. Every new lemma of §9.2–§9.4 is still to be written. Nothing here counts as a kill.
• Soundness of the abstract functions (§5) is argued case by case and checked on random instantiations (A1–A4) and exhaustively on small lists (A5). The formal _spec lemmas are the real proof.
• Rocq feasibility of final_check. Time and memory of vm_compute on 192 iterations of lists up to 38,120 tokens is estimated, not measured. Fuel is measured and suffices (§9.5, check C9).
• Equivalence partners (notes.md) follow from this one only through the upstream equivalence files. That is not part of this proof.

Review log

2026-10-13, written (informal_proof stage).

• Built on the observe stage (notes.md). Design changes against its plan:
• lower bounds sit inside the block tokens (W10 l, W11 l) instead of a separate representation;
• the "explicit pairs on the far side" are made on demand by the two peel cases of LOv_rec, not stored. The stored version would roughly double the list.
• The chain starts at x2 (step 38,573) instead of x0 (847): the blocks of cycles 0 and 1 are short and must stay explicit.
• The halting predicate is "doomed" (§4.7): deep part halts ⇒ whole list halts, through two walk-in rules found by simulation (19 and 12 steps). Its base case is the 13-token far tail (1,368 steps, minimal). This replaces the notes' plan of an inductive predicate mirroring LOv with a far-end carry case. The carry is followed by a 321-step run that depends on two more tokens, so a pure "carry ⇒ halt" case would not be sound on its own.
• maxv was measured: 194 is the smallest that works. 256 is used.
• Added during self-review: C4b (keep once per cycle), C5b (LInc stops per block, 0–3), C8 (the chain cannot start at x0 or x1). The §7.2 bound formula was corrected to 255 − (192 − k) − 3.
• Checker fixes during writing:
• C6 first asserted 195/194, but the real threshold is 194/193;
• C7 first compared raw token strings, and differed at cycle 4 only because fast.py keeps a pair next to a block explicit where step_rec merges it. It now compares after merging pairs into adjacent blocks of the same kind.
• Self-review pass.
• Every number in §6–§8 was re-read against work/check_proof.out.
• The three far-run configurations in §8.2 came from a scratch trace; check W7c now compares them cell by cell.
• The §5.4 peel0 condition ("V' not starting with W0") only fixes the case order; peel0 is sound for any V'.
• The §7.2 bound "at most three LInc stops per block" is descriptive. The proof does not use it: the chain computation simply succeeds.

2026-10-13, skeptic round 1: sound, 4 minor gaps, all fixed.

• §5.2, §5.3 failure rows. They now name the misaligned case: a W1 not followed by an explicit W0 or W1 token (lone, or followed by a block). §5.4 lists what "anything else" covers.
• New check A5: every abstract list of ≤ 5 tokens over W0, W1, W10(0..1), W11(0..1) (9,331 lists, 111,111 instantiations). All three functions are sound on every instantiation, and a misaligned W1 is always rejected.
• §9.4 doom_rec. It is now recursive and tests equality with x_far' before it strips a token. This avoids the ordering trap the skeptic named (x_far' starts with W1' W1').
• The spec needs only one-token inversions of Lmp', so no Lmp'_app_inv. walkk is replaced by doomed_pow (induction inside Doomed).
• New checks H6 (doom_rec(z) is true and stops at the H3 split) and H7 (doom_rec sound on 164 random lists, 328 instantiated runs).
• §9.5 fuel. Measured under TM3's convention (new check C9): 422,885 LInc_rec calls, smallest slack 35, deepest call 41 levels. This matches the skeptic's independent measurement. The 2 * length x + 4 fallback is dropped. vm_compute time is still unmeasured (§11).
• §5.4 peel0. Dropped: 0 of the 18,336 W11 cases use it. Its lemma (old L4) is removed, so old L5 and L6 are now L4 and L5. The checker's LOv_rec has no peel0 case either.
• C1–C8 are unchanged (C8 still fails at cycles 2 and 25). A3 now samples 7,179 instances instead of 10,020, because inputs that needed peel0 now fail.
• Re-run: 46 checks, 0 FAIL (43 − old L4 + A5, C9, H6, H7). --quick also passes.