Machine #4 1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---: Rocq log

Round 1 (2026-10-10): DONE, check_kill PASS

• Kill file: machines/1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---/1RB0LA_0RC1RD_0LD1RE_1LA0RB_0RD1RF_1RC---.v (502 lines). Compiles in about 6 s with -native-compiler yes. Print Assumptions nonhalt: Closed under the global context.
• tools/check_kill.sh exit 0: RESULT: PASS -- this is a kill, 0 assumptions, coqchk pass (2.0 s). Full output: rocq/check_kill.out, sha256 f91548736cf9715968e94b7161d9e707332b09f8a3fd7ebf653ebc8f177000d2.
• Compile helper: rocq/compile.sh file.v (copies to a temp dir as Cand.v, ulimit -v 8000000, flock, one coqc at a time).

Structure (follows proof.md; names from SBCv7 TM4)

Imports only Individual62, Arith, Lia, String (no Longitudinal). 1. 21 shift rules + D0R' (D0R shifted by 01) by es. OVL is stated as 0inf <A 001 0101 r -> 0inf 1010 001 E> 01 r so it matches the output of D1Ls. 2. Repeated rules ALs BLs ARs BRs D1Ls D0R's: manual induction + lpow_shift' (scratch pattern from proof.md 6). 3. Counter: Fixpoint ctr k n (k digits, MSB first, via Nat.div2/Nat.odd); ctr_even, ctr_odd, ctr_ones (2^k-1 = all d1), ctr_pow, ctr_ov (2^k+1 at k+1 digits); CTR by induction on k with Nat.Even_or_Odd. OV = D1Ls, OVL, D0R's, OVR, FLIP, FR3. RT (round trip, no overflow) = ALs, CTR, ARs. OVRT = ALs, OV, ARs. 4. QC (one front step: FL, RT, FR1, RT, FR2, RT, FR3, ARs) for any right side r. 5. Pc/Qc = proof.md's P/Q. R1, R1s (R1 repeated), R2, Pfin (R1s then R2, equation premises), R3. 6. Conversion gadget: Hit0/Hit1 (a reflection adding 0/1 A block), Inductive Gad G T D (T rounds, D blocks added, ending with FE0). gad_even z (FR1^(z+1), FE0), gad_odd z (FR1, FR2, (FR4, FR2)^z, FE1..FE4, FE0). - ConvNo: any Gad, no overflow -> Pc K (n+T) (a+D) 0 (gives R4 = Conv0, R5 = Conv1). - PostOV: rounds after an overflow, each a QC round plus a hit -> Qc ... y 0. - ConvOV: induction on Gad; at n = 2^(k+1)-1 the round is OVRT + hit, then PostOV (m = rounds left); otherwise RT + hit and the IH. Gives R5o = Conv1o. Generic in the gadget, so the even case would be free too. 7. Cycle index (k,i,y,z) = Qc (k+2) (3i + 2^(k+1)+1) (1+2i) y z (= proof.md S with Y = y+2i, Z = z-i, so no negative numbers). Inv = the hexagon in these coordinates + 64 <= 2^(k+1). cycle_step: y>=2 R3; y=0 Conv0+Pfin; y=1 Conv1+Pfin or Conv1o. Every side condition and the hexagon's invariance are single lia calls, with 2^(S (S k)) = 2*2^(S k) given as a hypothesis. 8. init0 by esx (17,215 steps), init : c0 -->* CfgF 5 0 16 0 by apply init0 (conversion computes ctr 7 65). nonhalt = multistep_nonhalt + progress_nonhalt_cond with index (k,i,y,z) and P = Inv.

What worked / failed

• FAILED (fixed): Require Import Lia alone does not provide Nat.div2_double; add Arith.
• FAILED (fixed): a bare 1/0 in x' = 1 or a tuple is parsed in sym_scope (S1/S0); use 1%nat, O, (5,0,16,0)%nat. Arguments of my own nat-typed definitions (Pc K n X 0, Qc ... 1 ...) are fine.
• FAILED (fixed, my slip): R2 had an extra ARs after OVRT (OVRT already moves past the A blocks).
• WORKED: Ltac fw H := eapply evstep_trans; [solve [apply H; lia] | ]. Explicit arguments where the goal's shape differs only by conversion (bA^^x <* bA vs bA^^(S x), bA^^1 vs bA, bBr^^0), e.g. fw (RT K (S n) (S x)), fw (FL (ctr K n <* bA^^x) (bBr^^z *> 0inf)): apply then only needs conversion.
• WORKED: keep configurations folded (Pc/Qc) at chain ends and close with ev_eq/prog_eq + f_equal; lia instead of matching arithmetic syntactically. Lemmas whose result indices are only constrained by premises (Pfin, Conv1o) take equation premises, so apply Pfin; lia works.
• WORKED: every proof compiled on the first full compile except the three slips above (about 6 s total).