/machines/1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---/proof.md · raw

1RB0LD_1RC0RE_1LD0RE_1LA0LA_1RB1RF_1RB---: delta proof from kill #33 (Checkpoint B)

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 (validated as a scratch compile; check_kill not run)

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. check_proof.py's delta_text applies exactly these edits (each one asserted to match the expected number of times). rocq/make_delta.py writes its output to rocq/delta_check.v, and rocq/compile.sh compiles it (Coq 8.20.1, -native-compiler no); the record is rocq/delta_check.out (sha256 of the file, Print Assumptions nonhalt, exit code). §V checks that the file is the delta of #33's pinned .v byte for byte, that with comments stripped it differs from #33's code only by the substitutions above, and that the compile record is clean. This is evidence for Checkpoint B, not a kill: the kill stage copies the file to machines/<tm>/<tm>.v and runs tools/check_kill.sh. Only that PASS counts.

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 data/discord/; 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 rocq/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. 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, or does the maintainer want the parent's proof restated in full?