Rocq log: 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB (twin of #12)

Formalization round 1 (2026-10-10)

Result: 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB.v (894 lines, 980 sentences), check_kill PASS (exit 0): compile 4.1 s with native on, 0 assumptions (closed under the global context), coqchk -norec pass in 1.3 s, sha256 03cda8e9509021e918c20ac00d87da2325d44f6a40ac24f4b4bd33d81ef18940. Full output: rocq/check_kill.out. Compile helper: rocq/compile.sh (a copy of #12's; temp dir in the scratchpad, ulimit -v 8000000, NATIVE=yes for native).

Built from #12's passing .v (machines/1RB1LC_1RC1LB_1LD0RB_0LE1RD_---0LF_0LA1LF/...v) with the proof.md §8 delta. It compiled on the first attempt, with no tactic changes: 1. tm string -> 1RB1LA_1LC0RA_0LD1RC_---0LE_0LF1LE_1RF1LB (byte-identical to holdout line 676). 2. <{{A}} -> <{{F}} in tR1, tR3, tR2, tR3c and conf (sed). tR3/tR3c (R3', 4 more steps through the detour F0 F0 F1 B1 A1 A0) still close by plain es, and tR3c by rewrite (const_unfold _ S0) at 1. es.. 3. New Ep_tm2 W W' : Ep W 2 W' -> conf [] (2::2::W) -->+ conf [] (2::2::W'), placed right after Life_shape: destruct (Life_shape _ _ _ HL 2 _ eq_refl) as (W'' & E & Hc & Hm). inversion E; subst. then push0_ok (h = 2) and Life_tm _ _ _ (Hm 3 ltac:(lia)) []. 4. init : c0 -->* conf [] [2; 2; 1] by the same unfold conf, lside, rside. cbn [lpow app]. solve_init. (48 steps). 5. nonhalt: C i := conf [] (2 :: 2 :: snd i), and the step is replace (cost [] n) with 2 in HE by reflexivity. exact (Ep_tm2 _ _ HE). 6. Header comment (twin relation, delta list, AI-assistance line) and the closing rule table (R3' detour, Ep_tm2, start: ... (48 steps), top: conf [] (2::2::O_n) -->+ conf [] (2::2::O_(n+1))).

Everything else (updt, push/pop, Life, Life_tm, Ep, Ep_tm (kept, unused), Life_shape, the epoch rules, the list library, Core/Inv, step_lemma, main) is #12's text unchanged. The zero-slack point of proof.md §5 needs nothing new: step_lemma returns Ep W (cost [] n) W' with exact cost, and cost [] n = 2 by reflexivity.

Not done: packaging (status.json, notes.md Kill section, submission/) is out of scope for this round.

Packaging (2026-10-10)

Fresh check_kill run for the submission at 16:52:22Z: PASS, 17/17 checks, compile 4.2 s (native on), 0 assumptions, coqchk pass 1.3 s, same sha256 03cda8e9…ef18940 (submission/check_kill.txt). The independent audit's --json run (16:50:40Z) also passed. status.json is KILLED_NONHALT (previous version saved as rocq/status.prev.json). submission/proof.md is built from the working proof.md by rocq/make_submission_proof.py (header/status/AI lines, a §8 "Done as planned" map, the §9 gap closed). submission/parent-proof.md is #12's submission proof.md, copied verbatim because this delta proof cites it as P§n.