1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---: delta proof from kill #11 (#11b, Checkpoint B)

• Machine: 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---, viewer https://bbchallenge.org/1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---
• Holdout list: line 511 of data/holdouts/BB6_holdouts_740.txt (the current list), byte for byte (tools/holdouts.py contains: exit 0; grep -x -F; od -c). Also line 541 of the 778 list and on all 27 snapshots. Its eqv_1590 group has no other member. It is not in busycoq: no entry in data/solved_index.tsv, and no file in vendor/busycoq names it.
• Existing work: there may be some, by hipparcos. The community sheet credits this string to hipparcos:
• Results row 1276: "Skelet 1-like Class 2", Sources: one link, Done By: hipparcos, no status, no notes.
• Level 1 tab, row 44: Sources: one link, Done By: hipparcos, no status, no notes.
• Both links go to the Discord thread https://discord.com/channels/960643023006490684/1432566675533992019 (started 2025-10-28). We could not read the thread.

The live sheet, re-fetched on 2026-10-10, is byte-identical to the 2026-10-09 export on these tabs. The row just below, Results 1277, is kill #33 1RB0RE_1LC0RE_1LD0LD_1RA0LC_1RA1RF_1RA---, with the note "Machine with the most common transitions" and no claim. Dennis reads the claim as being on #33; the sheet puts it on this string (notes.md has the details). Either way we prove this machine as part of the #11 family (Dennis, 2026-10-10). The submission must say plainly that hipparcos may already have worked on it. - Parent: kill #11 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD--- (KILLED_NONHALT, check_kill PASS). "P§n" means section n of #11's proof.md; sections 1–5 have the same numbers in its submission copy. The formal delta (§5) starts from #11's .v (sha256 8bca47b1…53c0, 694 lines). - Written for: the string itself. - Result. This machine is #11's machine with its states renamed by τ = (A,B,C,D,E,F) ↦ (E,A,B,C,D,F), with no mirror. It starts in #11's state B, not A. So it runs a different orbit of the same macro map: - the window lemmas, the rules M and O, the invariant INV and its closure carry over unchanged, with the K head state renamed B ↦ A; - only the initial segment and the base change: 732 steps to K((1,1,10); 8, 1) (class A), instead of 483 steps to K((1,1,2); 8, 5); - adjusted invariant: none. - Evidence: check_proof.py, SUMMARY PASS (§6). The formal delta of §5 compiles as a scratch file (rocq/delta_check.v, 8.4 s, closed under the global context). tools/check_kill.sh has not been run, so this is not a kill. - Status: CHECKPOINT_B (informal delta complete and validated). - AI assistance: this proof sketch, the scripts and the checks were produced with the help of Claude (Anthropic).

0. The map

τ: A↦E, B↦A, C↦B, D↦C, E↦D, F↦F (a 5-cycle on A–E). Row τ(s) of this table is #11's row s with every target state t replaced by τ(t). Symbols and directions are unchanged. For example, #11's C1 = 0RB becomes 0Rτ(B) = 0RA, which is this machine's B1. check_proof.py §S checks the 12 cells and searches all 720 renamings with and without the mirror: τ is the only map from #11's table to this one. (From #33's table the only map is CEABDF with the mirror, start #33's C; from #33b's, BCEADF with the mirror, start #33b's D.)

Lemma R (relabelling). For a configuration c, let τc be c with its head state renamed by τ; the tape and head position stay the same. Then c → c′ under #11 if and only if τc → τc′ under this machine, and c is halted exactly when τc is (F1 is the only undefined cell, and τ fixes F). So every #11 run c →ⁿ c′ gives a run τc →ⁿ τc′ here, of the same length, and conversely.

Start. This machine's c0 is 0^inf A> 0^inf = τ(0^inf B> 0^inf). So its run is τ of #11's machine run from 0^inf B> 0^inf. It is not #11's own run, which starts in A. §R checks this in lockstep for 2·10⁶ steps (2·10⁷ in the long run): state = τ(#11's state), same symbol written, same move, identical tapes at the end.

Halting cell. Only D1 = 1LF enters F (it is τ of #11's E1), and F1 is ---. So the machine halts exactly when D reads 1 with a 1 to its left.

1. What carries over unchanged

The window lemmas on this table (X> = head in state X on the next cell, <X = on the previous cell):

S1 A>01 -2-> 10A>        S2 B>10 -2-> 01B>        S3 01<C -2-> <C10        S4 10<D -2-> <D01
S5 B>1101 -6-> 10B>11    S6 0A>10 -6-> 100A>      T1 A>00 -3-> <D01        T2 000<D -5-> 100A>
T3 100<D -3-> <D011      T4 01<D -2-> <C11        T5 10<C -2-> <D01        T6 00<C -3-> 10B>
T7 B>11 -2-> 00B>        T8 B>11011 -9-> 10000A>  T9 0^inf 1001<D -13-> 0^inf 1001000A>   T10 A>11 -2-> 00A>
T11 A>0 -1-> 1B>         T12 B>11000 -13-> <D01101   T13 101<D -3-> <D011   T14 A>1101 -4-> 0010A>

The digit lemmas become: Lb (10)^u (01)^v <D → <D (01)^u (10)^(v−1) 11; Lf (10)^u 00 (01)^v <D → (10)^(u+1) (01)^(v−1) B> 11; Rb B> 11 (01)^u (10)^(v−1) 11 → (10)^u 00 (01)^(v−1) B> 11; Ro A> (01)^u (10)^(v−1) 11 → (10)^(u−1) 1 (10)^(v−1) 000 A>. Steps and side conditions are #11's.

The rules in busycoq comment style, for this machine:

1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---     (= tau of 1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, tau = EABCDF)

K(d_1 .. d_m; a, b) := 0^inf 10 01 d_1 .. d_m (10)^a 000 (10)^b A> 0^inf
digit (u,0,v) := (10)^u 00 (01)^v,   (u,1,v) := (10)^u (01)^v      (d_m least significant)

start from K((1,1,10); 8, 1)                                  (step 732, section 2)

M  (carry; some bit is 0; j* = index of the LAST bit-0 digit):
   K(.., (u,0,v), (u_j,1,v_j)_{j*<j<=m}; a, b) --> K(.., (u+1,1,v-1), (u_j,0,v_j-1)_{j*<j<=m}; a+1, b+2)
   steps 32 + 8a + 8b + 4v + sum_{j>j*} (8 u_j + 4 v_j);  needs v >= 1, u_j, v_j >= 1 (j > j*), a, b >= 0
   if v = 1, the digit (u+1,1,0) drops (re-reading, P section 1)
O  (overflow; all bits 1):
   K((u_1,1,v_1) .. (u_m,1,v_m); a, b) --> K((0,0,u_1), (v_1-1,0,u_2), .., (v_{m-1}-1,0,u_m), (v_m,1,a); b+3, 1)
   steps 89 - 4m + 8a + 20b + 4 sum u_j + 8 sum v_j;  needs m >= 1, all u_j, v_j >= 1, a >= 1, b >= 0

2. What changes: initial segment and base (replaces P§4)

Direct simulation of this machine from the blank tape (§C). A K-configuration is state A on a cell with only blanks from there to the right, only blanks left of the leading 1001, and the text in between parsing as a K. Up to step 732 they occur exactly at these steps (and #11 from 0^inf B> 0^inf gives the same list, as Lemma R says):

Two legs of the init use rule cases the invariant argument never needs (the LSB drop, and O at m = 0). That does not matter: the proof only uses the 732-step run as one finite computation. The table just explains it. (§H still checks the last leg link by link with #11's O chain at m = 0.)

Compare #11 from A: K-configurations at 142, 283 and 383 (not in INV), then its base K((1,1,2); 8, 5) at 483. The third start of the same table, kill #33b (start C, mirrored), reaches K((1,1,9); 8, 1) at 687.

INV at the base K((1,1,10); 8, 1) (P§3; derived quantities as in P§1): - top (1,1,10): bit 1, u_1 = 1; m = 1; - V = 1, R_tot = R_1 = 0, R1_1 = 0; - ubar_1 = 1 (odd), vbar_1 = 10 ≥ 1 (also the LSB condition); - S = 8 + 0 − 2 = 6 ≥ 1, T = 1 − 1 = 0 ≥ 0; - a = 8 ≥ 1, b = 1 odd, a + R_tot = 8 even; - Common holds, and class A holds (top (1,1,v), every vbar ≥ 1, every ubar odd, S ≥ 1).

In the additive Rocq form of #11's .v (INV, PA, Rof, LSBok, at ([d1 1 10], 8, 1)): Rof = 0; a + R + 2 = 10 ≥ 4; b + 3 + 2R = 4 ≥ 4 (tight); a + R + 1 = 9 ≥ 4; v_m = 10 ≥ R + 1; (a + R) mod 2 = 0; b mod 2 = 1; PA (d1 1 10) 0 0: canon, 10 ≥ 1, ub = 1 odd and = 1. §B evaluates all 12 clauses. Every clause is linear arithmetic on constants, so #11's base tactic line closes it (§5).

3. The argument (complete)

Theorem. 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC--- does not halt from the blank tape.

1. Initial segment. The machine runs from c0 to K((1,1,10); 8, 1) in exactly 732 steps without halting. This is a finite exact computation (§C); in Rocq it is solve_init.
2. Base. INV([(1,1,10)], 8, 1) holds, in class A (§2).
3. Transfer. P§3.2 (coverage) and P§3.3 (closure): every INV state has a macro step M or O, of at least 32 machine steps, to an INV state. These statements are about the triples and a, b, and the macro steps are #11's rule instances K → K′. By Lemma R, each instance is a run τK →⁺ τK′ of this machine, of the same length. So coverage and closure hold verbatim for the configurations K_A = τK.
4. Conclusion. By induction from the base, the run is an infinite chain of macro steps, each of at least one machine step, so it never halts (progress_nonhalt_cond with P := INV, as in P§5). No macro step presents the halting cell: each is an exact computation from one K to the next, composed of window lemmas in which F reads only 0. ∎

Nothing in #11's argument after its init depends on #11's own orbit. Its orbit statistics (P§7) are evidence, not premises.

4. How this orbit relates to its siblings (explanation, not a premise)

Three of the four holdouts with this table (#11, #33b and this machine) run orbits of the same macro map that lock together in the shared triple notation: - With kill #33b (same table mirrored, started in #11's C; base K((1,1,9); 8, 1) at step 687): from macro step 0 on, the two states are equal except for one exponent, larger by 1 here, on the top digit, and the same rule fires at every macro step. - With kill #11 (base K((1,1,2); 8, 5) at step 483): from macro step 54 on (step 25,851 here, 25,618 in #11), the states are equal except for one top-digit exponent, larger by 4 here, with the same rule at every step. This is #33b's +3 against #11, plus 1. - Where the extra exponent sits: v_1 in class A, u_2 in class B (the top is (0,0,1) there), u_1 in class C. O sends it from v_1 to digit 2's u (A → B), the top fall merges it into the new top's u (B → C), and the next O sends it to the new top's v (C → A). - Checked for 3·10⁵ macro steps (to t ≈ 2.2·10¹¹, 80 overflows; §X) and for 1.2·10⁶ in the long run (t ≈ 3.7·10¹²).

It explains the "exact trajectory twin of #11" seen at 10⁹ steps in the family sweep: 77,693 cells and 38,841 nonzeros here, against #11's 77,685 and 38,836 (+8 cells = four extra blocks) and #33b's 77,691 and 38,839 (+3 blocks). Kill #33 (the fourth start) runs a different orbit: 76,245 cells at 10⁹.

5. Formalization delta (validated as a scratch compile; check_kill not run)

Copy #11's .v (sha256 8bca47b193b15a0cbd664fcbafa9bf6a39dfc4c9ca261e1d8f95cb0f425553c0, 694 lines) and change only the following: 1. TM_from_str "1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---". 2. Rename every state name {{X}} by τ, simultaneously: {{B}} → {{A}} (22 occurrences), {{C}} → {{B}} (18), {{D}} → {{C}} (5), {{E}} → {{D}} (18). #11's file never names A or F. This covers the window lemmas, digit lemmas, sweeps (LbS, RbS, RoS), chunks and K. The es/follow proofs go through unchanged, because τ maps transitions to transitions (Lemma R). 3. Lemma init: c0 -->* K [d1 1 10] 8 1. (732 steps, the same unfold K, L0. cbn. solve_init.) and, in nonhalt, change (K [d1 1 10] 8 1) with (Kc ([d1 1 10], 8, 1)). #11's own tactic line closes the base goal (§2). 4. The header comment, the three chunk comments that name head states, and the rule block at the end.

Everything else is #11's text: every proof script, M_spec/Mdrop_spec/O_spec and their statements, dg, map0, map1, Oz, Oout, INV, step, and the structure of nonhalt.

Done as a scratch check. check_proof.py's delta_text applies exactly these edits (each one asserted to match the expected number of times). rocq/make_delta.py writes its output to rocq/delta_check.v (696 lines), and rocq/compile.sh compiles it (Coq 8.20.1, -native-compiler no): 8.4 s, exit 0, nonhalt : ~ halts tm c0, Print Assumptions nonhalt: Closed under the global context. The record is rocq/delta_check.out (it starts with the sha256 of the file). It compiled on the first try, with no tactic changes. §V checks that the file is the delta of #11's pinned .v, byte for byte; that with comments stripped it differs from #11's code only by the substitutions above; and that the compile record is clean and belongs to this exact file. This is evidence for Checkpoint B, not a kill: the kill stage copies the file to machines/<tm>/<tm>.v and runs tools/check_kill.sh. Only that PASS counts.

6. Evidence (python3 -B check_proof.py, defaults, about 23 s; output in check_proof.out)

The script imports #11's check_proof.py read-only, for its abstract model, its invariant, its random-INV generator, its window-lemma table, its chain builders and its abstract checks. Everything that depends on the machine or the start is re-run on this machine's own table with its own simulator.

Long run, --seed 2026 --tm-steps 1e9 --orbit 1.2e6 --induct 6e5 --lockstep 2e7 --no-rocq (122 s, check_proof_long.out): SUMMARY PASS. It includes: - §R lockstep for 2·10⁷ steps; - §D, the real machine against the model at all 19,332/19,332 macro boundaries to step 999,838,005 (O 53, M0 9,639, M1 4,846, M2 2,422, M3 1,209, M4 602, M5 298, M6+ 262; drops: 30 top, 12 mid; INV classes A 7,523, B 6,307, C 5,502); - §G, INV along 1.2·10⁶ macro steps of the abstract orbit (t ≈ 3.7·10¹², 16 digits, 93 overflows) and 600,000 random-INV induction steps; - §X, the couplings for 1.2·10⁶ macro steps.

11's skeptic review covered the rules and INV (P, Review log). It applies unchanged, because both are the same statements here.

7. Checkpoint B (Dennis)

pending. Nothing needs a decision. The format is #33b's: this delta, with #11's proof attached as the parent. If you would rather have #11's proof restated in full for this machine, say so.