W4-3-sib2 / W4-3c 1RB---_1LC0LA_1LD0LC_1RE0LB_1RF0RE_1LC0RD: Rocq log

Formalization round 1 (workflow W4-3-sib2, 2026-10-12, machine DREAM)

State found at the start of the round: the kill file already existed and had a check_kill PASS (Class 2 close-out stage 2; rocq/check_kill.log, sha256 48b42caf..d1d3, 2,621 lines, compile 72.31 s, 0 assumptions, coqchk timeout at 600 s = policy A warning). submission/ holds a byte-identical copy.

What the file proves (all closed, no Admitted): - the parent W4-3's kill file verbatim with its tm renamed tmP (simulator, blocks, chain, Lemma T, left word, right-region programs, Lemma S, Inv, inv_step); - base case init28 : F;; tape0 -->* ev_cfg [] (fun _ => const S0) cfg28 (line 2386), 38 native_compute pieces (37 x 500,000 + 71,554 simulator steps = 18,571,554); - L28 / nus28 = [[18701; 6227; 2069; 683]; [233; 8; 9; 8]; [12; 1; 0; 0]; 0^4 x 3] and inv28 : Inv (C5, 2, 0, nus28); - nonhalt_P : ~ halts tmP (F;; tape0); perm_sib : Perm (flip tm) tmP phi (phi = A->F, B->A, C->B, D->C, E->D, F->E); nonhalt : ~ halts tm c0 via flip_halts + perm_halts.

This round: no edit to the .v (it is final, the package copy is byte-identical, and the sibling W4-3b's file has the same layout and wording). Re-ran check_kill on the unchanged file, as an independent second run: see check_kill_round1.log (result recorded below).

House-style check of the header: machine string, template named (verify/SBCv6.v Module TM21 outer shape, verify/Sk1like_TC_v1.v simulator idea), AI line, Checked line with the Print Assumptions result, rule-table block at the bottom, no repo-local paths (grep for vendor/ machines/ tools/ rocq/ scripts/ reports/ /home: none). One wording point left as is: the header says "Informal proof: the parent's write-up (proof.md), which covers this start (its base case)", while this machine's own proof.md is now the delta proof and the package ships the parent's as parent-proof.md. Changing it means a new sha256 for both siblings and their packages, so it is a packaging decision, not a formalization one.

Result of the round-1 re-run (rocq/check_kill_round1.log): PASS, exit 0, checked_at 2026-10-13T04:59:34Z, same sha256 48b42cafcdb8bf0653960ac7b4552c8cb99e4afe0f26623d183b8deb9020d1d3, compile 57.29 s (no other Coq job running), Print Assumptions: 0 (closed), coqchk timeout at 600 s (policy A, SKIP), integrity PASS. Warnings as before: the second TM_from_str literal (tmP), native-compiler notes. Run under ulimit -s unlimited / ulimit -v 8000000.

Packaging (workflow W4-3-sib2, 2026-10-12)

Header line 35 changed (comment only) to the house-style "Informal proof: the accompanying write-up (proof.md), which builds on the parent's write-up." diff against the audited copy (sha256 48b42caf..d1d3) shows only that line. Fresh check_kill on the final file (sha256 f9b7173d..af9b): PASS, exit 0, 2026-10-13T05:24:36Z, compile 58.9 s, 0 assumptions, coqchk timeout 600 s (policy A), integrity PASS; raw output check_kill_package.out / .log, run under ulimit -s unlimited / ulimit -v 8000000, no other Coq job running. submission/ holds a byte-identical copy.