1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB: never halts (delta proof from kill #12)

• Machine: 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB, viewer https://bbchallenge.org/1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB
• Holdout list: line 676 of data/holdouts/2026-10-07_778.txt, byte for byte. Sheet: Results row 833, class "Counter Class 4", no status, no notes, no links. Level 0 note "-". The Direct Simulation tab lists it only as not yet simulated to 1e14. It is not in either local Discord file. In busycoq it appears only as tm' of Eqv.v module TM113 (eqv: halts tm c0 <-> halts tm' c0). That lemma is an equivalence, not a proof for either side, and data/solved_index.tsv has no proof for it.
• Parent: kill #12, 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF (KILLED_NONHALT, check_kill PASS). Its proof.md (cited as P§n below) and its passing .v (cited as P.v) are in machines/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF/.
• Status: delta proof, written 2026-10-10 (overnight, unattended). Every claim is checked by simulation in check_proof.py (labels R, A, C, B, T, H, F, G). Not formalized yet. Checkpoint B (Dennis) is pending.
• AI assistance: drafted by Claude (Anthropic).

Summary. The twin is not #12 up to state renaming or L/R mirroring. It is #12 renamed by σ (below), with one transition changed and a different start state. In the parent's names the twin is the parent with A0 := 1RA (instead of 1RB), started on a blank tape in state B. This gives exactly three changes, and nothing else changes: 1. One TM rule. A0 is read only at the first step of R3. There the new transition takes a 6-step detour to the same configuration that the parent reaches in 2 steps. So R3 becomes R3', with the same tape effect and 4 more steps. 2. Initial segment. Starting in state B, the twin reaches conf([], [2,2,1]) in 48 steps. The parent reaches conf([], [3,2,1]) in 50. 3. Top-level invariant. The twin returns to conf([], [2,2]+O_n([])) for every n, where the parent returned to conf([], [3,2]+O_n([])). The edge frame has a budget of 2 children per epoch instead of 3, and every top epoch spends exactly 2, so there is zero slack.

The run model, the epoch rules and the Theorem (P§1.1–§3) carry over verbatim. They are statements about the run model only, and P.v machine-checks them. This is the TM113 argument of P§6.1 with R3 replaced by R3'.

1. The relation (explicit map)

σ maps twin states to parent states: A→B, B→C, C→D, D→E, E→F, F→A. The run model's head state is the parent's A, which is the twin's F.

• σ(parent) = 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RA1LB, which is exactly Eqv.v TM113.tm. The twin is TM113.tm with F0 changed from 1RA to 1RF (string index 37).
• The twin's start state A is σ⁻¹(B). So the twin's blank start is the parent's blank tape in state B.
• Search (evidence R). I compared the twin against all 720 relabelings of the parent, each both as is and L/R-mirrored (1,440 candidates). None matches. σ is the unique closest one, with 1 differing transition, and the next closest has 5. Among relabelings that keep the start state (π(A) = A), the closest differ in 6 transitions, or 9 when mirrored.

From here on, rules are written in parent names: the head state is A, and twin names are given in brackets. That way every rule of P§1–§3 can be cited unchanged. In twin names the parent's <A is <F.

2. Changed rule: R3 becomes R3' (the only TM-level change)

Where A0 is read. By Lemma RM and the initial segment (P§1.1, P§5), the whole run splits into the macro rules of P§1. Each of them is a fixed transition sequence, listed in P§1. A0 occurs in exactly one of these sequences: as the first transition of R3. R1, R2 and R2e start with A1, and so does HALT. CW, DW and FW use C1/B1/B0, D1 and F1. So changing A0 changes R3 and nothing else.

Why this is so: in the parent, A is entered only by F0 = 0LA [twin E0 = 0LF], the last transition of every macro rule. A then reads the last cell of lside L. That cell is a 1 when L ≠ [] (the top run), and the edge 0 when L = [], which is the p = 0 case of RM, R3. In the twin, A [twin F] is also entered by the changed transition itself (A0 = 1RA, twin F0 = 1RF), but only inside the R3' detour below. Evidence A6: in the twin, F0 occurs in none of R1, R2, R2e or HALT.

R3   (parent)  0^inf <A 0 1^(k+1) 0 0 1^m 0 r  -->  0^inf 1^(k+2) <A 0 1^(m+1) 0 0 r     3k+2m+11
               = A0 B0 · CW(k) · C1 B0 C0 · DW(m+2) · D0 E1 · FW(m+1) · F0
R3'  (twin)    0^inf <A 0 1^(k+1) 0 0 1^m 0 r  -->  0^inf 1^(k+2) <A 0 1^(m+1) 0 0 r     3k+2m+15
               = A0 A0 A1 C1 B1 B0 · CW(k) · C1 B0 C0 · DW(m+2) · D0 E1 · FW(m+1) · F0
                 [twin names: F0 F0 F1 B1 A1 A0 · CW(k) · ...]

The detour. Call the head cell e, the next cell z (the 0), and the first cell of 1^(k+1) u.

The result is e = 1, z = 1, with C reading u. The parent reaches this same configuration after A0 = 1RB, B0 = 1RC. From here both machines run the identical sequence CW(k) · C1 B0 C0 · ..., which uses no A0. The detour touches only e, z and u. It needs u = 1, which holds because c_1 >= 1 in the domain, and the cells left of e play no part. So R3' also holds with an arbitrary left side l 0 <A 0 1^(k+1) ..., the form of P.v's tR3. Evidence A2: 500 random instances with 0^inf on the left and 500 with a random left side (k, m in 0..25, random r). The tape, head, state and step count are exact. Under σ the twin's transition sequence equals the parent's, with A0 B0 replaced by A0 A0 A1 C1 B1 B0.

Unchanged rules. CW, DW, FW, R1, R2, R2e and HALT (P§1) are unchanged: they use the same transitions in the same order and take the same number of steps. Evidence A1, A3, A4, A5: 500 instances each of R1, R2 and R2e, plus 40 of HALT. The twin's transition sequence equals the parent's under σ. HALT is 0^inf 1 <A 0 r, then A1 C0 D0, and E reads 0 [twin: F1 B0 C0, then D reads 0 at ---].

3. Unchanged: run model, epoch rules, Theorem

• Lemma RM (P§1.1) holds for the twin as stated. RM's push for p = 0 is R3' instead of R3, which has the same tape effect and so the same model step (push c_1 + 1, same R-update). The model therefore does not change at all. Only one TM step count changes: an R3 macro step now costs 4 more steps. Evidence B1: run model = twin TM at every macro step for 40,000 macro steps from step 48. B2: the raw twin was scanned at every step up to 4·10^8 for left-edge configurations (state F, every cell at or left of the head blank). It finds exactly 41: conf([],[1]) at step 8 and conf([],[2,2]+O_n([])) for n = 0..39 (the last at step 330,296,492). Each is at the model's exact step with the twin's step counts, and nothing else appears. A control run with the parent's R3 count gives the same words at different steps, so the check does see the +4. B3: 11 of these returns re-checked with the tools/sim.py C core.
• Epoch rules U0–U2, TR, TL, TF, X, T, S (P§2) and the Theorem with Inv and AL (P§3) hold verbatim. They are statements about the run model (lists of naturals) and mention no TM step counts, and their proofs use only the model. P.v proves them, from Life to Theorem main. In P.v the TM appears only in tR1, tR2, tR3, tR3c and the conf encoding, through push_ok, push0_ok, pop_ok, Life_tm, Ep_tm, init and nonhalt.
• "Each epoch takes at least 9 macro steps, so at least 9 TM steps" (P§6) still holds, since every macro step is at least one TM step.

4. Changed: the initial segment

c0 = 0^inf B> 0^inf   [twin: 0^inf A> 0^inf]
 --8-->   0^inf <A 0 1 0^inf            = conf([], [1])         B0 C0 D1 D1 D0 E1 F1 F0   [twin A0 B0 C1 C1 C0 D1 E1 E0]
 --15-->  0^inf 1^2 <A 0 1 0^inf        = conf([2], [1])        R3' (k=0, m=0)
 --15-->  0^inf 1 0 1 <A 0 1 0^inf      = conf([1,1], [1])      R1  (n=0, m=0, x=0)
 --10-->  0^inf <A 0 1^2 0^2 1 0^inf    = conf([], [2,2,1]) = conf([], [2,2]+O_0([]))     R2e (k=0)

That is 48 steps. TM113 takes the same path in 44 steps, using R3 (11 steps) instead of R3' (15). The first 8 steps are the parent's state-B transitions and use no A0, since A is entered only at step 8. Evidence C: the exact tapes at steps 8, 23, 38 and 48, and the steps at which the head is in A [twin F]: 8, 9, 10 (the R3' detour), 23, 38, 48.

5. Changed: the top-level invariant

Parent (P§4, §6). The run is at Edge(O_n([])) = conf([], [3,2]+O_n([])). R3 creates the edge frame with value 4, which is a budget of 3 children. Every top epoch costs 2, so there is one unit of slack.

Twin. The run is at conf([], [2,2]+O_n([])). R3' creates the edge frame with value 3, a budget of 2. Every top epoch costs exactly 2, so there is zero slack.

Budget-2 edge lemma (P§6.1). Suppose Ep(W) = (c, W') with c <= 2, in k macro steps. Then conf([], [2,2]+W) --> conf([], [4-c, 2]+W') in the same k macro steps, and L ≠ [] in between.

Proof. This is the TL argument of P§2 with an empty context. Run Edge(W) (budget 3) and conf([],[2,2]+W) (budget 2) side by side. In the first macro step, R3 pushes 4 in the first run and R3' pushes 3 in the second, and the R-update is the same in both because it depends only on R. From then on the stacks are [4-i]+S and [3-i]+S, with the same S and R, where i counts the children that the bottom frame B has created. Go through the cases of P§2: - Pushes, and pops with |S| >= 2, read only S and R, so both runs make the same step. - When S = [], B is on top and creates child i+1 <= c <= 2. So 3-i >= 2, and B pushes in both runs. - The final pop (|S| = 1) is R2e in both runs. In the first, [4-c,1] -> []; in the second, [3-c,1] -> [] with 3-c >= 1, giving R := [4-c,2]+W'.

The budget-2 run could halt only if B were on top with value 1. That is a request for a third child, which needs c >= 3. ∎

In Coq this is an instance of lemmas already proved in P.v. Ep W 2 W' is Life 4 R0 (Pop 2 (3::2::W')). Life_shape at z = 3 gives Life 3 R0 (Pop 2 (2::2::W')). push0_ok at h = 2 gives conf [] (2::2::W) -->+ conf [3] R0, and Life_tm with L = [] finishes.

Top-level step. Apply the Theorem (P§3) with M = []. Since I([]) is empty, every epoch Ep(O_n([])) exists and costs exactly 2. The budget-2 lemma with c = 2 then gives conf([], [2,2]+O_n([])) --> conf([], [2,2]+O_{n+1}([])) in at least 9 TM steps, for every n. With §4, the twin passes through conf([], [2,2]+O_n([])) for every n and never halts. ∎

Zero slack. A single cost-3 top epoch would halt the twin. The parent's Theorem rules this out with exact costs ("cost 3 iff n ∈ I(M)"), and its Coq form, step_lemma with cost [] n = 2 by reflexivity, is exact too. A bound "cost ≤ 3" would have been enough for the parent but would not be enough here. Evidence H: the budget-2 lemma holds in all 398 cases with c <= 2 (the top orbit, marker orbits, and arbitrary words), and in all 88 cost-3 cases the budget-2 run halts. F: O_n([]) for n <= 37, all costs 2 (the parent's check, imported).

6. The undefined transition

The twin's --- is D0, which is the parent's E0. D is entered only by C0 (0LD) [parent D0 = 0LE]. Exactly as in P§6, it reads 0 only in the HALT pattern 0^inf 1 <A 0, and that is the halting case the top-level argument excludes. Evidence G: in 2·10^6 steps from blank, D is entered 100,132 times, always from C0 and always reading 1. A5: the HALT pattern halts after 3 steps, reading D0.

7. Trajectory twin (observation)

The twin, TM113 (= the parent started in state B) and the parent all pass through the same words O_n([]). The twin and TM113 pass through the same configurations conf([],[2,2]+O_n([])). At return n the twin is 4(n+1) steps later: one R3' per top epoch, plus one in the init. The parent passes through conf([],[3,2]+O_n([])), whose first run is one cell longer. Evidence T1–T3, raw scans to 4·10^8 steps: TM113.tm's scan equals the scan of the parent started in B, and the step offsets are exact. T4: at step 10^9 the twin has visited 133 cells (87 nonzeros), TM113 also 133 (87), and the parent 134 (89). This matches the observer's "134/133 cells".

8. Formal delta (plan for the .v; Eqv.v is not needed)

Copy P.v and change only the following: 1. Definition tm := Eval compute in (TM_from_str "1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB"). 2. Change the head state <{{A}} to <{{F}} in tR1, tR3, tR2 and tR3c, and in conf. All four should still close by es, since tR3/tR3c are just 4 steps longer. push_ok, push0_ok, pop_ok, Life_tm, Ep_tm and everything from Life to Theorem main stay unchanged. 3. Add Lemma Ep_tm2 W W' : Ep W 2 W' -> conf [] (2 :: 2 :: W) -->+ conf [] (2 :: 2 :: W'), proved from Life_shape (z = 3), push0_ok (h = 2) and Life_tm (L = []), as in §5. 4. Lemma init : c0 -->* conf [] [2; 2; 1]. by solve_init (48 steps). 5. In nonhalt, use C i := conf [] (2 :: 2 :: snd i) and Ep_tm2 in place of Ep_tm. The cost [] n = 2 rewrite stays as it is. 6. Update the closing comment block: rule table with R3' (+4 steps), start: c0 -->* conf [] [2;2;1] (48 steps), and top: conf [] (2::2::O_n) -->+ conf [] (2::2::O_(n+1)).

This is a direct proof whose string is the holdout entry. It does not go through TM113.eqv.

9. Evidence and gaps

ulimit -v 6000000; python3 -B check_proof.py runs every check below in about 1 minute. --quick runs a subset in a few seconds. --model also re-runs the parent's model-level sections D, E1 and E2, which do not depend on the TM. The script exits 0 iff everything passes. It imports the parent's check_proof.py for the run model, and it needs a C compiler for scripts/edge_scan.c, a copy of the parent's scan with an edge-state argument. Output: scripts/check_proof_out.txt (full run, seed 2026: ALL CHECKS PASSED, 52 s). The --model sections are the parent's own code on the same model, so with the same seed they give the parent's recorded result (machines/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF/scripts/check_proof_out_review1.txt, ALL CHECKS PASSED), and P.v proves that layer anyway. They were not re-run here.

Gaps. - The unchanged part (run model, epoch rules, Theorem) is machine-checked in P.v. The changed part is checked only by simulation: R3', the 48-step init, and the budget-2 top step. The top step is an instance of the Coq-proved Life_shape, so the formal risk is small. The only new tactic work is in §8 items 2–5. - No other gaps. The delta changes no case split of RM, and it uses no new property of the Theorem beyond the exact costs at M = [], which P.v already provides.