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

1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---: delta proof from kill #3 (Checkpoint B)

0. The map

twin state 0 1 = σ(parent state) parent 0 parent 1
A 1RB 1RF σ(C) 1RD 1RF
B 1LC 0LE σ(D) 1LA 0LE
C 1RD 0LB σ(A) 1RB 0LD
D 1RA 0RC σ(B) 1RC 0RA
E 1RE 1LB σ(E) 1RE 1LD
F 0RD --- σ(F) 0RB ---

σ: A↦C, B↦D, C↦A, D↦B, E↦E, F↦F. It is an involution. Twin row σ(s) equals parent row s with every target state t replaced by σ(t). For example, parent A1 = 0LD becomes 0Lσ(D) = 0LB, which is twin C1. Symbols and directions are unchanged.

check_proof.py §S searches all 720 renamings, each with and without mirroring. σ is the only map that works.

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′ in the parent if and only if σc → σc′ in the twin, and c is halted exactly when σc is. So every parent run c →ⁿ c′ gives a twin run σc →ⁿ σc′ of the same length, and the converse also holds.

Start. The twin's c0 is 0^inf A> 0^inf = σ(0^inf C> 0^inf). The parent's own run starts in A, and after two steps (A0 = 1RB, B0 = 1RC) it is at 0^inf 1 1 C> 0^inf. So the twin's run is the parent's machine run from 0^inf C> 0^inf: the parent's run without the two 1s its first two steps write. It is not the parent's run. §S checks the twin from blank against the relabelled parent from 0^inf C> 0^inf in lockstep: 2·10⁶ steps, identical at every step.

Halting cell. Only A1 enters F in the twin, and only D0 enters A. So the twin halts exactly when it reaches D> 0 1 1, which is σ of the parent's B> 0 1 1.

1. What carries over unchanged

parent item twin reason
P§1 family K(h; P; T) K_C(h; P; T) := σK(h; P; T) = 0^inf <C (10)^h 11001 [p_1,q_1,d_1] … [p_L,q_L,d_L] T 0^inf: the same words, with head state C Lemma R
P§2 rules Dec, DecMerge, DecMergeTail, DecMergeEmpty, End, EndLast, Ov, X1, X2 and outside cases (o1)–(o7) identical (table below), with <A read as <C; step counts unchanged Lemma R. Also re-checked on the twin's own table: §A, 405/405 random instances
P§3.1 reduction (domain D, chain of rule applications) identical uses only the rules
P§3.2 counter lemmas L1–L6 identical statements about the abstract map
P§3.3 INV+(e) (statement P§3.8.1) and the period theorem identical statement and proof read only (h, P, T) and the rules, never the start
P§3.4–3.6, P§3.8.2–3.8.5 (one cycle pair, preservation) identical same
P§2 halting demonstrations (o1), (o3), (o6) (1,480 / 1,554 / 1,684 steps) identical, from σK Lemma R
P§3.7 initial segment and base changed: §2 different start

The rules in busycoq comment style, for the twin (Z := pairs 1..k−1, all d = 0, q ≥ 2; touch (p,q,d) := (p+1, q−1, 1−d)):

1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---       (= sigma of 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, sigma = (A C)(B D))

[p,q,d] := (10)^p (01)^q s(d),  s(1) = 0001, s(0) = 0010
K(h; P; T) := 0^inf <C (10)^h 11001 [p_1,q_1,d_1] ... [p_L,q_L,d_L] T 0^inf,   T in { -, (10)^t 1, (101)^2 (01)^k }

Dec            K(h; Z ++ (p,q+2,1) :: R; T)             -->+ K(h+4; touch Z ++ (p+1,q+1,0) :: R; T)
DecMerge       K(h; Z ++ (p,1,1) :: (p',q',d') :: R; T)  -->+ K(h+4; touch Z ++ (p+p'+3,q',d') :: R; T)
DecMergeTail   K(h; Z ++ [(p,1,1)]; (10)^t 1)           -->+ K(h+4; touch Z; (10)^(p+t+3) 1)
DecMergeEmpty  K(h; Z ++ [(p,1,1)]; -)                  -->+ K(h+4; touch Z; (10)^(p+2) 1)
End            K(h; Z ++ [(p,q+2,0)]; -)                -->+ K(h+4; touch Z ++ [(p+1,q+1,0)]; (10)^1 1)
EndLast        K(h; Z ++ [(p,1,0)]; -)                  -->+ K(h+4; touch Z; (10)^(p+4) 1)
X2             K(h; Z ++ [(p,q+2,0)]; (101)^2 (01)^(k+1)) -->+ K(h+4; touch Z ++ [(p+1,q+1,0); (3,k+1,1)]; -)
Ov             K(h; (p1+2,q1,0) :: Y; (10)^t 1)         -->+ K(2; (h+5,p1+1,0) :: ovp q1 Y t; -)
X1             K(h; (p1+2,q1,0) :: Y ++ [(pa+1,1,0); (pb,1,0)]; -)
                                                        -->+ K(2; (h+5,p1+1,0) :: ovpX q1 Y (pa+1); (101)^2 (01)^(pb+3))
               (Ov, X1: Y all d = 0, all p,q >= 1, q1 >= 1; ovp/ovpX as in the parent's .v)

start: c0 -->(1,088) K(2; (11,13,0); -) -->(78,026) K(2; (95,68,0),(34,33,1),(10,15,1),(1,26,1); -)

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

Direct simulation of the twin from the blank tape (§C, §D). A canonical configuration is state C on a new leftmost cell, with the tape to its right parsing as a K.

twin step twin K parent step parent K
20 K(2; −; −), L = 0 8 K(0; −; −)
359 K(2; (9,1,0); −), in D: EndLast predicts the next one exactly 275 K(2; (7,1,0); −)
551 K(6; −; T1(13)), L = 0, outside D 451 K(6; −; T1(11))
1,088 K0′ = K(2; (11,13,0); −) 956 K0 = K(2; (11,11,0); −)

As in the parent, the run passes through L = 0 before K0′, so the argument starts at K0′. From K0′ on, every canonical transition is the one the rules predict: 1,534 of 1,534 to step 3·10⁷. Re-pairings (Ov/X1) happen at steps 2,009, 4,822, 8,579, 19,744, 34,493 and 79,114; the parent's are 1,845, 4,610, 8,319, 19,436, 34,137 and 78,710. The base is the E-start right after re-pairing 6:

B' = K(2; (95,68,0), (34,33,1), (10,15,1), (1,26,1); -)      at step 79,114
B  = K(2; (95,68,0), (34,33,1), (10,15,1), (1,24,1); -)      the parent's base, at step 78,710

INV+(e) at B′, clause by clause, as stated in P§3.8.1 (L = L* = 4, regular start, θ = 5): - (a) h = 2, every block ≥ 1, p_1 = 95 ≥ 7; T = −, digits (0,1,1,1), far pair (p_4, q_4) = (1, 26) with p_4 ≥ 1 and q_4 ≥ 6; - (b) q_1 + 1 = 69 ≥ 40, q_2 = 33 ≥ 20, q_3 = 15 ≥ 10; - (c) p_j + d_j = 95, 35, 11, all odd; - (d) L* = 4 ≥ 3; - (e) p_1 + 1 = 96 ≥ 64 and p_2 = 34 ≥ 16.

Only clause (a) reads q_4, and only as the lower bound q_4 ≥ 6. Every other number is the parent's.

3. The argument (complete)

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

  1. Initial segment. The twin runs from c0 to B′ in exactly 79,114 steps without halting. This is a finite exact computation (§C, §D); in Rocq it is one esx.
  2. Base. INV+(e)(B′) holds (§2).
  3. Transfer. The parent's period theorem (P§3.8.1, proof P§3.8.4) says: from an E-start satisfying INV+(e), every K up to the next E-start is in D, INV+(e) holds again there, and there are at least two macro steps, each of at least one machine step. Its statement and proof use only the rules of P§2 and arithmetic on (h, P, T). By Lemma R, each rule instance K →⁺ K′ of the parent is a twin run σK →⁺ σK′ of the same length. So the theorem holds verbatim for the twin's configurations σK.
  4. Conclusion. By induction from B′, the twin's run is an infinite chain of rule applications, each taking at least one step, so it never halts. This is the parent's P§3.1 reduction with K0, B replaced by K0′, B′. A rule application never presents the halting cell D> 0 1 1, because each rule is an exact computation from one K to the next. ∎

Nothing in the parent's argument depended on the parent's own orbit beyond P§3.7. The orbit-specific statistics in P§3.3 and P§5 (r values, merge counts, X1 count) are evidence, not premises.

4. How the twin's orbit relates to the parent's (the coupling; explanation, not a premise)

Observation. At every macro step from the first canonical configuration on, the twin's K is the parent's K with exactly one exponent larger by 2, and the two orbits apply the same rule. The larger exponent is always the far block:

where the +2 sits when
q_L, the far pair's q regular E-starts and through the E-cycle
p_L, the last pair's p (P§3.4's t₀) L-starts, until EndLast
t in T1(t) after EndLast / DecMergeTail, until Ov
k in T2(k) after X1, until X2, whose new pair (3, k, 1) puts it back on q_L
h only at step 20, where twin h = 2 and parent h = 0; at step 359 it is already on p_1 = p_L

Checked at every macro step to L = 16 (539,656 steps) and at every re-pairing to L = 300 (§X2, 1,089 re-pairings, including 3 X1/X2 detours). It was also checked to L = 600 (2,209 re-pairings; check_proof.py --lmax 600, output in check_proof_l600.out). Each cycle has the same rule sequence and the same number of decrements.

Why it persists (Lemma C, a corollary of P§3.4). - Take a parent E-start K that satisfies INV+(e), and let K⁺ be K with q_L (or k, at a T2 start) raised by 2. Then the cycle pair from K⁺ applies the same rules, and it ends at the parent's next E-start with q_L raised by 2. - In the E-cycle, the far pair (or the pair X2 appends, whose q is k) gets exactly two touches (P§3.4 S1: q_L ≥ 6, or k ≥ 4, and it loses 2). Its q is at least 3 at each touch in the parent, so also in the twin. The only branch either touch reads is "q = 1 or q ≥ 2": the borrow touch is a Dec (not DecMergeTail or DecMergeEmpty), and at V = 0 the rule is End (not EndLast or X1). The Ov then copies q_L into the new last pair's p. - In the L-slot, that p (t₀) is never compared. It enters only additively, with coefficient 1, in these places: - EndLast's t = p + 4; - the fused p of a DecMerge at M−1; - X1's T2 parameter; - DecMergeTail's t. - t and k likewise enter only additively: Ov's last-pair q = t + 1, and X2's new q = k. - So the +2 never changes a branch, and it never reaches an interior pair. That is why INV+(e) needs no change.

This also accounts for the size difference at 10⁹ steps: - twin: 67,347 cells (−67,163..183) and 33,668 nonzeros; - parent: 67,343 cells and 33,665 nonzeros.

The twin lags the parent by a slowly growing number of steps: 132 steps at K0′ and 404 at the base, because every sweep over the far block is 4 cells longer. The trajectories are therefore not identical, but they are coupled exactly.

5. Formalization delta (for the Rocq stage; not done here)

Copy the parent's .v (sha256 91861259…fcbf) and change only the following: 1. TM_from_str "1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---". 2. Rename states in the statements of the 14 sweep lemmas and in K, applying σ simultaneously: {{A}} → {{C}} (4 occurrences), {{B}} → {{D}} (12), {{D}} → {{B}} (19). The parent never names C, E or F. The es proofs should go through unchanged, because σ maps transitions to transitions (Lemma R). 3. init0 : c0 -->* K 2 [(11,13,false)] TN (1,088 steps); base with last pair (1%nat, 26%nat, true); init by esx (79,114 steps; the parent's 78,710-step esx took about 30 s). 4. J_base: the same script (cbn … repeat split; lia). The only changed clause is PN E1 at n = 0 for the last pair, q ≥ tv + 2^0 + 1 = 3, and 26 satisfies it. §B evaluates the transcribed PC E1 clauses at B′, all true. The parent's rocq/jcheck.py J holds at every macro step from B′ for 34 re-pairings. 5. Jstep, every ob_*/inv_* lemma and nonhalt: verbatim. Update the closing comment's start line.

Then run tools/check_kill.sh. Only that PASS makes it a kill.

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

The script imports the parent's check_proof.py read-only, for its abstract map and checkers. Everything that depends on the machine or the start is re-run on the twin's own table and orbit.

§ what result
S σ unique over 720 × 2 maps, involution; lockstep 2·10⁶ steps twin vs σ(parent from C); parent's step 2 = 11 C> PASS
A all 9 parent rules, 45 random instances each, simulated on the twin's table with head state C; halting cell D> 0 1 1 PASS 405/405
C blank → K(2; (11,13,0); −) at step 1,088; earlier canonical configs as in §2 PASS
D direct simulation to 3·10⁷: 1,534/1,534 transitions rule-predicted; base B′ at step 79,114 PASS
B INV+(e) at B′ (parent's inv_violations); Rocq PC E1 clauses at B′ (and at B, sanity); only q_4 differs PASS
G parent's G2 (every P§3.8 lemma at every cycle pair) and F (every INV clause at every cycle) on the twin's orbit to L* > 300 (542 cycle pairs, 245 L-slot merges, x ∈ {3,4,5} all seen); parent's jcheck J for 34 re-pairings PASS
X coupling: every macro step to L = 16, every re-pairing to L = 300; one exponent +2, far block, same rules PASS
G, X at L = 600 --lmax 600 --steps 2000000 (6.5 min, check_proof_l600.out): G2 and F over 1,102 cycle pairs (2,209 overflows, 3 X1), X2 over 2,209 re-pairings PASS

Start-independent checks of the parent (P§5: G1 skeptic counterexamples, G3 1,027,584 exhaustive starts, G4 random chains, E2 endgame table) test the abstract map only, so they apply unchanged and are not repeated.

7. Checkpoint B (Dennis)

pending. One question for the reviewer: is "same table up to σ, new init and base, invariant unchanged" acceptable as the informal proof for the submission, or does the maintainer want the parent's proof restated in full?