1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB: never halts

• Machine: 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB, viewer https://bbchallenge.org/1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB
• Holdout: on the current BB(6) holdout list. In busycoq it appears only as tm' of verify/Eqv.v, Module TM113, whose eqv : halts tm c0 <-> halts tm' c0 relates it to TM113.tm = 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RA1LB. That lemma is an equivalence, not a proof that either machine runs forever.
• Written for: the string itself. The .v proves ~halts tm c0 for this string directly and does not use TM113.eqv.
• Template: the proof of 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF, called the parent below. Its write-up accompanies this one as parent-proof.md and is cited as P§n, with that write-up's section numbers. The parent's own .v is 1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF.v; the .v here contains all of it, with only the changes listed in §8, so it is checked on its own. The parent is not in busycoq; TM113.tm is the parent with its states renamed. This machine, called the twin below, differs from the parent as follows (§1). Under the state renaming σ it is the parent with A0 = 1RA instead of 1RB, started on a blank tape in the parent's state B. Equivalently, it is TM113.tm with F0 = 1RF instead of 1RA.
• Status: fully formalized. The accompanying 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v (896 lines) proves Lemma nonhalt: ~halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c). It compiles in about 4 s, Print Assumptions nonhalt is closed (no axioms), and coqchk passes.
• Where each section lives in the .v: §2 tR3, tR3c (R3'), tR1, tR2; §3 the parent's model layer, unchanged: updt, updt_shape, push_ok, push0_ok, pop_ok, Life, Life_tm, Ep, Ep_tm, Life_shape, frame_step, U0–U2, ruleS, TRF, replay, ruleT, ruleX, Orb, Inv, step_lemma, main; §4 init; §5 Ep_tm2, nonhalt. §8 lists every difference from the parent's .v.

Summary. The parent is a recursive counter (P§0–§3). The tape is a stack of runs of 1s. An epoch starts and ends with the head at the left edge, and the edge frame has a budget of child creations per epoch; the machine halts exactly when that budget runs out. The parent's Theorem (P§3) says that every epoch of the marker-free top-level orbit costs exactly 2. The twin is not the parent up to state renaming or L/R mirroring. It is the parent renamed by σ⁻¹ (§1), 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 returns 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 the .v contains the parent's proofs of them unchanged. The argument is the one for TM113.tm in 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 (character 37 of the string, counting from 0).
• The twin's start state A is σ⁻¹(B). So the twin's blank start is the parent's blank tape in state B.
• No relabeling, mirrored or not, gives an exact match. Among all 720 state relabelings of the parent, each taken as is and L/R-mirrored (1,440 tables), σ⁻¹ is the unique closest to the twin, with 1 differing transition; the next closest has 5. Among relabelings that keep the start state (π(A) = A), the closest differ in 6 transitions, or 9 when mirrored.

Notation is the parent's: conf(L, R), words, tails and marker words (P§0), Ep(W) = (c, W') and the orbit O_n(M) (P§2), Inv and AL (P§3). 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 (P§1.1) and the initial segment (§4, whose first 8 steps use no A0), 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. Every other transition is the same in both machines under σ. 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.

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) ..., which is the form of tR3; tR3c is its instance at the left edge.

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. 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 ---]. The twin's macro rules, in parent names, with l and r arbitrary and all parameters >= 0:

R1   l 1^(n+2) <A 0 1^(m+1) 0 0 1^x 0 r  -->  l 1^(n+1) 0 1^(m+1) <A 0 1^(x+1) 0 0 r      3m+2x+15   (tR1)
R3'  l 0 <A 0 1^(k+1) 0 0 1^m 0 r        -->  l 1^(k+2) <A 0 1^(m+1) 0 0 r                3k+2m+15   (tR3, tR3c)
R2   l 1^(j+1) 0 1^(k+1) 0 1 <A 0 r       -->  l 1^(j+1) <A 0 1^(k+2) 0 0 r               k+10       (tR2)
R2e  0^inf 1^(k+1) 0 1 <A 0 r             -->  0^inf <A 0 1^(k+2) 0 0 r                   k+10       (tR2, l = 0^inf)
HALT 0^inf 1 <A 0 r                       -->  A1 C0 D0, then E reads 0: halt             3

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.
• 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. In the .v they are the lemmas from Life to Theorem main, identical to the parent's apart from the added Ep_tm2 (§5, §8). The TM appears only in tR1, tR2, tR3, tR3c and the conf encoding, used through push_ok, push0_ok, pop_ok, Life_tm, Ep_tm, Ep_tm2, 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 (init in the .v, by solve_init). TM113.tm 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.

5. Changed: the top-level invariant

Parent (P§4, P§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 (as in 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 the .v the case c = 2 is Ep_tm2 : Ep W 2 W' -> conf [] (2::2::W) -->+ conf [] (2::2::W'), an instance of the parent's lemmas. 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. In the .v this is nonhalt: multistep_nonhalt with init, then progress_nonhalt_cond with C i := conf [] (2 :: 2 :: snd i), step_lemma at M = [], and Ep_tm2. ∎

Zero slack. A single cost-3 top epoch would halt the twin. If Ep(W) = (3, W'), the coupling in the proof above runs unchanged until B is on top (S = []) after its second child and has to pay for a third. There the budget-3 run has B = 2 and pushes (R1), while the budget-2 run has B = 1 at depth p = 1: that is conf([1], R) = 0^inf 1 <A 0 r, the HALT pattern. 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" is enough for the parent but not here.

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. The R3' detour (F0 F0 F1 B1 A1 A0) contains no C0 [parent D0], and in the first 8 steps of §4 the C0 at step 5 is followed by D1 [parent D0 E1].

7. Trajectory twin (remark)

The twin, TM113.tm (= the parent started in state B) and the parent all pass through the same words O_n([]). The twin and TM113.tm 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 initial segment. The parent passes through conf([],[3,2]+O_n([])), whose first run is one cell longer. Checked by direct simulation to 4·10^8 steps: the left-edge returns of TM113.tm are those of the parent started in state B, and the step offsets are exactly as stated. At step 10^9 the twin has visited 133 cells (87 nonzero), TM113.tm also 133 (87), and the parent 134 (89).

8. The .v, relative to the parent's .v

The .v is the parent's .v with the head state <{{A}} written <{{F}}, and with these differences: 1. Definition tm := Eval compute in (TM_from_str "1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB"). 2. tR3 and tR3c have the parent's statements and proofs and state R3' (§2): tR3 closes by plain es, and tR3c by es after rewrite (const_unfold _ S0) at 1, as in the parent's .v. Here es also runs the 4 extra steps of the detour. 3. 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. It sits right after Life_shape. 4. Lemma init : c0 -->* conf [] [2; 2; 1]. (48 steps, solve_init). 5. nonhalt uses C i := conf [] (2 :: 2 :: snd i) and Ep_tm2 in place of Ep_tm. The rewrite cost [] n = 2 by reflexivity is the parent's.

Everything else, from updt through main, is the parent's text. Ep_tm (the parent's value-4 edge step) is still in the file but unused.

9. Numerical checks

Checked by direct simulation of the transition tables. These checks are evidence only; the result rests on the .v alone. - Relation (§1): σ⁻¹ applied to the parent gives TM113.tm exactly, and the twin differs from it only at F0. - Rules (§2): R1, R2 and R2e on 500 random instances each, and R3' on 500 instances with 0^inf on the left and 500 with a random left side (k, m in 0..25, random r), match exactly in tape, head, state and step count. Under σ each uses the parent's transition sequence, except that R3' has A0 A0 A1 C1 B1 B0 [twin F0 F0 F1 B1 A1 A0] where R3 has A0 B0. A0 [twin F0] occurs in no instance of R1, R2, R2e or HALT. HALT halts after 3 steps, reading D0 [parent E0], in all 40 instances. - Initial segment (§4): the tapes at steps 8, 23, 38 and 48 are as listed, and the head is in A [twin F] exactly at steps 8, 9, 10 (the R3' detour), 23, 38 and 48. - Run model (§3): the model equals the twin at every macro step for 40,000 macro steps from step 48. - Left-edge returns (§3, §5): every step up to 4·10^8 was scanned for configurations in state F [parent A] with every cell at or left of the head blank. There are 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 at the step the model predicts with R3' costing 3k+2m+15 steps. With R3's 3k+2m+11 the predicted steps differ, so the scan distinguishes R3' from R3. 11 of these returns were re-checked with a second, independent simulator. - Budget-2 edge lemma (§5): it holds in all 398 tested cases with c <= 2 (the top orbit, marker orbits and arbitrary words). In all 88 tested cases with c = 3, the budget-2 run halts. - Top level (§5): along O_n([]) for n <= 37, every epoch costs 2 and Inv holds. - Undefined transition (§6): in the first 2·10^6 steps from blank, D [parent E] is entered 100,132 times, always from C0 and always reading 1.

Gaps: none. The delta changes no case split of RM, and it uses no property of the Theorem beyond the exact costs at M = [], which step_lemma provides.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic); corrections from an independent audit by GPT-6 Astra (OpenAI).