Radix-4 inverse butterfly

Level 3g – butterfly4 inverse: structural and ZMod-level correctness.

The inverse butterfly uses negated twiddles: instead of roots[s+j2] for t1 it uses mod32 - roots[2*s - j2] (when j2 > 0) which equals -roots[2*s - j2] in ZMod (and similarly for t2, t3). Since mod64 = 3*2^30 + 1, we have primRoot^{(mod64-1)/2} = -1 in ZMod mod64, so the negated twiddle equals ω^{(mod64-1)/len * (len - j2)} * R where ω = primRoot.

theorem neg_root_zmod (r : UInt32) (hr : r.toNat < mod32.toNat) : ↑(mod32 - r).toNat = -↑r.toNat

Negation of a UInt32 < mod32 in ZMod mod32.toNat: (mod32 - r).toNat ≡ -r (mod mod32).

theorem twiddle_neg_exp_identity (m len s j2 : ℕ) (hlen : len = 2 * s) (hdvd : 2 * len ∣ m) (hj2 : j2 < s) : m / len * (s - j2) + m / 2 = m / len * (len - j2)

Key Nat arithmetic identity: when len = 2 * s and 2 * len ∣ m, m / len * (s - j2) + m / 2 = m / len * (len - j2) (for j2 < s). This is what makes the inverse twiddle computation work for t1, t2.

theorem twiddle_neg_exp_identity_t2 (m len j2 : ℕ) (hdvd : 2 * len ∣ m) (h2_dvd : 2 ∣ m) (hj2 : j2 ≤ len) : m / (2 * len) * (len - j2) + m / 2 = m / (2 * len) * (2 * len - j2)

Variant Nat arithmetic identity for the t2 twiddle (with len' = 2*len, s' = len): when 2 * len ∣ m and 2 ∣ m, m / (2 * len) * (len - j2) + m / 2 = m / (2 * len) * (2 * len - j2) for j2 ≤ len.

theorem twiddle_neg_exp_identity_t3 (m len s j2 : ℕ) (hlen : len = 2 * s) (hdvd : 2 * len ∣ m) (hj2 : j2 < s) : m / (2 * len) * (s - j2) + m / 2 = m / (2 * len) * (2 * len - s - j2)

Key Nat arithmetic identity for the t3 twiddle: when len = 2 * s and 2 * len ∣ m, m / (2 * len) * (s - j2) + m / 2 = m / (2 * len) * (2 * len - s - j2).

theorem butterfly4_inverse_getElem_pos0 {N : ℕ} (roots a : Vector UInt32 N) (s len i2 j2 : ℕ) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) (hne10 : i2 + j2 + s ≠ i2 + j2) (hne20 : i2 + len + j2 ≠ i2 + j2) (hne30 : i2 + len + j2 + s ≠ i2 + j2) : have t1 := if j2 > 0 then mod32 - roots.getD (2 * s - j2) 0 else roots.getD s 0; have t2 := if j2 > 0 then mod32 - roots.getD (2 * len - j2) 0 else roots.getD len 0; have aB := montMul a[i2 + j2 + s] t1; have aD := montMul a[i2 + len + j2 + s] t1; have P := addMod32 a[i2 + j2] aB; have R_v := addMod32 a[i2 + len + j2] aD; have t2R := montMul t2 R_v; (butterfly4 a true roots s len i2 j2)[i2 + j2] = addMod32 P t2R

theorem butterfly4_inverse_getElem_pos2 {N : ℕ} (roots a : Vector UInt32 N) (s len i2 j2 : ℕ) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) (hne12 : i2 + j2 + s ≠ i2 + len + j2) (hne32 : i2 + len + j2 + s ≠ i2 + len + j2) : have t1 := if j2 > 0 then mod32 - roots.getD (2 * s - j2) 0 else roots.getD s 0; have t2 := if j2 > 0 then mod32 - roots.getD (2 * len - j2) 0 else roots.getD len 0; have aB := montMul a[i2 + j2 + s] t1; have aD := montMul a[i2 + len + j2 + s] t1; have P := addMod32 a[i2 + j2] aB; have R_v := addMod32 a[i2 + len + j2] aD; have t2R := montMul t2 R_v; (butterfly4 a true roots s len i2 j2)[i2 + len + j2] = subMod32 P t2R

theorem butterfly4_inverse_getElem_pos1 {N : ℕ} (roots a : Vector UInt32 N) (s len i2 j2 : ℕ) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) (hne31 : i2 + len + j2 + s ≠ i2 + j2 + s) : have t1 := if j2 > 0 then mod32 - roots.getD (2 * s - j2) 0 else roots.getD s 0; have t3 := mod32 - roots.getD (2 * len - j2 - s) 0; have aB := montMul a[i2 + j2 + s] t1; have aD := montMul a[i2 + len + j2 + s] t1; have Q := subMod32 a[i2 + j2] aB; have S_v := subMod32 a[i2 + len + j2] aD; have t3S := montMul t3 S_v; (butterfly4 a true roots s len i2 j2)[i2 + j2 + s] = addMod32 Q t3S

theorem butterfly4_inverse_getElem_pos3 {N : ℕ} (roots a : Vector UInt32 N) (s len i2 j2 : ℕ) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) : have t1 := if j2 > 0 then mod32 - roots.getD (2 * s - j2) 0 else roots.getD s 0; have t3 := mod32 - roots.getD (2 * len - j2 - s) 0; have aB := montMul a[i2 + j2 + s] t1; have aD := montMul a[i2 + len + j2 + s] t1; have Q := subMod32 a[i2 + j2] aB; have S_v := subMod32 a[i2 + len + j2] aD; have t3S := montMul t3 S_v; (butterfly4 a true roots s len i2 j2)[i2 + len + j2 + s] = subMod32 Q t3S

theorem inverse_twiddle_bound {N : ℕ} (roots : Vector UInt32 N) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (len' j' : ℕ) (h2 : 2 ≤ len') (hdvd : len' ∣ N) (hj' : j' < len' / 2) (idx : ℕ) (hidx : idx < N) (heq : idx = len' / 2 + j') : (mod32 - roots[idx]).toNat < mod32.toNat

Helper: a root value at a valid NTT index is < mod32, and its negation mod32 - r is also < mod32 (because ω^e * R is nonzero in ZMod mod32.toNat).

theorem inverse_t1_zmod {N : ℕ} (roots : Vector UInt32 N) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hN_dvd : N ∣ mod64.toNat - 1) (hj2 : j2 < s) (h_idx_pos : 2 * s - j2 < N) (h_idx_pos_eq : 2 * s - j2 = s + (s - j2)) (h_idx_zero : s < N) : ↑(if j2 > 0 then mod32 - roots.getD (2 * s - j2) 0 else roots.getD s 0).toNat = ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)) * ↑montR1.toNat

theorem inverse_t2_zmod {N : ℕ} (roots : Vector UInt32 N) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hN_dvd : N ∣ mod64.toNat - 1) (hj2 : j2 < s) (h_idx_pos : j2 > 0 → 2 * len - j2 < N) (h_idx_pos_eq : 2 * len - j2 = len + (len - j2)) (h_idx_zero : len < N) : ↑(if j2 > 0 then mod32 - roots.getD (2 * len - j2) 0 else roots.getD len 0).toNat = ↑primRoot.toNat ^ ((mod64.toNat - 1) / (2 * len) * (2 * len - j2)) * ↑montR1.toNat

theorem inverse_t3_zmod {N : ℕ} (roots : Vector UInt32 N) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hN_dvd : N ∣ mod64.toNat - 1) (hj2 : j2 < s) (h_idx : 2 * len - j2 - s < N) (h_idx_eq : 2 * len - j2 - s = len + (s - j2)) : ↑(mod32 - roots.getD (2 * len - j2 - s) 0).toNat = ↑primRoot.toNat ^ ((mod64.toNat - 1) / (2 * len) * (2 * len - s - j2)) * ↑montR1.toNat

theorem inverse_t1_bound {N : ℕ} (roots : Vector UInt32 N) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hj2 : j2 < s) (h_idx_pos : 2 * s - j2 < N) (h_idx_pos_eq : 2 * s - j2 = s + (s - j2)) (h_idx_zero : s < N) : (if j2 > 0 then mod32 - roots.getD (2 * s - j2) 0 else roots.getD s 0).toNat < mod32.toNat

Helper: bound on inverse t1 value: t1.toNat < mod32.toNat.

theorem inverse_t2_bound {N : ℕ} (roots : Vector UInt32 N) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (len j2 : ℕ) (hlen_pos : len > 0) (hlen_dvd : 2 * len ∣ N) (hj2 : j2 < len) (h_idx_pos : j2 > 0 → 2 * len - j2 < N) (h_idx_pos_eq : 2 * len - j2 = len + (len - j2)) (h_idx_zero : len < N) : (if j2 > 0 then mod32 - roots.getD (2 * len - j2) 0 else roots.getD len 0).toNat < mod32.toNat

Helper: bound on inverse t2 value: t2.toNat < mod32.toNat.

theorem inverse_t3_bound {N : ℕ} (roots : Vector UInt32 N) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hj2 : j2 < s) (h_idx : 2 * len - j2 - s < N) (h_idx_eq : 2 * len - j2 - s = len + (s - j2)) : (mod32 - roots.getD (2 * len - j2 - s) 0).toNat < mod32.toNat

Helper: bound on inverse t3 value: t3.toNat < mod32.toNat.

theorem butterfly4_inverse_ZMod_pos0 {N : ℕ} (roots a : Vector UInt32 N) (ha : (a.all fun (x : UInt32) => decide (x < mod32)) = true) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len i2 j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hN_dvd : N ∣ mod64.toNat - 1) (hj2 : j2 < s) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) : ↑(butterfly4 a true roots s len i2 j2)[i2 + j2].toNat = ↑a[i2 + j2].toNat + ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)) * ↑a[i2 + j2 + s].toNat + ↑primRoot.toNat ^ ((mod64.toNat - 1) / (2 * len) * (2 * len - j2)) * (↑a[i2 + len + j2].toNat + ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)) * ↑a[i2 + len + j2 + s].toNat)

theorem butterfly4_inverse_ZMod_pos2 {N : ℕ} (roots a : Vector UInt32 N) (ha : (a.all fun (x : UInt32) => decide (x < mod32)) = true) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len i2 j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hN_dvd : N ∣ mod64.toNat - 1) (hj2 : j2 < s) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) : ↑(butterfly4 a true roots s len i2 j2)[i2 + len + j2].toNat = ↑a[i2 + j2].toNat + ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)) * ↑a[i2 + j2 + s].toNat - ↑primRoot.toNat ^ ((mod64.toNat - 1) / (2 * len) * (2 * len - j2)) * (↑a[i2 + len + j2].toNat + ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)) * ↑a[i2 + len + j2 + s].toNat)

theorem butterfly4_inverse_ZMod_pos1 {N : ℕ} (roots a : Vector UInt32 N) (ha : (a.all fun (x : UInt32) => decide (x < mod32)) = true) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len i2 j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hN_dvd : N ∣ mod64.toNat - 1) (hj2 : j2 < s) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) : ↑(butterfly4 a true roots s len i2 j2)[i2 + j2 + s].toNat = ↑a[i2 + j2].toNat - ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)) * ↑a[i2 + j2 + s].toNat + ↑primRoot.toNat ^ ((mod64.toNat - 1) / (2 * len) * (2 * len - s - j2)) * (↑a[i2 + len + j2].toNat - ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)) * ↑a[i2 + len + j2 + s].toNat)

theorem butterfly4_inverse_ZMod_pos3 {N : ℕ} (roots a : Vector UInt32 N) (ha : (a.all fun (x : UInt32) => decide (x < mod32)) = true) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len i2 j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hN_dvd : N ∣ mod64.toNat - 1) (hj2 : j2 < s) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) : ↑(butterfly4 a true roots s len i2 j2)[i2 + len + j2 + s].toNat = ↑a[i2 + j2].toNat - ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)) * ↑a[i2 + j2 + s].toNat - ↑primRoot.toNat ^ ((mod64.toNat - 1) / (2 * len) * (2 * len - s - j2)) * (↑a[i2 + len + j2].toNat - ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)) * ↑a[i2 + len + j2 + s].toNat)

theorem butterfly4_inverse_ZMod_combined {N : ℕ} (roots a : Vector UInt32 N) (ha : (a.all fun (x : UInt32) => decide (x < mod32)) = true) (hroots : ntt_roots_correct N roots) (hroots_bnd : (roots.all fun (x : UInt32) => decide (x < mod32)) = true) (s len i2 j2 : ℕ) (hlen : len = 2 * s) (hlen_dvd : 2 * len ∣ N) (hN_dvd : N ∣ mod64.toNat - 1) (hj2 : j2 < s) (hbnd0 : i2 + j2 < N) (hbnd1 : i2 + j2 + s < N) (hbnd2 : i2 + len + j2 < N) (hbnd3 : i2 + len + j2 + s < N) : have τ₁ := ↑primRoot.toNat ^ ((mod64.toNat - 1) / len * (len - j2)); have τ₂ := ↑primRoot.toNat ^ ((mod64.toNat - 1) / (2 * len) * (2 * len - j2)); have τ₃ := ↑primRoot.toNat ^ ((mod64.toNat - 1) / (2 * len) * (2 * len - s - j2)); have r := butterfly4 a true roots s len i2 j2; have A₀ := ↑a[i2 + j2].toNat; have A₁ := ↑a[i2 + j2 + s].toNat; have A₂ := ↑a[i2 + len + j2].toNat; have A₃ := ↑a[i2 + len + j2 + s].toNat; ↑r[i2 + j2].toNat = A₀ + τ₁ * A₁ + τ₂ * (A₂ + τ₁ * A₃) ∧ ↑r[i2 + len + j2].toNat = A₀ + τ₁ * A₁ - τ₂ * (A₂ + τ₁ * A₃) ∧ ↑r[i2 + j2 + s].toNat = A₀ - τ₁ * A₁ + τ₃ * (A₂ - τ₁ * A₃) ∧ ↑r[i2 + len + j2 + s].toNat = A₀ - τ₁ * A₁ - τ₃ * (A₂ - τ₁ * A₃)

Bundle the four inverse-butterfly position results into a single conjunction, mirroring butterfly4_forward_ZMod_combined.