W4-2 formalization log

Kill file: machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF.v. Compile helper: rocq/cc.sh FILE.v (temp dir, ulimit -s unlimited, ulimit -v 8000000, native on). Scratch versions: rocq/t1.v .. rocq/t6.v (t6.v = kill file without header/invariant/nonhalt); t*_part.v = the pieces.

Round 1 (2026-10-11)

Design (differs from the BECv5 template on purpose; template kept for R n m, RS, the overall shape): - The left word is WS e o := wd (e+o) e o *> const 0, the word W(e,o) of proof.md (bit d of e on cell 2d, bit d of o on cell 2d+1, cell 0 read by A). wd_WS/WS_split make the padding irrelevant. - phi is an inductive relation PA e o e' o' (A scanning an E-cell) / PF (F scanning an E-cell), one constructor per digit pair (00/10/01/11). phi_spec (mutual induction via Combined Scheme) proves PA e o e' o' -> WS e o <{{A}} r -->+ WS e' o' {{B}}> r for every r. So the left step L0/L1 of proof.md is ONE lemma; everything about phi^j is then pure arithmetic on PA derivations (no TM, no sideRLs). - PAs j = j-fold iterate. bounces: PAs j x y -> K x (j+n) m -->* K y n (j+m) (L-step + RS). - No determinism of phi is ever needed: every orbit lemma constructs the derivation.

PROVED (all Qed, kill file compiles in ~5 s): - TM level: RS (es), OVe/OVo (es; OVo needs the R 0 (u+2+m) form, then es closes it), init0 (esx, 32 steps to K 1 0 0 1 = S(std,1,1)), phi_spec, bounces, OV_even, OV_odd. - Words: WS_split, WS_00/10/01/11, WS_shift, WS_1, WS_pow. - Orbits: INC_std(s), Gap(s) (SW(i) with arbitrary high bits), F_inc, F_carry, PF_inc0, PAs_dbl (phi^(2j)(Dx) = D phi^j x), PAs_dbl1 (odd version), and the general Sweep lemma: low part (c, o=2^P(2o1+1)) of h digit pairs with c < 2^(P+1) reaches 2^h*(E',O') in 2^(h+1) - 2o - c steps when PF E O E' O' (high part entered in F mode). Proof by induction on h, cases on parity of o and c, using doubling; no single-step SW lemma needed. O3-O6 are all instances of Sweep + Gaps + INC (see below). - Packed counter: pkE N := N - 2^(log2 N), pkO N := 2^(log2 N - 1), pk_eq, INC_pk(s). - Macro rules, ALL 11 (statements use l = bitlen(k)-1, b = 1+i+m; S3/P4 use l = S (h+u), v = 2^u(2g+1)): BS_S0, BS_S1a (k = 2^l), BS_S1b (2k+b >= 2^(l+2)), BS_S2 (2k+b+1 = 2^(l+2); does not need "k not a power of 2"), BS_S3a (g=0), BS_S3b (g>=1, n >= 2^(h+1)-2g), BS_P0, BS_P1, BS_P2, BS_P3, BS_P4a, BS_P4b; helpers OVoS0 (R3 reset + S0), S3_pre, P4_pre, std_ov, pk_ov, pk_ov_full. Conclusions are literally St s' shapes: std K N' 0 0 m', pk K (pkE N') (pkO N') 0 m'. - nonhalt is proved from init0 + progress_nonhalt_cond with P := I and one admitted lemma step_I.

check_kill (end of round 1): FAIL only on forbidden (the one Admitted of step_I); args, input, framework, framework_build, structure, tm_text, theorem_text all PASS. Kill file 942 lines, compiles in ~7.5 s.

OPEN (step_I is the only Admitted): 1. (DONE in round 1, kept for reference) BS_S3a/b, BS_P4a/b recipes: - S3: k = 2^(S l1)+r, 1<=r<2^l1. Sweep l1 low (0,r), Hi=(0,2), PF_inc0 2 -> (0, 32^l1) in 2^(S l1)-2r steps; then Gaps l1 (c=0,E=0,o1=1) v more steps; PAs_last splits off the last step; OV_even with a=g, c=32^h, l1=h+u -> K (32^h) g n 0; g=0: INC_stds; g>=1: Sweep h low (0,g), Hi=(3,0), PF2 1 0 2 0 (PA1 0 0 1 0 (PA0 0 0)) = PF 3 0 4 0, then INC_stds. - P4: x=(2^(S l1), r): Sweep l1 low (0,r), Hi=(2,0), PF0 1 0 -> (2^(S l1), 2^l1); Gaps l1 with E=1; split; OV_even with a = 2^h+g, c = 2^h -> K (2^h) (2^h+g) n 0; g=0: pk_eq h (32^h) + INC_pks; g>=1: Sweep h low (0,g), Hi=(1,1), PF3 0 0 0 1 (PF0 0 0) -> pk(2^(h+2)), INC_pks. 2. step_I (the only remaining work): case split of proof.md 4.2 (Lemma S) and closure 4.3 (Lemma C). Plan: decompose N with lowbit (S N) (N+1 = 2^i(2k+1)), k = 0 or highbit-style l with 2^l <= k < 2^(l+1); for pk states rewrite N into (2*(2^l+r)+1)*2^i-1 (the form BS_P use); T-position cases; for S3/P4 lowbit v. One lemma per rule: "I s -> precondition -> I s'" with all powers named (lia after Nat.pow_succ_r'). Note the statement form of St (true,N,m) is K (pkE N) (pkO N) 0 m, same as BS_P conclusions.

Tactics that worked / failed: see atlas/rocq-notes.md, section "Machine W4-2 ... round 1".

Hints for step_I (round 2)

• Shapes the BS lemmas need: std N = (2*k+1)*2^i-1; pk N = (2*(2^l+r)+1)*2^i-1 (r < 2^l) or 2^i-1 (P0, i >= 2). Get them from lowbit (S N) (S N = 2^i (2k+1)) and, for k >= 1, l := Nat.log2 k (Nat.log2_spec), r := k - 2^l. Rewrite the state with replace N with (...) before apply BS_*.
• S3/P4 need l = S (h+u): get u, g from lowbit v (v = 2r+b+1-2^(l)... see the BS statements), then h := l-1-u; prove u <= l-1 from v < 2^l via Nat.pow_lt_mono_r_iff.
• I is stated with Nat.even tests; destruct with destruct (Nat.even N) eqn:... and convert via Nat.even_spec/Nat.Even_or_Odd. Parity facts needed: N = m mod 2 (class P), T even at dirty states (u >= 1).
• Coverage order (proof.md 4.2): std k=0 -> S0; k = 2^l -> S1a; else T > 2^(l+2) -> S1b, T = 2^(l+2) -> S2, T < 2^(l+2) -> S3 (I forces i=0, class P, r < 2^(l-1), T > 3*2^l, u >= 1, n >= j0). pk: k=0 -> P0 (i>=2 from N>=2: N = 2^i-1 >= 2); r=0 -> P1; T > 2^(l+1) -> P2 (note BS_P2 needs 2^(l+1) <= 2r+b, i.e. T >= 2^(l+1)+1); T = 2^(l+1) -> P3; T < 2^(l+1) -> P4.
• For S1a vs S1b: S1b's hypothesis 2^(l+2) <= 2k+b also covers k = 2^l when b >= 2^(l+1); S1a covers k = 2^l always.

Round 2 (2026-10-11)

step_I is proved; the kill file has no Admitted. Kill file 1217 lines, compiles in ~65 s (t8.v); round-1 file kept as rocq/kill_round1_backup.v. Scratch: t7.v (first version that compiled, 350 s), t8.v (= kill file body; t8_mid.v is the new section), cct.sh = cc.sh with coqc -time.

New section "Coverage and closure" (proof.md 4.2/4.3), all Qed: - I_std/I_pk: I as pure linear arithmetic, parities as x mod 2 (lia handles nat mod 2/mod 4 directly in Coq 8.20 with Arith + ZifyNat). Proof: par (N+m); par N (destruct Nat.even with eqn, turn into mod facts via even_mod/odd_mod), then lia. - close_diag (D = 0 results), close_std/close_pk (N' = D+n with simple sufficient bounds: D <= 3 odd, or D even with the two parity-dependent bounds). - Nfacts: S N = 2^i(2k+1) -> i=0, N=2k | i=1, N=4k+1 | i>=2, (S N) mod 4 = 0, 8k+4 <= S N. Tactic nfacts destructs it with [-> ->] (substitutes i and N), then lia. - log2_facts: k >= 1 -> k = 2^l + r, r < 2^l (from Nat.log2_spec). - split_v: 1 <= v < 2^l, v even -> l = S(h+u), v = 2^u(2g+1), u >= 1, g < 2^h (lowbit + Nat.pow_lt_mono_r_iff + Nat.mul_lt_mono_pos_l). - C_S1, C_P1, C_P2 (closure of the rules whose bound needs I of the old state) and Cov_S3, Cov_P4 (coverage: I forces i=0 / i<=1, class P, r < 2^(l-1), T in the final gap, T even, n > 2^l). Each is a small standalone lemma: apply I_* in HI; set (Z := 2^l) in *; clearbody Z; nfacts ...; lia. - step_std, step_pk: lowbit (S N), k = 0 -> S0/P0; else log2_facts, replace N with ((2*(2^l+r)+1)*2^i-1), r = 0 -> S1a/P1; lt_eq_lt_dec T 2^(l+2) (std) / T 2^(l+1) (pk) -> S1b/S2/S3, P2/P3/P4. S3/P4: Cov_, split_v, then facts E1: 2^(S(h+u)) = 2(2^h2^u), HU: 22^h <= 2^h2^u, HU2 (u>=2 -> 42^h <= 2^h*2^u), pow_par h, then BS_S3a/b, BS_P4a/b + close_std/close_pk. - step_I = step_pk / step_std by destruct s as [[[|] N] m].

Speed: the first version (one big lia per closure with the full I hypothesis in context) compiled in 350 s (single lia calls up to 64 s). Moving every use of I into a small standalone lemma, and clearing I/Hk before the S3/P4 arithmetic, brought it to 65 s (largest: C_S1 17 s, C_P2 14 s).

check_kill (end of round 2): RESULT: PASS, exit 0 (log: rocq/check_kill_round2.log). All checks PASS: forbidden, structure, tm_text, theorem_text (line 1178), compile 65.5 s, tm_rocq, theorem_rocq, isolation, assumptions (Print Assumptions nonhalt: closed, 0 entries), coqchk -norec 26.3 s, integrity. sha256 of the kill file: 20521ad7e52872407bf6a03250bdd5064676def5b770fd65ab06eb49026238f1. - 2026-10-11 packaging: fresh check_kill PASS (65.8 s compile, coqchk 29.6 s), log rocq/check_kill_final.log; submission/ written.