/machines/1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA/proof.md · raw

1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA (#7): never halts (delta proof against kill #30)

Δ1. The conjugacy: #7 is #30 mirrored and renamed

          #7                    #30
      0     1               0     1
 A   1RB   0RA          A  1RB   0RF
 B   1LC   0LD          B  1RC   1RF
 C   1LE   1LD          C  1LD   0RE
 D   0LB   0RE          D  ---   0LE
 E   1RF   0LA          E  1LA   0LE
 F   ---   0RA          F  0RA   0LC

The map. Let σ send #7's states to #30's:

#7 state A B C D E F
σ (#30 state) E A B F C D

Its inverse sends #30's A, B, C, D, E, F to #7's B, C, E, F, A, D. For every state q and symbol s:

#7[q][s] = (w, d, q') ⟺ #30[σq][s] = (w, −d, σq'),

and #7[q][s] is undefined exactly when #30[σq][s] is. The only such pair is #7's F0 and #30's D0. For example, #7's A row 1RB 0RA becomes 1LA 0LE, which is #30's E row.

From here on everything is in #30's frame and uses #30's notation (#30 §2): hubs K(a, b, X), left records L(k, T), pre-records L'(k, T), the grammars G ⊂ O ⊂ H, the end words E*, budgets N = k + 1, ordinary and special residues.

Δ2. Initial segment (direct simulation)

Start from 0^inf E> 0^inf and use #30's table. Up to step 1059, the configurations of the form L(k, T) are exactly the five below. Here "of the form" means state A reads a blank, every cell to its left is blank, and 101 follows. X3 checks this at every step, with #7's own table in #7's frame.

record step k (of L(k, T)) T residue Y (T = 000 Y) N = k+1 kind covered by #30's rules?
e1 15 0 0001 1 = t1 1 special (G) Et1 at once. The eat is at a G word, but N = 1 is not ≥ β + 2
e2 81 1 000010010001 01 a z 1 2 special (E*) no: the digestion costs 2 > N − 2 = 0; the eat meets 11 a z 1 ∉ G
e3 183 3 0001000010001 10 00 010001 4 special (E*) no: it costs 11 > N − 2 = 2
e4 573 5 000010010010001000110010001 01 a^2 z 1000110010001 6 neither (Y ∉ H) the epoch is covered (LP0/LP11/LPC on the prefix, then eats at G words, ending at e5), but (I1) fails at e4
e5 1059 16 0001 1 = t1 17 special (G) yes: the base (Δ3)

The next record is e6 = L(23, 000 10 00 010001) at step 2915, with N = 24.

Δ3. The base of #30's orbit induction, clause by clause

30's induction (#30 §5 D.6) starts at its epoch 3: L(7, 000 t2), N = 8, a special residue, κ = 0. #7's base is e5: L(16, 000 t1), N = 17, also a special residue.

The running maximum. In D.6, k_t is k(W_t), the number of blocks of the W in the residue Y_t = 11 a^x z W, and k(W) = 0 for a special residue. It is not the record index of L(k, T) in Δ2's table. The running maximum is taken from e5 on: κ_t := max_{5 ≤ s ≤ t} k(W_s). At the base, κ_5 = k(W_5) = 0: Y_5 = t1 is special and has no W. The record index of e5 is 16, but it does not enter the invariant. Read with it, (I4) would fail at the base, since N_lo(16) = 2^19 − 2^14 is far above 17. X4 checks both readings.

clause (#30 D.6) at e5 holds
form L(k, 000 Y), then R to K(1, k+1, Y) record index k = 16, Y = 1, so K(1, 17, 1) yes (simulated, X3)
Y ∈ H (needed for #30 §4, Lemma H) 1 = t1 ∈ G ⊂ H yes
(I1) Y is ordinary or special special: t1 ∈ G yes
(I2) if ordinary: η ≥ 0, S ≤ U(κ, ·), x ≤ xmax(κ) vacuous (no W) yes
(I3) c ≤ Γ(k, κ), so k + c ≤ G(κ), with k = k(W) and c = 0 if special k(W) = 0, c = 0, κ_5 = 0; 0 ≤ Γ(0, 0) = 0 and 0 ≤ G(0) = 0 yes
(I4) N ≥ N_lo(κ) = 2^(κ+3) − 2^(⌊(G(κ)+1)/2⌋+4) 17 ≥ N_lo(κ_5) = N_lo(0) = 8 − 16 = −8 yes
epoch e5 finishes (β ≤ N − 2) Y ∈ G, so β = 0 ≤ 15; the next record is e6 yes (model = TM)

This is #30's base case, "κ = 0, special", word for word, with t1 in place of t2. Both are tails in G, so the digestion is empty and the reset D.4(r) applies.

No earlier record can serve as the base. At e1 (N = 1) the budget is below β + 2. The induction step from e2 or e3 fails, because their digestion does not fit in N, and #30's rules indeed do not cover those epochs. e4's residue is not in H, so (I1) fails there, although its epoch is computed by the rules and ends at e5. X4n checks all of this.

Δ4. Why the rest of #30's argument applies unchanged

30's argument has three kinds of parts. Statements about the table hold for every configuration. Statements about one epoch hold for any epoch K(1, N, Y) with Y ∈ H and enough budget. The rest is the orbit induction with its base and its finite part. Only the base and the finite part refer to the starting configuration.

#30 part depends on the start? for #7
§1 the halting transition (D0 = #7's F0) no Δ1 maps it
§3 rules W1–W11, S1–S3, RP0/RP1, LP*, B, eats E1g/E2g/E0/Et1–Et3, R, D6 (exact runs in every context) no: statements about the table unchanged
§4 Lemma H, eat coverage, the one-epoch corollary no: for any epoch K(1, N, Y) with Y ∈ H unchanged
§5 D.0 (positions, (P1), (P2), Lemma P, Lemma C, termination of Φ) no: per digestion unchanged
D.1 cost recursion, D.2 levels, D.3 shape and mass bound, D.5 value bound no: per epoch unchanged
D.4(a), (b), (e), (r) no: from epoch t to t+1 unchanged
D.4(c) unrolling ("stops … at epoch 3, whose residue t2 is special") only through the base stops at e5 (residue t1, special) instead. In D.6 it is subsumed by the step (I2)t ⇒ (I2){t+1}.
D.6 orbit invariant (I1)–(I4) only the base base = Δ3. The step uses only D.4, Lemma C, D.5 and N_{t+1} > N_t
D.7 Bnd, Bnd_worst(κ), F = {0..11}, N* = 14,796, the closed-form tail for κ ≥ 64 no: arithmetic in κ unchanged
D.8 finite part (the epochs with N < N*) yes recomputed for #7's orbit (Δ5)
§6 initial segment yes replaced by Δ2
§7 conclusion only "t ≥ 3" reads "t ≥ 5"

Spelled out: - The induction runs from t = 5. While N_t < N*, the step "epoch t finishes" (β_t ≤ N_t − 2) is the explicit computation of Δ5. For N_t ≥ N* it is D.7, with the same case split on κ_t ∈ F. - Every epoch has N_{t+1} ≥ N_t + 1 (#30 §4 corollary), so N reaches N* after finitely many epochs and stays above it. - Every epoch reaches the next left record. So the sequence of left records is infinite and #7 never halts.

#30's finite part cannot be reused. #7's orbit from e5 shares no epoch (N, Y) with #30's orbit from its epoch 3, nor with W4-1's orbit, up to N = 20,000. The three starts never merge before the threshold, so #7 needs its own finite part.

Δ5. #7's finite part

Informal route (#30's threshold N* = 14,796). The rules-only orbit (#30 §3, no TM inside) runs from K(1, 17, t1) (e5) on. - The epochs with N < 14,796 are e5 to e591, 587 epochs. e592 has N = 14,804. - None of them has an eat at a word outside G or a word without a rule, and each has β ≤ N − 2. - check_proof.py runs #30's section D from e5 to N ≥ 400,000. The links of Lemma D (H3, FIN, D.1, Lemma C, D.2–D.5, D.4(a)–(c), (e), (r), D.6G, D.7a/b/n/s) hold on every epoch. - The same orbit equals the TM's left records: a fresh Python run to 2·10^7 steps, and a C run to 10^11 steps (X5).

Formal route (#30's .v: Inv, threshold 17,705). #30's .v closes with nonhalt_from and the invariant ∃κ, Inv κ N Y (#30 .v §8.3). Inv contains N ≥ 17,705, so the .v's finite part must run until N first reaches 17,705: - orbit f 687 17 t1 = Some (17724, Y_692): 687 epochs (e5..e691), landing at e692, the first record with N ≥ 17,705 (e691 has N = 17,670). Coq's vm_compute gives the same value: fin7 : orbit 100000 687 17 t1 = Some (17724, Y692) with Y692 := p11 16 (gw B692 0), where B692 lists the ten blocks of W below (Δ6). - Y_692 = '11' a^16 z W, with W = a(6) z a(1) z b(1) z b(1) z a(1) z b(1) z a(1) z a(1) z b(1) z a(0) (bare tail). So k(W) = 10 and m(W) = 4,396. - Inv 10 17724 Y_692 holds, clause by clause:

clause value bound
N ≥ Nstar 17,724 17,705
N ≥ Nlo(10) = 2^13 − 8·2^⌊(13+3)/2⌋ 17,724 6,144
Y = p11 x (gw bs s), s ≤ 3, length bs ≤ 10 x = 16, 10 blocks, s = 0 yes
Mw(W) = Σ w(q) e_q, w(q) = 2^⌊(q+1)/2⌋ 66 A(10) = 2,219
M2(W) = Σ 2^(q+1) e_q 1,032 B(10) = 5,601
x 16 X(10) = 2,291

(κ = 11 also works; κ = 10 is the least.) From there inv_step (proved in #30's .v, start-independent) carries Inv to every later epoch. As a check, Inv also holds at every later epoch of the rules-only orbit, with κ the running maximum, up to N ≥ 400,000 (V2). - Transcription check. The Python bound functions reproduce #30's §8.3 table for κ = 8..13. The Python model reproduces #30's fin694 (orbit 691 8 t2 = (17713, Y694)) and inv694 (Mw 77, M2 1,054) exactly (V0). So the numbers above are what Coq's orbit and Inv should compute for #7.

Δ6. Rocq plan (delta)

Recipe: #30's .v plus the #24 bridge (atlas/rocq-notes.md, "#24 formalization round 1"). 1. Top of the file. tm := TM_from_str "1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA" (#7) and tm30 := TM_from_str "1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC". The three step notations -->, -->* and -->+ are on tm30. check_kill only warns about the second literal. 2. Keep #30's .v verbatim up to and including orbit_sound. This covers Sections 1–10 (LP, Phi, sound, epoch_tm, the model, the potentials, Inv, inv_step, the threshold) and the start of Section 11 (orbit, orbit_sound). None of it depends on the start. It refers to the machine only through the notations, so it compiles on tm30 unchanged. Three of #30's lemmas are about #30's own start K(1, 8, t2): init : c0 -->* K 8 t2, fin694 and inv694. They still compile on tm30, but #7 does not use them, so they can be dropped. 3. Replace the rest of Section 11. #30's tail cannot stay verbatim. Its nonhalt_from is stated as ~ halts tm c0 and uses progress_nonhalt_cond tm, so it no longer typechecks against epoch_tm on tm30. Its Lemma nonhalt would also be defined twice. The new tail: - nonhalt_from_c c N0 y0 P : c -->* K N0 y0 → P N0 y0 → (∀ N y, P N y → ∃ k y', Phi 1 N y k y' ∧ P (S k) y') → ~ halts tm30 c. This is #30's nonhalt_from with the start made generic and tm30 in place of tm. - init7 : E;; tape0 -->* K 17 t1, 1,114 steps from state E. The proof is unfold K. cbn - [tape0]. followed by #30's solve_init script, with its first line replaced by change (E, tape0) with (cconfig_to_config (nil,nil,S0,E)). There are two tactic details. In #30's scope the literal 0 in #24's (nil,nil,0,D) parses as nat, so the cconfig head must be S0. And cbn -[tape0] collides with busycoq's -[ step-notation token, so it must be written cbn - [tape0], with a space. - fin7 : orbit 100000 687 17 t1 = Some (17724, Y692) by vm_compute, with Y692 := p11 16 (gw B692 0) and B692 the ten blocks of Δ5. It is about the size of #30's 691-epoch fin694. - inv7 : Inv 10 17724 Y692, by inv694's script with x = 16 (exists 16, B692, 0). - nonhalt_E : ~ halts tm30 (E;; tape0), from nonhalt_from_c with P N y := ∃ k, Inv k N y, the start init7 followed by orbit_sound … fin7, the base inv7 and the step inv_step. - phi = σ (A↦E, B↦A, C↦B, D↦F, E↦C, F↦D) and perm7 : Perm (flip tm) tm30 phi. - nonhalt : ~halts tm c0 by flip_halts, then change (halts (flip tm) (A;; tape0)), then perm_halts with perm7 and nonhalt_E. 4. Header. Rewrite it for #7: the conjugacy, the start E, init7, the finite part to e692 (N = 17,724) and the bridge. #30's header describes the start K(1, 8, t2) and epoch 694. 5. State of the draft. rocq/M7_draft.v (sha256 3de5d2f4…92e5) is exactly steps 1–3: #30's text up to inv694 unchanged, without #30's nonhalt_from and nonhalt, and with the new tail. It compiles in about 17–20 s. tools/check_kill.sh gives PASS on 17 of 17 checks (rocq/check_kill_draft.out): coqchk passes in 127 s, Print Assumptions nonhalt is closed, and the only tm_text warning is the expected one for the second TM_from_str literal. Step 4 is still open: the draft's header comment is #30's, so the draft is not public-ready. RQ (Δ7) ties the stored log to the draft's hash, and the draft's B692 to the Python model. 6. Timing (wave 4 ranking): finish W4-1 and #7 before #30 is posted, and submit the three starts of this table as one family. W4-1's .v differs from #7's only in step 3 and the header (no mirror, start B, its own init, finite part and Inv).

Δ7. Checks (check_proof.py, seeds 1 and 2; data/check_proof_seed{1,2}.json)

Earlier analysis (superseded, kept in notes.md)

Before this route, #7 was worked in its own frame over three funded stages (deepen, closure_ctl, struct_invariant, flush_lemma; notes.md from "Deepen pass" on, and decisions/). That analysis used round starts, swept tokens and a carry transducer, and it parked as STUCK on the flush lemma: no linear flush bound, and bounded-post H_3 escapes. It never noticed that the table is #30's. In #30's terms, the "slow carry" it could not bound is the nested digestion (D6). Lemma D bounds it in the counter's value, which is what the flush-lemma decision guessed (a value-form bound, as for #28). That analysis is superseded and is not used here.