Forward NTT outer-loop: radix4Middle, outerLoop, bit-reversal, preprocessing

This file contains the larger forward-pass outer-loop lemmas split out from OuterLoopHelpers to keep per-file elaboration memory bounded.

theorem radix4Middle_advances_inv {m : ℕ} (n q : ℕ) (hq2 : q + 2 ≤ n) (hm_eq : m = 2 ^ n) (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) (hinv : outerLoop_inv n q ⋯ hm_eq v a) (len : UInt64) (hlen : len.toNat = 2 ^ (q + 1)) : have s := len >>> 1; outerLoop_inv n (q + 2) hq2 hm_eq v (radix4Middle false roots s.toNat len.toNat (m / (2 * len.toNat)) 0 a)

theorem outerLoop_len_shift (q : ℕ) (len : UInt64) (hlen : len.toNat = 2 ^ (q + 1)) (hq3 : q + 2 + 1 < 64) : (len <<< 2).toNat = 2 ^ (q + 2 + 1)

theorem outerLoop_from_inv {m : ℕ} (n q : ℕ) (hm_eq : m = 2 ^ n) (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) (hq : q ≤ n) (hinv : outerLoop_inv n q hq hm_eq v a) (len : UInt64) (hlen : len.toNat = 2 ^ (q + 1)) (hq_even : Even (n - q)) (fuel : ℕ) (hfuel : n ≤ q + 2 * fuel) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); ∀ (k : Fin m), ↑(nttInplace.outerLoop false roots a len fuel)[↑k].toNat = ref_ntt n ω (fun (j : Fin (2 ^ n)) => ↑(toMont v[Fin.cast ⋯ j]).toNat) (Fin.cast hm_eq k)