1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---: 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 (holdout lists, parent pointer, status), a pointer at the end of §0's Lemma C, the §4 heading and a closing paragraph in §4 on how the plan was carried out, §6 (open items) and the AI line. This is a delta proof: it cites the parent's informal proof as "the parent's §n". The parent's proof is in this folder as parent-proof.md, a verbatim copy of kill #3's submission proof.md (revision 3 with a submission header; same section numbers). Its remarks that this machine is not formalized predate this kill. The scripts, logs and Rocq scratch files cited below (check_proof.py, check_proof_full.log, assemble.py, jcheck.py, parent_from_D.v and its .diff/.out) live in the working directory and are not in this folder.

• Machine: 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC--- (pilot #24), viewer https://bbchallenge.org/1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---
• Holdout lists: on every holdout-list snapshot we have, from 2024-06-14 (12,091) to 2026-10-07 (778; line 622, byte for byte). Sheet: Results CSV line 1289 gives the class "Skelet 1-like Class 2" with empty status, notes, sources and done-by; the Classifications tab lists it under that class with no note. It is not in our Discord exports, not in busycoq at the pin and not in our index of solved machines. Unclaimed.
• Parent: kill #3 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB--- (KILLED_NONHALT, check_kill PASS). This proof uses the parent's proof.md (revision 3, sha256 e8843536…) and its kill file (sha256 91861259…; since then only that file's header comment has changed). check_proof.py pins both, and prints WARN if either one changes. In this folder the parent's proof is parent-proof.md.
• Verdict. The twin is the parent, mirrored and with its states renamed, but started in the parent's state D instead of A. Every macro rule, outside case, lemma and invariant of the parent's proof carries over unchanged. The delta is the initial segment and the base E-start (§3), and the base differs from the parent's in one number, the far pair's q (25 instead of 24).
• Status: KILLED_NONHALT (2026-10-10). 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---.v (1,363 lines) proves Lemma nonhalt : ~ halts tm c0. in Coq 8.20.1 against unmodified busycoq (commit 0940bb9c). check_kill (our checker) PASS: compile 40.0 s with -native-compiler yes, Print Assumptions nonhalt closed, coqchk pass in 14.6 s (check_kill.txt). The §4 route was followed. Lemma C needed no hand-written induction: busycoq's flip_halts and perm_halts give it once Perm (flip tm) tm3 phi is checked entry by entry (§4, "Done"). check_proof.py gives SUMMARY PASS, and its negative controls all FAIL as they should (§5).

0. The map

The renaming is φ: A↦D, B↦A, C↦B, D↦C, E↦E, F↦F, and every direction flips (L↔R). For every twin entry, the entry (write w, move d, go to q′) in row q becomes the parent's entry in row φ(q), which is (w, flip(d), φ(q′)). This holds for 12 of 12 entries, including the undefined F1 ↦ F1. No other renaming works, with or without the mirror: check_proof.py §M tries all 2 × 720 candidates and finds exactly this one. A renaming without the mirror never fits.

Lemma C (conjugacy). Let μ(q, (l, s, r)) := (φ(q), (r, s, l)), which swaps the two sides of the tape and renames the state. Mirroring the tape turns move_left into move_right and back. So c -[twin]-> c' holds iff μ c -[parent]-> μ c', and c is halted for the twin iff μ c is halted for the parent. By induction on the number of steps, the twin halts from c0 iff the parent halts from μ(c0) = (D, tape0), after the same number of steps. In the .v, the direction that is needed (twin halts ⇒ parent halts from (D, tape0)) is perm_twin plus busycoq's flip_halts and perm_halts (§4).

Why this is not "identical up to renaming". μ(c0) is (D, tape0), not the parent's c0 = (A, tape0). The twin is the parent run from a different start, and its orbit is a different orbit of the same family. K0′ below is not K0. No canonical configuration of the twin occurs among the parent's in the first 3·10⁵ steps. In lockstep, the two abstract orbits differ at every macro step, by one unit (§3.9).

Halting transition. Only D1 (1LF) enters F, and only C0 (1LD) enters D. So the twin halts exactly when it reaches 1 1 0 <C, the mirror image of the parent's B> 0 1 1.

1. Family (the parent's §1, mirrored)

[p,q,d]^R := s^R(d) (10)^q (01)^p        s^R(1) := 1000,  s^R(0) := 0100
K'(h; P; T) := 0^inf  T^R  [p_L,q_L,d_L]^R ... [p_1,q_1,d_1]^R  10011 (01)^h  B> 0^inf
T^R in { - ,  T1^R(t) := 1 (01)^t ,  T2^R(k) := (10)^k 101101 }

K′(h; P; T) is exactly μ⁻¹(K(h; P; T)): the parent's word, reversed, with the head in state B (the twin's name for the parent's A) on the blank cell to its right. The parameters (h, P, T), V, touches, goodness and depth are all as in the parent's §1 and §3.3. The twin's tape grows to the right where the parent's grows to the left. At 10⁹ steps the twin spans cells −182..67,162 and the parent −67,161..181.

2. Rules: unchanged

Every rule of the parent's §2 (Dec_k, DecMerge_k, DecMergeTail, DecMergeEmpty, End, EndLast, Ov, X1, X2) holds for K′ on the twin with the same side conditions, the same effect on (h, P, T) and the same number of steps (Lemma C). The domain D and the outside cases (o1)–(o7) are the same sets of parameters. For reference, in the abstract form both machines share:

Dec            (h; Z ++ (p,q+2,1) :: R; T)          -> (h+4; touch Z ++ (p+1,q+1,0) :: R; T)
DecMerge       (h; Z ++ (p,1,1) :: (p',q',d') :: R; T) -> (h+4; touch Z ++ (p+p'+3,q',d') :: R; T)
DecMergeTail   (h; Z ++ [(p,1,1)]; T1(t))           -> (h+4; touch Z; T1(p+t+3))
DecMergeEmpty  (h; Z ++ [(p,1,1)]; -)               -> (h+4; touch Z; T1(p+2))
End            (h; Z ++ [(p,q+2,0)]; -), V=0        -> (h+4; touch Z ++ [(p+1,q+1,0)]; T1(1))
EndLast        (h; Z ++ [(p,1,0)]; -), V=0          -> (h+4; touch Z; T1(p+4))
Ov             (h; (p1,q1,0) :: Z; T1(t)), V=0, p1>=2 -> (2; (h+5,p1-1,0) :: ovp q1 Z t; -)
X1             (h; (p1,q1,0) :: Z ++ [(pa,1,0);(pb,1,0)]; -), V=0, p1>=2 -> (2; (h+5,p1-1,0) :: ovpX q1 Z pa; T2(pb+3))
X2             (h; Z ++ [(p,q+2,0)]; T2(k)), V=0    -> (h+4; touch Z ++ [(p+1,q+1,0); (3,k,1)]; -)
   (Z: pairs with d = 0 and q >= 2; touch (p,q,d) = (p+1,q-1,1-d); ovp/ovpX: the parent's re-pairings)

As a check that does not go through Lemma C, check_proof.py §A runs the twin's own table from mirrored words. All 405 random instances (45 per rule, all h mod 4, sizes 2–300) reach the predicted K′ exactly.

3. Argument: what changes

3.1–3.6 and 3.8: unchanged. These sections use only the rules of §2 and the invariant INV+(e) at an E-start. They never use the orbit from the blank tape. In particular, the parent's Theorem (period) (§3.8.1) is a statement about every K that satisfies INV+(e): every K of the next cycle pair is in D, and INV+(e) holds again at the next E-start. Its proof (§3.8.2–3.8.4: L1–L6, L5′, the S2 table, the survival of pairs 1 and 2) applies word for word. So does the Rocq form of the same step, the parent's Jstep : forall s, J s -> exists s', Cf s -->+ Cf s' /\ J s', which is proved for all states.

No invariant needs adjusting. The base, below, satisfies INV+(e) (and J) with the same constants as the parent's base.

3.7 Initial segment and base: CHANGED.

As in the parent, the twin passes through L = 0 before K0′. At step 316, EndLast applies and predicts step 500 exactly, and step 500 has L = 0, which is outside D. So the argument starts at K0′. From K0′ the rules apply at once (End at step 1313, Ov at step 1926).

INV+(e) at the twin's base, in the parent's §3.8.1 form (L* = 4, regular start): - (a) h = 2, p_1 = 95 ≥ 7, digits (0,1,1,1), far pair (1, 25, 1) with p_L ≥ 1 and q_L = 25 ≥ 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, p_2 = 34 ≥ 16.

These are the parent's numbers, except that the far q is one larger; INV+(e) asks only q_L ≥ 6 of it. The same goes for the Rocq invariant J (phase E1): the only clause that involves the far pair's q is q >= tv + 2^0 + 1, with tv = d_L = 1, so it reads q ≥ 3 (here q = 25), and every other clause has the parent's values. So J_base goes through with the parent's proof (repeat split; lia).

Conclusion. Every configuration from K0′ to the base is in D, by exact computation. The base satisfies INV+(e), so by the Theorem every configuration after it is in D. The twin therefore never halts (parent's §3.1, applied to K′ through Lemma C).

Shorter alternative base. The E-start after overflow 4, K′(2; (47,32,0),(16,15,1),(4,21,1); −) at step 19,589, also satisfies INV+(e) and J, with L* = 3. It would cut the Rocq init from 78,911 steps to 19,589. The parent's E-start after overflow 4 satisfies both too.

3.9 Why the trajectories look the same (informational; not used). Run in lockstep, the two abstract orbits apply the same rule at every macro step, and their states differ by exactly +1 on one far-end block. check_proof.py §L checked this to L = 120, about 2^124 macro steps. The extra unit moves around a fixed loop: - it is on the far q at an E-start; - the E-cycle's Ov moves it to the new last pair's p (t₀, a tail block); - EndLast moves it into the tail T1; - the next Ov moves it back to the far q.

On an X1 detour it rides T2(k) and then X2's new pair (3, k, 1). It is never on x or on an interior block, which is why the rule sequence cannot differ. It also explains the 67,345 vs 67,343 cells at 10⁹: one extra 2-cell block, on the mirrored side.

4. Formalization (delta to the parent's .v; done)

Recommended: reuse the parent's kill file unchanged, and add a conjugacy lemma. 1. Keep the parent's development (K, the 9 macro rules, J, Jstep) for the parent's table under a second name, say tm3, with the local -->*/-->+ notations bound to tm3. Make the top-level Definition tm := TM_from_str "1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---". check_kill only warns about a second TM_from_str literal (our checker's tm_text warning). 2. mu (q,(l,s,r)) := (phi q, (r,s,l)). Prove c -[tm]-> c' -> mu c -[tm3]-> mu c' and halted tm c -> halted tm3 (mu c). The proof is a destruct over 6 states × 2 symbols and the two step constructors, using move_left/move_right swapping under mu. Then derive halts tm c0 -> halts tm3 (D, tape0) by induction on the step count. 3. init' : (D, tape0) -[tm3]->* K 2 base' TN: 78,911 steps, or 19,589 from the overflow-4 base. Use solve_initD, not esx. esx takes its fast vm_compute path (solve_init) only for goals that start at c0; from (D, tape0) it falls back to symbolic es, and a scratch run did not finish in 14 minutes (killed at 2.5 GB). solve_initD is busycoq's solve_init with its first rewrite replaced by change (D, tape0) with (cconfig_to_config (nil,nil,0,D)), and it closes init' in seconds (parent_from_D.v). 4. J_base' : J (mkst 2 base' TN E1 false), with the parent's proof. 5. nonhalt : ~ halts tm c0 from 2–4, multistep_nonhalt and progress_nonhalt_cond with Jstep.

The alternative is to mirror the whole 1,301-line file by hand (swap *>/<* and {{X}}>/<{{X}}, rename the states). That is more work and adds no trust.

Done (2026-10-10). assemble.py generated the kill file from the parent's passing .v (sha256 91861259…, before the parent's comment-only header edit). It asserts that each edit applies exactly once, and no hand edits were made afterwards. Steps 1, 3, 4 and 5 were carried out as written. Step 2 changed: busycoq already has both halves of Lemma C, so no mu and no induction on the step count were written. - Flip.flip_halts : halts tm c -> halts (flip tm) (flip_conf c) does the mirror. flip_conf c0 is A;; tape0 by conversion, because the blank tape is symmetric. - Permute.perm_halts : Perm tm tm' f -> halts tm (q;; t) -> halts tm' (f q;; t) does the renaming, with φ(A) = D. - The one new proof obligation is perm_twin : Perm (flip tm) tm3 phi: the halting entry and all 11 transitions, closed case by case (cbn, then discriminate/reflexivity or inversion). This is §0's 12/12 table identity, checked in the kernel.

Compared with the parent's .v, 22 lines were replaced and 82 added: the header, the tm/tm3 naming, solve_initD, init0/base/init, nonhalt_D, the conjugacy and the closing comment. Where each item lives:

Like the parent's .v, this file proves the parent's per-step invariant J, not the period theorem. J contains INV+(e) in projected form at every E-start. So the kill rests on the .v alone, and the prose here and in the parent's §3 is the explanation.

5. Evidence (python3 -B check_proof.py [--selftest], about 21 s; check_proof_full.log)

The script has its own direct simulator of the twin string, which §A, §C, §D and §S use. It reuses the parent's abstract map, inv_violations and cycle_pair_checked (check_proof.py), and the parent's J (jcheck.py), all pinned by sha256. Default run: SUMMARY PASS. - §M: the table identity holds for 12/12 entries; the map is unique among 1,440 candidates; the start state goes to D; the twin halts only at 1 1 0 <C. - §S: twin from blank and parent from (D, tape0) in lockstep for 5·10⁶ steps. At every step the state is the mapped one, the symbol read is the same and the transition is the mirrored one. At the end the tapes are mirror images (2,651 nonzeros each). - §A: 405/405 rule instances on the twin's own table. - §C/§D: K0′ at step 1021. 1,534/1,534 canonical transitions to 3·10⁷ steps are predicted by the abstract map, and the base is reached at step 78,911. - §B: INV+(e) at the base, clause by clause; J holds; the only difference from the parent's base is pair 4's q (25 vs 24); the overflow-4 option checks out too. - §G: the parent's cycle_pair_checked, which checks every identity and inequality of proof.md §3.8, run on the twin's orbit from the base to L* > 300. Result: 542 cycle pairs (539 EndLast slots, 3 X1 slots), 245 L-slot merges, x = 3/4/5/≥6 all seen, min p_1′/(2^(L*′+2)−1) = 1.000, min p_2′/2^(L*′) = 2.234, all pass. - §J: the parent's Rocq invariant J at every macro step from the base for 30 re-pairings: 80,792 Decs, including an X1/X2 detour; no failure. - §L (informational): the lockstep of §3.9, to L = 120: PASS. - §N (--selftest): seven negative controls (wrong map, parent started in A, rules on the unmirrored table, the parent's K0, the parent's base, and the skeptic's start for G and J). Each one FAILs, as it should. - The parent's orbit-independent evidence (its §G1, §G3 = 1,027,584 exhaustive starts, §G4 = 120,000 random cycle pairs) and its Rocq Jstep cover the Theorem for every INV+(e) start. They are not re-run here. - 1e9 direct simulation (our simulator, C core): the twin has not halted, has 33,665 nonzeros and spans 67,345 cells; the parent, 33,665 nonzeros and 67,343 cells.

6. Open items

• Dennis's Checkpoint B reading (non-blocking). No Checkpoint B notes were on file when this was packaged.
• Formalized (§4, "Done"): the parent's file plus 82 lines. Lemma C took about 15 lines (phi, perm_twin, nonhalt) instead of the planned 40–60, because busycoq ships flip_halts and perm_halts.
• Rocq sanity check, done. parent_from_D.v is the parent's kill file with four changes (parent_from_D.diff):
• an Ltac solve_initD;
• init0 and init start from (D, tape0), reaching K(2; (11,12,0); −) and then the base with q_4 = 25;
• the base has q_4 = 25 instead of 24;
• the final lemma is nonhalt_D : ~ halts tm (D, tape0), where tm is still the parent's table.

It compiles: rc=0 in 39.7 s, and Print Assumptions nonhalt_D reports Closed under the global context (parent_from_D.out). The parent's unchanged J_base proof (repeat split; lia) and Jstep go through. So "the parent never halts from (D, tape0)" is machine-checked, and at that point the only link of the delta not yet in Rocq was Lemma C (conjugacy; now perm_twin, §4). This file is not a kill: check_kill needs the twin's string and ~ halts tm c0, which needs steps 1, 2 and 5 of the route above. - Related: look-alike #25 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD--- is a plain renaming of the parent (σ = (A C)(B D), no mirror), started in the parent's state C. Another agent has already killed it (KILLED_NONHALT) by renaming the states in the parent's .v with a script. That shortcut does not carry over to #24: mirroring busycoq terms swaps the arguments of *>/<*, which a text substitution cannot do. Hence route §4 (conjugacy lemma) here.

AI assistance: the informal proof and the Coq formalization were produced with the help of Claude (Anthropic), and checked by our checker, check_kill.