1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA (W5-8c): never halts (delta proof from W5-8)
This machine is W5-8, 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF (the parent), with its states renamed. There is no mirror. It starts in the parent's state E instead of A, so it runs the parent's transition table 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 E the parent's table enters the family K after 6,950,830 steps. Then 18 macro steps, all by the parent's rules, reach Even(13299, 220) at step 163,638,058. From there the parent's double cycle runs unchanged.
- Machine:
1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA, viewer https://bbchallenge.org/1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA - Holdout: line 636 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.(sha256beef54a5…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 The renaming
Write σ for the map from the parent's states to this machine's states:
sigma (parent state -> this state): A -> E, B -> C, C -> D, D -> F, E -> A, F -> B
Row σ(q) of this table is the parent's row q, with every target state t replaced by σ(t). The written symbols and the moves are unchanged.
| this state | 0 | 1 | = σ(parent state) | parent 0 | parent 1 |
|---|---|---|---|---|---|
| A | 1RB | 0RD | σ(E) | 1RF | 0RC |
| B | 0RC | 0LB | σ(F) | 0RB | 0LF |
| C | 0RD | 1RD | σ(B) | 0RC | 1RC |
| D | 1LE | 1RA | σ(C) | 1LA | 1RE |
| E | 1RC | 1LF | σ(A) | 1RB | 1LD |
| F | --- | 1LA | σ(D) | --- | 1LE |
For example, the parent's A1 = 1LD becomes 1Lσ(D) = 1LF, which is this machine's E1. 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 R
For a configuration c of the parent's table, let σc be the same tape and head position, with the head state q replaced by σ(q).
Lemma R. 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), and this machine's cell (σ(q), s) is "write w, move d, go to σ(t)". So the result is σc′.
D0 is the only undefined cell of the parent's table, and F0 = σ(D)0 is the only undefined cell of this one. 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 and the family K
Start. This machine starts from 0^inf A> 0^inf. Since σ(E) = A, that is σ of 0^inf E> 0^inf. So this machine's run is σ of the parent's table run from state E, step for step, on the same tape.
The family K. The parent's family (P§2) is
K(n,a,b,c,d) = 0^inf <F G 1^n 0 1^a 0110 1^b 0^6 1^c 0110 1111 0^6 1^d 0110 0110 111 0^inf
where G is the parent's 43-cell gadget. The head is in state F on the 0 just left of G. On this machine σK(n,a,b,c,d) is the same tape with the head in state σ(F) = B.
There is no mirror, so left records stay left records, and every configuration K(...) below is reached at a left record.
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 R each is an exact run of this machine too, with the same domain and the same step count.
In particular the double cycle (P§4) holds here in the form
sigma Even(n, x) --> sigma 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 E. On this machine they are read through σ.
2. The opening run
2.1 The direct part
From 0^inf E> 0^inf, the parent's table reaches
K(2583, 70, 76, 43, 18)
after exactly 6,950,830 steps. It is the first left record of that run whose configuration is in the family K.
Equivalently, this machine reaches σK(2583,70,76,43,18), in state B, after 6,950,830 steps from the blank tape, and no earlier left 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, 18 macro steps by the parent's rules reach the Even family. Each row applies its rule as many times as shown. The step numbers are the sums of the rules' step formulas.
| after | rule | step | configuration |
|---|---|---|---|
| opening | (direct run) | 6,950,830 | K(2583,70,76,43,18) |
| 1 | S^8 | 9,032,398 | K(2967,6,108,43,50) |
| 2 | T6 | 12,743,660 | K(3559,60,112,35,18) |
| 3 | S^7 | 15,134,804 | K(3895,4,140,35,46) |
| 4 | TE | 19,523,338 | K(4451,54,82,97,18) |
| 5 | S^6 | 22,019,854 | K(4739,6,106,97,42) |
| 6 | T6 | 27,598,730 | K(5331,112,104,35,18) |
| 7 | S^13 | 34,176,106 | K(5955,8,156,35,70) |
| 8 | T8 | 40,451,682 | K(6495,82,86,117,18) |
| 9 | S^10 | 46,448,502 | K(6975,2,126,117,58) |
| 10 | TO | 54,377,014 | K(7563,152,120,35,18) |
| 11 | S^18 | 67,117,990 | K(8427,8,192,35,90) |
| 12 | T8 | 75,779,054 | K(8967,118,86,137,18) |
| 13 | S^14 | 87,253,370 | K(9639,6,142,137,74) |
| 14 | T6 | 97,978,338 | K(10231,188,136,35,18) |
| 15 | S^23 | 119,736,338 | K(11335,4,228,35,110) |
| 16 | TE | 131,447,656 | K(11891,142,82,161,18) |
| 17 | S^17 | 149,713,782 | K(12707,6,150,161,86) |
| 18 | T6 | 163,638,058 | K(13299,220,148,35,18) |
The chain is
S^8 T6 S^7 TE S^6 T6 S^13 T8 S^10 TO S^18 T8 S^14 T6 S^23 TE S^17 T6
It is not the parent's chain: this run starts with other values of a, b, c, d, and its collisions come in a different order.
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 163,638,058. In that run, these 126 configurations (the start, and the result of every single application of a rule) are exactly the K-shaped left records up to step 163,638,058.
2.3 Every application is in its rule's domain
The domains are those of P§1:
| rule | a | b | c | d |
|---|---|---|---|---|
| S | even, ≥ 10 | even, ≥ 6 | odd, ≥ 7 | even, ≥ 2 |
| TE | 4 | even, ≥ 88 | 35 | even, ≥ 20 |
| TO | 2 | even, ≥ 82 | odd, ≥ 37 | even, ≥ 18 |
| T6 | 6 | even, ≥ 82 | odd, ≥ 35 | even, ≥ 18 |
| T8 | 8 | even, ≥ 88 | 35 | even, ≥ 20 |
Every rule also needs n odd. Here n starts at 2583, and every rule adds an even constant to n (48, 556, 588, 592 or 540), so n stays odd.
Parities. In every row of section 2.2, a, b and d are even and c is odd. Within a block S^k, S adds 4 to b and d, subtracts 8 from a and keeps c, so the parities hold at every single application too.
Bounds in a block S^k. b and d only grow and c stays fixed, so the first application has the smallest b, c and d. a falls by 8 each time, so the last application has the smallest a.
The table below lists, for each row, the configuration the rule is applied to, the values of a over the applications, and the first application's b, c, d.
| row | rule | applied to | a | b | c | d |
|---|---|---|---|---|---|---|
| 1 | S^8 | K(2583,70,76,43,18) | 70, …, 14 | 76 | 43 | 18 |
| 2 | T6 | K(2967,6,108,43,50) | 6 | 108 | 43 | 50 |
| 3 | S^7 | K(3559,60,112,35,18) | 60, …, 12 | 112 | 35 | 18 |
| 4 | TE | K(3895,4,140,35,46) | 4 | 140 | 35 | 46 |
| 5 | S^6 | K(4451,54,82,97,18) | 54, …, 14 | 82 | 97 | 18 |
| 6 | T6 | K(4739,6,106,97,42) | 6 | 106 | 97 | 42 |
| 7 | S^13 | K(5331,112,104,35,18) | 112, …, 16 | 104 | 35 | 18 |
| 8 | T8 | K(5955,8,156,35,70) | 8 | 156 | 35 | 70 |
| 9 | S^10 | K(6495,82,86,117,18) | 82, …, 10 | 86 | 117 | 18 |
| 10 | TO | K(6975,2,126,117,58) | 2 | 126 | 117 | 58 |
| 11 | S^18 | K(7563,152,120,35,18) | 152, …, 16 | 120 | 35 | 18 |
| 12 | T8 | K(8427,8,192,35,90) | 8 | 192 | 35 | 90 |
| 13 | S^14 | K(8967,118,86,137,18) | 118, …, 14 | 86 | 137 | 18 |
| 14 | T6 | K(9639,6,142,137,74) | 6 | 142 | 137 | 74 |
| 15 | S^23 | K(10231,188,136,35,18) | 188, …, 12 | 136 | 35 | 18 |
| 16 | TE | K(11335,4,228,35,110) | 4 | 228 | 35 | 110 |
| 17 | S^17 | K(11891,142,82,161,18) | 142, …, 14 | 82 | 161 | 18 |
| 18 | T6 | K(12707,6,150,161,86) | 6 | 150 | 161 | 86 |
Every entry meets its rule's bounds:
- In the S rows the smallest a is 10 (row 9), the smallest b is 76, every c is at least 35 and every d is 18.
- The TE rows have c = 35, b ≥ 140 and d ≥ 46.
- The TO row has b = 126, c = 117 and d = 58.
- The T6 rows have b ≥ 106, c ≥ 43 and d ≥ 42.
- The T8 rows have c = 35, b ≥ 156 and d ≥ 70.
3. The double cycle's domain holds at the end of the opening
The last row is
K(13299, 220, 148, 35, 18) = Even(13299, 220)
since (220 + 76)/2 = 148. Here n = 13299 is odd, x = 220 = 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
Even(13299, 220) --> Even(16747, 252) --> Even(20579, 284) --> ...
with x = 220 + 32j. The parent's own orbit has x = 212 + 32j. Both lie on the line x - 2y = -76 of P§4, since b = (x + 76)/2 is the definition of Even.
4. The argument
Theorem. 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA does not halt from the blank tape.
-
Relation. By Lemma R, this machine's run is σ of the parent's table run from
0^inf E> 0^inf(section 1.3). -
Direct part. That run reaches K(2583,70,76,43,18) after 6,950,830 steps without halting (section 2.1).
-
Macro steps. The parent's rules S, T6, TE, T8 and TO take it to Even(13299, 220) at step 163,638,058. Each application is inside its rule's domain (section 2.3).
-
Double cycle. From there the parent's double cycle applies forever (section 3, P§4). Each round takes at least one step (P§6).
-
Conclusion. So the parent's table run from E is infinite. By Lemma R this machine's run is too, step for step. ∎
The halting cell. Here only E1 = 1LF enters F. So this machine halts exactly when E reads a 1 that has a 0 on its left.
E1 is σ of the parent's A1 = 1LD, and Lemma R 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 three starts of the table
The table has three entries in the 740 list.
| line | machine | start in the parent's table | mirror | Even reached |
|---|---|---|---|---|
| 214 | 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF |
A | no | Even(12863, 212) at step 153,126,993 |
| 418 | 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF |
C | yes | Even(12857, 212) at step 153,013,640 |
| 636 | 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA |
E | no | Even(13299, 220) at step 163,638,058 |
Line 214 is the parent and line 418 is its mirrored sibling, each with its own proof. This delta proves line 636.
Starts B and F give no further entries. On the blank tape, B0 = 0RC leaves the tape blank and enters C, and F0 = 0RB leaves it blank and enters B. So these runs are the start-C run, delayed by one or two steps.
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) Ev N X = Even(2N+1, 8X+52)
The delta keeps the parent's file with its table named tmP (as the mirrored sibling's proof does) and changes three things.
The bridge. Let φ = σ⁻¹, which maps this machine's states to the parent's. Then Perm tm tmP phi holds cell by cell (busycoq's Permute.v), and φ(A) = E. So perm_halts turns halts tm c0 into halts tmP (E;; tape0). No flip is needed.
The direct opening. A new lemma
E;; tape0 -->* Kr 1291 35 38 21 9 (6,950,830 steps)
proved by busycoq's list configurations, cut into pieces at left records as in the parent.
The macro steps. The 18 rows of section 2.2 as follows with the parent's lemmas, ending at Ev 6649 21:
follow (S_iter 8 1291 2 35 18 8). follow (T6' 1483 13 4 16).
follow (S_iter 7 1779 1 53 14 8). follow (TE' 1947 26 13).
follow (S_iter 6 2225 2 38 45 8). follow (T6' 2369 12 31 12).
follow (S_iter 13 2665 3 49 14 8). follow (T8' 2977 34 25).
follow (S_iter 10 3247 0 40 55 8). follow (TO' 3487 22 40 20).
follow (S_iter 18 3781 3 57 14 8). follow (T8' 4213 52 35).
follow (S_iter 14 4483 2 40 65 8). follow (T6' 4819 30 51 28).
follow (S_iter 23 5115 1 65 14 8). follow (TE' 5667 70 45).
follow (S_iter 17 5945 2 38 77 8). follow (T6' 6353 34 63 34).
Then progress_nonhalt_simple on (N, X) from (6649, 21), exactly as in the parent.
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; it runs either table and counts left or right records) and a scanner for K-shaped left records (scripts/kscan.c, built to work/kscan; it parses the tape by run lengths). 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.
| section | what is checked |
|---|---|
| T | the string; line 636 of the 740 list byte for byte, exactly once, no CR (parent: line 214); only F0 undefined, F entered only by E1; sheet rows: Results class only, level-0 no status, classifications only in the "Bouncer + Chaotic Edge" column, no other sheet file; Discord: only the UBRRBA to-do list; busycoq index: absent; upstream tree at 9cf9e88: none of the 1,440 variants of the table |
| REL | σ maps the parent's table onto this one, 12/12 cells, without the mirror, and is the only map of 720 × 2; canonical forms equal (this from A, parent from E); start = σ(E); lockstep with the parent's table from E in Python, every step (same position, state σ, same tape); after 163,638,058 steps the C runner's tapes are equal |
| OPEN | 6,950,830 steps from blank to σK(2583,70,76,43,18) on this machine and to K(2583,70,76,43,18) on the parent's table from E; no earlier K-shaped left record in either (C scanner, any state; and tools/sim.py events); the 18 rows: every application in its domain, the step sums; the 126 K-shaped left records to 163,638,058 of both runs = the start, every single rule application and the end; every row by direct simulation of this machine; one unbroken run to σEven(13299,220) at 163,638,058 |
| INV | 13299 odd, 220 = 4 mod 8, 220 ≥ 52, b = 148 |
| DC | whole double cycles of this machine from σEven(n, x), x = 52 … 252, exact configuration and steps; the orbit from step 163,638,058: every even and odd run start by direct simulation of this machine, chained and as one unbroken run from blank, to 2·10⁹ steps (5·10⁸ --quick, 10¹⁰ --full); every K-shaped left record of this machine in that range is the next point predicted by S, TE or TO |
| PLAN | section 6: the half-length start and end, and each follow's arguments give the lemma's left side at the row's start and its right side at the row's end |
| PAR | the parent's check_proof.py in the same mode and seed: exit 0, every check PASS, and its MR (symbolic proofs of S, TE, TO, T6, T8), DC and HALT sections present and passing; log in work/parent_check_proof_<mode>_seed<S>.log |
| REM | the table of section 5: the three list lines, their starts and mirror flags (canonical forms), and the Even step of lines 214 and 418 by direct simulation |
| HALT | σ(D) = F; D0 the only undefined cell of the parent, F0 of this machine; no halt of this machine in its first 163,638,058 steps |
| DOC | the relation table, σ, the opening rows, the domain rows, the chain and the follow arguments are quoted here exactly as checked; everything before section 7 lints with 0 errors |
8. Checkpoint B (Dennis)
Pending (non-blocking).
Review log
- 2026-10-13, delta proof stage (workflow W5-8c). First version: relation (σ, no mirror, the only map), Lemma R, opening 6,950,830 direct steps + 18 macro steps by the parent's rules to Even(13299,220) at 163,638,058, double cycle from the parent. check_proof.py 83/83 PASS with seed 1 and seed 2 (default, 105 s each) and seed 1
--full(373 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 σ, a wrong S count in row 1, one wrong step number in the table and one wrong follow argument each make the expected checks fail. After a last prose pass (sections 2.1, 2.2, 7) DOC, OPEN, INV and PLAN were re-run: 39/39 PASS.