Inverse NTT outer-loop: radix4Middle advance, outerLoop induction

Mirrors OuterLoopHelpersForward for the inverse pass (inverse = true).

theorem inv_at_n_implies_ref_ntt_inverse {m : ℕ} (n : ℕ) (hm_eq : m = 2 ^ n) (v a : Vector UInt32 m) (hinv : outerLoop_inv_inverse n n ⋯ hm_eq v a) : have ω := ↑primRoot.toNat ^ ((mod64.toNat - 1) / m); ∀ (k : Fin m), ↑a[↑k].toNat = ref_ntt n ω⁻¹ (fun (j : Fin (2 ^ n)) => ↑v[Fin.cast ⋯ j].toNat) (Fin.cast hm_eq k)

When outerLoop_inv_inverse holds at q = n, the array computes the DFT with ω⁻¹.

theorem radix4Middle_advances_inv_inverse {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_inverse n q ⋯ hm_eq v a) (len : UInt64) (hlen : len.toNat = 2 ^ (q + 1)) : have s := len >>> 1; outerLoop_inv_inverse n (q + 2) hq2 hm_eq v (radix4Middle true roots s.toNat len.toNat (m / (2 * len.toNat)) 0 a)

theorem outerLoop_from_inv_inverse {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_inverse 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 true roots a len fuel)[↑k].toNat = ref_ntt n ω⁻¹ (fun (j : Fin (2 ^ n)) => ↑v[Fin.cast ⋯ j].toNat) (Fin.cast hm_eq k)