1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA: delta proof from kill #4 (Checkpoint B)

• Machine: 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA, viewer https://bbchallenge.org/1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA
• Holdout list: line 17 of data/holdouts/2026-10-07_778.txt, byte for byte. Its equivalence-group member is 1RB0LC_1LC0RB_0LD1LA_0RA1LE_0LA1LF_1LD--- (line 24 of 2026-10-07_eqv_1590.txt).
• Sheet: Results row 915, "Sync bouncer counter", with no status, notes or done-by. It is on mxdys's UBRRBA_TODO list (line 45) and dyuan01's Oct 1 longitudinal list (line 7, <E (0, 1, 0, 0, 0, 0)). Both lists are fair game per Dennis, and #4 was on both too.
• Vendor: the string occurs once, as tm' in Eqv_v2.v Module TM7. That module proves only halts tm c0 <-> halts tm' c0, where tm = 1LB0RC_1RC0LB_0RD1RA_0LA1RE_0RA1RF_1RD--- is #4's table renamed by BCDAEF and started in #4's D. It is an equivalence with no nonhalt proof, so the machine is unclaimed.
• Parent: kill #4, 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC--- (KILLED_NONHALT; check_kill PASS on its current .v, sha256 51e3dea1…e923, 504 lines). "P§n" means section n of the parent's proof.md.
• Written for the string itself.
• Result. The twin is #4's machine with its states renamed by σ = EDBCFA (A→E, B→D, C→B, D→C, E→F, F→A), with no mirror. It starts in #4's state F, not A, so it runs a different orbit of the same macro map.
• The rules, the cycle lemma, the hexagon invariant and its proof carry over unchanged.
• Only the initial segment changes: c0 →(16,590) S(6,14,4) = Q(7,65,1,14,4), where the parent has c0 →(17,215) S(6,16,0).
• Adjusted invariant: none. The base lies in R_64, on the facet 4Y+2Z ≥ N (64 = 64), as the parent's base does.
• Evidence.
• check_proof.py: ALL CHECKS PASSED in 7 s (sections S, L, A, M, I, C, B, H, O; check_proof.out; see §6).
• rocq/plan_check.v is #4's .v with the §5 delta applied by script. It compiles in 6.7 s, and Print Assumptions nonhalt gives "Closed under the global context" (rocq/plan_check.out). It is a plan check, not the kill file, and check_kill has not been run.
• Status: CHECKPOINT_B. The informal delta is complete and validated; formalization is not done yet.
• AI assistance: written by Claude (Anthropic) under Dennis's direction.

0. The map

The twin's row σ(s) is the parent's row s with every target state t replaced by σ(t); symbols and directions are unchanged. For example, parent C1 = 1RE becomes 1Rσ(E) = 1RF, which is twin B1. check_proof.py §S searches all 720 renamings, each with and without mirroring: σ is the only map that works.

Lemma R (relabelling). For a configuration c, let σc be c with its head state renamed by σ; the tape and the head position stay the same. Then c → c′ in the parent if and only if σc → σc′ in the twin, and c is halted exactly when σc is. So every parent run c →ⁿ c′ gives a twin run σc →ⁿ σc′ of the same length, and the converse also holds.

Start. The twin's c0 is 0^inf A> 0^inf = σ(0^inf F> 0^inf). - From F, the parent writes F0 = 1RC and is at 0^inf 1 C> 0^inf after one step. - From its own start A it does A0 = 1RB, B0 = 0RC and is at 0^inf 1 0 C> 0^inf after two steps.

These are different tapes, so the twin's run is the parent's machine on a different orbit, not the parent's run. §L checks the twin from blank against the relabelled parent from 0^inf F> 0^inf in lockstep for 2·10⁶ steps: identical at every step.

Halting cell. The twin's only undefined cell is A1 = σ(F1). By Lemma R, P§4's "Why F1 is never reached" becomes this: - The twin enters A only by F1 = 1RA (= σ of the parent's E1 = 1RF), inside FR3, FR4, FE1 and FE3. - Each time, A then reads a 0.

1. What carries over unchanged

The rules in busycoq comment style, for the twin:

1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA     (= sigma of 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---, sigma = EDBCFA)

C_k(n): n in k bits MSB first, 1 -> 1010, 0 -> 0010;   A = 00111, B = 10111;  moving head <E 001 / 001 F>
P(k,n,X,z)   := 0^inf C_k(n) A^X B^z 00 B> 0^inf
Q(k,n,x,y,z) := 0^inf C_k(n) A^x 111 A^y B^z 00 B> 0^inf                    (x >= 1)

R1  P(k,n,X,z)      --> P(k,n+1,X,z+1)                     n+1 <= 2^k-1
R2  P(k,2^k-1,X,z)  --> Q(k+1,2^k+1,1,X-2,z+1)             X >= 2
R3  Q(k,n,x,y+2,z)  --> Q(k,n+3,x+2,y,z+1)                 n+3 <= 2^k-1
R4  Q(k,n,x,0,z)    --> P(k,n+z+2,x+z+1,0)                 n+z+2  <= 2^k-1
R5  Q(k,n,x,1,z)    --> P(k,n+2z+7,x+z+4,0)                n+2z+7 <= 2^k-1
R5o Q(k,n,x,1,z)    --> Q(k+1,2^k+1+3m,1+2m,x+z+2-2m,0)    m := n+2z+7-2^k >= 0,  x+z+2-2m >= 1,  3m <= 2^k-2
steps: R1 32X+32z+16t(n)+47,  R2 32X+32z+16k+61,  R3 96x+32y+32z+16(t(n)+t(n+1)+t(n+2))+197

cycle (N = 2^k):  S(k,Y,Z) := Q(k+1, N+1+3m, 1+2m, Y-2m, Z+m),  m = max(0,-Z)
  S(k,2j,Z)   -->+ S(k+1, 3j+Z,   N-3-4j-Z)
  S(k,2j+1,Z) -->+ S(k+1, 3j+3+Z, N-8-5j-2Z)
invariant (N >= 64):  8Y >= N, 8Y <= 3N, 3Z <= N, 8Z >= -N, 4Y+2Z >= N, 20Y+16Z <= 9N
start: c0 -->(16590) S(6,14,4) = Q(7,65,1,14,4)        [parent: c0 -->(17215) S(6,16,0)]

2. What changes: the initial segment (replaces P§5)

Direct simulation of the twin from the blank tape (§I). A canonical configuration is a right-edge visit in state B that parses as P or Q.

The step numbers in the "how" column are both direct-simulation values and the parent's runner step sums from 1,711 (they agree exactly, §I). The argument needs only the first and last rows: the exact 16,590-step run and its end configuration.

From step 1,711 on, every canonical configuration of the twin's run is the one the rules predict, at the predicted step: 857 of 857 to 3·10⁷ (§C).

The base, clause by clause. In the parent's Rocq coordinates the base is CfgF 5 0 14 4 = Qc 7 (3·0 + (2^6+1)) (1+2·0) 14 4. Inv 5 0 14 4 holds:

In proof.md's coordinates (N = 64, Y = 14, Z = 4), every facet of the hexagon holds, and 4Y+2Z ≥ N is tight (64 = 64). The parent's base S(6,16,0) is tight on the same facet. The cycle-lemma hypotheses also hold there: - (a) Y+2Z = 22 ≥ 1; - (b) 3⌊Y/2⌋ = 21 ≤ 62; - Y = 14 is even, so F(14,4) = (25, 29). Then (c) holds: 25 ≥ 0, 25+58 ≥ 1 and 36 ≤ 126; - (d) Z′ = 29 ≥ 1.

All of these also follow from P§4 (i), since the base is in R_64. check_proof.py §B checks each clause, and includes two negative controls: Inv 5 0 13 4 and Inv 5 0 14 3 fail.

3. The argument (complete)

Theorem. 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA does not halt from the blank tape.

1. Initial segment. The twin runs from c0 to σS(6,14,4) in exactly 16,590 steps without halting. This is a finite exact computation (§I); in Rocq it is one esx.
2. Base. (Y,Z) = (14,4) is in R_64 (§2).
3. Transfer. Take P§4's cycle lemma and the invariance of R_N under F_N (proved in P§4 (i)–(ii), with the vertex check in P§7 §5). Together they say: for k ≥ 6 and (Y,Z) ∈ R_N, the parent goes S(k,Y,Z) →⁺ S(k+1,F_N(Y,Z)), and F_N(Y,Z) ∈ R_2N. - Their statements and proofs use only the P§2 rules and arithmetic on (k,Y,Z). - By Lemma R, each parent run S →⁺ S′ is a twin run σS →⁺ σS′ of the same length. - So the same holds for the twin's configurations σS.
4. Conclusion. By induction from the base, the twin's run is an infinite chain of runs σS(k,·) →⁺ σS(k+1,·), each at least one step long. So it never halts. This is P§4's conclusion paragraph with "the run reaches S(6,16,0)" replaced by "the run reaches S(6,14,4)"; both points are in R_64. A twin run never reads A1, because by Lemma R it is the image of a parent run, which never reads F1 (P§4). ∎

Nothing in the parent's argument depends on its own orbit except P§5. The orbit statistics in P§5 and P§7 §6 (the history rows, the rule tallies) are evidence, not premises.

In the parent's .v this is visible directly: - cycle_step : Inv k i y z -> exists k' i' y' z', CfgF k i y z -->+ CfgF k' i' y' z' /\ Inv k' i' y' z' does not mention the start. - Only init (c0 -->* CfgF 5 0 16 0) and the last goal of nonhalt (Inv 5 0 16 0) do. §5 replaces exactly those two.

4. How the twin's orbit relates to the parent's (explanation, not a premise)

There is no exact coupling here, unlike #25 and #3, where one far exponent is +2 at every step. The two machines just visit different points of the same contracting map. Both stay in the hexagon, and the branch sequences differ:

• Rules used. From the base to S(14,·) (check_proof.py §O), the twin's run applies R1 5,046 times, R2 7, R3 2,025, R4 6, R5 1, R5o 1 and R4o never. Its one R5o, Q(11,1430,271,1,321) → Q(12,2142,63,532,0) at step 17,498,220, has m = 31. That is the m ≥ 1 case of the R5o domain (P§3.3), which the parent's own orbit also uses.
• Size. At 10⁹ steps the twin spans 29,054 cells (−28..29,025); the parent spans 23,607 (+23%). At 3·10⁹ the twin has 47,451 cells and 18,841 nonzeros, with no halt.

5. Formalization delta (for the Rocq stage)

Copy the parent's .v (sha256 51e3dea1f666153c9884283725e1d166428c79fc7d13216c101e567b398ee923, 504 lines) and change only the following: 1. The TM string. Change it in TM_from_str, the header and the closing comment block. 2. State names. Rename {{X}} simultaneously by σ: {{A}} → {{E}} (37 occurrences), {{C}} → {{B}} (6), {{E}} → {{F}} (35). The parent names no other state. Every es proof goes through unchanged by Lemma R. For readability, also rename <A, C> and E> in the comments. 3. init. init0 : c0 -->* 0inf <* d1 <* d0^^5 <* d1 <* bA <* <[1;1;1] <* bA^^14 <* bB^^4 <* <[0;0] {{B}}> 0inf, by esx (16,590 steps), and init : c0 -->* CfgF 5 0 14 4, by apply init0. 4. nonhalt. Start index (5,0,14,4)%nat. The final unfold Inv. cbn. lia. closes Inv 5 0 14 4; the tight clause is a <=. 5. Everything else verbatim: the counter, QC, Gad and its lemmas, Conv0/Conv1/Conv1o, Inv, cycle_step. Update the closing comment's start line.

Plan check (done). rocq/make_plan_check.py applies items 1–4 (it checks the occurrence counts, and that the parent names only A, C and E) and writes rocq/plan_check.v. It also replaces the header comment with a "plan check" note and appends Print Assumptions nonhalt.. - Compiled with rocq/compile.sh (Coq 8.20.1, unmodified busycoq 0940bb9, -native-compiler yes, ulimit -v 8000000): 6.7 s, exit 0, "Closed under the global context". - Apart from state names, it differs from the parent's .v only in the header comment, the TM string (TM_from_str and the closing comment), init0/init, the start index, two comment lines and the appended Print Assumptions.

Still to do. - Produce machines/1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA/1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v: the same content with a proper header, and with the state letters in the closing comment block renamed. - Run tools/check_kill.sh on it. Only that PASS makes this a kill. - The proof is direct on the holdout string. Eqv_v2.v TM7 is not needed.

6. Evidence (check_proof.py, 7 s, ALL CHECKS PASSED; output in check_proof.out)

The script loads the parent's check_proof.py read-only, for its abstract model: the rule words and step counts, the derivation runner, the families, S/F and the hexagon. Everything that depends on the machine or the start is run on the twin's own table.

python3 -B check_proof.py --kmax 15 extends §O one level, to S(15,9476,4529) at step 5,039,089,135: 9/9 cycle states and 43 boundaries, ALL CHECKS PASSED in 22 s (check_proof_k15.out).

7. Checkpoint B notes (Dennis)

None on file yet. Fold any notes in here before submission.