1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---: never halts (delta proof from kill #3)

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 (parent pointer, status, AI line), the §5 heading and a closing paragraph in §5 that says how the plan was carried out, and a line in §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 #3's submission proof.md with the same section numbers. Its remarks that this machine is not formalized predate this kill. The scripts it cites (check_proof.py, check_proof.out, check_proof_l600.out, and the parent's check_proof.py and jcheck.py) live in the working directory and are not in this folder.

• Machine: 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---, viewer https://bbchallenge.org/1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---
• Holdout list: line 293 of the 2026-10-07 holdout list (778 machines), byte for byte. Sheet: Results row 1280 and the Classifications tab, both "Skelet 1-like Class 2", class only (no status, notes, sources or "done by"). Not in our Discord exports. So it is unclaimed.
• Parent: kill #3, 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (KILLED_NONHALT, check_kill PASS). This file uses the parent's proof.md (revision 3, §3.8 authoritative) and its .v. Section numbers like "P§3.8" refer to the parent's proof.md (here: parent-proof.md).
• Written for: the string itself.
• Result. The twin is the parent's machine with its states renamed by σ = (A C)(B D), with no mirror. It starts in the parent's state C, not A. So it runs a different orbit of the same macro map:
• The rules, the outside cases, the invariant INV+(e) and the period theorem carry over unchanged.
• Only the initial segment and the base E-start change. The base differs from the parent's in one number: the far q is 26, not 24.
• Adjusted invariant: none.
• Evidence: check_proof.py, SUMMARY PASS (§6).
• Status: KILLED_NONHALT (2026-10-10). The §5 delta was applied to the parent's .v, and check_kill (our checker) passes on the result (check_kill.txt: 0 assumptions, coqchk pass).
• AI assistance: the informal proof and the Coq formalization were produced with the help of Claude (Anthropic), and checked by our checker, check_kill.

0. The map

σ: 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

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.

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:

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 (done as planned)

Copy the parent's .v (sha256 91861259…fcbf, before the parent's comment-only header edit) 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 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 our checker, check_kill. Only that PASS makes it a kill.

Done as planned (2026-10-10). A script applied items 1–5 to the parent's passing .v, each edit asserting exactly one match. The σ-swap counts came out as predicted: {{C}} 4, {{D}} 12, {{B}} 19. Every es sweep proof re-closed verbatim, and so did J_base's script with q_4 = 26. The file compiled on the first attempt, and check_kill (our checker) passed on the first run. Apart from the state names, the diff to the parent's .v is 36 changed lines: the header comment, the TM string, init0, base, the closing rule-table comment, and comments with step counts. Where each item lives in the .v:

Like the parent's .v, this file proves the parent's per-step invariant J and not the period theorem. J contains INV+(e) in projected form at E-starts. Lemma R is not a premise of the formal proof either: every rule is re-proved on the twin'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 §3 is the explanation.

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.

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 (no Checkpoint B notes were on file when this was packaged). 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?