1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---: never halts

• Machine: 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---, viewer https://bbchallenge.org/1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---
• 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, with no equivalence lemma to another machine.
• Template: the proof of 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, that is, its .v and the write-up for 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, which accompanies this one. This text cites that write-up as P§n, with its own section numbers. That proof is not a busycoq module; its loose template is verify/SBCv6.v, Module TM21.
• How this machine differs: its table is that machine's table with the states renamed by σ = (A C)(B D), with no mirror (§0). Every transition corresponds. What differs is the start: from the blank tape, this machine runs that machine from state C instead of A.
• Status: formalized in the accompanying .v, verify/Skelet1LikeC2_1RB1RF.v (1,308 lines). It proves Lemma nonhalt : ~ halts tm c0. in Coq 8.20.1 against unmodified busycoq BB6 (commit 0940bb9c) and imports only Individual62 from busycoq. Print Assumptions nonhalt: Closed under the global context. coqchk passes. It compiles in about 70 s.
• Where each section lives in the .v:
  • §0: tm.
  • §1: K (head state C), RP, RT; the 14 sweep lemmas Start, PassR, Borrow, PassL, EndPh, EndT, EndLastT, MergeB, MergeE, OvT, OvL, OvEnd, X1Sw, X2T; the list-sweep lemmas PassesR, PassesL, OvPasses; the macro rules Dec, DecMerge, DecMergeTail, DecMergeEmpty, EndR (End), EndLast, X2, Ov, X1.
  • §2: init0 (K0′), base and init (B′), J_base.
  • §3: J, Jstep, nonhalt.
  • §5 lists every difference from the .v for 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.

Summary. Write M for this machine and M_P for 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---. - M is M_P with its states renamed by σ = (A C)(B D). M starts in A = σ(C), so M from the blank tape is M_P run from 0^inf C> 0^inf. That is a different orbit of the same macro map. - Everything in P§1–P§3 that is about the macro map carries over unchanged (§1): the family K (now with head state C), the nine rules, the outside cases, the counter lemmas, the invariant INV+(e) and the period theorem. - Only the initial segment and the base E-start change (§2, in place of P§3.7). The base differs from M_P's in one number: the far q is 26, not 24. INV+(e) holds there, so no clause of the invariant changes. - The two orbits are coupled: at every macro step, M's K and M_P's K_P have the same parameters except that M's far block is 2 longer, and both apply the same rule (§4). This explains why nothing else changes, but the proof does not use it. - The .v is the .v for M_P with three changes: the state names in the statements of its 14 sweep lemmas, of its list-sweep lemmas PassesR, PassesL and OvPasses, and of K are renamed by σ, the TM string is M's, and the start (init0, base) is new. Every proof script is unchanged (§5).

0. The map

σ: A↦C, B↦D, C↦A, D↦B, E↦E, F↦F. It is an involution. M's row σ(s) equals M_P's row s with every target state t replaced by σ(t). For example, M_P's A1 = 0LD becomes 0Lσ(D) = 0LB, which is M's C1. Symbols and directions are unchanged.

Lemma R (relabelling). For a configuration c, let σc be c with its head state renamed by σ; the tape and the head position stay the same. Then c → c′ in M_P if and only if σc → σc′ in M, and c is halted exactly when σc is. So every M_P run c →ⁿ c′ gives an M run σc →ⁿ σc′ of the same length, and conversely.

Proof. The transition of M in state σ(s) reading b is M_P's transition in state s reading b, with its target state renamed by σ, and F is undefined on 1 in both. ∎

Start. M's c0 is 0^inf A> 0^inf = σ(0^inf C> 0^inf). M_P's own run starts in A, and after two steps (A0 = 1RB, B0 = 1RC) it is at 0^inf 1 1 C> 0^inf. So M's run is M_P run from 0^inf C> 0^inf: M_P's run without the two 1s that its first two steps write. It is not M_P's run.

Halting cell. In M, only A1 enters F, and only D0 enters A. So M halts exactly when it reaches D> 0 1 1, which is σ of M_P's B> 0 1 1.

1. What carries over unchanged

Throughout, K(h; P; T) denotes M's family 0^inf <C (10)^h 11001 [p_1,q_1,d_1] … [p_L,q_L,d_L] T 0^inf. It is σ applied to M_P's family of P§1, which has head state A and is written K_P(h; P; T) here: K(h; P; T) = σK_P(h; P; T), the same words with head state C.

The rules in busycoq comment style, for M. Here Z := pairs 1..k−1, all with d = 0 and q ≥ 2, and touch (p,q,d) := (p+1, q−1, 1−d):

1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---       (= sigma of 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, sigma = (A C)(B D))

[p,q,d] := (10)^p (01)^q s(d),  s(1) = 0001, s(0) = 0010
K(h; P; T) := 0^inf <C (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 -->(1,088) K(2; (11,13,0); -) -->(78,026) K(2; (95,68,0),(34,33,1),(10,15,1),(1,26,1); -)

2. What changes: initial segment and base (in place of P§3.7)

The following is direct simulation of M from the blank tape (§6). A canonical configuration is state C on a new leftmost cell, with the tape to its right parsing as a K.

As for M_P, 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,534 of 1,534 up to step 3·10⁷. - Re-pairings (Ov/X1) happen at steps 2,009, 4,822, 8,579, 19,744, 34,493 and 79,114. - M_P's happen at steps 1,845, 4,610, 8,319, 19,436, 34,137 and 78,710.

The base is the E-start right after re-pairing 6:

B' = K(2; (95,68,0), (34,33,1), (10,15,1), (1,26,1); -)      at step 79,114
B  = K_P(2; (95,68,0), (34,33,1), (10,15,1), (1,24,1); -)    M_P's base, at step 78,710

INV+(e) at B′, clause by clause, as stated in P§3.8.1 (L = L* = 4, regular start, θ = 5): - (a) h = 2, every block ≥ 1, p_1 = 95 ≥ 7; T = −, digits (0,1,1,1), far pair (p_4, q_4) = (1, 26) with p_4 ≥ 1 and q_4 ≥ 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 and p_2 = 34 ≥ 16.

Only clause (a) reads q_4, and only as the lower bound q_4 ≥ 6. Every other number is M_P's.

3. The argument (complete)

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

1. Initial segment. M runs from c0 to B′ in exactly 79,114 steps without halting. This is a finite exact computation (§2); in the .v it is init, one esx.
2. Base. INV+(e)(B′) holds (§2).
3. Transfer. The period theorem (statement 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_P(h; P; T) →⁺ K_P(h′; P′; T′) of M_P is an M run K(h; P; T) →⁺ K(h′; P′; T′) of the same length, since K = σK_P. So the theorem holds verbatim for M's configurations K(h; P; T).
4. Conclusion. By induction from B′, M's run is an infinite chain of rule applications, each taking at least one step, so it never halts. This is the reduction of P§3.1 with K0 and B replaced by K0′ and B′. A rule application never presents the halting cell D> 0 1 1, because each rule is an exact computation from one K to the next. ∎

The argument for M_P depends on M_P's own orbit only through its initial segment and base (P§3.7, and the base values quoted in P§3.3 and P§3.8.1); here §2 replaces them. The orbit statistics in P§3.3 and P§5 (r values, merge counts, X1 count) are evidence, not premises.

4. How M's orbit relates to M_P's (explanation, not a premise)

Observation. From the first canonical configuration on, the canonical configurations of M and of M_P correspond one to one. At each of them, M's K and M_P's K_P have the same parameters except that exactly one exponent of M's is larger by 2, and from K0′ on the two orbits apply the same rule at every macro step. The larger exponent is always in the far block:

Each cycle has the same rule sequence and the same number of decrements in both orbits (§6 gives the range checked).

Lemma C (a corollary of P§3.4). - Take an E-start X = K_P(h; P; T) of M_P that satisfies INV+(e), and let X⁺ be X with q_L (or k, at a T2 start) raised by 2. Then the cycle pair from X⁺ applies the same rules as the one from X, and it ends at M_P's next E-start after X with q_L raised by 2. - In the E-cycle, the far pair (or the pair X2 appends, whose q is k) gets exactly two touches (P§3.4 S1: q_L ≥ 6, or k ≥ 4, and it loses 2). Its q is at least 3 at each touch from X, so also from X⁺. The only branch either touch reads is "q = 1 or q ≥ 2": the borrow touch is a Dec (not DecMergeTail or DecMergeEmpty), and at V = 0 the rule is End (not EndLast or X1). The Ov then copies q_L into the new last pair's p. - In the L-slot, that p (t₀) is never compared. It enters only additively, with coefficient 1, in these places: - EndLast's t = p + 4; - the fused p of a DecMerge at M−1; - X1's T2 parameter; - DecMergeTail's t. - t and k likewise enter only additively: Ov's last-pair q = t + 1, and X2's new q = k. - So the +2 never changes a branch, and it never reaches an interior pair. This is why INV+(e) needs no change.

This also accounts for the small size difference at 10⁹ steps (§6). M lags M_P by a slowly growing number of steps: 132 steps at K0′ and 404 at the base, because every sweep over the far block is 4 cells longer. So the trajectories are not identical, but they are coupled exactly.

5. The .v file, and how it differs from the .v for M_P

The .v is the .v for M_P (1,303 lines) with the following changes. Outside comments, there are no others. 1. TM_from_str "1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---". 2. The state names in the statements of the 14 sweep lemmas, of the list-sweep lemmas PassesR, PassesL and OvPasses, and of K are renamed by σ, simultaneously: - {{A}} → {{C}}: 4 occurrences (3 in the sweep lemmas, 1 in K); - {{B}} → {{D}}: 12 (10 in the sweep lemmas, 2 in PassesR); - {{D}} → {{B}}: 19 (15 in the sweep lemmas, 2 in PassesL, 2 in OvPasses).

M_P's .v never names C, E or F. Every es proof is M_P's text, unchanged: by Lemma R, the symbolic run on M's table is M_P's run with the states renamed. The induction proofs of PassesR, PassesL and OvPasses are M_P's text too; they only chain PassR, PassL and OvL. 3. init0 : c0 -->* K 2 [(11,13,false)] TN (1,088 steps); base with last pair (1%nat, 26%nat, true); init : c0 -->* K 2 base TN by one esx (79,114 steps). 4. J_base keeps M_P's script (cbn …; repeat split; lia). At B′ only two clauses of J read q_4: 1 <= q and the E1 clause at n = 0, q >= tv + 2 ^ 0 + 1 = 3 (tv = d_4 = 1). 26 satisfies both. 5. J, Jstep, every ob_* and inv_* lemma, and nonhalt are M_P's text, unchanged.

The comments (the header, the closing rule-table comment, and the comments with step counts) describe M.

Like the .v for M_P, this .v does not prove the period theorem as one lemma. It proves the per-step invariant J described in P§4, which contains INV+(e) in projected form at E-starts. Lemma R is not used in the .v either: each sweep lemma is proved by es on M's own table, and Lemma R explains why the same proof scripts close. The result rests on the .v alone; the prose here and in P§3 explains it.

6. Numerical sanity checks

These checks are independent of the .v. "Simulation" means direct simulation of the transition table. - σ is the only one of the 720 state renamings, each with and without mirroring, that maps M_P's table to M's. It is an involution. - M from the blank tape and M_P from 0^inf C> 0^inf, relabelled by σ, agree at every step for 2·10⁶ steps. M_P from the blank tape is at 0^inf 1 1 C> 0^inf after 2 steps. - Each of the nine rules of §1 was simulated on M's own table, with head state C, on 45 random instances (405 in all). Every instance reaches the predicted K exactly. The halting cell is D> 0 1 1. - From the blank tape, simulation gives: - the canonical configurations of §2 at steps 20, 359, 551 and 1,088; - up to step 3·10⁷, 1,534 of 1,534 canonical transitions after K0′ predicted by the rules; - B′ at step 79,114. - INV+(e) holds at B′ clause by clause. The clauses of J evaluate to true at B′, and also at M_P's base B. B′ and B differ only in q_4. - On M's orbit from B′ to L* > 300 there are 542 cycle pairs, with 245 L-slot merges and x = 3, 4 and 5 all occurring. On it: - every equality and inequality of P§3.8 holds at every cycle pair, and every clause of INV+(e) holds at every cycle; - J holds at every macro step from B′ for 34 re-pairings; - to L = 600 (1,102 cycle pairs, 2,209 re-pairings, 3 X1), every equality and inequality of P§3.8 and every clause of INV+(e) still hold. - The coupling of §4 (one exponent larger by 2, in the far block, same rules) holds: - at every macro step to L = 16 (539,656 steps); - at every re-pairing to L = 300 (1,089 re-pairings, including 3 X1/X2 detours); - at every re-pairing to L = 600 (2,209 re-pairings). - At 10⁹ steps, M's tape spans 67,347 cells (−67,163..183), with 33,668 nonzero cells. M_P's spans 67,343 cells, with 33,665 nonzero cells. - The start-independent checks of P§5 (exhaustive small starts, random chains, the far-end table of P§3.4) test only the abstract macro map, so they apply to M unchanged.

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