/machines/1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---/rocq/log.md · raw

Rocq log: 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---

Formalization round 1 (2026-10-10)

Result: check_kill PASS, exit 0, on the first compile and the first check_kill run. - Kill file: 1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---.v, 1,309 lines, sha256 a12c060311a6a0b94054174d5882ac2316ec37e22b464ee475b6d30bf877128e. - check_kill: compile 54.4 s (native on), coqchk -norec 17.4 s, 0 assumptions (Print Assumptions: closed). Full output: rocq/check_kill.out. - Dev compile (temp dir in the session scratchpad, ulimit -s unlimited; ulimit -v 8000000): 52.2 s wall, max RSS 0.86 GB.

How the file was made (proof.md §5 recipe, no hand edits to proof scripts)

Source: kill #3's on-disk .v, sha256 cfa603a3…3031 (1,303 lines, check_kill PASS). 1. Simultaneous rename of {{X}} via placeholders, rho: {{A}}->{{D}}, {{B}}->{{A}}, {{D}}->{{C}}. Counts before: A 4, B 12, D 19 (C, E, F 0). After: D 4, A 12, C 19, as proof.md §5 predicted. 2. TM_from_str "1RB0RD_1RC1RF_1LD0LE_1RA0LC_1RE1LC_0RA---". 3. init0 : c0 -->* K 2 [(7,4,false)] TN (402 steps, esx; unused, kept for parallelism). 4. base := [(47,32,false); (40,33,true); (13,34,true)] (3 pairs, L* = 3); init is the parent's script, an esx over 38,732 steps. 5. J_base, Jstep, all inv_*/ob_* lemmas and nonhalt: verbatim. Checked by awk-extracting Require Import ZifyNat .. Lemma nonhalt from both files: byte-identical. 6. Comments: house-style header (rho, start state, 38,732, template line kept as "Loose template: verify/SBCv6.v, Module TM21", AI line, "Checked: ... busycoq BB6 (commit 0940bb9) ...; Print Assumptions nonhalt: Closed under the global context."), the Start section comment, and the closing rule-table block (TM line with rho, <D in K, the start line c0 -->(402) K(2; (7,4,0); -) -->(38,330) K(2; (47,32,0),(40,33,1),(13,34,1); -)). No repo-local path prefixes in the file (grep clean). - Full textual delta vs #3: rocq/delta_vs_parent3.diff (48 parent lines changed, all in comments, the 14 sweep-lemma statements + K + 3 sweep-composition statements, the TM string, init0 and base).

What failed

Nothing. Every es sweep lemma re-closed unchanged under rho (Lemma R). J_base's cbn; repeat split; lia closes the 3-pair base, including the tight clause h + 4(tv+w) + 6 = 48 >= 12w = 48.

Packaging (2026-10-10)