1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB: never halts

• Machine: 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB, viewer https://bbchallenge.org/1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB. A BB(6) holdout on every holdout list since June 2024, and on the current 740-machine list (line 590 there), class "Bell eats counter". Written for the string itself: no mirror.
• Parent: the table is that of 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC (the parent) with its states renamed by σ (§1), and this proof extends the kill for that machine. The parent's write-up is shipped alongside as parent-proof.md; "parent §n" is section n there. From the blank tape, this machine runs the parent's table from 0^inf B> 0^inf (in the parent's names): a different orbit of the same epoch map.
• Template: the parent's .v, which is adapted from verify/FractalBEC.v, tm10 (1LB0LF_1LC1LF_1RD1LB_---0RE_1RA0RE_0LA0RC) and keeps only its marker bounce RInc (parent §8.1). Mirrored, tm10 differs from the parent only in C1. Relative to the parent's .v, the state names in the statements are renamed by σ, and the start init, the finite part and the final nonhalt call are new (§8). The rules, the model, the potentials, the invariant and its inductive step inv_step are the parent's text.
• Status: formalized in the accompanying 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v (1,755 lines). It proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c), importing only Individual62 from busycoq. Print Assumptions nonhalt: Closed under the global context. It compiles in about 15 s with -native-compiler yes, and coqchk re-checks it in about 65 s, most of it the finite part's vm_compute.
• Where each section lives in the .v (its sections are comment banners; every lemma is top level):
• §1: tm (top of the file) and the closing table comment. σ is applied to the state names in the statements of Sections 1–4; there is no bridge lemma;
• §2: Section 2 (word, enc) and Section 6 (gw, ginc, gval);
• §3: Section 1 (the finite runs, each one es), Section 2 (LP, Phi, LPspec, Phispec), Section 3 (sound), Section 4 (K, epoch_tm) and Section 5 (lpf, phif, model_sound);
• §4: Sections 6–9 (gcount, DigT_exists);
• §5: Sections 7–11 (Dig_cost, Dig_mass, Dig_len, the bound functions, N1, N2, Inv, next_inv, inv_step, nonhalt_from);
• §6: init (Section 4); orbit, orbit_sound, B691, Y691, fin691 and inv691 (Section 11);
• §7: nonhalt (end of Section 11).

Summary

• Hub. The tape is 0^inf (110)^a 0 (011)^b B> X 0^inf. A bounce moves the marker 0 one block to the right, applies the local pass LP to the counter word X (a binary +1 when X is a clean counter), and spends one 011 of the budget b.
• Eat. At b = 1 the machine eats the lowest digit of X. An a-block eat gives new budget. A b-block eat, or a bare tail, sweeps the (110)^a run into a new left record 0^inf <E 101 (001)^k 000 Y.
• Epoch. The next epoch starts at K(1, k+1, Y), where the residue Y is not a clean counter. Its first bounces digest it. The digestion is recursive: at a b-block, one bounce runs a whole sub-epoch on the rest of the word (D6).
• Where halting is. The machine halts only if an eat happens before the digestion is done. The invariant Inv bounds the digestion cost by a constant times about 2^(k/2), against a budget N ≳ 2^(k+3). It is closed for N ≥ 17,705.
• This machine. From the blank tape it reaches K(1,3,t1) at step 55. The rules-only model then runs 691 epochs to K(1, 17712, Y691), where Inv 11 holds. From there inv_step carries the invariant forever.
• The two orbits merge (not used in the proof). The model orbit of this machine and the parent's are different until epoch index 795 of both, at N = 20,922, and identical from then on [C]. Before that, this machine's orbit is another orbit of the same macro map.

1. The machine, the renaming σ, the halting transition

       this machine            parent
      0     1               0     1
 A   1RB   1RF          A  1RB   0RF
 B   1LC   0RD          B  1RC   1RF
 C   ---   0LD          C  1LD   0RE
 D   1LE   0LD          D  ---   0LE
 E   1RA   0RF          E  1LA   0LE
 F   0RE   0LB          F  0RA   0LC

Lemma S (renaming). Let σ map the parent's states to this machine's: A→E, B→A, C→B, D→C, E→D, F→F. Then for every state q and symbol r, this machine's cell (σ q, r) is the parent's cell (q, r) with the target state renamed by σ. This holds for all 12 cells, the halting cell included [S1]. - Equivalently, with φ = σ⁻¹ (A→B, B→C, C→D, D→E, E→A, F→F) and tm30 the parent's table, busycoq's Perm tm tm30 φ holds (verify/Permute.v). That is, this machine's (q, s) is undefined iff tm30's (φ q, s) is, and tm (q,s) = Some (s', d, q') iff tm30 (φ q, s) = Some (s', d, φ q') [S2]. - Consequence: this machine's run from (q, t) is, step for step, tm30's run from (φ q, t) with the states renamed. The tape and head positions are the same. Since φ A = B, this machine from the blank tape is tm30 from 0^inf B> 0^inf. This is checked for 2·10^6 steps [S5].

The only halting transition is C reading 0 (the parent's D0) [S3]. In busycoq a configuration is halted when no transition is defined for it, so the machine halts exactly when it is in C reading 0. C is entered only by B0 = 1LC [S4], which moves left. So one step before, the machine is in B reading 0 with a 0 in the cell to its left (the pattern 0 B> 0). B is entered only by A0 = 1RB, which leaves a 1 to B's left, and by F1 = 0LB [S6]. So the halted configuration comes exactly two steps after a configuration 0 0 F> 1: F1 gives 0 B> 0 0, then B0 gives C reading 0, the only undefined transition [S7]. An exhaustive check over 5-cell windows confirms that this is the only way to be in C reading 0 after two steps [S8]. (Under the convention that also counts the halting transition as a step, it is three steps.)

Rule table in busycoq comment-block style (this machine's names; words as in the .v, Section 2):

(*
      0     1
 A   1RB   1RF
 B   1LC   0RD
 C   ---   0LD
 D   1LE   0LD
 E   1RA   0RF
 F   0RE   0LB
 = 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC with its states renamed A->E, B->A, C->B, D->C, E->D

 words       blk d e w = d01 (001)^e 000 w    p11 x w = 11 (001)^x 000 w    p01 x w = 01 (001)^x 000 w
             p00 w = 00 w    p10 w = 10 w     t0 = ''   t1 = 1   t2 = 010001   t3 = 110001
 hub         K(a,b,w)  = 0^inf (110)^a 0 (011)^b B> w 0^inf           (the .v's K N y is K(1,N,y))
 pre-record  P(k,y)    = 0^inf <D 01 (001)^k 000 y 0^inf              (D0 = 1LE: the left record next)
 left record L(k,T)    = 0^inf <E 101 (001)^k T 0^inf

 LP   (local pass)  l 011 B> w  -->+  l <E 100 w'        (d = 0)
                    l 011 B> w  -->+  l <E 101 000 w'    (d = 1)     for LP w w' d (18 constructors)
 Phi  (epoch map)   l (110)^a 0 (011)^b B> w  -->+  l <D 01 (001)^k 000 y        for Phi a b w k y
   bounce   b >= 2: LP w w' d, then Phi (a+1) (b-1+d) w'
   eats     b = 1:  a-block -> Phi (a+2) (e+1) rest;  b-block -> P(a, p11 (e+d) w');
                    t0 -> P(a+1, t1);  t1 -> P(a, p01 1 t1);  t2 -> P(a, p10 (p00 t2));  t3 -> Phi (a+1) 1 (blk false 0 t0)
   D6       LP (p10 (blk true e w)) (blk false k y) when Phi 1 (e+1) w k y   (one bounce runs a sub-epoch)
 Rst        P(k,y) -->+ K(1, k+1, y)                                  3k + 8 steps
 epoch      K(1,N,y) -->+ K(1,k+1,y')   whenever Phi 1 N y k y'

 start      c0 -->(55) K(1,3,t1);  691 epochs (rules only) -->* K(1,17712,Y691);  Inv 11 17712 Y691
 invariant  Inv k N y (the .v, Section 11): every Inv epoch has a Phi successor that is again Inv
*)

2. Notation, words, families

• Configurations use the busycoq/wiki notation. In l q> r the head is in state q and reads the first symbol of r. In l <q r it reads the last symbol of l. Sides are written in reading order (left to right).
• Chunks: a = 001, b = 101, z = 000. A block is d01 a^e, an a-block if d = 0 and a b-block if d = 1, with exponent e ≥ 0.
• Words are the .v's type word: t0..t3, blk d e w = d01 (001)^e 000 w, p11 x w, p01 x w, p00 w, p10 w. enc w is the cell string followed by 0^inf. Two words with the same enc are the same tape. Examples: p10 t0 ≡ t1, p00 t0 ≡ t0, p10 t1 ≡ blk true 0 t0, p00 t1 ≡ blk false 0 t0.
• Counter words G: gw bs s for a block list bs and a tail t_s (s ≤ 3). There are k = |bs| blocks, LSB first.
• The value is gval bs s = (4+s)·2^k + Σ d_i 2^i, which lies in [4·2^k, 8·2^k).
• ginc is binary +1 on the value. Tails step t0 → t1 → t2 → t3, and t3 → blk false 0 t0 is the overflow (d = 1).
• Residues: an ordinary residue is p11 x (gw bs s). A special residue is one of t1, p01 1 t1 or p10 (p00 t2).
• Families (this machine's names):
• hub K(a, b, w) := 0^inf (110)^a 0 (011)^b B> enc w. The 0 after (110)^a is the marker. The .v's K N y is K(1, N, y).
• pre-record P(k, y) := 0^inf <D 01 (001)^k 000 enc y. Here D reads a blank.
• left record L(k, T) := 0^inf <E 101 (001)^k T. It is one step after P(k, y), with T = 000 y (D0 = 1LE).

3. Rules (this machine's names)

Every statement below is an exact transition with universally quantified contexts. A rule never reads the cells of l or of r, except that its end may be "the head arrives on the last cell of l".

3.1 Window and shift rules (the informal proofs of the es lemmas) [W]

[W] checks each rule in 4 contexts (all-0, all-1 and random l, r), with n = 1..14 for S1–S3 and the step counts as listed.

3.2 The finite runs of the .v's Section 1 [V]

These 27 lemmas are the .v's Section 1. Each is proved by one es (Rst after one const_unfold rewrite). They are the parent's runs with σ applied to the state names: {{A}}→{{E}}, {{C}}→{{B}}, {{E}}→{{D}}. Exponents are symbolic, and l, r are arbitrary. The step counts are exact.

For each lemma, [V] does the following: - It parses the statement from the .v text. - It runs this machine from the left side, for every assignment of the exponents in 0..6 and 4 contexts. - It requires the right side to be reached head-relative, in busycoq's sense, without reading a cell of l or r. The step counts above are fitted and then re-checked on every sample. - As a control, the parent's text (state names not renamed) is run on the parent's table. It passes with the same step counts [V30, V2].

3.3 The local pass LP (the .v's LP w w' d; proof = Section 3 sound) [LP]

LPspec w w' d: for every l, l 011 B> enc w -->+ l <E outp(d) enc w', with outp(0) = 100 and outp(1) = 101000. LP never reads left of the 011.

The D6 sub-epoch works in the context l 0111: the cell left of the sub-hub's (110) holds a 1 where a standalone hub has a 0. Every Phi run reads only cells at or right of its marker. It stops the first time the head reaches the cell left of (110)^a, in state D, so the context does not matter. W10 then reads that 1 and exits.

3.4 The epoch map Phi (the .v's Phi a b w k y) [PH]

Phispec a b w k y: for every l, l (110)^a 0 (011)^b B> enc w -->+ l <D 01 (001)^k 000 enc y. The <D reads the last cell of l.

Case split at b = 1 (the eats), by the word: a-block → E1, b-block → E2, t0..t3 → E0, Et1, Et2, Et3. Up to enc-equality, also p10 t0 ≡ t1, p10 t1 ≡ b-block, p00 t0 ≡ t0 and p00 t1 ≡ a-block. Every other word at b = 1 has no rule; this is an unsafe eat. Two such eats, K(a, 1, '11' z t3) and K(a, 1, '00' t3), do halt (negative control [N]). Every G word at b = 1 has an eat [PH].

3.5 Restart and one epoch

• Rst: P(k, y) -->+ K(1, k+1, y) in 3k + 8 steps, for every y [R]. The first step, D0 = 1LE, gives the left record L(k, 000 y).
• epoch_tm (.v Section 4): Phi 1 N y k y' → K(1, N, y) -->+ K(1, k+1, y'). This is sound applied with l = 0^inf, followed by Rst.

3.6 The computable model (.v Section 5)

lpf n w and phif n a b w are fuel-bounded functions that follow the constructors above. model_sound states that every Some result is an LP/Phi derivation. orbit f n N y iterates phif f 1 N y n times with N := k + 1, and orbit_sound turns orbit … = Some (N', y') into K N y -->* K N' y'. An independent implementation of lpf, phif (same cases in the same order, same fuel accounting; the bounce loop is iterative), orbit and Inv gives the numbers of §6. As a control, it reproduces the parent's .v's fin694 literal exactly, and Inv 10 17713 Y694 [M].

4. Coverage

This section is the parent's, unchanged: words do not mention states. - Lemma H (parent §4). Every hub word has exactly one LP rule, and LP maps hub words into hub words. The case split is on the normalized word: - G words: toggle, carry or tail step; - a block in front of a non-G word: LP_a, or LP_b with the rest by induction on length; - O words, by their prefix: 11 → LP11, 01 → LP0, 00 → LP0, 10 W → by W (tail, LPT, LP_5 at an a-block, LP_6 at a b-block); - the 23 end words, by the table. - Eats: every G word at b = 1 has an eat (§3.4). An eat at a non-G word is the only uncovered case. - In the .v, Lemma H is not stated by itself. DigT_exists and gcount build the LP/Phi derivation for every word that Inv allows, and the computable model covers the words of the finite part.

5. Invariant, inductive step and progress (independent of the start)

5.1 Domain: Inv k N y (the .v, Section 11)

Weights and bounds: - w(q) = 2^⌊(q+1)/2⌋, v2(q) = 2^⌊q/2⌋, p2(q) = 2^(q+1); - Ws(P) = Σ_{q<P} w(q), V2s(P) = Σ_{q<P} v2(q), Pf(k) = max(12, k+3); - Af(k) = 5 Ws(Pf k) + 6 w(Pf k) + 2 Ws(k); - Bf(k) = Af(k) + 5 V2s(Pf k) + 6 v2(Pf k) + 2^(k+1); - Xf(k) = Af(k) + 5 Pf(k) + 7; - Costf(k) = 2 Xf(k) + 2 + 2 Af(k) + 11 Ws(Pf k) + 13 w(Pf k); - Nlo(k) = 2^(k+3) − 8·2^⌊(Pf(k)+3)/2⌋, and Nstar = 17,705.

For a block list bs with exponents e_q at positions q, let Mw(bs) = Σ_q w(q) e_q and M2(bs) = Σ_q p2(q) e_q.

Inv k N y holds iff all of these hold: - N ≥ 17,705; - N ≥ Nlo(k); - y is special (t1, p01 1 t1 or p10 (p00 t2)), or y = p11 x (gw bs s) with s ≤ 3, |bs| ≤ k, Mw(bs) ≤ Af(k), M2(bs) ≤ Bf(k) and x ≤ Xf(k).

Here k bounds the number of blocks seen so far, like κ in the parent's write-up (parent D.6).

[T] recomputes this table and the two threshold facts N1 and N2 below for every k < 200.

5.2 Inductive step: inv_step : Inv k N y → ∃ kk y', Phi 1 N y kk y' ∧ ∃ k', Inv k' (S kk) y'

The proof (.v Sections 7–11; written out in parent §8.3) has these steps: 1. Positions (N1). 7·2^k + Bf(k) < 2^(Pf(k)+1) for every k. The Q potential 2^f·(m + 2Σ 2^i(e_i+1) + p) never exceeds its start value plus 3·2^(f+n), and it starts below 7·2^k + M2(bs). So no digestion creates a counter position ≥ Pf(k) (QI_Ps). 2. Digestion exists. DigT_exists gives DigP x bs s n c bsp sp: the residue reaches the counter word gw bsp sp in n own-level bounces with c absorptions. The constructors are the prefix (2x+2 bounces), LP_5 at an a-block, LP_6 at a b-block (sub-epoch GPhi, then the next level nested in the new block, LPs_nest), and the end chains DigE. 3. Cost (N2, Lemma D). Dig_cost gives n ≤ 2 Mw + 2x + 2 + 11 Ws(P) + 13 w(P) ≤ Costf(k). Also Costf(k) + 2 ≤ 17,705 for k ≤ 11, and Costf(k) + 2 ≤ Nlo(k) for k ≥ 12. So n + 2 ≤ N: the digestion ends inside the budget, and every eat of the epoch is at a G word. 4. Counting ends. gcount: the potential Ψ = value + budget + Σe − #blocks never grows at a bounce and drops at every E1. So the counting phase GPhi (1+n) (N+c−n) bsp sp r reaches E2, E0, Et1, Et2 or Et3. epoch_ord composes everything into Phi 1 N y (rk r) (ry r). 5. Invariant again (next_inv). Dig_mass is used three times: weights (2w(ℓ−1), w), (2^ℓ, v2) and (1, 1). With Dig_len, GPhi_rel and GPhi_val, they give Mw(W') ≤ Af(k'), M2(W') ≤ Bf(k') and x' ≤ Xf(k'), with k' = max(k, k(W')). - If k(W') > k, the value bound gives 2^(k(W')+3) ≤ N' + 8·2^⌊(Pf+3)/2⌋, i.e. N' ≥ Nlo(k'). Otherwise N' > N ≥ Nlo(k). - A special residue digests by an end chain: at most 13 bounces, 5 absorptions and one block with e = 0.

inv_step is a statement about words and Phi. It is proved once for all k, N, y, so it applies to this machine's orbit unchanged. As a sanity check, [J] runs the model on from epoch 691 to epoch 1,200 (N = 33,240). On every epoch, Inv κ_t N_t Y_t holds with κ_t the running maximum of k(W), which is the choice next_inv makes.

5.3 Progress

• Each epoch is K(1, N, y) -->+ K(1, kk+1, y') (epoch_tm). This is at least one step; in fact at least 3·kk + 8, from Rst alone.
• Also kk + 1 ≥ N + 1, since a + b ≤ S (rk r) (GPhi_rk). So N strictly grows. Progress itself only needs -->+.
• progress_nonhalt_cond with P(N, y) := ∃ k, Inv k N y on the configurations K(1, N, y) gives non-halting from any configuration where P holds.

6. Initial segment and finite part (the only new part)

6.1 Blank tape to the first hub: 55 steps [I]

So only the first three steps are not rule applications. The left record at step 4, which reads L(0, '') once the blanks after it are dropped, is the ordinary record L(0, 000·t0). The full trace:

 0                   A> 0                A0 = 1RB
 1  1                B> 0                B0 = 1LC
 2                   C> 11               C1 = 0LD
 3                   D> 001              D0 = 1LE
 4                   E> 0101             E0 = 1RA
 5  1                A> 101              A1 = 1RF
 6  11               F> 01               F0 = 0RE
 7  110              E> 1                E1 = 0RF
 8  1100             F> 0                F0 = 0RE
 9  11000            E> 0                E0 = 1RA
10  110001           A> 0                A0 = 1RB
11  1100011          B> 0                B0 = 1LC
12  110001           C> 11               C1 = 0LD
13  11000            D> 101              D1 = 0LD
14  1100             D> 0001             D0 = 1LE
15  110              E> 01001            E0 = 1RA
16  1101             A> 1001             A1 = 1RF
17  11011            F> 001              F0 = 0RE
18  110110           E> 01               E0 = 1RA
19  1101101          A> 1                A1 = 1RF
20  11011011         F> 0                F0 = 0RE
21  110110110        E> 0                E0 = 1RA
22  1101101101       A> 0                A0 = 1RB
23  11011011011      B> 0                B0 = 1LC
24  1101101101       C> 11               C1 = 0LD
25  110110110        D> 101              D1 = 0LD
26  11011011         D> 0001             D0 = 1LE
27  1101101          E> 11001            E1 = 0RF
28  11011010         F> 1001             F1 = 0LB
29  1101101          B> 00001            B0 = 1LC
30  110110           C> 110001           C1 = 0LD
31  11011            D> 0010001          D0 = 1LE
32  1101             E> 11010001         E1 = 0RF
33  11010            F> 1010001          F1 = 0LB
34  1101             B> 00010001         B0 = 1LC
35  110              C> 110010001        C1 = 0LD
36  11               D> 0010010001       D0 = 1LE
37  1                E> 11010010001      E1 = 0RF
38  10               F> 1010010001       F1 = 0LB
39  1                B> 00010010001      B0 = 1LC
40                   C> 110010010001     C1 = 0LD
41                   D> 0010010010001    D0 = 1LE
42                   E> 01010010010001   E0 = 1RA
43  1                A> 1010010010001    A1 = 1RF
44  11               F> 010010010001     F0 = 0RE
45  110              E> 10010010001      E1 = 0RF
46  1100             F> 0010010001       F0 = 0RE
47  11000            E> 010010001        E0 = 1RA
48  110001           A> 10010001         A1 = 1RF
49  1100011          F> 0010001          F0 = 0RE
50  11000110         E> 010001           E0 = 1RA
51  110001101        A> 10001            A1 = 1RF
52  1100011011       F> 0001             F0 = 0RE
53  11000110110      E> 001              E0 = 1RA
54  110001101101     A> 01               A0 = 1RB
55  1100011011011    B> 1

(Each line is step left-of-head state> head-and-right, with blanks outside.) In the .v, init : c0 -->* K 3 t1 is one solve_init. On the parent's table the same run is B;; tape0 -->* K 3 t1 with the parent's K (state C), also 55 steps [I]. The .v's text of K is reached from c0 at step 55 on this machine's table, and the parent's K from B;; tape0 at step 55 on the parent's [I].

6.2 The finite part: 691 model epochs [F]

orbit 100000 691 3 t1 = Some (17712, Y691), with

B691 = [(false, 10); (false, 6); (true, 1); (false, 1); (true, 1); (false, 1); (true, 1); (false, 1); (false, 1); (true, 1); (false, 0)]
Y691 = p11 10 (gw B691 0)
     = p11 10 (blk false 10 (blk false 6 (blk true 1 (blk false 1 (blk true 1 (blk false 1
         (blk true 1 (blk false 1 (blk false 1 (blk true 1 (blk false 0 t0)))))))))))

• N runs 3, 8, 10, 14, 22, 24, 35, 38, 46, 64, 74, 88, 101, … (index 100: 1,748; 300: 6,698; 500: 12,186; 600: 15,057; 690: 17,684; 691: 17,712).
• The fuel is never close to running out: the smallest fuel left at any call over the 691 epochs is 82,287 of 100,000 [F2].
• Index 691 is the first epoch with N ≥ 17,705. No earlier epoch satisfies Inv k for any k ≤ 40 [F3, F9]. Under the parent's write-up threshold N* = 14,796 (parent D.7), the finite part would end at index 591 (N = 14,797).
• Equivalently, orbit 100000 692 1 t0 = Some (17712, Y691) from the step-11 hub [F7]. The .v starts from K 3 t1.
• The same orbit is the TM's: the model's epoch from K(1, N, y) equals the next left record (k, T) of the TM for all 518 records of a 10^11-step log (to step 99,729,345,754, N = 12,698), and a fresh run to 2·10^7 steps gives the same records [O1, O2]. The record at step 42 is the epoch from K(1,1,t0) [O1].

6.3 The invariant at the end: Inv 11 17712 Y691 [F]

k = 11 is forced. k ≤ 10 fails on |bs| = 11, and k ≥ 12 fails on Nlo(12) = 28,672 > 17,712 [F4, F6]. The value is m(W) = 8,788. The margin in Nstar ≤ 17712 is 7; it is exact arithmetic, checked by vm_compute in inv691.

7. Conclusion

1. c0 -->(55) K(1, 3, t1) (§6.1).
2. K(1, 3, t1) -->* K(1, 17712, Y691): 691 epochs of the model, each an exact TM run by model_sound and epoch_tm (§6.2).
3. Inv 11 17712 Y691 (§6.3).
4. From any K(1, N, y) with ∃k, Inv k N y, inv_step gives an epoch -->+ to another such configuration (§5.2). progress_nonhalt_cond turns this into ~ halts (§5.3).

Hence this machine never halts from the blank tape.

Why C0 is never executed. Every rule is an exact run of this machine that es proves in the .v (the parent's runs under σ) [V], and an es proof cannot pass through an undefined transition. C0 can only be met at an unsafe eat: b = 1 on a word outside G, for example K(a,1,'11' z t3) or K(a,1,'00' t3), which really do halt [N]. Such an eat needs the digestion to outlast the budget. Step 3 of §5.2 (n + 2 ≤ N) rules that out on every epoch where Inv holds. Epochs 0–690 are the explicit model run, where no eat is unsafe: phif returns Some on all of them. In machine terms, the run never reaches 0 0 F> 1 (§1), the configuration that is halted two steps later.

8. The formal proof

The .v is the parent's .v with σ applied to the state names and a new start. 1. The table. tm := TM_from_str "1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB" is the only TM literal in the file, and the step notations -->, -->* and -->+ are on tm. 2. σ on the state names. The parent's .v names only three states: 23 {{A}}, 28 {{C}} and 8 {{E}}. They become {{E}}, {{B}} and {{D}}, simultaneously. Every one of these 59 tokens is in a Lemma or Definition statement (the Section 1 runs, LPspec, Phispec, K, Rst); none is in a proof script, and no such statement binds a variable named A–F, so the renaming cannot capture [X]. By Lemma S each renamed Section 1 statement is a true run of this machine with the parent's step count [V], and each closes again by es. Everything after Section 1 refers to the machine only through LPspec, Phispec, K and the notations, so it is the parent's text unchanged. 3. New: - init : c0 -->* K 3 t1 (Section 4), one solve_init, 55 steps (§6.1); - B691, Y691 and fin691 : orbit 100000 691 3 t1 = Some (17712, Y691) by vm_compute (Section 11), in place of the parent's fin694 (also 691 epochs, from K 8 t2); - inv691 : Inv 11 17712 Y691, by the script of the parent's inv694 with exists 10, B691, 0; - the nonhalt call: nonhalt_from 17712 Y691 with P N y := ∃ k, Inv k N y, the start init followed by orbit_sound … fin691, the base exists 11. exact inv691, and the step inv_step. 4. With comments stripped, the lines that differ from the parent's .v are the TM literal, the 53 lines that carry renamed state tokens, and the lines of item 3. Every other proof script is the parent's. 5. busycoq's Perm/perm_halts (verify/Permute.v) would give the same result from the parent's file with the state names kept, at the cost of a second TM literal and a bridge lemma. The renaming needs neither. 6. Every lemma is top level (no Section, Module, Hypothesis or Axiom). Besides busycoq's Individual62, the file imports only the stdlib Lia, String, List and Arith. Section numbers in its comments (write-up 3.x, D.x, Lemma C) refer to the parent's write-up.

9. Numerical checks

All of these are by direct simulation of the transition tables, or by the rules-only model (no TM inside). They are evidence only; the result rests on the .v alone. The randomized checks ran with two seeds, and every check below passed. - [S] σ on 12/12 cells; Perm tm tm30 φ on 12/12; C0 the only undefined cell; C entered only by B0; B entered only by A0 and F1; the blank run equals the parent's run from 0^inf B> 0^inf for 2·10^6 steps. - [S7] from 0 0 F> 1 in 202 contexts: B reads 0 after one step, and C reads 0 (halted) after two. - [S8] the converse, exhaustive over 6 states × 32 five-cell windows: being in C reading 0 after exactly two steps means starting as 0 0 F> 1, and after one step means starting as 0 B> 0. - [X] the state tokens of the parent's .v (23 {{A}}, 28 {{C}}, 8 {{E}}, none of B, D, F) and of this .v after σ; every token inside a statement; no capture; Inductive LP has 18 constructors and Phi 8. - [V] the 27 Section 1 statements, parsed from the .v, with exponents 0..6 and 4 contexts each, head-relative comparison, no read of l/r, and fitted step formulas. The parent's text on the parent's table is the control. - [W] W1–W11 and S1–S3 with n ≤ 14, with the stated step counts. - [LP] lpf against the TM: - every word with at most two non-tail constructors and exponents ≤ 2, plus every word with at most three and exponents ≤ 1 (4,844 words, 4,502 with a rule), in 3 contexts; - 1,500 random large words (exponents to 40, nested D6 included), per constructor. - [PH] phif against the TM: - exhaustive small cases (a ≤ 2, b ≤ 5); - every G word with k ≤ 3 and e ≤ 2, at b = 1 and a ∈ {0, 1, 3}, has an eat, and the eat is the TM run; - 1,400 random large cases (a ≤ 40, b ≤ 45), bounces and eats. - [R] Rst for k ≤ 60 with 6 residues each, 3k + 8 steps. - [N] two non-G eats halt (a ∈ {1, 2, 5}). - [I] the milestones of §6.1; the .v's K reached at step 55 from both starts; the full trace of §6.1 equal to the run line by line (left part, state, head and right part, transition label) for all 56 lines. - [F] fin691, Inv 11 component by component, the uniqueness of k, the first Inv epoch, the fuel, the alternative orbit … 692 1 t0. - [M] control: the parent's fin694 and inv694 reproduced. - [O] model = TM on all 518 logged left records to 10^11 steps, and on a fresh run to 2·10^7 steps. - [T] N1 and N2 for k < 200, Costf 11 + 2 = Nstar, and the table of §5.1. - [J] Inv along the orbit from epoch 691 to 1,200 with the running κ. - [C] (informational) the orbits of this machine and the parent first meet at index 795 of both (N = 20,922) and are identical from there on. - [D] the parent's checks of Lemma D (parent D.0–D.8, parent §9) on this machine's rules-only orbit to N ≥ 400,000: 11,074 epochs, all links pass. This is the same epoch count as the parent's own, because the orbits have merged by then.

10. Siblings

• The parent (740 list line 710) starts in its own A.
• 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA (740 list line 381) has the same table, mirrored, and starts in the parent's E. It needs its own initial segment and finite part, and busycoq's flip_halts and perm_halts (verify/Flip.v, verify/Permute.v) for the mirror and the renaming. It is not covered here.
• The other starts of the table are not holdouts: this machine's B and C halt at once, and its F is the parent's own run one step later.

Gaps: none.

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