Rocq log: 1RB1RF_1LC0LE_1RD0LB_1RA0RC_1RE1LB_0RD--- (machine #25)
Round 1 (2026-10-10)
Result: check_kill PASS, exit 0 (full report in rocq/kill.out). Checked at 2026-10-10T16:57:17Z:
- compile 69.3 s, native on;
- coqchk -norec passed in 24.6 s, no timeout;
- Print Assumptions of nonhalt: closed, 0 assumptions;
- 1,305 lines, 1,484 sentences, sha256 766d227080425b8550e793e3f13cacf99bae3d7626a6b17b490cce51d7f979fc.
How the file was made (proof.md §5 delta, applied mechanically)
The source was the parent kill file machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/…---.v
(sha256 91861259…fcbf). A Python script made these changes, each asserting exactly one match:
1. A new header comment. It keeps the house-style disclosure line.
2. A simultaneous σ-swap of the state names in the whole body, by regex over {{X}}: A→C, B→D, D→B (C→A
would also apply, but C does not occur).
- Parent counts A 4, B 12, D 19; twin counts C 4, D 12, B 19, as proof.md §5 predicts.
- Only the 14 es sweep lemmas and K name states.
3. The TM string.
4. init0 : c0 -->* K 2 [(11,13,false)] TN, 1,088 steps.
5. base: last pair (1, 26, true) instead of (1, 24, true).
6. The closing rule-table comment: <C replaces <A, and the start line now reads
c0 -->(1,088) K0' -->(78,026) B'.
Unchanged: every es proof, the macro rules, J/PN/PI/TC, every ob_*/inv_* lemma, Jstep,
the J_base script (cbn; repeat split; lia, which closed with q_4 = 26), init (esx, now
79,114 steps) and nonhalt.
Compiles
rocq/cc.shdev compile, native on: rc = 0 in 66.5 s, first try. No edits were needed after it.tools/check_kill.sh: PASS on the first run.
What failed
Nothing. Lemma R from proof.md (σ maps transitions to transitions) is why the es proofs re-close
verbatim. The base differs only in q_4, and J_base's arithmetic absorbs it.
Packaging (2026-10-10)
- Fresh check_kill for the submission, 17:02:48Z, on the same sha256
766d2270…79fc: PASS, exit 0, 17/17 checks, compile 68.6 s (native on), coqchk 24.6 s, 0 assumptions, 97 s wall. Output:rocq/check_kill_submission.out, copied tosubmission/check_kill.txt. rocq/make_submission_proof.pybuildssubmission/proof.mdfrom the working proof.md, which it leaves untouched. Each edit asserts exactly one match.submission/parent-proof.mdis a verbatim copy of #3'ssubmission/proof.md.