1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---: never halts

• Machine: 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---, viewer https://bbchallenge.org/1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---
• Holdout: on the current BB(6) holdout list. Class: "Skelet 1-like Class 2".
• Written for: the string itself. The .v proves nonhalt for this string directly; it applies no mirror or state renaming.
• Parent: 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, which never halts by its own accompanying write-up and .v. This machine has the parent's table with the states renamed by ρ (A↦D, B↦A, C↦B, D↦C; E and F fixed; no mirror), and it starts in the parent's state B (§0). This is a delta write-up. P§n means §n of the write-up for 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, and every section number cited that way is that write-up's own.
• Template: none in busycoq for this table. The parent's loose busycoq template is verify/SBCv6.v, Module TM21 (P§4). Up to comments, the .v here is the parent's .v with ρ applied to the state names and three changed lines: the TM string, init0 and base (§5).
• Status: formalized in the accompanying .v, verify/Skelet1LikeC2_1RB0RD.v (1,309 lines). It proves Lemma nonhalt : ~ halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c), importing Individual62 from busycoq. It compiles in about 52 s with -native-compiler yes. Print Assumptions nonhalt is closed, and coqchk passes.
• Where each section lives in the .v:
  • §1 family and rules: K, RP, RT, Tl; the 14 sweep lemmas Start, PassR, Borrow, PassL, EndPh, EndT, EndLastT, MergeB, MergeE, OvT, OvL, OvEnd, X1Sw, X2T (each a plain es on this machine's table); the list sweeps PassesR, PassesL, OvPasses; the macro rules Dec, DecMerge, DecMergeTail, DecMergeEmpty, EndR, EndLast, X2, Ov, X1.
  • §2 initial segment and base: init0 (K0′, 402 steps), base and init (B′, 38,732 steps), J_base.
  • §3 argument: the invariant J with PN, PI, PC, TC; Jstep; nonhalt.

Summary. The parent's table, run from the parent's state B instead of A, is the same machine run on a different orbit of the same macro map. - What carries over. Everything in the parent's proof that does not mention the start carries over by renaming: the family K, the nine macro rules, the outside cases, the invariant INV+(e) and its period theorem (P§3.8), and the per-step invariant J of the parent's .v with its preservation lemma Jstep. - What changes. Only the initial segment and the base. The machine reaches K0′ = K(2; (7,4,0); −) at step 402, and the base E-start B′ = K(2; (47,32,0),(40,33,1),(13,34,1); −) at step 38,732. - The invariant is unchanged. B′ has L* = 3, the smallest value INV+(e) allows, and every clause of INV+(e) and of J holds there. The parent's theorem covers L* = 3 (§3). - A different orbit. This orbit is not a shifted copy of the parent's: its base differs in every number but h, and it has 3 pairs where the parent's base has 4 (§4).

0. The map

ρ: A↦D, B↦A, C↦B, D↦C, E↦E, F↦F. It is the 4-cycle (A D C B), and ρ⁻¹ = (A B C D). - Row ρ(s) of this machine is row s of the parent with every target state t replaced by ρ(t). Symbols and directions are unchanged. For example, parent A1 = 0LD becomes 0Lρ(D) = 0LC, which is D1 here. - Among all 720 state renamings, each with and without mirroring, ρ is the only one that maps the parent's table to this one.

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 this machine, and c is halted exactly when ρc is. So every parent run c →ⁿ c′ gives a run ρc →ⁿ ρc′ of this machine of the same length, and the converse also holds.

Start. This machine's c0 is 0^inf A> 0^inf = ρ(0^inf B> 0^inf). - The parent's own run starts in A. After one step (A0 = 1RB) it is at 0^inf 1 B> 0^inf. - So this machine's run is the parent machine run from 0^inf B> 0^inf: the parent's run without the 1 its first step writes. It is not the parent's run.

Halting cell. Only B1 (1RF) enters F, and only A0 (1RB) enters B. So the machine halts exactly when it reaches A> 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 this machine (Z := pairs 1..k−1, all d = 0, q ≥ 2; touch (p,q,d) := (p+1, q−1, 1−d)):

1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---       (= rho of 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---,
                                                  rho: A->D, B->A, C->B, D->C, E, F fixed)

[p,q,d] := (10)^p (01)^q s(d),  s(1) = 0001, s(0) = 0010
K(h; P; T) := 0^inf <D (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 q [] t = [(q,t+1,1)],    ovp q ((p',q',_) :: Y) t = (q,p',1) :: ovp q' Y t,
                ovpX q [] pa = [(q,pa,0)],   ovpX q ((p',q',_) :: Y) pa = (q,p',1) :: ovpX q' Y pa)

start: c0 -->(402) K(2; (7,4,0); -) -->(38,330) K(2; (47,32,0),(40,33,1),(13,34,1); -)

2. What changes: initial segment and base (replaces P§3.7)

These are facts of direct simulation of this machine from the blank tape. A canonical configuration is state D 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,607 of 1,607 to step 3·10⁷; - 5,323 of 5,323 to step 3·10⁸ (Dec 5,266, Ov 26, End 13, EndLast 13, DecMerge 3, DecMergeTail 2).

Re-pairings (Ov/X1) happen at steps 1,083, 3,520, 6,965, 17,738, 23,871 and 38,732. The parent's are at 1,845, 4,610, 8,319, 19,436, 34,137 and 78,710. As in the parent, the E-starts are the configurations after even re-pairings.

The E-starts after re-pairings 2 and 4 cannot be the base, because both have L* = 2 and INV(d) needs L* ≥ 3: - after re-pairing 2 (step 3,520): K(2; (23,14,0),(3,9,1); −), which also fails (e2); - after re-pairing 4 (step 17,738): K(2; (47,32,0),(16,30,1); −).

The .v invariant J fails there too, since PI for pair 1 needs n = L − 1 ≥ 2. The base is the E-start after re-pairing 6:

B' = K(2; (47,32,0), (40,33,1), (13,34,1); -)                at step 38,732   (L = L* = 3)
B  = K(2; (95,68,0), (34,33,1), (10,15,1), (1,24,1); -)      the parent's base, at step 78,710   (L* = 4)

INV+(e) at B′, clause by clause, as stated in P§3.8.1. Here L = L* = 3, it is a regular start, θ = 5, e_1 = 2 and e_2 = 1. The interior pairs are j = 1, 2: - (a) h = 2, every block ≥ 1, p_1 = 47 ≥ 7; T = −, digits (0,1,1), far pair (p_3, q_3) = (13, 34) with p_3 ≥ 1 and q_3 ≥ 6; - (b) q_1 + 1 = 33 ≥ 5·2² = 20, q_2 = 33 ≥ 5·2 = 10 (r_1 = 8.25, r_2 = 16.5); - (c) p_1 + d_1 = 47, p_2 + d_2 = 41, both odd; - (d) L* = 3 ≥ 3, with equality; - (e) p_1 + 1 = 48 ≥ 2⁵ = 32 and p_2 = 40 ≥ 2³ = 8.

p_1 = 47 = 3·2^(L*+1) − 1. This is the bound the parent's argument gives for p_1 at every regular start (P§3.8.1, P§3.8.4 (e1)), attained here. The parent's base attains it too, with 95 at L* = 4.

J at B′, J (mkst 2 base TN E1 false): P ≠ [], TC E1 false TN, and PC E1 for every pair (the parent's Definitions PN, PI, PC, P§4). Write n for the number of pairs to the right, tv for the digit value from the pair up, and w = 2^n:

All clauses hold; J_base closes them by lia. The tight clause is tight at every regular start: h = 2, tv = 2^L − 2 and w = 2^(L−1) give exactly 12w.

The next E-start, K(2; (95,68,0),(34,33,1),(34,33,1),(10,38,1); −) after re-pairing 8 (step 104,510), has L* = 4, and INV+(e) and J hold there as well. B′ is the earliest E-start where they hold.

3. The argument (complete)

Theorem. 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA--- does not halt from the blank tape.

1. Initial segment. The machine runs from c0 to B′ in exactly 38,732 steps without halting. This is a finite exact computation; in Rocq it is one esx (init).
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 run ρK →⁺ ρK′ of this machine of the same length. - So the theorem holds verbatim for this machine's configurations ρK.
4. Conclusion. By induction from B′, the 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 and B replaced by K0′ and B′. - A rule application never presents the halting cell A> 0 1 1, because each rule is an exact computation from one K to the next. ∎

L* = 3 is inside the theorem's scope. The theorem assumes INV+(e), whose clause (d) is L* ≥ 3, so B′ meets it with equality. The proof uses the size of L* in three places, and each holds at L* = 3: - P§3.8.4 Step 2 and (d): M = L* + 1 ≥ 4 pairs at the L-start, so pairs 1 and 2, the x-pair and the last pair are distinct; - P§3.8.3: the pair-1 and pair-2 budgets need L* ≥ 2; - P§3.8.4 (e2): needs L* ≥ 2.

Nothing in P§3.4–3.5 or P§3.8 assumes L* ≥ 4. The case L* = 3 was also checked numerically, for the parent's abstract map and for starts near B′ (§6). In Rocq, Jstep is proved for every J state, and B′ satisfies J (§2).

Beyond the initial segment and the base (P§3.7, and the base checks in P§3.3 and P§3.8.1), nothing in the parent's argument depends on the parent's orbit. The orbit-specific numbers quoted in the parent's write-up (r values, merge counts, X1 counts) are not premises.

4. How this orbit relates to the parent's (explanation, not a premise)

No coupling. Two other holdout machines have the same table up to renaming and mirroring: 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD--- (the table started in the parent's C) and 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC--- (mirrored, started in the parent's D). At every macro step their K is the parent's K with one far exponent larger, by +2 and +1 respectively. This machine has no such coupling: - B′ differs from B everywhere but h. It has one pair fewer, and every block differs. - The E-start sequences never meet. Among the first 120 E-starts of each orbit, counted from each base, none is shared. A shifted copy of the parent's orbit would share all but finitely many. - The next E-start is the parent's base reshaped. The E-start after B′ is K(2; (95,68,0),(34,33,1),(34,33,1),(10,38,1); −): the parent's base with an extra (34,33,1) pair and a different far pair. - L* runs one behind, then catches up. This machine's L* at the n-th E-start trails the parent's by one for a while (E-start 10: 9 vs 10; 20: 15 vs 16), and later the two agree (E-start 119: both 73). - The tape is wider. At 10⁹ steps this machine's tape spans 79,454 cells (−79,241..212), with 39,718 nonzeros. The parent's spans 67,343 cells, with 33,665 nonzeros, so this tape is 18% wider.

Same macro map, same behaviour. On its own orbit to L* > 600, this machine shows the parent's pattern: - 1,102 cycle pairs, 1 X1 slot (x ∈ {3, 4, 5} all seen) and 504 L-slot merges (494 interior Ep run-outs); - INV(b) margins comparable to the parent's: the minimum interior r is 8.25 at regular E-starts and just under 8 after the X1 slot (thresholds 5 and 4). On the parent's orbit the minima are 7.5 and 7.906.

5. The .v file

The .v is the parent's .v with the following changes, and no others: 1. tm is TM_from_str "1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---". 2. The state names are renamed by ρ simultaneously wherever the parent's .v names a state: in the statements of the 14 sweep lemmas (28 occurrences), of the list sweeps PassesR, PassesL and OvPasses (2 each, 6 in all) and of K (1): - the parent's {{A}} (4 occurrences), {{B}} (12) and {{D}} (19) become {{D}}, {{A}} and {{C}}; - the parent's .v names no other state (no {{C}}, {{E}} or {{F}}), so this .v has {{D}} 4 times, {{A}} 12 times and {{C}} 19 times, and no {{B}}, {{E}} or {{F}}; - the proof scripts are the parent's, verbatim: a plain es for each sweep lemma, and induction over the list for PassesR, PassesL and OvPasses. The es scripts re-close because ρ maps each transition of the parent to a transition of this machine (Lemma R). 3. The start: - init0 : c0 -->* K 2 [(7,4,false)] TN (402 steps; not used by nonhalt); - base := [(47,32,false); (40,33,true); (13,34,true)], a 3-element list; - init : c0 -->* K 2 base TN by one esx over 38,732 steps. 4. J_base uses the parent's script (cbn … repeat split; lia). Every clause is a closed arithmetic fact at B′ (§2). The tight one, h + 4(tv + w) + 6 = 48 ≥ 12w = 48, is closed by lia exactly as in the parent. 5. The comments: the header, the start, and the closing rule table (TM line, <D in K, start line).

Everything from Require Import ZifyNat to Lemma nonhalt (J, Jstep, every ob_* and inv_* lemma, and nonhalt) is byte-identical to the parent's .v. Where each item lives:

Like the parent's .v, this file proves the parent's per-step invariant J (P§4), not the period theorem. J contains INV+(e) in projected form at E-starts, and Jstep is proved for every J state, so the L* = 3 base needs no special case. Lemma R is not a premise of the formal proof either: every rule is re-proved on this machine's own table by es, and Lemma R explains why those proofs re-close. So the result rests on the .v alone. The prose here and in P§3 is the explanation.

6. Numerical checks

• Renaming. Among the 720 state renamings, each with and without mirroring, only ρ maps the parent's table to this one.
• Lockstep. This machine from the blank tape and the parent from 0^inf B> 0^inf, relabelled by ρ, agree at every step for 2·10⁶ steps.
• Rules. Each of the nine rules was simulated on this machine's table with head state D, on 45 random instances each: 405 of 405 give exactly the predicted K. The halting cell is A> 0 1 1.
• Initial segment. From the blank tape, step 121 is K(2; −; T1(4)) with L = 0, and step 402 is K0′ = K(2; (7,4,0); −).
• Rule-predicted run. Checked by direct simulation: from K0′, 1,607 of 1,607 canonical transitions to 3·10⁷ steps, and 5,323 of 5,323 to 3·10⁸ steps, are the ones the rules predict. B′ is the configuration at step 38,732, after re-pairing 6.
• Base. Every clause of INV+(e) and of J holds at B′ (and at the parent's base B). The E-starts after re-pairings 2 and 4 fail (d) and J.
• Orbit, abstract map.
• From B′ to L* > 300: every lemma of P§3.8 holds at every step of 537 cycle pairs (239 L-slot merges, x ∈ {3, 4, 5} all seen), and every INV clause holds at every cycle.
• From B′ to L* > 600: the same checks hold over 1,102 cycle pairs (2,205 re-pairings, 1 X1 slot).
• J holds at every macro step over 34 re-pairings (125,503 Dec steps).
• L* = 3 near B′. 5,000 random regular starts with L* = 3 that satisfy INV+(e), with values up to about twice those of B′, were each followed for one cycle pair, with every clause checked at every step. All pass; the next L* is 3 in 403 cases and 4 in 4,597.
• Parent's abstract map. The checks that do not depend on the start apply unchanged: every lemma of P§3.8 on 1,027,584 exhaustive small starts with L* = 3 and 4 (regular and T2 starts, values at or just above the thresholds), on random chains of cycle pairs starting at L* = 3..40, and the far-end table of P§3.4 for x = 1..15.

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