Inverse NTT outer-loop correctness #
This file contains the heavy inverse-pass outer-loop lemmas, split out from OuterLoopHelpers
to keep per-file elaboration memory bounded. The lightweight inverse infrastructure
(outerLoop_inv_inverse, ntt_sub_input_inv, the _gen structural lemmas, twiddle_inv_exp,
and the ntt_sub_input_inv_block_* lemmas) lives in OuterLoopHelpers.
theorem
radix4Inner_single_block_correct_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)
(hm_dvd : m ∣ 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_inv n q ⋯ hm_eq v (4 * b + k)) j2)
(r : Fin (2 ^ (q + 2)))
(hidx : b * 2 ^ (q + 2) + ↑r < m)
: