1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB: never halts (informal proof, W4-1)

• Machine: 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB, viewer https://bbchallenge.org/1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB
• Holdout lists: byte-exact at line 590 of data/holdouts/BB6_holdouts_740.txt and line 626 of 2026-10-07_778.txt; on all 26 snapshots since 2024-06-14. Its equivalence group in the 778 eqv file is a singleton. Sheet: results.csv row 1046, class "Bell eats counter", with status/notes/sources/done-by blank. No Discord thread found, and no upstream proof (busycoq BB6 HEAD 9cf9e88 has no file for this string, for #30's or for #7's).
• Written for the string itself: no mirror. The proof goes through kill #30 (1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC, check_kill PASS). W4-1's table is #30's table with the states renamed by σ (§1). So W4-1 from the blank tape is #30's table run from 0^inf B> 0^inf (#30's names).
• What is new here: the start. Everything else is #30's rule set, word model and invariant, restated in W4-1's state names. Their proofs are in #30's .v (Sections 1–10 and inv_step) and do not mention the start. The new parts are:
• the initial segment (55 steps to K(1,3,t1), §6.1);
• the finite part (691 model epochs to N = 17,712, §6.2);
• the invariant at its end (Inv 11 17712 Y691, §6.3);
• the conjugacy or renaming that moves #30's statements to this table (§8).
• Status: CHECKPOINT_B. Skeptic round 1 found the argument sound, with five minor gaps, all fixed (review log). Both Rocq routes of §8 have been built as drafts and pass check_kill (§8.3). check_proof.py (this directory) tests every claim below on W4-1's own table: exhaustive small cases and random large ones. Its section letters are given in brackets, e.g. [V], and the results are in §9.

0. 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. #30's 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, W4-1 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 #30's inv_step carries the invariant forever.
• The two orbits merge (not used in the proof). The model orbit of W4-1 and the one of #30 are different until epoch index 795 of both, at N = 20,922, and identical from then on [C]. Before that, W4-1's orbit is another orbit of the same macro map.

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

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

Lemma S (renaming). Let σ map #30's states to W4-1's: A→E, B→A, C→B, D→C, E→D, F→F. Then for every state q and symbol r, W4-1's cell (σ q, r) is #30'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), busycoq's Perm tm tm30 φ holds (Permute.v). That is, W4-1'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: the W4-1 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, W4-1 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 (#30'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 (W4-1 names; words as in #30's .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 (#30's .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 #30's .v 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 (W4-1 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 (W4-1 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 #30's .v Section 1, renamed [V]

These 27 lemmas are each proved by one es in #30's .v (Rst after one const_unfold rewrite). Here they are written with σ applied: {{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 and applies σ to the state tokens. - It runs W4-1 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 unrenamed text is run on #30'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'. scripts/vmodel.py is a Python mirror of lpf, phif (same cases in the same order, same fuel accounting; the bounce loop is iterative), orbit and Inv. As a control, it reproduces #30's proved fin694 literal exactly, and Inv 10 17713 Y694 [M].

4. Coverage

This section is #30's, unchanged: words do not mention states. - Lemma H (#30 proof.md §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 (#30's .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 #30's write-up.

[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 (#30 .v Sections 7–11; written out in #30 submission/proof.md §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 W4-1'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 step-4 record seen in observe (L(0, '')) 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. Its tm30 form is B;; tape0 -->* K 3 t1 (#30's K, with C>), also 55 steps [I]. The parsed .v text of K, renamed, is reached from c0 at step 55 on W4-1's table, and #30's K from B;; tape0 at step 55 on tm30'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 #30's write-up threshold N* = 14,796 (Lemma D, informal), 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 can use either; this write-up uses 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 the 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 observe-stage notes give Nlo(12) as 31,744. The value is 28,672; the conclusion is the same.) The value is m(W) = 8,788.

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 W4-1 never halts from the blank tape.

Why C0 is never executed. Every rule is an exact run that es proves in #30's .v. Under σ these are W4-1 runs [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. Lemma plan for Rocq (template: kill #30's .v)

Template. machines/1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC/1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC.v (1,726 lines, sha256 93a493f5…0c0, check_kill PASS: 15.5 s compile, coqchk 67.7 s, 0 assumptions). Applies: yes. - Sections 1–10, together with Inv, next_inv, inv_step, orbit and orbit_sound of Section 11, are statements about #30's table, words and arithmetic. None of them mentions the start. - Only these depend on the start: init : c0 -->* K 8 t2, B694/Y694/fin694/inv694, and the nonhalt call (nonhalt_from 17713 Y694, exists 10). - Both routes below have been built from #30's .v and pass check_kill as drafts (§8.3). Route B is the one for this machine's file.

8.1 Route A, conjugacy (#24's recipe without flip)

1. Definition tm := Eval compute in (TM_from_str "1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB"). This is the top-level literal that check_kill compares.
2. Definition tm30 := Eval compute in (TM_from_str "1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC")., with the three -->/-->*/-->+ notations bound to tm30. check_kill only warns about a second literal (as for #24).
3. Sections 1–3 and 5–10 verbatim. All es lemmas stay about tm30, with no edits.
4. Section 4: keep K and epoch_tm, and replace init: Ltac solve_initB := change (B, tape0) with (cconfig_to_config (nil,nil,0,B)); repeat rewrite Str_cons_def; repeat rewrite <-Str_app_assoc; repeat rewrite simpl_directed_head_l; repeat rewrite simpl_directed_head_r; repeat rewrite l_const0_app_nil; repeat rewrite r_const0_app_nil; repeat rewrite config_to_cconfig; apply cconfig_evstep_dec_spec with (n:=1000000); vm_compute; reflexivity. Lemma init : B;; tape0 -->* K 3 t1. Proof. unfold K. cbn. solve_initB. Qed. This is busycoq's solve_init started in B. esx/solve_init take the vm_compute path only from c0 (atlas/rocq-notes.md, #24). The run is 55 steps.
5. Section 11: keep Nstar_ge, opq, Mw, M2, Inv, next_inv, inv_step, orbit and orbit_sound. Replace the finite part: Definition B691 : blks := [(false, 10); (false, 6); (true, 1); (false, 1); (true, 1); (false, 1); (true, 1); (false, 1); (false, 1); (true, 1); (false, 0)]. Definition Y691 : word := p11 10 (gw B691 0). Lemma fin691 : orbit 100000 691 3 t1 = Some (17712, Y691). Proof. vm_compute. reflexivity. Qed. Lemma inv691 : Inv 11 17712 Y691. (* inv694's script with exists 10, B691, 0 *)
6. Restate nonhalt_from for the start B;; tape0. Its statement changes in the hypothesis (B;; tape0 -->* K N0 y0) and the conclusion (~ halts tm30 (B;; tape0)). Its body needs one token edit. #30's body calls apply (progress_nonhalt_cond tm (nat * word) ...) with tm named explicitly. In route A, tm is W4-1's table, so a verbatim body does not typecheck against ~ halts tm30 (B;; tape0). The call must read progress_nonhalt_cond tm30 ... [X7, K4]. The rest of the body is #30's, because multistep_nonhalt and progress_nonhalt_cond are generic in the TM and the configuration: ``` Lemma nonhalt_from N0 y0 (P : nat -> word -> Prop) : B;; tape0 --> K N0 y0 -> P N0 y0 -> (forall N y, P N y -> exists k y', Phi 1 N y k y' /\ P (S k) y') -> ~ halts tm30 (B;; tape0). Proof. intros H0 HP0 Hstep. eapply multistep_nonhalt. { exact H0. } apply (progress_nonhalt_cond tm30 (nat * word) (N0, y0) (fun i => K (fst i) (snd i)) (fun i => P (fst i) (snd i))); [| exact HP0]. ( the rest of #30's body, unchanged *) Lemma nonhalt_B : ~ halts tm30 (B;; tape0). Proof. apply (nonhalt_from 17712 Y691 (fun N y => exists k, Inv k N y)).
   • eapply evstep_trans; [exact init | exact (orbit_sound _ _ _ _ _ _ fin691)].
   • exists 11. exact inv691.
   • intros N y [k Hk]. destruct (inv_step k N y Hk) as (kk & y' & H1 & H2). exists kk, y'. split; [exact H1 | exact H2]. Qed. ```
7. The bridge (busycoq Permute.v, exported by Individual62): ``` Definition phi (q : Q) : Q := match q with A => B | B => C | C => D | D => E | E => A | F => F end. Lemma perm_w41 : Perm tm tm30 phi. Proof. split.
   • intros [] [] H; cbn in *; try discriminate; reflexivity.
   • intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity. Qed. Lemma nonhalt : ~ halts tm c0. Proof. intros H. change (halts tm (A;; tape0)) in H. exact (nonhalt_B (perm_halts _ _ _ _ _ perm_w41 H)). Qed. ``phi A = Bby computation, soperm_haltsgiveshalts tm30 (B;; tape0). Do not usecongruencefor thePerm` goals (#24: it fails).
8. The closing comment block is §1's, and the header comment must be public-safe (no names, no repo paths).

This is also the route #7 needs, plus busycoq's flip_halts. #7 is the same table mirrored and started in #30's E: route A plus flip, with its own init (about 1,060 steps to K 17 t1) and finite part (687 epochs). That is a fact about #7's file. It does not bind this machine's file (§8.3).

8.2 Route B, renaming (the #25/F2 recipe; the route for this file)

• Use #30's file with the TM string replaced. Apply A→E, C→B, E→D simultaneously to the 59 state tokens (23 {{A}}, 28 {{C}}, 8 {{E}}; there is no {{B}}, {{D}} or {{F}}) [X2, X5].
• Every occurrence is in a Lemma/Definition statement: Section 1 lemmas, LPspec, Phispec, K, Rst. None is in a proof script, and no such statement binds a variable named A–F, so the substitution cannot capture [X3, X4]. The 27 renamed Section-1 statements are true W4-1 runs with the template's step counts [V], so every es closes again.
• Keep init : c0 -->* K 3 t1 with solve_init. Use the finite part of route A step 5, and nonhalt as in #30 with nonhalt_from 17712 Y691, orbit_sound … fin691 and exists 11. exact inv691.
• In the compiled draft (§8.3), all 27 renamed es lemmas re-prove on W4-1's own table, as [V] predicts, and solve_init closes init from c0.
• Comments mention C>, E>, <A and so on, and need hand renaming (cosmetic).

8.3 Both routes compiled (skeptic round 1)

The review built both routes mechanically from #30's .v. The generators are scripts/mk_routeA.py (#30's .v → route A) and scripts/mk_routeB.py (#30's .v and route A's finite-part text → route B). Each generator emits one Print Assumptions nonhalt. line, which is dropped. The results pass tools/check_kill.sh. The logs are data/check_kill_route{A,B}.log. The drafts are in the session scratchpad, /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/w41rev/ck/ (A) and /tmp/claude-1000/-home-dennis/dbf3e2a9-21e7-4eb2-b481-38a0113aca31/scratchpad/w41rev/ckB/ (B), each named 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v. If the scratchpad is gone, the generators rebuild them byte for byte from the sha-pinned #30 .v. [K] does exactly that and reads the two logs.

• Route B is the choice for W4-1's file. It has one TM literal, no bridge and no check_kill warning. "#7 needs route A" is a fact about #7's own file, not this one.
• Neither draft is submission-ready. Both still open with #30's header comment and close with #30's table comment [K7]. Before the file is copied into this directory as 1RB1RF_1LC0RD_---0LD_1LE0LD_1RA0RF_0RE0LB.v, the formalization stage rewrites:
• the header: public-safe (no names, no repo paths), in W4-1 names (hub K(a,b,X) = 0^inf (110)^a 0 (011)^b B> X 0^inf), with the start c0 -->(55) K(1,3,t1) and the finite part fin691 (691 epochs from K(1,3,t1) to N = 17,712, then Inv 11), and with the "Checked:" line restated for this file;
• the closing comment: §1's table block;
• in route B, the comments that still say C>, <A, E> and so on. Then check_kill is re-run on the final file.
• The new proof text is small: init, fin691, inv691, the nonhalt call and, in route A only, the restated nonhalt_from and the 15-line bridge.
• The margin in Nstar ≤ 17712 is 7. It is exact arithmetic, checked by vm_compute in inv691.

9. Evidence (python3 -B check_proof.py --seed S; data/check_proof_seed{1,2}.{log,json})

Results of the latest full runs are in the review log. Per section: - [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 tm30's B-start run 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 template's sha256; token counts before and after renaming; every token inside a statement; no capture; Inductive LP has 18 constructors and Phi 8 [X6]; progress_nonhalt_cond tm (nat * word) occurs once, which is route A's one-token edit [X7]. - [K] the two drafts of §8.3: - scripts/mk_routeA.py and scripts/mk_routeB.py on the sha-pinned #30 .v, minus the one Print Assumptions line, reproduce both sha256s; - both logs are PASS for those sha256s (0 assumptions, coqchk pass, framework 0940bb9); - route A has the one tm_text warning, route B none; - the text facts of each draft (literals, the tm30 edit, the bridge, the renamed token counts, fin691/inv691/exists 11); - both still carry #30's header and closing comments (a to-do, [K7]). check_kill itself is not re-run by check_proof.py. - [V] the 27 Section-1 statements, parsed from the .v and renamed, with exponents 0..6 and 4 contexts each, head-relative comparison, no read of l/r, and fitted step formulas. The unrenamed text on tm30 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 text reached at step 55 from both starts; the full trace of §6.1, parsed from this file, 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: fin694 and inv694 of #30 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 W4-1 and #30 first meet at index 795 of both (N = 20,922) and are identical from there on. - [D] #30's write-up Lemma D chain (D.0–D.8) on W4-1's rules-only orbit to N ≥ 400,000: 11,074 epochs, all links pass. This is the same epoch count as #30's own, because the orbits have merged by then.

10. Siblings

• #30 (740 line 710): the template, killed. Started in its own A.
• #7 (740 line 381, 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA) has the same table, mirrored, started in #30's E. Observe found that the model predicts its left records from step 1,059 on, and that Inv holds after 687 epochs. Route A plus flip_halts covers it.
• The other starts of the table are not holdouts: W4-1's B and C halt at once, and W4-1's F is #30's own run one step later.

11. Checkpoint B (Dennis)

Not reviewed by Dennis yet. Formalization can start (non-blocking checkpoint, high confidence). Open questions: 1. Route for this machine's file: route B (rename the 59 state tokens) is recommended. Both routes compile and pass check_kill as drafts (§8.3). For W4-1's own file, route B gives one TM literal, no bridge and no check_kill warning. Route A (tm30 plus Perm/perm_halts) is the pattern #7's file needs, with flip_halts; that does not bind this file. Unless you prefer route A, the formalization stage starts from the route-B draft and rewrites its comments (§8.3). 2. The merge of the two orbits at epoch 795: mention it in the public write-up or Discord message (it explains why the two holdouts behave the same), or leave it internal?

Review log

• 2026-10-10 (informal_proof stage, agent): first version.
• Wrote the full rule table in W4-1 names (window/shift rules; the 27 Section-1 runs with exact step counts; the LP and Phi constructors with their proofs), coverage, the invariant and step from #30's .v, progress, the 55-step initial segment with its full trace, the finite part (fin691, Inv 11) and a lemma plan for both routes.
• New facts found while checking:
  1. The blank tape reaches the pre-record P(0, t0) at step 3. Steps 3–55 are Rst, Phi_E0 and Rst, so the step-4 record of observe is an ordinary one.
  2. W4-1's and #30's model orbits merge at epoch index 795 of both (N = 20,922). Before that they are distinct, after it identical. The proof does not use this. It explains why #30's Lemma D run to N = 400,000 has the same 11,074 epochs here.
  3. notes.md's "Nlo 12 = 31,744" is a slip for 28,672. The conclusion (k = 11 forced) stands.
• Checker: check_proof.py ALL PASS on seeds 1 and 2 (179 claims each, about 93 s each with section D; data/check_proof_seed{1,2}.{log,json}). --quick (no D, smaller samples) is ALL PASS in about 23 s.
• Not done in this stage: the .v (route A of §8.1 is the next step), and Checkpoint B. The mechanism is #30's with confidence high, so formalization can start without waiting for Checkpoint B.
• 2026-10-11 (skeptic round 1, agent revision): the skeptic found the argument sound, with five gaps, all minor and none fatal or major. All five are fixed, and each fix has a check: 1. The Rocq plan had not been compiled (§8.3, §11 Q1). The review built both routes mechanically from #30's .v, and both pass check_kill:
  • route A: fe781969…, compile 17.6 s, coqchk 73.6 s, 0 assumptions, one warning for the second TM literal;
  • route B: c81ad0ae…, compile 15.8 s, coqchk 68.5 s, 0 assumptions, no warning. The changes:
  • §8.3 records both runs and the to-do: rewrite the header and closing comment before the file enters this directory.
  • The recommendation is now route B for this machine's file (§8, §8.2, §11 Q1). The "#7 needs route A" reason concerns #7's file.
  • The generators are copied into scripts/mk_routeA.py and scripts/mk_routeB.py, and the check_kill logs into data/check_kill_route{A,B}.log.
  • New check section [K] regenerates both drafts byte for byte from the sha-pinned #30 .v (minus the one Print Assumptions line) and reads the logs. 2. §8.1 step 6 said the nonhalt_from body is unchanged. It needs the one-token edit progress_nonhalt_cond tm30 …, because tm is W4-1's table in route A. The body is now written out. Checked by [X7] (#30's call occurs once) and [K4] (the route-A draft has the edit). 3. Typo in the §6.1 trace at step 47. The right side is 010010001, not 010001. A new [I] check parses the whole trace from this file and compares all 56 lines with the run (left part, state, head and right part, transition label). Before the fix it failed on exactly line 47 (55/56); now it passes 56/56. 4. §1 counted the undefined C0 as a step. In busycoq's sense, the machine is halted two steps after 0 0 F> 1 (F1, then B0, then C reading 0). It is three only if the halting transition counts as a step. §1 and the last sentence of §7 are reworded. New checks: [S7], the forward direction in 202 contexts, and [S8], the converse, exhaustive over 6 states × 32 five-cell windows (also for one step: 0 B> 0). The [S6] label is corrected. 5. notes.md disagreed with this file. The threshold N* = 14,796 is first reached at index 591 from K(1,3,t1) (N = 14,797), as §6.2 says, not at "epoch 593". LP has 18 constructors, not 19. Both are corrected in notes.md, and the 19 also in observe.json. A new [X6] counts the constructors in #30's .v: LP 18, Phi 8. [F9] already checked index 591.
• Checker: check_proof.py is ALL PASS on seed 1 (88.2 s) and seed 2 (88.1 s), 201 claims each, with section D. --quick is ALL PASS (199 claims, 23.1 s). Logs: data/check_proof_seed{1,2}.{log,json}.
• Re-check of gaps after the fixes: none fatal or major. Status → CHECKPOINT_B.
• What is left:
  • formalization: start from the route-B draft, rewrite its header and closing comment and its state-name comments (§8.3), copy it into this directory, and run check_kill on the final file;
  • Dennis's Checkpoint B answers (§11), which do not block.