W5-1 formalization log (rocq/log.md)

Round 1 (2026-10-13)

• Kill file built from rocq/plan_check_full.v (sha256 3197daf2..., the round-1 skeptic's plan check of proof.md 8, which compiled with -native-compiler no in 65.5 s, closed). Plan-check files left untouched.
• Edits on the copy (formal-stage items 1 and 9 of proof.md 8):
• header comment replaced: 349's string, tmP and f349, "Adapted from verify/BECv5.v, Module TM1 / Module TM2 (the same table as tmP except F1)", the detour change, initF, the conjugacy, disclosure line, Checked line; no repo-local paths;
• comment refs updated to this proof.md (macro rules 3.4 -> 3.6);
• three short comments added (before TF2: the detour; before solve_initF; before tm: the conjugacy);
• trailing Print Assumptions nonhalt. removed;
• closing busycoq-style rule-table comment block = proof.md 1, adapted (TP -> tmP, internal labels dropped).
• No proof script changed relative to the plan check.
• check_kill (2026-10-13T09:08:08Z): PASS, exit 0 (rocq/check_kill_r1.log). File sha256 32cbc5c17ddb0b7e094514fe5f9130a9ef0ec09919c17838b3472134f60e4e88, 1,278 lines; compile 64.0 s with -native-compiler yes; coqchk -norec pass in 26.7 s; Print Assumptions nonhalt: closed (0 assumptions), which is what the header's Checked line says. Only warning: the second TM_from_str literal (tmP, a different machine), expected. Peak RSS of the whole run 1.2 GB.
• Nothing open for the formal stage.

Packaging (2026-10-13)

• Fresh check_kill on the unchanged kill file (sha256 32cbc5c1…4e88): PASS, exit 0, 09:13:45Z; compile 64.1 s with -native-compiler yes, coqchk -norec pass 27.2 s, 0 assumptions. Verbatim output = submission/check_kill.txt.
• submission/ built (the .v copied byte for byte; proof.md, README.md, discord.md written). No .v edits.