Rocq log: 1RB0RA_1LC0LD_1LE1LD_0LB0RE_1RF0LA_---0RA (#7)

Formalization round 1 (2026-10-10, machine DREAM)

Result: check_kill PASS (exit 0, 17/17) on the kill file [local working file] - sha256 dfb0fb2c8b2ab8a0d302bd3b271f7d81964d9e6e3baa710eef79e0036f700f28, 1,790 lines, 2,028 sentences. - Compile 15.1 s (native on), coqchk -norec 66.1 s, Print Assumptions nonhalt: closed (0 assumptions). - Only warning: the second TM_from_str literal (tm30, the parent), as expected. - Full log: rocq/check_kill.out.

What the file is

Built from the scratch draft rocq/M7_draft.v (sha256 3de5d2f4…92e5, itself a PASS) by asserted single-match edits (script in the session scratchpad, build.py): 1. Header rewritten for #7 in house style: the machine, the conjugacy phi (A->E, B->A, C->B, D->F, E->C, F->D, mirror), start E, the delta list (tm30, init7, fin7/inv7, nonhalt_from_c/nonhalt_E, perm7 + flip_halts/perm_halts), the parent cited as "the kill for 1RB0RF_1RC1RF_1LD0RE_---0LE_1LA0LE_0RA0LC", Adapted-from line (the parent kill, which follows verify/FractalBEC.v, tm10), a note that write-up section numbers in comments are the parent's, AI line, Checked line. No repo-local paths, no double quotes in comments. 2. Section 4: the parent's init : c0 -->* K 8 t2 replaced in place by solve_initE + init7 : E;; tape0 -->* K 17 t1 (1,114 steps; comment gives L(16,0001) at 1059 and both tapes in #7's own frame, re-simulated this round). 3. Section 11: the parent's B694/Y694/fin694/inv694 dropped (they were about the parent's start); B692/Y692/fin7/inv7 in their place; finite-part banner updated. The tail (nonhalt_from_c, nonhalt_E, phi, perm7, nonhalt) is the draft's. 4. Bottom comment block: both tables side by side, the bridge, the parent's hub/record/pre-record, the start in both frames, the finite part.

Audit

• Comment-stripped diff against the parent's kill file: the only removed code lines are the tm definition and the three notations on tm, init, B694/Y694/fin694/inv694, nonhalt_from, nonhalt. Everything else is verbatim.
• Dropping the parent's fin694 (a second 691-epoch vm_compute) halves coqchk: 127 s for the draft, 66 s now.

Open (not this file)

• status.json / STATUS.md still describe the draft; submission package (submission/proof.md with writeup_lint, README) not built; joint submission with W4-1 per proof.md Δ6 item 6.