/machines/1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---/work/submission-proof.pre-clean.md · raw

1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---: never halts (delta proof from kill #33)

Submission copy of the working proof.md, made 2026-10-10 after the kill. The mathematics is unchanged. Only these parts were updated: the title, the header (holdout-list wording, parent pointer, evidence, status, AI line), the §5 heading and its closing paragraph (how the plan was carried out, and where each item lives in the .v), and §7. This is a delta proof: it cites the parent's informal proof as P§n. The parent's proof is in this folder as parent-proof.md, a verbatim copy of kill #33's submission proof.md with the same section numbers. Its remark that this machine (its D-start row) is not formalized predates this kill. The scripts and records it cites (check_proof.py, check_proof.out, check_proof_long.out, the parent's check_proof.py, and the scratch compile of the §5 delta) live in the working directory and are not in this folder.

0. The map

this state 0 1 = σ(#33 state) #33 0 #33 1
A 1RB 0LD σ(D) 1RA 0LC
B 1RC 0RE σ(A) 1RB 0RE
C 1LD 0RE σ(B) 1LC 0RE
D 1LA 0LA σ(C) 1LD 0LD
E 1RB 1RF σ(E) 1RA 1RF
F 1RB --- σ(F) 1RA ---

σ: A↦B, B↦C, C↦D, D↦A, E↦E, F↦F (a 4-cycle on A–D). Row σ(s) of this table is #33's row s with every target state t replaced by σ(t); symbols and directions are unchanged. For example, #33's D1 = 0LC becomes 0Lσ(C) = 0LD, which is this machine's A1. check_proof.py §S checks the 12 cells and searches all 720 renamings with and without mirroring: σ is the only map from #33's table to this one. The only map from kill #11's table is CDABEF with the mirror, start #11's C (= #33's table relation composed with #11 → #33).

Lemma R (relabelling). For a configuration c, let σc be c with its head state renamed by σ; the tape and head position stay the same. Then c → c′ under #33 if and only if σc → σc′ under this machine, and c is halted exactly when σc is (F1 is the only undefined cell, and σ fixes F). So every #33 run c →ⁿ c′ gives a run σc →ⁿ σc′ here, of the same length, and conversely.

Start. This machine's c0 is 0^inf A> 0^inf = σ(0^inf D> 0^inf). So its run is σ of #33's machine run from 0^inf D> 0^inf. It is not #33's run (which starts in A). §R checks this in lockstep for 2·10⁶ steps (state = σ(#33's state), same symbol written, same move, identical tapes at the end).

Halting cell. Only E1 = 1RF enters F, and F1 is ---, exactly as in #33 (σ fixes E and F). So the machine halts exactly when E reads 1 with a 1 to its right.

1. What carries over unchanged

#33 item this machine reason
P§1 family K(d_1..d_m; a, b) K_D := σK = 0^inf <D (01)^b 000 (01)^a d~_m .. d~_1 1001 0^inf, the same words with head state D, the same digits d~(u,0,v) = (10)^v 00 (01)^u, d~(u,1,v) = (10)^v (01)^u and the same derived quantities (U_j, R_j, R1_j, ubar, vbar, S, T) Lemma R
P§2.1 window lemmas S1–S6, T1–T14 and digit lemmas Lb, Lf, Rb, Ro identical words and step counts, states renamed by σ (list below) Lemma R. Also re-run on this table: §L, 20/20, transitions = σ of #33's
P§2.2–2.3 the chains for M and O; P§2 rules M and O with their step formulas and domains identical, <C read as <D Lemma R. Also re-run on this table: §A (M 700/700, O 350/350, random INV states 2,836/2,836) and §H (every link of #33's chains, renamed, 47,216/47,216)
P§3 invariant INV = Common ∧ (A ∨ B ∨ C), facts F0–F3, coverage, closure identical stated on the triples (u, β, v) and a, b only; never reads the start or the state names
P§5 progress / "why F reading 1 is never used" identical (E1 occurs only in T4, T9, T13, where F then reads 0; §L) Lemma R
P§6 Rocq: M_spec, Mdrop_spec, O_spec, their supports, the abstract part (INV, F1–F3, macro_step) identical text, {{X}} renamed by σ §5
P§4 initial segment and base changed: §2 different start

The window lemmas on this table (X> = head in state X on the next cell, <X = on the previous cell):

S1 10<D -2-> <D01        S2 01<A -2-> <A10        S3 B>10 -2-> 01B>        S4 E>01 -2-> 10E>
S5 1011<A -6-> 11<A01    S6 01<D0 -6-> <D001      T1 00<D -3-> 10E>        T2 E>000 -5-> <D001
T3 E>001 -3-> 110E>      T4 E>10 -2-> 11B>        T5 B>01 -2-> 10E>        T6 B>00 -3-> <A01
T7 11<A -2-> <A00        T8 11011<A -9-> <D00001  T9 E>1001000 -13-> <D0001001   T10 11<D -2-> <D00
T11 0<D -1-> <A1         T12 00011<A -13-> 10110E>   T13 E>101 -3-> 110E>  T14 1011<D -4-> <D0100

The rules in busycoq comment style, for this machine:

1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---     (= sigma of 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, sigma = BCDAEF)

K(d_1 .. d_m; a, b) := 0^inf <D (01)^b 000 (01)^a d~_m .. d~_1 1001 0^inf
d~(u,0,v) := (10)^v 00 (01)^u,   d~(u,1,v) := (10)^v (01)^u        (d_m least significant)

start from K((1,1,9); 8, 1)                                   (step 687, section 2)

M  (carry; some bit is 0; j* = index of the LAST bit-0 digit):
   K(.., (u,0,v), (u_j,1,v_j)_{j*<j<=m}; a, b) --> K(.., (u+1,1,v-1), (u_j,0,v_j-1)_{j*<j<=m}; a+1, b+2)
   steps 32 + 8a + 8b + 4v + sum_{j>j*} (8 u_j + 4 v_j);  needs v >= 1, u_j, v_j >= 1 (j > j*), a, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, P section 1)
O  (overflow; all bits 1):
   K((u_1,1,v_1) .. (u_m,1,v_m); a, b) --> K((0,0,u_1), (v_1-1,0,u_2), .., (v_{m-1}-1,0,u_m), (v_m,1,a); b+3, 1)
   steps 89 - 4m + 8a + 20b + 4 sum u_j + 8 sum v_j;  needs m >= 1, all u_j, v_j >= 1, a >= 1, b >= 0

2. What changes: initial segment and base (replaces P§4)

Direct simulation of this machine from the blank tape (§C). A K-configuration is state D on a blank cell with only blanks to its left, the tape to its right parsing as a K. They occur exactly at these steps up to 687 (and #33 from 0^inf D> 0^inf gives the same list, as Lemma R says):

step K-configuration in INV? next macro step
101 K((1,1,1); 2, 1) no: S = 0 (class A needs S ≥ 1) O, 133 steps
234 K((0,0,1), (1,1,2); 4, 1) no: LSB vbar = 2 − 2 = 0 M1 with the top falling, 92 steps
326 K((2,0,1); 5, 3) no: its only digit is bit 0 with v = 1 M0 with an LSB drop, 100 steps
426 K(; 9, 5) no: m = 0 O at m = 0 (P§2.3), 261 steps
687 K((1,1,9); 8, 1) yes, class A O, 245 steps, to K((0,0,1),(9,1,8); 4, 1) (class B)

Two legs of the init use rule cases the invariant argument never needs (the LSB drop, and O at m = 0). That does not matter: the proof only uses the 687-step run as one finite computation. The table just explains it.

Compare #33: K-configurations at 82 (K(; 3, 1)) and 215 (K((1,1,3); 4, 1)). The other two starts of the same table: #11 (start B of #33's table) reaches K((1,1,2); 8, 5) at 483, hipparcos's machine (start C) K((1,1,10); 8, 1) at 732 (P§0).

INV at the base K((1,1,9); 8, 1) (P§3; derived quantities as in P§1): - top (1,1,9): bit 1, u_1 = 1; m = 1; - V = 1, R_tot = R_1 = 0, R1_1 = 0; - ubar_1 = 1 (odd), vbar_1 = 9 ≥ 1 (also the LSB condition); - S = 8 + 0 − 2 = 6 ≥ 1, T = 1 − 1 = 0 ≥ 0 (tight, as at #33's base); - a = 8 ≥ 1, b = 1 odd, a + R_tot = 8 even; - Common holds, and class A holds (top (1,1,v), every vbar ≥ 1, every ubar odd, S ≥ 1).

In the additive Rocq form of #33's .v (INV, PA, Rof, LSBok, at ([d1 1 9], 8, 1)): Rof = 0; a + R + 2 = 10 ≥ 4; b + 3 + 2R = 4 ≥ 4; a + R + 1 = 9 ≥ 4; v_m = 9 ≥ R + 1; (a + R) mod 2 = 0; b mod 2 = 1; PA (d1 1 9) 0 0: canon, 9 ≥ 1, ub = 1 odd and = 1. §B evaluates all 12 clauses. Only v_1 (9 vs 3), a (8 vs 4) and the step count differ from #33's base, and every clause that reads them is a lower bound.

3. The argument (complete)

Theorem. 1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB--- does not halt from the blank tape.

  1. Initial segment. The machine runs from c0 to K((1,1,9); 8, 1) in exactly 687 steps without halting. This is a finite exact computation (§C); in Rocq it is solve_init.
  2. Base. INV([(1,1,9)], 8, 1) holds, in class A (§2).
  3. Transfer. P§3.2 (coverage) and P§3.3 (closure): every INV state has a macro step M or O, of at least 32 machine steps, to an INV state. These statements are about the triples and a, b, and the macro steps are #33's rule instances K → K′. By Lemma R, each such instance is a run σK →⁺ σK′ of this machine of the same length. So coverage and closure hold verbatim for the configurations K_D = σK.
  4. Conclusion. By induction from the base, the run is an infinite chain of macro steps, each of at least one machine step, so it never halts (progress_nonhalt_cond with P := INV, as in P§5). No macro step presents the halting cell: each is an exact computation from one K to the next, composed of window lemmas in which F reads only 0. ∎

Nothing in #33's argument after its init depends on #33's own orbit. The orbit statistics in P§7 (class counts, drop counts, overflows) are evidence, not premises.

4. How this orbit relates to its siblings (explanation, not a premise)

Coupling with kill #11. In the shared triple notation, this machine's macro orbit and #11's (from #11's base K((1,1,2); 8, 5) at step 483) merge into a fixed offset after 54 macro steps (step 25,718 here, 25,618 in #11): - from then on, at every macro step, the two states are equal except for one exponent, larger by 3 here, on the top digit: v_1 in class A, u_2 in class B (the top is (0,0,1) there), u_1 in class C; - the same rule fires at every macro step; - checked for 299,946 macro steps (to t ≈ 2.2·10¹¹, 80 overflows; §X), and for 1,199,946 in the long run (t ≈ 3.7·10¹², 93 overflows).

Where the +3 travels (observed, not proved): O sends the top's v_1 to digit 2's u (class A → B, new top (0,0,1)), the top fall merges digit 2's u into the new top's u (B → C), and the next O sends u_1 to the new top's v (C → A). The coupling is not used anywhere in §3, so it needs no proof. It explains the "exact trajectory twin of #11" seen at 10⁹ steps: 77,691 cells (−77,517..173) and 38,839 nonzeros here, against #11's 77,685 and 38,836. The +6 cells are the three extra 10/01 blocks.

Against #33 (the parent of the formal proof): a different orbit, with no such coupling (76,245 cells and 38,119 nonzeros at 10⁹).

5. Formalization delta (done as planned)

Copy #33's .v (sha256 37cb180280f0896396a28bb32a548a6bfdd22d0b47b2f526230ed2208dbb2053, 671 lines) and change only the following: 1. TM_from_str "1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---". 2. Rename every state name {{X}} by σ, simultaneously: {{A}} → {{B}} (5 occurrences), {{C}} → {{D}} (22), {{D}} → {{A}} (18); {{E}} (18) stays, and #33 never names B or F. This covers the window lemmas, digit lemmas, sweeps (LbS, RbS, RoS), chunks and K. The es/follow proofs go through unchanged, because σ maps transitions to transitions (Lemma R). 3. Lemma init: c0 -->* K [d1 1 9] 8 1. (687 steps, the same unfold K, R0. cbn. solve_init.) and, in nonhalt, change (K [d1 1 9] 8 1) with (Kc ([d1 1 9], 8, 1)). The base goal is closed by #33's own tactic line (§2: every clause is linear arithmetic on constants). 4. The header comment and the comments that name the head state.

Everything else is #33's text: every proof script, M_spec/Mdrop_spec/O_spec and their statements, dg, map0, map1, Oz, Oout, INV, macro_step, nonhalt's structure.

Done as a scratch check, then as the kill (2026-10-10). check_proof.py's delta_text applies exactly these edits, each one asserted to match the expected number of times. The σ counts came out as predicted: {{B}} 5, {{D}} 22, {{A}} 18, {{E}} 18. The scratch output compiled on the first attempt (Coq 8.20.1, Print Assumptions nonhalt: closed under the global context), and §V checks that it is the delta of #33's pinned .v byte for byte and that, with comments stripped, it differs from #33's code only by the substitutions above. The kill file is that scratch file with only its header comment rewritten (code below the header byte-identical). check_kill (our checker) passed on the first run, and twice more on the same sha256 (6238e25c…51bd; the fresh run in this folder is check_kill.txt). No tactic was changed. Where each item lives in the .v:

item .v
§1 window lemmas S1_1..S6_1 and S1..S6 (one block by es, then shift_rule_L/R; S5 by induction), T1..T14 (es)
P§2.1 digit lemmas Lb, Lf, Rb, Ro; the digit word dg, K, R0
P§2.2–2.3 chains for M and O sweeps LbS, RbS, RoS; chunkA, chunkC, chunkO, Ozeq
rules M (with and without a drop) and O M_spec, Mdrop_spec, O_spec (#33's statements)
P§3 INV, F1–F3, closure INV (with PA, PB, Rof, LSBok), F1, F2, macro_step (#33's text)
§2 init and base init : c0 -->* K [d1 1 9] 8 1 (687 steps, solve_init); the base goal in nonhalt
§3 conclusion nonhalt (multistep_nonhalt + progress_nonhalt_cond with P := INV)

Lemma R is not a premise of the formal proof: every window lemma is re-proved on this machine's own table by es, and Lemma R explains why those proofs re-close. So the kill rests on the .v alone; the prose here and in the parent's §2–§5 is the explanation.

6. Evidence (python3 -B check_proof.py, defaults, about 20 s; output in check_proof.out)

The script imports #33's check_proof.py read-only, for its abstract model, its invariant, its random-INV generator, its chain builders and its abstract checks. Everything that depends on the machine or the start is re-run on this machine's own table with its own simulator.

§ what result
S line 388 byte-exact; 26 snapshots; sheet rows; not in our Discord exports; eqv group = {this, #33 from E, #33 from F}; σ = BCDAEF the only map (720 × 2), start = #33's D; 12/12 cells; #11 → this = CDABEF + mirror from C (unique); only E1 enters F, F1 the only undefined cell PASS 13/13
R lockstep, this machine from blank vs σ(#33 from 0^inf D> 0^inf), 2·10⁶ steps PASS
L #33's 20 window lemmas renamed by σ, exact on this table, never reading outside the window, transitions = σ of #33's; F entered only in T4/T9/T13, reading 0 PASS 21/21
A M 700/700 (k = 0..6, drops, u* = 0, a, b ≥ 0; rightmost cell read = right 0 of the flipped 00), O 350/350 (m = 1..7; rightmost read 3 right of the old 1001), random INV states one macro step on this table PASS
H #33's M chain (box + 500 random) and O chain (box m = 0..4 + 300 random), every link renamed by σ and checked on this table (whole tape, head, state), plus the init leg K(;9,5) → K((1,1,9);8,1) PASS 47,216/47,216
C blank: K at 101, 234, 326, 426 (none in INV, reasons as in §2), 687 = K((1,1,9);8,1); the legs O, M1 (top drop), M0 (LSB drop), O at m = 0; #33 from D gives the same list; derived quantities; next O (245 steps) to class B, also run on the machine PASS 17/17
D the real machine from blank vs the model at every macro boundary from step 687 to 3·10⁷ (whole tape, head, state; INV at each) PASS 3,384/3,384 (long run: 19,332/19,332 to 10⁹)
B INV at the base, set form (class A) and the 12 clauses of the Rocq additive form PASS 13/13
G INV along the abstract orbit from the base, 3·10⁵ macro steps; #33's induction on random INV states (1.5·10⁵) and drop algebra (2·10⁴), abstract map only PASS
X coupling with #11's orbit (§4), informational PASS
V the scratch .v (delta_check.v) = §5 delta of #33's pinned .v, byte for byte; code differs only by the substitutions; compile record clean PASS

Long run, --seed 2026 --tm-steps 1e9 --orbit 1.2e6 --induct 6e5 --lockstep 2e7 (118 s, check_proof_long.out): SUMMARY PASS. It includes: - §R lockstep for 2·10⁷ steps; - §D, the real machine against the model at all 19,332/19,332 macro boundaries to step 999,837,328 (O 53, M0 9,639, M1 4,846, M2 2,422, M3 1,209, M4 602, M5 298, M6+ 262; drops: 30 top, 12 mid; INV classes A 7,523, B 6,307, C 5,502); - §G, INV along 1.2·10⁶ macro steps of the abstract orbit (t ≈ 3.7·10¹², 16 digits, 93 overflows) and 600,000/600,000 random-INV induction steps; - §X, the coupling with #11 for 1,199,946 macro steps.

Start-independent checks of #33 that test the abstract map only (P§7 checks 7 and 9) are re-run in §G. #33's skeptic review (P, Review log) covered the rules and INV; it applies unchanged, because both are the same statements here.

7. Checkpoint B (Dennis)

pending (no Checkpoint B notes were on file when this was packaged). Question for the reviewer: is "same table up to σ, new init and base, invariant unchanged" acceptable as the informal proof for the submission (as for #25), with #33's proof.md attached as the parent (parent-proof.md), or does the maintainer want the parent's proof restated in full?