1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---: never halts

• Machine: 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---, viewer https://bbchallenge.org/1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---
• Holdout: on the current BB(6) holdout list.
• Written for: the string itself. This is a delta write-up against the write-up for 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---. Below, the parent is that machine, the twin is this one, and "parent §n" is section n of the parent's write-up. The twin's table is the parent's table mirrored (every L↔R) with its states renamed by φ: A↦D, B↦A, C↦B, D↦C, E↦E, F↦F (§0). So the twin from the blank tape is the parent started from 0^inf D> 0^inf instead of 0^inf A> 0^inf.
• Template: the parent's .v, whose development (family, sweep and macro lemmas, invariant J, Jstep) is reused verbatim for the parent's table; the parent's own loose template is verify/SBCv6.v Module TM21 (parent §4). The mirror and the renaming use busycoq's verify/Flip.v (flip, flip_halts) and verify/Permute.v (Perm, perm_halts). Relative to the parent's .v, only the initial segment, one number of the base E-start (the far pair's q: 25 instead of 24) and the final transfer to the twin differ.
• Status: formalized in the accompanying verify/Skelet1LikeC2_1RB0RE.v (1,364 lines), which proves Lemma nonhalt : ~ halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c). Print Assumptions nonhalt reports Closed under the global context. It compiles in about 40 s with -native-compiler yes, and coqchk accepts it.
• Where each section lives in the .v: §0 Lemma C phi, perm_twin, and busycoq's flip_halts and perm_halts inside nonhalt; §1 sd, RP, Tl, RT, K; §2 the 14 sweep lemmas (Start … X2T), PassesR, PassesL, OvPasses and the macro lemmas Dec, DecMerge, DecMergeTail, DecMergeEmpty, EndR, EndLast, X2, Ov, X1; §3 (parent §3.1–3.8) J, Jstep; §3.7 solve_initD, init0, base, init, J_base; conclusion nonhalt_D, nonhalt.

Summary. The parent is a binary down-counter (parent §1–§2). Its configurations are K(h; P; T): a marker (10)^h 11001, then a list of pair blocks (10)^p (01)^q s(d) whose digits d form a binary number V, then a tail T. Each macro step decrements V by touching the pairs up to the borrow; a block that runs out merges with its neighbour; once V reaches 0, an End step and an overflow (Ov, or the X1/X2 detour) re-pair the list. The parent's proof is an invariant INV+(e) at E-starts (parent §3.8.1) that one cycle pair preserves (the Theorem (cycle pair), parent §3.8), formalized as a per-step invariant J (Jstep). The twin's table is the parent's, mirrored and renamed (§0), so the twin from the blank tape runs exactly as the parent from 0^inf D> 0^inf, on the mirror-image tape (Lemma C). That run is a different orbit of the same macro map. From K0′ = K(2; (11,12,0); −) at step 1,021 on, every macro step is one of the rules, and the run reaches the E-start K(2; (95,68,0),(34,33,1),(10,15,1),(1,25,1); −) at step 78,911. This is the parent's base except for the far pair's q (25 instead of 24), and it satisfies INV+(e) and J with the parent's constants. So the parent's rules, invariant and Theorem apply unchanged, and only the initial segment and the base are new (§3.7).

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. Among all 2 × 720 candidates (720 renamings, with or without the mirror) this is the only one that fits; in particular no renaming without the mirror 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 the parent's 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 (parent §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 parent §1, §3.2 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 parent §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, 405 random rule instances (45 per rule, all h mod 4, sizes 2–300), run on the twin's own table from mirrored words, reach the predicted K′ exactly (§5).

3. Argument: what changes

3.1–3.6 and 3.8: unchanged

Parent §3.1–3.6 and §3.8 use only the rules of §2 and the invariant INV+(e) at an E-start. They never use the orbit from the blank tape; parent §3.1's reduction is applied here from K0′, and in the .v from the base (§3.7). In particular, the parent's Theorem (cycle pair) (parent §3.8.1) is a statement about every E-start K that satisfies INV+(e): every configuration through the next two re-pairings is in D, and INV+(e) holds again right after the second one. Its proof (parent §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 form of parent §3.8.1 (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 has the parent's proof (repeat split; lia).

Conclusion. The twin's run from the blank tape reaches the base after 78,911 steps by exact computation, so it does not halt before the base (init, through Lemma C). The base satisfies INV+(e), so by the Theorem every configuration after it is in D. The twin therefore never halts (parent §3.1, applied to K′ through Lemma C). The rules also predict every transition from K0′ to the base, so every configuration from K0′ to the base is in D as well; the formal proof does not need this, since init reaches the base by direct execution.

3.9 Why the two orbits look alike (not used in the proof)

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. This holds on the abstract orbits up to L = 120, about 2^124 macro steps (§5). 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

The .v does not mirror the parent's development. Mirroring a busycoq tape term swaps the arguments of *> and <* (and {{X}}> with <{{X}}), which is not a textual renaming. Instead the file keeps every parent lemma about the parent's table and transfers the result to the twin through Lemma C.

1. Two tables. The top-level Definition tm := TM_from_str "1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---" is the twin. tm3 := TM_from_str "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---" is the parent, and the local notations -->*/-->+ are bound to tm3. Everything up to nonhalt_D is about tm3, and apart from the start (item 2) it is the text of the parent's .v: the family K, the 14 sweep lemmas, the 9 macro rules, J and Jstep.
2. Start. init : D;; tape0 -->* K 2 base TN (78,911 steps), with base the list of §3.7 (far pair (1,25,true)), and init0 : D;; tape0 -->* K 2 [(11,12,false)] TN (K0′, 1,021 steps; nonhalt does not use it). Both are by direct execution with solve_initD. busycoq's 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, which is far too slow for 78,911 steps. solve_initD is busycoq's solve_init with its first rewrite replaced by change (D, tape0) with (cconfig_to_config (nil,nil,0,D)).
3. The parent from D. J_base : J (mkst 2 base TN E1 false) has the parent's proof. nonhalt_D : ~ halts tm3 (D;; tape0) follows from multistep_nonhalt with init and progress_nonhalt_cond with P := J and Jstep.
4. Lemma C, the direction used. busycoq already contains both halves, so no simulation lemma for μ is 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 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.

nonhalt : ~ halts tm c0 applies flip_halts, then perm_halts with perm_twin, and refutes the result with nonhalt_D.

Compared with the parent's .v, the file changes or adds only the header comment, the tm/tm3 naming, solve_initD, init0/base/init, nonhalt_D (the parent's nonhalt, restated for tm3 from 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 per-cycle Theorem. J contains INV+(e) in projected form at every E-start (parent §4). So the result rests on the .v alone, and the prose here and in parent §3 is the explanation.

5. Numerical sanity checks

None of these is used by the proof. - Map. The table identity of §0 holds for 12/12 entries, and φ with the mirror is the only fit among the 2 × 720 candidate maps; the start state A goes to D; the twin halts only at 1 1 0 <C. - Lockstep simulation. The twin from the blank tape and the parent from 0^inf D> 0^inf, simulated 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 nonzero cells each). - Rules on the twin's own table. 405/405 random instances (45 per rule, all h mod 4, sizes 2–300) reach the predicted K′ exactly. - Initial segment. Checked by direct simulation: K0′ at step 1,021; all 1,534 canonical transitions up to 3·10⁷ steps are the ones the abstract map predicts; the base is reached at step 78,911. - Base. INV+(e) holds clause by clause and J holds; the only difference from the parent's base is pair 4's q (25 vs 24). 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) (L* = 3: 33 ≥ 20, 15 ≥ 10; 47 and 17 odd; 48 ≥ 32, 16 ≥ 8) and J. - Cycle pairs on the twin's orbit. Every identity and inequality of parent §3.8 holds from the base to L* > 300: 542 cycle pairs (539 EndLast slots, 3 X1 slots), 245 L-slot merges, x = 3, 4, 5 and ≥ 6 all occur; min p_1′/(2^(L*′+2)−1) = 1.000 and min p_2′/2^(L*′) = 2.234. - Invariant J. J holds at every macro step from the base for 30 re-pairings: 80,792 Decs, including an X1/X2 detour. - Lockstep of the abstract orbits (§3.9): the same rule at every macro step and a +1 difference on one far-end block, up to L = 120. - Orbit-independent checks of the Theorem. For the parent, the Theorem was checked on 1,027,584 exhaustive small starts and 120,000 random cycle pairs (parent §5); these checks do not depend on the orbit and apply here unchanged. - Long run. Direct simulation to 10⁹ steps: the twin has not halted, has 33,665 nonzero cells and spans 67,345 cells; the parent from 0^inf A> 0^inf has 33,665 nonzero cells and spans 67,343 cells.

AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).