W5-8b 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF: Rocq log

Round 1 (2026-10-13)

Kill file: ../1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF.v, built from the parent's kill file (W5-8, sha256 beef54a5…cf48) by assemble.py (asserted single-match edits; no hand edits). Route 1 of proof.md 6 (conjugacy).

What is proved

• The parent's whole development unchanged, on tmP (= the parent's TM_from_str; \btm\b -> tmP): S_step, TE, TO, T6, T8 (es'), S_iter, DC, cc_steps(_spec), cc_steps'(_spec), rl, LR, Kr_cc.
• New opening for tmP from C;; tape0: init : C;; tape0 -->* Kr 976 17 34 22 9 (4,098,826 steps), six pieces cut at left records 696,153 / 1,398,101 / 2,094,215 / 2,795,005 / 3,495,649 (opening_chunks.py -> chunks.txt; the script asserts that the final configuration is Kr_list 976 17 34 22 9, i.e. K(1953,34,68,45,18)). Piece lengths 696,153 / 701,948 / 696,114 / 700,790 / 700,644 / 603,177 (all < 702k as in the parent). The first piece starts by change (C;; tape0) with (cconfig_to_config ([], [], 0, C)).
• opening : Kr 976 17 34 22 9 -->* Ev 6428 20: the parent's 20 follows with N 3 smaller (opening_args.py -> opening_args.txt; its K values equal proof.md 2.2's table row by row).
• nonhaltP : ~halts tmP (C;; tape0): multistep_nonhalt + progress_nonhalt_simple on (N, X) from (6428, 20).
• Bridge: phi = sigma^-1 (A->C, B->A, C->B, D/E/F fixed), perm : Perm (flip tm) tmP phi (split; intros [] [] ...; cbn in *; try discriminate; reflexivity / inversion H; subst; reflexivity), nonhalt by flip_halts + change (halts (flip tm) (A;; tape0)) + perm_halts. No flip_halts_iff, so no functional extensionality: Print Assumptions nonhalt = Closed under the global context.
• First compile (coqc, native on, 8 GB cap): exit 0, 6.4 s, max RSS 0.52 GB.

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: PASS (round 1)

tools/check_kill.sh <kill file> 1RB1LE_1LC1RD_0LA1LA_---1RE_1LF0LA_0LC0RF under ulimit -s unlimited; ulimit -v 8000000: RESULT: PASS, exit 0 on the first run (2026-10-13T12:54:59Z). sha256 7bd5af92f5c137c6355744f598e7882be3101d63ee857bbe02e970d083b326f0, 407 lines. Compile 6.5 s native; coqchk -norec pass 44.5 s (check_kill max RSS 3.7 GB); 0 assumptions (closed). Only warning: the second TM_from_str literal (the parent's string, tmP). Log: check_kill_r1.log.

What failed

• Nothing. The route needed no new lemma beyond the 9-line bridge; the parent's es' rules, S_iter, DC and the 20-follow chain compiled unchanged on tmP with the new arguments.

Packaging (2026-10-13)

• Fresh check_kill on the unchanged kill file (sha256 7bd5af92..26f0) under ulimit -s unlimited; ulimit -v 8000000: PASS, exit 0 (2026-10-13T13:00:14Z), compile 6.6 s native, coqchk pass 44.4 s, 0 assumptions. Log: check_kill_final.log; public copy with path placeholders in ../submission/check_kill.txt.