W5-8 1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF: Rocq log

Round 1 (2026-10-13): check_kill PASS

Kill file: ../1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF.v (361 lines), sha256 beef54a54f6272e70cf2c6a90bd81a899416bd572ecc84431a685ed38cbacf48. check_kill (under ulimit -s unlimited; ulimit -v 8000000): PASS, exit 0; compile 6.5 s native, coqchk -norec pass 45.1 s (max RSS 3.3 GB), 0 assumptions (closed under the global context). Log: check_kill_final.log.

What is proved (all of proof.md section 8, as planned)

• Kr n a b c d = K(2n+1,2a,2b,2c+1,2d), Ev N X = Kr N (4X+26) (2X+32) 17 9 = Even(2N+1, 8X+52).
• S_step, TE, TO, T6, T8: each one es' with the statements of proof.md 8 verbatim. vm_compute 0.04 s (S) and 0.21-0.26 s (each collision, ~550k-600k concrete steps); no destruct needed for S (the d split of the write-up's executor does not arise: es' rotates blocks). Negative control: S with 6+b in place of 5+b fails. So es' finds the shift rules by itself. Probable mechanism for R2b (read from the ES_v3 source, not instrumented): after R1 the left side is [0;1]^^k *> 0 >> ..; rw_lpow_rotate turns it into 0 >> [1;0]^^k *> .. because the cell left of the block is a 0 (the write-up's 0-on-the-left condition); three concrete steps later the head is in the phase [1;0]^^k <F [0;0] and try_sr finds the 12-step rule (01) <F 00 -> <F 00 11 (context 2).
• S_iter (induction + follow), DC (four follows + prog_eq with lia_refl), opening (20 follows with explicit arguments from opening_args.py), nonhalt by multistep_nonhalt + progress_nonhalt_simple on (N, X).
• init : c0 -->* Kr 979 17 34 22 9 (4,097,897 steps), in six pieces, see below.

What failed and why

• FAILED (coqchk, memory): init as one piece. Bouncer_v3-style multistep_c' + native_check_eq compiles in 0.7 s (VM variant 1.0 s), but coqchk -norec re-checks the cast by lazy kernel conversion and died with Fatal error: out of memory at 7.1 GB after 20 s (cap 8 GB). Same with busycoq's list configurations (cconfig_step) and with a hand-written strict step function: coqchk memory is linear in the steps of one conversion (~2.7 KB per step: 100k steps 0.37 GB, 400k steps 1.15 GB, lazy and strict alike), time ~7 us per step.
• WORKED: cut the run at five left records (steps 694,884 / 1,397,500 / 2,099,620 / 2,790,296 / 3,493,040), chosen by opening_chunks.py (cconfig semantics replicated in Python; left records have l = [], m = 0, state F and a short run-length word, 15-20 pairs). Each piece is cc_steps'_spec n1 1000 n3 + vm_compute; reflexivity on LR W_k = cconfig_to_config ([], rl W_k, 0, F); the last one targets Kr_cc. coqchk then needs at most 3.3 GB.

Files

• t1.v, t2.v: first drafts (t2 = whole proof with a one-piece init; compiles, fails coqchk).
• c_S.v, c_TE.v, c_init.v, c_init2.v, c_lazy400.v, c_strict400.v: coqchk bisection tests.
• cc.sh (compile one file from a temp dir, 8 GB cap), chk.sh (compile + coqchk -norec).
• opening_args.py (lemma arguments of the 20 opening rows), opening_chunks.py / chunks.txt (left-record checkpoints of the 4,097,897-step run).