W5-3 formalization log

Kill file: machines/1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC/1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC.v. Compile helper: rocq/cc.sh FILE.v (temp dir, ulimit -s unlimited, ulimit -v 8000000, native on). Scratch versions: rocq/t1.v (low-level rules) .. rocq/t4.v (whole proof + Print Assumptions). The kill file is t4.v with comment-only edits (header, section comments, closing rule table) and the trailing Print Assumptions removed, built by rocq/mkkill.py (python3 mkkill.py <out.v>).

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

check_kill: RESULT: PASS -- this is a kill, exit 0 (log rocq/check_kill_round1.log). Compile 3.2 s native, coqchk -norec 1.0 s, Print Assumptions nonhalt: Closed under the global context. Kill file 530 lines, sha256 75932a97949d61ba11f16e0b8a6d0d6adf05f2e1a63231b44f0acddf0661da1a.

Design (proof.md section 8, H form; template BECv5 TM1 for the architecture only, no Longitudinal/sideRLs): - C n := BinInc [1;1] n; HF l r := l <{{E}} [1;0;1;1] *> r (the write-up's G form after TS); EC p N := HF (0inf <* [0;1]^^p) (C N) (= E(p,N)). Not named S (nat successor) or H. - Every count = a left lemma (L1, L0, L011, all es) + a right lemma packaged as Inc r r' := forall l, l <* [1;1;0;1] {{A}}> r -->+ HF l r'. - RIncG (A over (11)^n, CARRY, TS): es. RInc = RBinInc_spec with qR = [1;1;0;1], qL = [1;0;1;1]. - Inc00 r : Inc ([0;0] *> r) ([1;1] *> r) (RIncG with n = 0) for the Q counter in M4/M5 (b). - IncQ k x y : S x < 2^k -> Inc (Q k x y) (Q k (S x) y) for the misaligned counter Q k x y := Dk k x *> [0] *> C y, Dk a Fixpoint (low digit first). Dk_inc (exists t rest, ...) by induction on k; Dk_0, Dk_1, Dk_full, Dk_even, Dk_odd. - Cnt1/Cnt0/Cnt011: left lemma + any Inc. - Eat: LEat (EB, EAT0 C/F sweep, CS) on 0inf <* [0;1]^^b: es. Y rules Y1C (C(2n+1)), Y2C (C(4n)), Y3 v s r (generic right side), Y4 v m, Y1Q; ROvf (A over (11)^j, A01, A1s(2), RInc). All es (+ RInc where the counter is abstract). - Walks: W2 (two Inc hypotheses), Wk (W(a,b) on C, lt_wf_ind, result exponent a+b+a mod 2), W2Q (W2 iterated i times on Q, block written [0;1;0;1]^^i), Bk (B(s), block [1;1]^^s <* [1]), W0k (W0(c,d), block [0;1] <* [0;1;0;1]^^c). - Macro rules: BS1 (N = n2+1), BS2 (n4), BS3 (((m2+1)2^1-1)*2), BS4 (2^2), BS5 (2^(S(S(S t))), hypothesis 2^(S t) <= p+7). C_split : C (((m*2+1)*2^i-1)*2) = [0;0] *> [1;1]^^i *> [0;0] *> C m (BinInc_mul2 + BinInc_mulpow2sub1). - init : c0 -->* EC 2 4: replace (C 4) with ([0;0;0;0;1;1] *> 0inf) by reflexivity, change ([0;1]^^2) with [0;1;0;1], solve_init (171 steps). - step_J: coverage + closure of J(p,N): 1 <= N <= 2p. Split Nat.Even_or_Odd N, then of N/2, then lowbitS_cases K' for N = 4K'+2 (i = 0: M3, 1: M4, S (S i): M5); M5 arithmetic with T := 2^i, x <= x*T by nia, then lia. nonhalt: multistep_nonhalt + progress_nonhalt_cond over nat*nat.

Compile errors met and fixed (all quick): - Dk_inc: applied IH at S a instead of a (lia "Cannot find witness" on a false bound). - Wk, case a = 1: used pt3 where the equality had to come first; added pt_pre. - W2Q: f_equal; f_equal; lia split S (S x) + 2*i = x + 2*S i into false goals; use lia_refl. - Bk: wrong left context for Cnt1 ([1] vs [1;1]); the unification error was genuine. - BS5: rewrite Nat.pow_succ_r' in * destroyed the 2^i pattern C_split needs; rewrite only Hp. eapply pt_eq + instantiate -> "Not enough uninstantiated existential variables"; pt3 is right. !Str_app_assoc with nothing to rewrite fails; dropped.

Open: nothing for the kill. Packaging (submission files, status.json, STATUS.md) is outside this round.

Packaging (2026-10-13)

Fresh check_kill PASS on the unchanged kill file (sha256 75932a97…, 10:09:16Z, compile 3.4 s, coqchk 1.0 s); output verbatim in submission/check_kill.txt. status.json -> KILLED_NONHALT / done. No edits to the .v.