1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD---: never halts

This machine is a renamed copy of the machine 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---, whose proof accompanies this one. Swapping two pairs of state names turns one transition table into the other, and every transition matches.

The two machines differ only in where they start. Started on a blank tape, this machine does exactly what the other machine does when that one is started in a different state. So the two runs are different runs of the same macro rules (each rule is an exact run of the machine from one configuration of a fixed shape to the next).

The proof for the other machine therefore applies with one part replaced: the finite warm-up. This machine takes 79,114 steps to reach the configuration where the invariant argument begins. From there on, its run is an endless chain of the same macro rules, each taking at least one step, so it never halts.

Machine, template and status

• 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 it imports only Individual62 from busycoq.
• Print Assumptions nonhalt: Closed under the global context. coqchk passes.
• It compiles in about 70 s.
• §5 shows where each section lives in the .v, and lists every difference from the .v for 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.

Notation

• M is this machine, and M_P is 1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---.
• P§n is section n of the write-up for M_P.
• σ = (A C)(B D) is the renaming of states that turns M_P's table into M's (§0).
• K(h; P; T) is M's family of configurations, and K_P(h; P; T) is M_P's. Both are defined in §1.
• The terms of M_P's argument keep their meanings:
• the domain D (P§3.1);
• re-pairings, cycles, E-cycles, L-slots and their starts (E-starts, L-starts), the far pair and L* (P§3.3);
• the invariant INV+(e) (P§3.3, stated in full in P§3.8.1);
• cycle pairs (P§3.4) and the period theorem (statement P§3.8.1).

Summary

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). That covers 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 (§4). 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. This explains why nothing else changes, but the proof does not use it.

The .v is the .v for M_P with three changes (§5). Every proof script is unchanged.

• 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.
• The start (init0, base) is new.

0. The map

The renaming σ

σ:   A ↦ C,   B ↦ D,   C ↦ A,   D ↦ B,   E ↦ E,   F ↦ F

σ is an involution. M's row σ(s) equals M_P's row s with every target state t replaced by σ(t). Symbols and directions are unchanged.

For example, M_P's A1 = 0LD becomes 0Lσ(D) = 0LB, which is M's C1.

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
c is halted        exactly when        σc is halted

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 σ. F is undefined on 1 in both. ∎

Start

M's c0 is σ of M_P's configuration 0^inf C> 0^inf:

c0  =  0^inf A> 0^inf  =  σ(0^inf C> 0^inf)

M_P's own run starts in A. 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

This is σ of M_P's B> 0 1 1.

1. What carries over unchanged

The family K

Throughout, K(h; P; T) denotes M's family. It uses the pair blocks [p,q,d] and the tails T of P§1:

[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 { -,  T1(t) := (10)^t 1,  T2(k) := (101)^2 (01)^k }
V := sum_j d_j 2^(j-1)

P is the list of pairs (p_j, q_j, d_j), and L is its length. V is the counter of P§1, spelled by the digits d_j.

K is σ applied to M_P's family of P§1. That family has head state A, and it is written K_P(h; P; T) here:

K(h; P; T) = σK_P(h; P; T)        (the same words, with head state C)

What carries over

The rules, for M

The rules below are in busycoq comment style. They use two abbreviations:

Z              := pairs 1..k-1, all with d = 0 and q >= 2
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.

Initial segment

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.

Base

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 (with L = L* = 4, a regular start and θ = 5):

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 that from an E-start satisfying INV+(e):

• every K up to the next E-start is in D;
• INV+(e) holds again there;
• 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 of M_P is an M run of the same length, since K = σK_P:

M_P: K_P(h; P; T) →⁺ K_P(h′; P′; T′) M: K(h; P; T) →⁺ K(h′; P′; T′) (same length)

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. ∎

What the argument uses from M_P's orbit

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. 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)

Statement. 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);
• 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
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.

Step lag and tape size

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

Where each section lives in the .v

The changes

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. The start:

• 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;
• 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.

Side by side

What the .v proves, and what the prose is for

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.

The renaming

• σ 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.

The rules

• 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.

The start and the base

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.

The orbit from B′

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 (x as in P§3.4). 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).

Tape size at 10⁹ steps

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.

Checks of the abstract map

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).