1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF (W5-8b): never halts (delta proof from W5-8)

This machine is W5-8, 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (the parent), seen in a mirror and with its states renamed. It starts in the parent's state C instead of A. So it runs the parent's transition table, mirrored, from a different start.

The parent's proof works on a family K(n,a,b,c,d) of configurations at the start of a round trip. Five macro rules move between members of K, and two of them close a double cycle on the subfamily Even(n, x), which repeats forever.

From state C the parent's table enters the family K after 4,098,826 steps. Then the parent's own 20 opening macro steps apply in the same order, with the same a, b, c, d and with n smaller by 6. They reach Even(12857, 212) at step 153,013,640. From there the parent's double cycle runs unchanged.

• Machine: 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF, viewer https://bbchallenge.org/1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF
• Holdout: line 418 of the 740 list, byte for byte, exactly once.
• Sheet (Results tab): class "Bouncer + Chaotic Edge", with no status, notes, sources or "Done By".
• On Discord it appears only in mxdys's UBRRBA to-do list, which is a list of machines that are easy to accelerate, not a claim.
• busycoq BB6 (HEAD 9cf9e88) has no proof of it, nor of any renaming or mirror of its table.
• Parent: W5-8 (line 214 of the 740 list), never halts, with a complete Rocq proof Lemma nonhalt: ~halts tm c0. (sha256 beef54a5…cf48). Below, P§n is section n of the parent's write-up.
• Adjusted invariant: none. Only the opening changes.
• Status: the informal delta is complete and checked (section 7). It is not formalized; section 6 outlines the formal delta.
• AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

1. The relation

1.1 Mirror and renaming

Write σ for the map from the parent's states to this machine's states:

sigma (parent state -> this state):   A -> B,  B -> C,  C -> A,  D -> D,  E -> E,  F -> F
mirror:                               every move L becomes R and every R becomes L

Row σ(q) of this table is the parent's row q, with every direction reversed and every target state t replaced by σ(t). The written symbols are unchanged.

For example, the parent's A1 = 1LD becomes 1Rσ(D) = 1RD, which is this machine's B1. Among all 720 renamings, with and without the mirror, this is the only map from the parent's table to this one.

1.2 Lemma M

For a configuration c of the parent's table, let Φc be its mirror image with the head state renamed by σ:

• the cell at position p moves to position -p;
• the head moves with its cell, so a head at position h goes to -h;
• its state q becomes σ(q).

Lemma M. c → c′ in one step of the parent's table exactly when Φc → Φc′ in one step of this machine. And c is halted exactly when Φc is.

Proof. In c the head reads a symbol s in state q. Say the parent's cell (q, s) is "write w, move d, go to t". In Φc the head reads the same s in state σ(q). This machine's cell (σ(q), s) is "write w, move the other way, go to σ(t)". So it writes w on the same cell, moves to the mirror of where the parent's head moves, and enters σ(t). That is Φc′.

D0 is the only undefined cell of both tables, and σ fixes D. So the halting configurations correspond too. ∎

By induction on the number of steps, an exact run of the parent's table of N steps maps to an exact run of this machine of N steps, and back.

1.3 The start, records and the family K

Start. This machine starts from 0^inf A> 0^inf. Since σ(C) = A and the blank tape is its own mirror image, that is Φ of 0^inf C> 0^inf. So this machine's run is Φ of the parent's table run from state C, step for step.

Records. Φ turns left records into right records. A round trip of this machine starts at its right end.

The family K, mirrored. In the parent's family K(n,a,b,c,d) (P§2) the head is in state F on the 0 just left of the 43-cell gadget G. The mirror images are

Phi K(n,a,b,c,d) = 0^inf 1^3 0 1^2 0^2 1^2 0 1^d 0^6 1^4 0 1^2 0 1^c 0^6 1^b 0 1^2 0 1^a 0 1^n 0^2 1^2 0 1^5 0 1^2 0^2 1^5 0 1^2 0 1^6 0 1^2 0 1^4 0 1^2 0^2 F> 0^inf

The 43 cells before F> are G read backwards. Since σ(F) = F, the head is again in state F, now on the blank cell just right of the reversed gadget.

1.4 The parent's rules carry over

Each rule of the parent is an exact run of the parent's table: the shift rules R1 and R2b, the macro rules S, TE, TO, T6 and T8 (P§1, P§3). By Lemma M the mirror of each is an exact run of this machine, with the same domain and the same step count.

In particular the double cycle (P§4) holds here in the form

Phi Even(n, x)  -->  Phi Even(n + 12x + 808, x + 32)        (n odd, x = 4 mod 8, x >= 52)

From here on, configurations are written in the parent's coordinates, as members K(...) of the parent's table run from C. On this machine they are read through Φ.

2. The opening run

2.1 The direct part

From 0^inf C> 0^inf, the parent's table reaches

K(1953, 34, 68, 45, 18)

after exactly 4,098,826 steps. It is the first left record of that run whose configuration is in the family K.

Equivalently, this machine reaches Φ K(1953,34,68,45,18) at a right record after 4,098,826 steps from the blank tape, and no earlier right record has that shape. For comparison, the parent's own opening from A reaches K(1959,34,68,45,18) after 4,097,897 steps (P§5).

2.2 The macro steps

From there, the same 20 macro steps as in P§5 apply, in the same order. Each row applies its rule as many times as shown. The step numbers are the sums of the rules' step formulas.

The last column gives the parent's step at the same row, for comparison.

Each row's configuration was also confirmed by direct simulation of this machine at exactly that step, and by one unbroken run from the blank tape to step 153,013,640.

2.3 Every application is in its rule's domain

In every row, a, b, c and d are exactly the parent's values in P§5, and n is 6 smaller.

This is forced by the rules. In each of S, TE, TO, T6 and T8 the new a, b, c, d do not depend on n, and the new n is n plus a constant (P§1). So two runs that start with the same a, b, c, d keep them equal, and keep the same difference in n, as long as they apply the same rules.

The domains ask nothing of n except that it is odd. Here n starts at 1953 and changes by even constants, so it stays odd. The conditions on a, b, c, d are exactly the parent's, which P§5 checks row by row.

Only the step counts differ from the parent's, because every step formula has a term in n (for example 84n in S).

3. The double cycle's domain holds at the end of the opening

The last row is

K(12857, 212, 144, 35, 18) = Even(12857, 212)

since (212 + 76)/2 = 144. Here n = 12857 is odd, x = 212 = 4 (mod 8) and x ≥ 52.

These conditions are the whole domain of the double cycle, and the double cycle preserves them (P§4, closure). So no further invariant is needed.

The orbit from here is the parent's orbit from Even(12863, 212), with n smaller by 6 at every Even member: the double cycle adds 12x + 808 to n, which does not depend on n.

4. The argument

Theorem. 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF does not halt from the blank tape.

1. Relation. By Lemma M, this machine's run is Φ of the parent's table run from 0^inf C> 0^inf (section 1.3).

2. Direct part. That run reaches K(1953,34,68,45,18) after 4,098,826 steps without halting (section 2.1).

3. Macro steps. The parent's rules S, TO, T6, T8 and TE take it to Even(12857, 212) at step 153,013,640. Each application is inside its rule's domain (section 2).

4. Double cycle. From there the parent's double cycle applies forever (section 3, P§4). Each round takes at least one step (P§6).

5. Conclusion. So the parent's table run from C is infinite. By Lemma M this machine's run is too, step for step. ∎

The halting cell. Here only B1 = 1RD enters D. So this machine halts exactly when B reads a 1 that has a 0 on its right.

B1 is σ of the parent's A1 = 1LD, and Lemma M maps halts to halts. Every step of the run above lies inside the direct part or inside one of the parent's exact rules, and none of those halts (P§7.1).

Not a cryptid. As for the parent (P§7.2), the top-level map (n, x) ↦ (n + 12x + 808, x + 32) is affine and all its parities are fixed.

5. Remark: the third start of the table

Line 636 of the 740 list is the same table started in the parent's state E, without the mirror. Its run reaches Even(13299, 220) at step 163,638,058, so the double cycle would finish it too after its own opening. This delta proves only line 418.

6. Formalization delta (outline)

The parent's Rocq proof (P§8) has macro lemmas on half-length parameters, with Kr N a b c d = K(2N+1, 2a, 2b, 2c+1, 2d) and Ev N X = Even(2N+1, 8X+52). Two routes lead to Lemma nonhalt: ~halts tm c0. for this string.

Route 1: conjugacy. Keep the parent's file with its table named tmP. Then:

• flip tm is the parent's table up to renaming (busycoq Flip.v), and the renaming σ⁻¹ gives Perm between them (Permute.v). With flip_halts_iff and perm_nonhalt, the goal becomes ~ halts tmP (C;; tape0).
• New opening: C;; tape0 -->* Kr 976 17 34 22 9 for tmP, 4,098,826 steps, cut into pieces at left records as in the parent.
• The 20 rows by follow with the parent's lemma arguments, N smaller by 3, ending at Ev 6428 20.
• progress_nonhalt_simple on (N, X), exactly as in the parent.

Route 2: a direct copy. Define the mirrored family Kr' (the mirror image of Kr) on this machine's own table and let es' prove S, TE, TO, T6 and T8 again; the rest is the parent's file with the new opening c0 -->* Kr' 976 17 34 22 9. This avoids Flip.v and Permute.v, but it re-runs the five symbolic proofs on the mirrored side.

7. Evidence (python3 -B check_proof.py [--seed S] [--quick|--full] [--no-parent])

The script uses its own batch C runner (scripts/krun.c, built to work/krun), which runs either table and counts left or right records. It imports the parent's check_proof.py for the parent's rule statements (domains, updates, step formulas) and its K word. Logs: work/check_proof_*.log.

8. Checkpoint B (Dennis)

Pending (non-blocking).

Review log

• 2026-10-13, delta proof stage (workflow W5-8b). First version: relation (σ + mirror, the only map), Lemma M, opening 4,098,826 direct steps + the parent's 20 macro steps (n − 6) to Even(12857,212) at 153,013,640, double cycle from the parent. check_proof.py 58/58 PASS with seed 1 and seed 2 (default, 93 s each) and seed 1 --full (321 s); each run re-ran the parent's check_proof.py in the same mode (196/196). Mutation tests: a wrong n in the opening start, a wrong σ and one wrong step number in the table each make the expected checks fail. After a last prose pass (sections 1.2 and 6 and the header), DOC was re-run: PASS.