W5-8c 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA: Rocq log

Round 1 (2026-10-13): check_kill PASS

Kill file: ../1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA.v (458 lines), sha256 8c597d875a1125131e6a9f88fe63fc994b55df1ccecaba84b2c1d29909d00584. Built from the parent's kill file (W5-8, sha256 beef54a5…cf48) by assemble.py (asserted single-match edits, adapted from W5-8b's assemble.py; no hand edits). Route of proof.md 6: Perm bridge, no flip.

What is proved

• The parent's whole development unchanged, on tmP (\btm\b -> tmP): S_step, TE, TO, T6, T8 (es'), primed versions, S_iter, DC, cc_steps(_spec), cc_steps'(_spec), rl, LR, Kr_list, Kr_cc.
• New opening for tmP from E;; tape0: init : E;; tape0 -->* Kr 1291 35 38 21 9 (6,950,830 steps), ten pieces cut at the left records 694,787 / 1,378,765 / 2,077,151 / 2,768,045 / 3,469,055 / 4,155,515 / 4,854,845 / 5,552,637 / 6,254,851 (opening_chunks.py -> chunks.txt; the script asserts that step 6,950,830 is a left record and that its configuration is Kr_list 1291 35 38 21 9 = K(2583,70,76,43,18)). Piece lengths 683,978 .. 702,214 (parent's max ~702k). First piece starts by change (E;; tape0) with (cconfig_to_config ([], [], 0, E)).
• opening : Kr 1291 35 38 21 9 -->* Ev 6649 21: the 18 follows of proof.md 6 (opening_args.py -> opening_args.txt; its K values equal proof.md 2.2's table row by row, and the arguments equal proof.md 6's list).
• nonhaltP : ~halts tmP (E;; tape0): multistep_nonhalt + progress_nonhalt_simple on (N, X) from (6649, 21).
• Bridge: phi = sigma^-1 (A->E, B->F, C->B, D->C, E->A, F->D), perm : Perm tm tmP phi (split; intros [] [] ...; cbn in *; try discriminate; reflexivity / inversion H; subst; reflexivity), nonhalt by intros H; change (halts tm (A;; tape0)) in H; exact (nonhaltP (perm_halts _ _ _ _ _ perm H)).
• Scratch compile (cc.sh, native on, 8 GB cap): 7.6 s, max RSS 0.52 GB.

check_kill: PASS (round 1, first run)

tools/check_kill.sh <kill file> 1RB0RD_0RC0LB_0RD1RD_1LE1RA_1RC1LF_---1LA under ulimit -s unlimited; ulimit -v 8000000: RESULT: PASS, exit 0 (2026-10-13T13:28:27Z). Compile 7.85 s native; coqchk -norec pass 64.8 s (inside the 600 s cap); check_kill max RSS 3.8 GB; 0 assumptions (closed under the global context). Only warning: the second TM_from_str literal (the parent's string, tmP). Log: check_kill_r1.log.

What failed

• Nothing. 6.95M direct steps in ten ~700k pieces: coqchk 64.8 s (vs 44.5 s for 4.1M in six pieces), memory unchanged at ~3.8 GB peak, so pieces of ~700k stay safe with a tape of ~5,500 cells.

Files

• assemble.py (parent .v + chunks.txt + opening_args.txt + table_comment.txt -> kill file; refuses repo-local paths), opening_chunks.py, chunks.txt, opening_args.py, opening_args.txt, table_comment.txt, cc.sh (one compile from build/cc, 8 GB cap), check_kill_r1.log.