#11b 1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---: formalization log
Round 1 (2026-10-10)
Template: kill #11's .v (1RB0LE_1RC0RC_1LD0RB_1LA0LE_1LD1LF_1LD---, sha256 8bca47b1…53c0), the nearer of the two offered: this table is #11's renamed by tau = EABCDF with no mirror, so the delta is a text substitution. #33b would also need a mirror.
Starting point: rocq/delta_check.v, from rocq/make_delta.py, which applies proof.md §5 to #11's .v. It changes:
- the TM string;
- tau on every {{X}};
- init : c0 -->* K [d1 1 10] 8 1 (732 steps, same unfold K, L0. cbn. solve_init.);
- the matching change in nonhalt;
- comments.
It had already compiled cleanly (8.4 s, closed; rocq/delta_check.out).
Kill file ../1RB0RB_1LC0RA_1LE0LD_1LC1LF_1RA0LD_1LC---.v (701 lines) = delta_check.v with two comment-only changes:
- The header is in house style:
- the machine;
- "Adapted from the proof of … (kill #11), which is the mechanism of verify/SBCv6.v, Module TM21";
- tau and the start state;
- the delta summary;
- the existing-work line "There may be existing work on this machine by hipparcos (marked done on the community sheet, not yet in busycoq).";
- the informal proof as "the accompanying write-up (proof.md, …)";
- the AI-assistance line;
- the Checked line with "busycoq BB6 (commit 0940bb9)".
- The section banner "abstract invariant (proof.md section 3)" now reads "(section 3 of #11's write-up, carried over unchanged)". This machine's proof.md §3 is the argument, not the INV statement, which lives in #11's P§3.
diff against delta_check.v past the header: only that banner line. A grep for repo-local path prefixes (vendor/ machines/ tools/ rocq/ scripts/ reports/) and for "Dennis": none. The busycoq-style rule-table block at the bottom is kept (head state A>, start K((1,1,10); 8, 1) at step 732).
check_kill (rocq/check_kill.out), run once, with ulimit -s unlimited; ulimit -v 8000000, nothing else compiling: RESULT: PASS, exit 0.
- compile 9.2 s, native;
- coqchk 1.9 s (finished, so no timeout warning);
- 0 assumptions (closed);
- 12.4 s wall in all.
File: 701 lines, sha256 7fc83eeb9bd4307bcdcc66232e79875ae4cb486b55e1695f009850be7dfc2ae3.
Not done here (not this round's files): - status.json and STATUS.md; - the submission package. Its README and write-up must carry the same hipparcos line; - the independent audit.
Kill packaging (2026-10-10)
- Audit verified on sha256
7fc83eeb…2ae3. Cosmetic finding: internal labels in comments ("kill #11", "#11's .v", "#11's text", the line-277 banner). - Comment-only fix: the header and the banner say "the parent" (line 2 keeps #11's full string), "follows the architecture of verify/SBCv6.v, Module TM21", and the informal proof is "proof.md, a delta proof that cites the parent's write-up, parent-proof.md, as P section n". A first draft quoted "the parent" in double quotes; I dropped the quotes, because Coq lexes strings inside comments. Code identical with comments stripped (a nested-comment-aware strip, then compare).
- Fresh check_kill on the final file (
ulimit -s unlimited; ulimit -v 8000000, nothing else compiling): PASS, exit 0, compile 9.17 s native, coqchk 1.79 s, 0 assumptions, 12.3 s wall. 702 lines, 756 sentences, sha256153aa11aeb194c31281cc26d9ff28cacf6868c67ea16ebdb44ce3ecbec22290a. Output:../submission/check_kill.txt; the submission copy of the .v has the same sha256.