1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---: never halts

This machine never halts. Its transition table is the table of another machine, called the parent below, with four of its six states renamed.

The difference is where it starts: it starts in the state that corresponds to the parent's state B, not A. So it is the same machine, run on a different orbit of the same macro map.

Almost all of the parent's proof carries over by renaming. Only the initial segment of the run and the base, where the induction starts, are new.

Machine, parent and status

• 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.
• Relation to the parent: 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).
• Delta write-up: 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).
• The .v: 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 of this write-up lives in the .v is listed in §5.

Notation

This write-up uses the parent's notation. The table says where each piece is defined.

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 and the outside cases; - the invariant INV+(e) and its period theorem (P§3.8); - the per-step invariant J of the parent's .v, with its preservation lemma Jstep.

What changes

Only the initial segment and the base change. The machine reaches K0′ at step 402, and the base E-start B′ at step 38,732:

K0' = K(2; (7,4,0); -)                                at step 402
B'  = K(2; (47,32,0), (40,33,1), (13,34,1); -)        at step 38,732   (the base E-start)

The invariant is unchanged

B′ has L* = 3, the smallest value INV+(e) allows. 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

The renaming is

ρ:    A ↦ D,  B ↦ A,  C ↦ B,  D ↦ C,  E ↦ E,  F ↦ F
ρ   = (A D C B)        (a 4-cycle)
ρ⁻¹ = (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.

Relabelling

For a configuration c, let ρc be c with its head state renamed by ρ. The tape and head position stay the same.

Lemma R (relabelling).

c → c′ in the parent    if and only if    ρc → ρc′ in this machine
c is halted             exactly when      ρc is halted

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 start configuration is

c0 = 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

Each row below is an item of the parent's proof, what it becomes for this machine, and why.

The family for this machine is

K_D(h; P; T) := ρ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

The rules for this machine

The rules are below in busycoq comment style, for this machine. They use two abbreviations:

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.

The first configurations

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

Re-pairings are the Ov and X1 steps. They happen at these steps:

As in the parent, the E-starts are the configurations after even re-pairings.

Which E-start is the base

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); -)      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. Here it is next to the parent's base:

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′

Here is INV+(e) at B′, clause by clause, as stated in P§3.8.1. At B′: - L = L* = 3, and it is a regular start; - θ = 5, e_1 = 2 and e_2 = 1; - the interior pairs are j = 1, 2.

The value of p_1 meets a bound exactly:

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′

In the .v, the invariant at B′ is

J (mkst 2 base TN E1 false)

It asks for: - P ≠ []; - TC E1 false TN; - PC E1 for every pair.

The Definitions PN, PI and PC are the parent's (P§4). For each pair, 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. The values there,

h = 2,   tv = 2^L − 2,   w = 2^(L−1),

give exactly 12w.

The next E-start

The next E-start comes after re-pairing 8 (step 104,510):

K(2; (95,68,0), (34,33,1), (34,33,1), (10,38,1); -)

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

Proof.

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:

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

Nothing else depends on the orbit

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. At every macro step, their K is the parent's K with one far exponent larger, by the amount in the last column.

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′ (below) is 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, and later the two agree (table below).
• The tape is wider (table below).

The E-start after B′, and the parent's base:

E-start after B':   K(2; (95,68,0), (34,33,1), (34,33,1), (10,38,1); -)
parent's base B:    K(2; (95,68,0), (34,33,1), (10,15,1), (1,24,1); -)

L* at the n-th E-start:

The tape at 10⁹ steps:

So this machine's 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); - 504 L-slot merges (494 interior Ep run-outs).

Its INV(b) margins are comparable to the parent's. The table gives the minimum interior r on each orbit, with the thresholds.

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. These names occur 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 .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 (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 is byte-identical to the parent's .v. That includes:

• J and Jstep;
• every ob_* and inv_* lemma;
• nonhalt.

Where everything lives in the .v

Two views of the same layout. By section of this write-up:

By item, with the statements of the start lemmas:

What the .v proves

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 are the ones the rules predict;
• 5,323 of 5,323 to 3·10⁸ steps are too;
• 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);
• the same on random chains of cycle pairs starting at L* = 3..40;
• 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).