Rocq log: 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB--- (machine #2) #

Round 1 (2026-10-10) #

Work file: rocq/work.v; compile with rocq/compile.sh <file> (temp dir, ulimit -s unlimited, ulimit -v 8000000, flock so only one coqc runs).

Proved (compiles, 3.0 s, 449 MB) #

• Inc (I1-I4) and Inc_spec : Inc r r' -> sideRLs tm h (toRC r) (toRC r').
• RIncs = proof.md's R (TM7's 10 clauses, X1/C1 with an Inc premise, plus Z1 RIncs h1 0 [D1] [LD], Z0 RIncs h1 0 [D0] [D1]).
• RIncs_spec (all 12 bullets). New segment facts: seg_hx_ld k : segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^(1+k)) ld ld, seg_h1_ld k : segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^(1+k)) [1;1;1;0] ld (both rewrite lpow_add; change; segRLs_trans; [esx | wal]). Z0/Z1 by sideRLseq_O after rewriting with z1_eq : [1] *> d1 *> 0inf = ld *> 0inf, z0_eq : [1] *> d0 *> 0inf = d1 *> 0inf (cbn; f_equal x3; symmetry; apply const_unfold).
• BigStep (TM7's proof verbatim), start : c0 -->* S' [LD;D1] (by esx).

Pitfalls hit #

• esx does not solve segRLs tm h ?ls2 d1 d0 with an evar output list; give the list explicitly (@segRLs_sideRLs_concat tm h h).
• In RIncs_spec, intro H shadows the inductive type H (hx/h1); refer to the Inc premise with eassumption, not by name.
• The hx side is [] *> ld *> X; eapply segRLs_sideRLs_concat alone unifies w1 := []. Fix the shape with (w1:=[_;_;_]) (w2:=[_;_;_]).
• Stream identities with [1] must be stated before Open Scope nat (else [1] : list nat).

Finding (simulation, for proof.md's authors) #

• Without Z0/Z1, the set image(sweep) ∩ dom(sweep) is NOT closed: s = 0LLL00LLL1LL00L011LLLLL0L0LL10LL00L000L0L10LLL1 (47 digits) has sweep(s), sweep²(s) defined and sweep³(s) undefined (the third sweep ends in count mode with 0 passes at the last digit 1). So rocq-plan.md §3.5's 3-sweep idea would have failed. With proof.md's Z0/Z1 the third sweep is defined (...11101L), and TM7-style domain closure held on 96,795/96,795 random words of 5-70 digits.

Domain lemma and nonhalt (same round): DONE #

• Added (all Qed, file compiles in 3.6 s): Inc_total, Inc_fun, RIncs_eqk, RIncs_Inc (proof.md Lemma A), RIncs_nxt_1 (TM7's, unchanged), End_1, End_x, inversion helpers inv_hx_ld/d1/d0, inv_h1_ld/d1/d0, inv_z1, Inv, key (proof.md RIncs_nxt': RIncs tp k r r1 -> forall j rK tq q, RIncs tp (k+j) r rK -> Inv tp k j tq q -> exists r2, RIncs tq q rK r2), domain (instance tp = tq = hx, k = j = q = 0), nonhalt.
• nonhalt starts from S' [LD;D1] (step 16; start by esx); the invariant is TM7's P r := exists r', RIncs hx 0 r r', initial witness [LD;LD;LD;D1;D1] built by hand (hx_ld with Inc_d1 Inc_nil, hx_d0, hx_d1, rh_2 0, rh_0).
• proof.md's case table (§3.3) matched the Coq cases one to one; no case needed a change.

Kill file #

• ../1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---.v = work.v + header comment (machine, template, AI-assistance line) + rule-table comment at the bottom.
• tools/check_kill.sh <file> 1RB0RF_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---: RESULT: PASS -- this is a kill (exit 0, 2026-10-10T11:45:36Z), sha256 3b29083b31f348bb3172c47b7e51a389b324165d9c38a073a56d9f9a760a651d, compile 3.93 s, native on, 0 assumptions (closed), coqchk pass 1.08 s.