Additive NTT Intermediate Objects

Intermediate quotient-chain polynomials, intermediate novel bases, and the intermediate evaluation polynomials used by the Additive NTT recursion.

2. Intermediate Novel Polynomial Bases Xⱼ⁽ⁱ⁾ and evaluation polynomials P⁽ⁱ⁾

noncomputable def AdditiveNTT.intermediateNormVpoly {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {k : ℕ} (h_k : ↑i + k ≤ ℓ) : Polynomial L

The k-step subspace-vanishing polynomial Ŵₖ⁽ⁱ⁾.

i : Fin r is a loose index and h_k : i + k ≤ ℓ supplies its NTT-level bound. For k = 0 this is X; otherwise it is q⁽ⁱ⁺ᵏ⁻¹⁾ ∘ ⋯ ∘ q⁽ⁱ⁾.

theorem AdditiveNTT.intermediateNormVpoly_eval_is_linear_map {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {k : ℕ} (h_k : ↑i + k ≤ ℓ) : IsLinearMap 𝔽q fun (x : L) => Polynomial.eval x (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate i h_k)

theorem AdditiveNTT.base_intermediateNormVpoly {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (k : Fin r) (h_k : ↑k ≤ ℓ) : intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate 0 ⋯ = normalizedW 𝔽q β k

theorem AdditiveNTT.natDegree_intermediateNormVpoly {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {k : ℕ} (h_k : ↑i + k ≤ ℓ) : (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate i h_k).natDegree = 2 ^ k

The natDegree of Ŵₖ⁽ⁱ⁾(X) is 2^k.

theorem AdditiveNTT.degree_intermediateNormVpoly {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {k : ℕ} (h_k : ↑i + k ≤ ℓ) : (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate i h_k).degree = 2 ^ k

The degree of Ŵₖ⁽ⁱ⁾(X) is 2^k.

theorem AdditiveNTT.Polynomial.foldl_comp {L : Type u} [Field L] (n : ℕ) (f : Fin n → Polynomial L) (initInner initOuter : Polynomial L) : Fin.foldl n (fun (acc : Polynomial L) (j : Fin n) => (f j).comp acc) (initOuter.comp initInner) = (Fin.foldl n (fun (acc : Polynomial L) (j : Fin n) => (f j).comp acc) initOuter).comp initInner

theorem AdditiveNTT.intermediateNormVpoly_comp_qmap {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {destIdx : Fin r} (h_destIdx : ↑destIdx = ↑i + 1) (k : ℕ) (h_k : ↑i + k + 1 ≤ ℓ) : intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate i h_k = (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate destIdx ⋯).comp (qMap 𝔽q β i ⋯)

If i < ℓ and i + k + 1 ≤ ℓ, then Ŵₖ₊₁⁽ⁱ⁾ = Ŵₖ⁽ⁱ⁺¹⁾ ∘ q⁽ⁱ⁾.

theorem AdditiveNTT.intermediateNormVpoly_comp {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {destIdx : Fin r} {k l : ℕ} (h_destIdx : ↑destIdx = ↑i + k) (h_k : ↑i + k ≤ ℓ) (h_l : ↑i + k + l ≤ ℓ) : intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate i ⋯ = (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate destIdx ⋯).comp (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate i h_k)

noncomputable def AdditiveNTT.iteratedQuotientMap {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {destIdx : Fin r} {k : ℕ} (h_destIdx : ↑destIdx = ↑i + k) (h_destIdx_le : ↑destIdx ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)) : ↥(sDomain 𝔽q β h_ℓ_add_R_rate destIdx)

Maps a point from sDomain i to sDomain destIdx by a k-step quotient map.

i and destIdx are loose Fin r indices. h_destIdx identifies the destination as i + k, and h_destIdx_le supplies the NTT-level bound.

theorem AdditiveNTT.iteratedQuotientMap_congr_k {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {destIdx : Fin r} {k₁ k₂ : ℕ} (hk : k₁ = k₂) (h_destIdx₁ : ↑destIdx = ↑i + k₁) (h_destIdx₂ : ↑destIdx = ↑i + k₂) (h_destIdx_le : ↑destIdx ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)) : iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i h_destIdx₁ h_destIdx_le x = iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i h_destIdx₂ h_destIdx_le x

theorem AdditiveNTT.iteratedQuotientMap_succ_comp {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {midIdx destIdx : Fin r} (steps : ℕ) (h_midIdx : ↑midIdx = ↑i + 1) (h_destIdx : ↑destIdx = ↑i + (steps + 1)) (h_destIdx_le : ↑destIdx ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)) : iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i h_destIdx h_destIdx_le x = iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate midIdx ⋯ h_destIdx_le (iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i h_midIdx ⋯ x)

Composing one quotient step with a steps-step quotient map equals the steps + 1 step quotient map.

theorem AdditiveNTT.qMap_eval_mem_sDomain_succ {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {destIdx : Fin r} (h_destIdx : ↑destIdx = ↑i + 1) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)) : Polynomial.eval (↑x) (qMap 𝔽q β i ⋯) ∈ sDomain 𝔽q β h_ℓ_add_R_rate destIdx

The evaluation of qMap on an element from sDomain i belongs to sDomain (i+1). This is a key property that qMap maps between successive domains.

theorem AdditiveNTT.iteratedQuotientMap_k_eq_1_is_qMap {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) {destIdx : Fin r} (h_destIdx : ↑destIdx = ↑i + 1) (h_destIdx_le : ↑destIdx ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)) : iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i h_destIdx h_destIdx_le x = ⟨Polynomial.eval (↑x) (qMap 𝔽q β i ⋯), ⋯⟩

When k = 1, iteratedQuotientMap reduces to evaluating qMap directly. This shows that iteratedQuotientMap with k = 1 is equivalent to the single-step quotient map.

theorem AdditiveNTT.getSDomainBasisCoeff_of_sum_repr {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) [NeZero R_rate] (i : Fin r) (h_i : ↑i ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩)) (x_coeffs : Fin (ℓ + R_rate - ↑i) → 𝔽q) (hx : ↑x = ∑ j_x : Fin (ℓ + R_rate - ↑i), x_coeffs j_x • ↑((sDomain_basis 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ ⋯) j_x)) (j : Fin (ℓ + R_rate - ↑i)) : ((sDomain_basis 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ ⋯).repr x) j = x_coeffs j

theorem AdditiveNTT.getSDomainBasisCoeff_of_iteratedQuotientMap {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) [NeZero R_rate] (i : Fin r) (k : ℕ) {destIdx : Fin r} (h_destIdx : ↑destIdx = ↑i + k) (h_destIdx_le : ↑destIdx ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)) : have y := iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i h_destIdx h_destIdx_le x; ∀ (j : Fin (ℓ + R_rate - ↑destIdx)), ((sDomain_basis 𝔽q β h_ℓ_add_R_rate destIdx ⋯).repr y) j = ((sDomain_basis 𝔽q β h_ℓ_add_R_rate i ⋯).repr x) ⟨↑j + k, ⋯⟩

noncomputable def AdditiveNTT.sDomain.lift {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i j : Fin r) (h_j : ↑j < ℓ + R_rate) (h_le : i ≤ j) (y : ↥(sDomain 𝔽q β h_ℓ_add_R_rate j)) : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)

Lifts a point y from a higher-indexed domain sDomain j to the canonical base point of its fiber in a lower-indexed domain sDomain i, by retaining all coeffs for the corresponding basis elements

theorem AdditiveNTT.basis_repr_of_sDomain_lift {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i j : Fin r) (h_j : ↑j < ℓ + R_rate) (h_le : i ≤ j) (y : ↥(sDomain 𝔽q β h_ℓ_add_R_rate j)) : have x₀ := sDomain.lift 𝔽q β h_ℓ_add_R_rate i j h_j h_le y; ∀ (k : Fin (ℓ + R_rate - ↑i)), ((sDomain_basis 𝔽q β h_ℓ_add_R_rate i ⋯).repr x₀) k = if hk : ↑k < ↑j - ↑i then 0 else ((sDomain_basis 𝔽q β h_ℓ_add_R_rate j h_j).repr y) ⟨↑k - (↑j - ↑i), ⋯⟩

Applying the forward map to a lifted point returns the original point.

theorem AdditiveNTT.intermediateNormVpoly_comp_qmap_helper {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (k : Fin (ℓ - (↑i + 1))) : (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ ⋯).comp (qMap 𝔽q β ⟨↑i, ⋯⟩ ⋯) = intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ ⋯

A helper form of intermediateNormVpoly_comp_qmap for the strict stage i < ℓ and the remaining basis index k.

noncomputable def AdditiveNTT.intermediateNovelBasisX {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (j : Fin (2 ^ (ℓ - ↑i))) : Polynomial L

∀ i ∈ {0, ..., ℓ}, The i-th order novel polynomial basis Xⱼ⁽ⁱ⁾. Xⱼ⁽ⁱ⁾ := Π_{k=0}^{ℓ-i-1} (Ŵₖ⁽ⁱ⁾)^{jₖ}, ∀ j ∈ {0, ..., 2^(ℓ-i)-1}

theorem AdditiveNTT.base_intermediateNovelBasisX {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (j : Fin (2 ^ ℓ)) : intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate 0 ⋯ j = Xⱼ 𝔽q β ℓ ⋯ j

theorem AdditiveNTT.intermediateNovelBasisX_zero_eq_one {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) : intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate i h_i ⟨0, ⋯⟩ = 1

theorem AdditiveNTT.degree_intermediateNovelBasisX {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (j : Fin (2 ^ (ℓ - ↑i))) : (intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate i h_i j).degree = ↑↑j

The degree of an i-th order novel polynomial basis element Xⱼ⁽ⁱ⁾(X) is exactly j. Somewhat similar to proof of degree_Xⱼ.

theorem AdditiveNTT.even_index_intermediate_novel_basis_decomposition {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (j : Fin (2 ^ (ℓ - ↑i - 1))) : intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate i ⋯ ⟨↑j * 2, ⋯⟩ = (intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ ⋯ ⟨↑j, ⋯⟩).comp (qMap 𝔽q β i ⋯)

X₂ⱼ⁽ⁱ⁾ = Xⱼ⁽ⁱ⁺¹⁾(q⁽ⁱ⁾(X)) for i < ℓ and j < 2^(ℓ - i - 1).

theorem AdditiveNTT.odd_index_intermediate_novel_basis_decomposition {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (j : Fin (2 ^ (ℓ - ↑i - 1))) : intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate i ⋯ ⟨↑j * 2 + 1, ⋯⟩ = Polynomial.X * (intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ ⋯ ⟨↑j, ⋯⟩).comp (qMap 𝔽q β i ⋯)

X₂ⱼ₊₁⁽ⁱ⁾ = X * Xⱼ⁽ⁱ⁺¹⁾(q⁽ⁱ⁾(X)) for i < ℓ and j < 2^(ℓ - i - 1).

noncomputable def AdditiveNTT.intermediateEvaluationPoly {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : Polynomial L

∀ i ∈ {0, ..., ℓ}, The i-th order evaluation polynomial P⁽ⁱ⁾(X) := ∑_{j=0}^{2^(ℓ-i)-1} coeffsⱼ ⋅ Xⱼ⁽ⁱ⁾(X) over the domain S⁽ⁱ⁾. where the polynomial P⁽⁰⁾(X) over the domain S⁽⁰⁾ is exactly the original polynomial P(X) we need to evaluate, and coeffs is the list of 2^(ℓ-i) coefficients of the polynomial.

theorem AdditiveNTT.degree_intermediateEvaluationPoly_lt {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : (intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate i h_i coeffs).degree < 2 ^ (ℓ - ↑i)

noncomputable def AdditiveNTT.intermediateBasisVectors {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) : Fin (2 ^ (ℓ - ↑i)) → ↥(Polynomial.degreeLT L (2 ^ (ℓ - ↑i)))

The basis vectors for the intermediate level i.

@[reducible, inline]

abbrev AdditiveNTT.IntermediateCoeffVecSpace {r : ℕ} {L : Type u} {ℓ : ℕ} (i : Fin r) : Type u

The vector space of coefficients for polynomials of degree < 2^(ℓ-i).

def AdditiveNTT.intermediateToCoeffsVec {r : ℕ} {L : Type u} [Field L] {ℓ : ℕ} (i : Fin r) : ↥(Polynomial.degreeLT L (2 ^ (ℓ - ↑i))) →ₗ[L] IntermediateCoeffVecSpace i

The linear map from polynomials (in the subtype) to their coefficient vectors at level i.

noncomputable def AdditiveNTT.intermediateChangeOfBasisMatrix {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) : Matrix (Fin (2 ^ (ℓ - ↑i))) (Fin (2 ^ (ℓ - ↑i))) L

The Change-of-Basis Matrix from the Intermediate Novel Basis to the Monomial Basis. A_jk = coeff of X^k in intermediate basis vector X_j.

theorem AdditiveNTT.intermediateChangeOfBasisMatrix_lower_triangular {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) : (intermediateChangeOfBasisMatrix 𝔽q β h_ℓ_add_R_rate i h_i).BlockTriangular ⇑OrderDual.toDual

theorem AdditiveNTT.intermediateChangeOfBasisMatrix_diag_ne_zero {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (j : Fin (2 ^ (ℓ - ↑i))) : intermediateChangeOfBasisMatrix 𝔽q β h_ℓ_add_R_rate i h_i j j ≠ 0

theorem AdditiveNTT.intermediateChangeOfBasisMatrix_det_ne_zero {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) : (intermediateChangeOfBasisMatrix 𝔽q β h_ℓ_add_R_rate i h_i).det ≠ 0

@[reducible]

noncomputable def AdditiveNTT.intermediateChangeOfBasisMatrix_invertible {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) : Invertible (intermediateChangeOfBasisMatrix 𝔽q β h_ℓ_add_R_rate i h_i)

The intermediate change-of-basis matrix is invertible.

noncomputable def AdditiveNTT.monomialToINovelCoeffs {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (monomial_coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : Fin (2 ^ (ℓ - ↑i)) → L

Convert monomial coefficients to novel coefficients at level i. n = m * A⁻¹

noncomputable def AdditiveNTT.iNovelToMonomialCoeffs {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (novel_coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : Fin (2 ^ (ℓ - ↑i)) → L

Convert novel coefficients to monomial coefficients at level i. m = n * A

noncomputable def AdditiveNTT.getINovelCoeffs {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (P : Polynomial L) : Fin (2 ^ (ℓ - ↑i)) → L

theorem AdditiveNTT.monomialToINovel_iNovelToMonomial_inverse {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : iNovelToMonomialCoeffs 𝔽q β h_ℓ_add_R_rate i h_i (monomialToINovelCoeffs 𝔽q β h_ℓ_add_R_rate i h_i coeffs) = coeffs

Round trip inverse property: Monomial -> Novel -> Monomial

theorem AdditiveNTT.iNovelToMonomial_monomialToINovel_inverse {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : monomialToINovelCoeffs 𝔽q β h_ℓ_add_R_rate i h_i (iNovelToMonomialCoeffs 𝔽q β h_ℓ_add_R_rate i h_i coeffs) = coeffs

theorem AdditiveNTT.intermediateEvaluationPoly_from_inovel_coeffs_eq_self {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i ≤ ℓ) (P : Polynomial L) (hP_deg : P.degree < 2 ^ (ℓ - ↑i)) : intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate i h_i (getINovelCoeffs 𝔽q β h_ℓ_add_R_rate i h_i P) = P

Reconstruction Lemma: If P has degree < 2^(ℓ-i), and we convert its coefficients to the intermediate novel basis, the resulting intermediateEvaluationPoly is exactly P.

noncomputable def AdditiveNTT.evenRefinement {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : Polynomial L

The even and odd refinements of P⁽ⁱ⁾(X) which are polynomials in the (i+1)-th basis. P₀⁽ⁱ⁺¹⁾(Y) = ∑_{j=0}^{2^{ℓ-i-1}-1} a_{2j} ⋅ Xⱼ⁽ⁱ⁺¹⁾(Y) P₁⁽ⁱ⁺¹⁾(Y) = ∑_{j=0}^{2^{ℓ-i-1}-1} a_{2j+1} ⋅ Xⱼ⁽ⁱ⁺¹⁾(Y)

noncomputable def AdditiveNTT.oddRefinement {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : Polynomial L

theorem AdditiveNTT.evaluation_poly_split_identity {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : have P_i := intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate i ⋯ coeffs; have P_even_i_plus_1 := evenRefinement 𝔽q β h_ℓ_add_R_rate i h_i coeffs; have P_odd_i_plus_1 := oddRefinement 𝔽q β h_ℓ_add_R_rate i h_i coeffs; have q_i := qMap 𝔽q β i ⋯; P_i = P_even_i_plus_1.comp q_i + Polynomial.X * P_odd_i_plus_1.comp q_i

Key Polynomial Identity (Equation 39). This identity is the foundation for the butterfly operation in the Additive NTT. It relates a polynomial in the i-th basis to its even and odd parts expressed in the (i+1)-th basis via the quotient map q⁽ⁱ⁾. ∀ i ∈ {0, ..., ℓ-1}, P⁽ⁱ⁾(X) = P₀⁽ⁱ⁺¹⁾(q⁽ⁱ⁾(X)) + X ⋅ P₁⁽ⁱ⁺¹⁾(q⁽ⁱ⁾(X))

theorem AdditiveNTT.intermediate_poly_P_base {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽q))] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] [h_β₀_eq_1 : Fact (β 0 = 1)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (h_ℓ : ℓ ≤ r) (coeffs : Fin (2 ^ ℓ) → L) : intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate 0 ⋯ coeffs = polynomialFromNovelCoeffs 𝔽q β ℓ h_ℓ coeffs