1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---: never halts

This machine is another machine with its own write-up, called the parent below, seen in a mirror. Its table is the parent's table with left and right swapped and the states renamed. Started on a blank tape, it does step for step what the parent does when started in a different state, on the mirror-image tape.

The parent is a binary counter that counts down. Each macro step subtracts one from a number stored on the tape. When the number reaches zero, a few special steps re-pair the blocks that hold its digits.

Apart from its initial segment, the parent's proof never uses its run from the blank tape: from a starting configuration of the right shape on, the argument is general. This machine's run reaches such a configuration after 78,911 steps, so the same proof applies and the machine 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.

The parent and the twin

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;
• "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 φ (§0):

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

So the twin from the blank tape is the parent started from 0^inf D> 0^inf instead of 0^inf A> 0^inf.

Summary

The parent is a binary down-counter (parent §1–§2). Its configurations are K(h; P; T), which consist of:

1. a marker (10)^h 11001;
2. then a list of pair blocks (10)^p (01)^q s(d), whose digits d form a binary number V;
3. 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). It is 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′ at step 1,021 on, every macro step is one of the rules, and the run reaches an E-start at step 78,911:

step  1,021   K0′ = K(2; (11,12,0); −)
step 78,911   K(2; (95,68,0),(34,33,1),(10,15,1),(1,25,1); −)     (the E-start)

This E-start is the parent's base except for the far pair's q (25 instead of 24). 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).

Template and status

The template is the parent's .v. Its 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 two busycoq files:

• verify/Flip.v (flip, flip_halts);
• verify/Permute.v (Perm, perm_halts).

Relative to the parent's .v, only three things differ:

• the initial segment;
• one number of the base E-start (the far pair's q: 25 instead of 24);
• the final transfer to the twin.

Status: formalized in the accompanying verify/Skelet1LikeC2_1RB0RE.v (1,364 lines). It 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. The file 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.

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

twin row q:  (w, d, q′)    ↦    parent row φ(q):  (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 μ be the map that swaps the two sides of the tape and renames the state:

μ(q, (l, s, r)) := (φ(q), (r, s, l))

Mirroring the tape turns move_left into move_right and back. So for single steps and for halting:

c -[twin]-> c'          iff   μ c -[parent]-> μ c'
c halted for the twin   iff   μ c 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)

In the twin's orientation, the parent's family reads:

[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)). It is 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 (Lemma C), with:

• the same side conditions;
• the same effect on (h, P, T);
• the same number of steps.

The domain D and the outside cases (o1)–(o7) are the same sets of parameters.

For reference, here is the abstract form both machines share. In it:

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

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)]; -)

As a check that does not go through Lemma C, 405 random rule instances (45 per rule, all h mod 4, sizes 2–300) were run on the twin's own table from mirrored words. They 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;
• 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)

The twin's initial segment, next to the parent's:

As in the parent, the twin passes through L = 0 before K0′:

• at step 316, EndLast applies and predicts step 500 exactly;
• 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). Every other clause has the parent's values. So J_base has the parent's proof (repeat split; lia).

Conclusion. The argument has three steps.

1. 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).
2. The base satisfies INV+(e), so by the Theorem every configuration after it is in D.
3. 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. It does so in four parts.

1. Two tables. The top-level definition is the twin:

Definition tm := TM_from_str "1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---"

The parent is

tm3 := TM_from_str "1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---"

The local notations -->*/-->+ are bound to tm3, and everything up to nonhalt_D is about tm3.

Apart from the start (item 2), that part is the text of the parent's .v: the family K, the 14 sweep lemmas, the 9 macro rules, J and Jstep.

2. Start. Two lemmas, both by direct execution with solve_initD:

init : D;; tape0 -->* K 2 base TN (78,911 steps) init0 : D;; tape0 -->* K 2 [(11,12,false)] TN (K0′, 1,021 steps)

Here base is the list of §3.7 (far pair (1,25,true)). nonhalt does not use init0.

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. Two lemmas:

J_base : J (mkst 2 base TN E1 false) nonhalt_D : ~ halts tm3 (D;; tape0)

J_base has the parent's proof.

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

Mirror. Flip.flip_halts does the mirror:

Flip.flip_halts : halts tm c -> halts (flip tm) (flip_conf c)

flip_conf c0 is A;; tape0 by conversion, because the blank tape is symmetric.

Renaming. Permute.perm_halts does the renaming, with φ(A) = D:

Permute.perm_halts : Perm tm tm' f -> halts tm (q;; t) -> halts tm' (f q;; t)

New obligation. The one new obligation is

perm_twin : Perm (flip tm) tm3 phi

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

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

What differs from the parent's .v

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;
• the closing comment.

Where each item lives:

What the .v proves

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.
• φ 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 were 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).
• E-start after overflow 4. At step 19,589 the twin is at

K′(2; (47,32,0),(16,15,1),(4,21,1); −)

It 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; - the two ratio minima are

```
min p_1′/(2^(L*′+2)−1) = 1.000
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).