1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA: never halts (delta proof from kill #4)

Submission copy of the working proof.md, made 2026-10-10 after the kill. The mathematics is unchanged. Only these parts were updated: the title, the header (list and sheet lines, parent pointer, evidence, status, AI line), the §5 heading and its closing paragraphs, which now say how the plan was carried out, one file mention in §6, and §7. This is a delta proof: it cites the parent's informal proof as P§n. The parent's proof is in this folder as parent-proof.md, a verbatim copy of kill #4's submission proof.md with the same section numbers. The scripts it cites (check_proof.py, check_proof.out, check_proof_k15.out, and the parent's check_proof.py) live in the working directory and are not in this folder.

• Machine: 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA, viewer https://bbchallenge.org/1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA
• Holdout list: line 17 of the 2026-10-07 holdout list (778 machines), byte for byte. Its equivalence-group member is 1RB0LC_1LC0RB_0LD1LA_0RA1LE_0LA1LF_1LD--- (line 24 of the 2026-10-07 equivalence-class file, 1,590 machines).
• 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)). Neither list is a claim, and #4 was on both too.
• busycoq: 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 (here: parent-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).
• 1RB---_0LC1RF_1LE0RD_0RB1RC_1RD0LE_0RC1RA.v (in this folder) is #4's .v with the §5 delta applied by script. check_kill (our checker) passes on it: compile 7.0 s with -native-compiler yes, Print Assumptions nonhalt closed, coqchk pass in 2.1 s (check_kill.txt).
• Status: KILLED_NONHALT (2026-10-10). The §5 delta was applied to the parent's .v, and check_kill passes on the result: 0 assumptions, coqchk pass.
• AI assistance: the informal proof and the Coq formalization were produced with the help of Claude (Anthropic), and checked by our checker, check_kill.

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 (done as planned)

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. A script applied items 1–4 (checking the occurrence counts, and that the parent names only A, C and E), replaced the header comment with a "plan check" note and appended Print Assumptions nonhalt.. - Compiled with Coq 8.20.1 against unmodified busycoq 0940bb9, -native-compiler yes: 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.

Done as planned (2026-10-10). The kill file is the plan-check code with a proper header and the state letters in the closing rule-table comment renamed by σ; a script built it from the parent's .v, asserting every substitution count. The σ-swap counts came out as predicted ({{A}} 37, {{C}} 6, {{E}} 35). Every es shift-rule proof, the gadget induction and cycle_step re-closed verbatim, and the final unfold Inv. cbn. lia. closes the tight facet. The file compiled on the first attempt, and check_kill (our checker) passed on the first run. After the σ-swap and outside comments, it differs from the parent's .v in four lines: the TM string, init0, init and the start index. Where each item lives in the .v:

Lemma R is not a premise of the formal proof: every rule is re-proved on the twin's own table by es, and Lemma R explains why those proofs re-close. So the kill rests on the .v alone; the prose here and in the parent's §3–§4 is the explanation. The proof is direct on the holdout string; Eqv_v2.v TM7 is not used.

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

None on file when this was packaged (2026-10-10).