Single-block radix-4 correctness

This file contains radix4Inner_single_block_correct, split out from OuterLoopHelpers to keep per-file elaboration memory bounded.

theorem radix4Inner_single_block_correct {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (hm_dvd : m ∣ mod64.toNat - 1) (v roots : Vector UInt32 m) (hroots : ntt_roots_correct m roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (h_dvd : 2 ^ n ∣ mod64.toNat - 1) (a : Vector UInt32 m) (ha_bnd : (a.all fun (x : UInt32) => decide (x < mod32)) = true) (len : UInt64) (hlen : len.toNat = 2 ^ (q + 1)) (b : ℕ) (hb : b < 2 ^ (n - (q + 2))) (h_inv_k : ∀ k < 4, ∀ (j2 : Fin (2 ^ q)) (hidx_k : (4 * b + k) * 2 ^ q + ↑j2 < m), ↑a[(4 * b + k) * 2 ^ q + ↑j2].toNat = ref_ntt q (↑primRoot.toNat ^ ((mod64.toNat - 1) / 2 ^ q)) (ntt_sub_input n q ⋯ hm_eq v (4 * b + k)) j2) (r : Fin (2 ^ (q + 2))) (hidx : b * 2 ^ (q + 2) + ↑r < m) : have s := len >>> 1; have i2 := (b * 2 * len.toNat).toUInt64; ↑(radix4Inner false roots s.toNat len.toNat i2.toNat s.toNat 0 a)[b * 2 ^ (q + 2) + ↑r].toNat = ref_ntt (q + 2) (↑primRoot.toNat ^ ((mod64.toNat - 1) / 2 ^ (q + 2))) (ntt_sub_input n (q + 2) hq2 hm_eq v b) r

The single-block step: applying radix4Inner for one block produces the correct ref_ntt(q+2) values at all positions in that block, reading inputs from the level-q invariant at the four input positions.