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

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

0. The map

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

ρ: A↦D, B↦A, C↦B, D↦C, E↦E, F↦F. It is the 4-cycle (A D C B), and ρ⁻¹ = (A B C D). - Twin row ρ(s) is parent row s with every target state t replaced by ρ(t). Symbols and directions are unchanged. For example, parent A1 = 0LD becomes 0Lρ(D) = 0LC, which is twin D1. - check_proof.py §S searches all 720 renamings, each with and without mirroring. ρ is the only map that works. - The same search, against the siblings, gives the sibling maps of reports/family-sweep.md: the twin is BCDAEF(#25), started in #25's D, and the mirror of CDABEF(#24), started in #24's C. These are informational.

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 B> 0^inf). - The parent's own run starts in A. After one step (A0 = 1RB) it is at 0^inf 1 B> 0^inf. - So the twin's run is the parent's machine run from 0^inf B> 0^inf: the parent's run without the 1 its first step writes. It is not the parent's run. - §S checks the twin from blank against the relabelled parent from 0^inf B> 0^inf in lockstep: identical at every step for 2·10⁶ steps.

Halting cell. Only B1 (1RF) enters F in the twin, and only A0 (1RB) enters B. So the twin halts exactly when it reaches A> 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_D(h; P; T) := ρK(h; P; T) = 0^inf <D (10)^h 11001 [p_1,q_1,d_1] … [p_L,q_L,d_L] T 0^inf: the same words, with head state D 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 <D; 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)):

1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---       (= rho of 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---,
                                                  rho: A->D, B->A, C->B, D->C, E, F fixed)

[p,q,d] := (10)^p (01)^q s(d),  s(1) = 0001, s(0) = 0010
K(h; P; T) := 0^inf <D (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 -->(402) K(2; (7,4,0); -) -->(38,330) K(2; (47,32,0),(40,33,1),(13,34,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 D on a new leftmost cell, with the tape to its right parsing as a K.

twin step twin K note
121 K(2; −; T1(4)), L = 0 outside D (empty pair list); the parent's analogue is step 8, K(0; −; −)
402 K0′ = K(2; (7,4,0); −) first K in D; End predicts the next one exactly. Parent: K0 = K(2; (11,11,0); −) at step 956
598 K(6; (8,3,0); T1(1)) Ov next
1,083 K(2; (11,7,0),(3,2,1); −) re-pairing 1 (an L-start: far q = 2)

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,607 of 1,607 to step 3·10⁷; - 5,323 of 5,323 to step 3·10⁸ (Dec 5,266, Ov 26, End 13, EndLast 13, DecMerge 3, DecMergeTail 2; check_proof_3e8.out).

Re-pairings (Ov/X1) happen at steps 1,083, 3,520, 6,965, 17,738, 23,871 and 38,732. The parent's are at 1,845, 4,610, 8,319, 19,436, 34,137 and 78,710. As in the parent, the E-starts are the configurations after even re-pairings.

The E-starts after re-pairings 2 and 4 cannot be the base, because both have L* = 2 and INV(d) needs L* ≥ 3: - after re-pairing 2 (step 3,520): K(2; (23,14,0),(3,9,1); −), which also fails (e2); - after re-pairing 4 (step 17,738): K(2; (47,32,0),(16,30,1); −).

Rocq's J fails there too, since PI for pair 1 needs n = L − 1 ≥ 2. The base is the E-start after re-pairing 6:

B' = K(2; (47,32,0), (40,33,1), (13,34,1); -)                at step 38,732   (L = L* = 3)
B  = K(2; (95,68,0), (34,33,1), (10,15,1), (1,24,1); -)      the parent's base, at step 78,710   (L* = 4)

INV+(e) at B′, clause by clause, as stated in P§3.8.1. Here L = L* = 3, it is a regular start, θ = 5, e_1 = 2 and e_2 = 1. The interior pairs are j = 1, 2: - (a) h = 2, every block ≥ 1, p_1 = 47 ≥ 7; T = −, digits (0,1,1), far pair (p_3, q_3) = (13, 34) with p_3 ≥ 1 and q_3 ≥ 6; - (b) q_1 + 1 = 33 ≥ 5·2² = 20, q_2 = 33 ≥ 5·2 = 10 (r_1 = 8.25, r_2 = 16.5); - (c) p_1 + d_1 = 47, p_2 + d_2 = 41, both odd; - (d) L* = 3 ≥ 3, with equality; - (e) p_1 + 1 = 48 ≥ 2⁵ = 32 and p_2 = 40 ≥ 2³ = 8.

p_1 = 47 = 3·2^(L*+1) − 1 is the exact value the parent's proof gives at every regular start (P§3.8.1; the parent's base has 95 at L* = 4).

Rocq J at B′, J (mkst 2 base TN E1 false): P ≠ [], TC E1 false TN, and PC E1 for every pair (the parent's Definitions PN, PI, PC). Write n for the number of pairs to the right, tv for the digit value from the pair up, and w = 2^n:

pair n, tv, w PN E1 PI
1 (47,32,0) 2, 6, 4 q = 32 ≥ tv+3w+1 = 19; p+tv = 53 odd; p+tv+w = 57 ≥ 3w = 12 h even; n = 2 ≥ 2; p+tv+w+3 = 60 ≥ 11w = 44; h+4(tv+w)+6 = 48 ≥ 12w = 48 (tight, as at the parent's base: 96 ≥ 96)
2 (40,33,1) 1, 3, 2 q = 33 ≥ 10; p+tv = 43 odd; 45 ≥ 6 p+tv+w+1 = 46 ≥ 7w = 14
3 (13,34,1) 0, 1, 1 q = 34 ≥ tv+w+1 = 3; p+tv+w = 15 ≥ 3 —

All clauses hold (§B). The tight clause is tight at every regular start: h = 2, tv = 2^L − 2 and w = 2^(L−1) give exactly 12w.

3. The argument (complete)

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

  1. Initial segment. The twin runs from c0 to B′ in exactly 38,732 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 and B replaced by K0′ and B′. - A rule application never presents the halting cell A> 0 1 1, because each rule is an exact computation from one K to the next. ∎

L* = 3 is inside the theorem's scope. The theorem assumes INV+(e), whose clause (d) is L* ≥ 3, so B′ meets it with equality. The proof uses the size of L* in three places, and each holds at L* = 3: - P§3.8.4 Step 2 and (d): M = L* + 1 ≥ 4 pairs at the L-start, so pairs 1 and 2, the x-pair and the last pair are distinct; - P§3.8.3: the pair-1 and pair-2 budgets need L* ≥ 2; - P§3.8.4 (e2): needs L* ≥ 2.

Nothing in P§3.4–3.8 assumes L* ≥ 4. The parent's own evidence tested this case directly: - its §G3 exhaustive boxes include "reg L*=3" and "T2 L*=3" at the thresholds; - its G4 random chains start at L* = 3..40.

This file adds §N, 5,000 random L* = 3 starts around B′. In Rocq, Jstep is proved for every J state, and B′ satisfies J (§2).

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 (explanation, not a premise)

No coupling. #25 and #24 are coupled to the parent: at every macro step their K is the parent's K with one far exponent larger (by +2 for #25, +1 for #24). This twin has no such coupling. - B′ differs from B everywhere but h. It has one pair fewer, and every block differs. - The E-start sequences never meet. Among the first 120 E-starts of each orbit, counted from each base, none is shared (§O). A shifted copy of the parent's orbit would share all but finitely many. - The next E-start is the parent's base reshaped. The twin's E-start after B′ is K(2; (95,68,0),(34,33,1),(34,33,1),(10,38,1); −): the parent's base with an extra (34,33,1) pair and a different far pair. - L* runs one behind, then catches up. The twin's L* at the n-th E-start trails the parent's by one for a while (E-start 10: 9 vs 10; 20: 15 vs 16), and later the two agree (E-start 119: both 73). - The tape is wider. At 10⁹ steps the twin's tape spans 79,454 cells (−79,241..212), with 39,718 nonzeros. The parent's spans 67,343 cells, with 33,665 nonzeros, so the twin's tape is 18% wider.

Same macro map, same behaviour. On its own orbit to L* > 600, the twin shows the parent's pattern (check_proof_l600.out): - 1,102 cycle pairs, 1 X1 detour (x ∈ {3, 4, 5} all seen) and 504 L-slot merges (494 interior Ep run-outs); - INV(b) margins comparable to the parent's: minimum interior r = 8.25 at regular E-starts and just under 8 after the X1 slot (threshold 5, resp. 4). On the parent's orbit, read off #25's coupled run in its check_proof.out, the minima are 7.5 and 7.906.

The figures img/every1e6_1e9.png and img/parent3_every1e6_1e9.png show the same band structure at the same scale. The twin's left edge is farther out.

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

Copy the parent's current .v (sha256 cfa603a3…3031, check_kill PASS) and change only the following. This is the #25 recipe with a different renaming and base: 1. TM_from_str "1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---". 2. Rename states in the statements of the 14 sweep lemmas and in K, applying ρ simultaneously: - {{A}} → {{D}} (4 occurrences), {{B}} → {{A}} (12), {{D}} → {{C}} (19); - the parent never names C, E or F (checked: 0 occurrences); - after the swap, expect D 4, A 12 and C 19; - the es proofs should go through unchanged, because ρ maps transitions to transitions (Lemma R), and #25's σ-swap re-closed on the first try. 3. Change the start: - init0 : c0 -->* K 2 [(7,4,false)] TN (402 steps; unused, kept only for parallelism with the parent); - base := [(47,32,false); (40,33,true); (13,34,true)], a 3-element list; - init by esx over 38,732 steps, about half the parent's 78,710 (which took about 30 s). 4. J_base: the same script (cbn … repeat split; lia). Every clause is a closed arithmetic fact at B′ (§2). The tight one, h + 4(tv + w) + 6 ≥ 12w, is closed by lia exactly as in the parent. 5. Jstep, every ob_*/inv_* lemma and nonhalt: verbatim. Update the header and closing comments: the start line, the 78,710 → 38,732 and the <A → <D.

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

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

The script imports the parent's check_proof.py and rocq/jcheck.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 (DABCEF, plain); lockstep 2·10⁶ steps twin vs ρ(parent from 0^inf B> 0^inf); parent's step 1 = 1 B>; sibling maps (info) PASS
A all 9 parent rules, 45 random instances each, simulated on the twin's table with head state D; halting cell A> 0 1 1 PASS 405/405
C blank → step 121 (L = 0, outside D) → K0′ = K(2; (7,4,0); −) at step 402 PASS
D direct simulation to 3·10⁷: 1,607/1,607 transitions rule-predicted; base B′ at step 38,732 after re-pairing 6 PASS
B INV+(e) at B′ (parent's inv_violations, L* = 3); Rocq PC E1 clauses at B′ (and at B, sanity); the E-starts after re-pairings 2 and 4 fail (d) and J 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 (537 cycle pairs, 239 L-slot merges, x ∈ {3,4,5} all seen); parent's jcheck J for 34 re-pairings (125,503 Dec steps) PASS
N 5,000 random regular L* = 3 INV+(e) starts (thresholds up to about 2× B′), one checked cycle pair each (next L*: 3 in 403, 4 in 4,597) PASS
O (informational) orbit comparison and 10⁹-step tape statistics, §4 —
D at 3·10⁸ --steps 300000000 (66 s, check_proof_3e8.out): 5,323/5,323 PASS
G, N at L* = 600 --lmax 600 --steps 2000000 (3.4 min, check_proof_l600.out): G2 and F over 1,102 cycle pairs (2,205 overflows, 1 X1) PASS

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

7. Checkpoint B (Dennis)

pending. Questions 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? - Is the 3-pair base, at the lower edge L* = 3 of INV+(e), enough as it stands? The alternative is to start one E-start later, at the 4-pair K(2; (95,68,0),(34,33,1),(34,33,1),(10,38,1); −) after re-pairing 8 (step 104,510; INV+(e) and J hold there too), which costs an esx 2.7 times longer.