#24 1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---: Rocq log

Formalization round 1 (2026-10-10): check_kill PASS

Kill file: machines/1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---/1RB0RE_1LC0RA_1LD0LB_1LA1LF_1LE1RA_0LC---.v (1,361 lines, sha256 5dadb08f7130e5942620c4e2cbf9f455e40633327c3432e872fc163b0d297240).

check_kill: RESULT: PASS (exit 0). Native compile took 38.5 s, coqchk -norec passed in 11.6 s, and there are 0 assumptions (the isolated checker reports the theorem closed). One expected warning: tm_text: line 34: another TM_from_str literal '1RB0LD_…' (a different machine), which is the parent's table as tm3. Full output: rocq/kill.out.

How the file is built

rocq/assemble.py (run python3 -I assemble.py from rocq/) generates the whole kill file from the parent kill #3's .v. It pins the parent's sha256 91861259… and checks that each edit applies exactly once. No hand edits are made after it runs. 1. A new header. Definition tm is the twin. The parent's table becomes tm3, and the local -->*/-->+ notations are bound to tm3, so every sweep lemma, K, every macro rule, J and Jstep are the parent's, byte for byte. 2. The start, which is exactly rocq/parent_from_D.v's: Ltac solve_initD, init0 : D;; tape0 -->* K 2 [(11,12,0)] TN (1,021 steps), base with far pair (1,25,1), and init : D;; tape0 -->* K 2 base TN (78,911 steps). 3. The parent's nonhalt becomes nonhalt_D : ~ halts tm3 (D;; tape0) (same proof). After it comes the conjugacy: - phi (A->D, B->A, C->B, D->C, E->E, F->F); - perm_twin : Perm (flip tm) tm3 phi, proved by split; intros [] [] ...; cbn in * per case; - Lemma nonhalt: ~halts tm c0., by flip_halts (busycoq Flip.v), then change (halts (flip tm) (A;; tape0)), then perm_halts _ _ _ _ _ perm_twin (busycoq Permute.v), then nonhalt_D. 4. The bottom comment block: the parent family/rule table, the mirror map, and the twin's start chain.

Lemma C (conjugacy) needs no new induction

proof.md §4 planned a hand-written mu lemma of about 40-60 lines. busycoq already ships both halves: - Flip.flip_halts : halts tm c -> halts (flip tm) (flip_conf c); - Permute.perm_halts : Perm tm tm' f -> halts tm (q;; t) -> halts tm' (f q;; t).

Both are exported through Individual62 and need no axiom (Print Assumptions nonhalt is closed). flip_conf c0 reduces to A;; tape0 by conversion, because the blank tape is symmetric. Perm is closed by 12 concrete cases. Scratch test: rocq/conj_test.v, 0.7 s, closed.

What failed (small)

• perm_twin's None half failed with congruence. Fix: try discriminate; reflexivity.
• perm_twin's Some half also failed with congruence: it cannot use phi q' = phi D once q' = D because it does not compute phi D. Fix: inversion H; subst; reflexivity.

Timings (one coqc at a time, ulimit -v 8000000)

• Dev compile of the full file with -native-compiler yes: 39.3 s wall, 747 MB max RSS.
• check_kill: compile 38.5 s, coqchk 11.6 s. The parent took 67 s / 24 s with esx for its two inits; the cause of the difference was not investigated.