Additive NTT Intermediate Objects

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

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 (ℓ + 1)) (k : Fin (ℓ - ↑i + 1)) : Polynomial L

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 (ℓ + 1)) (k : Fin (ℓ - ↑i + 1)) : IsLinearMap 𝔽q fun (x : L) => Polynomial.eval x (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate i k)

theorem AdditiveNTT.base_intermediateNormVpoly {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) (k : Fin (ℓ + 1)) : intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨0, ⋯⟩ ⟨↑k, ⋯⟩ = normalizedW 𝔽q β ⟨↑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.Polynomial.comp_same_inner_eq_if_same_outer {L : Type u} [Field L] (f g : Polynomial L) (h_f_eq_g : f = g) (x : Polynomial L) : f.comp x = g.comp x

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 ℓ) (k : Fin (ℓ - ↑i - 1)) : intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ ⟨↑k + 1, ⋯⟩ = (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ ⟨↑k, ⋯⟩).comp (qMap 𝔽q β ⟨↑i, ⋯⟩)

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 ℓ) (k : Fin (ℓ - ↑i + 1)) (l : Fin (ℓ - (↑i + ↑k) + 1)) : intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ ⟨↑k + ↑l, ⋯⟩ = (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i + ↑k, ⋯⟩ ⟨↑l, ⋯⟩).comp (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ ⟨↑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 ℓ) (k : ℕ) (h_bound : ↑i + k ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩)) : ↥(sDomain 𝔽q β h_ℓ_add_R_rate ⟨↑i + k, ⋯⟩)

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 ℓ) (h_i_add_1 : ↑i + 1 ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩)) : Polynomial.eval (↑x) (qMap 𝔽q β ⟨↑i, ⋯⟩) ∈ sDomain 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩

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 ℓ) (h_i_add_1 : ↑i + 1 ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩)) : iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i 1 h_i_add_1 x = ⟨Polynomial.eval (↑x) (qMap 𝔽q β ⟨↑i, ⋯⟩), ⋯⟩

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 (ℓ + 1)) (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 ℓ) (k : ℕ) (h_bound : ↑i + k ≤ ℓ) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩)) : have y := iteratedQuotientMap 𝔽q β h_ℓ_add_R_rate i k h_bound x; ∀ (j : Fin (ℓ + R_rate - (↑i + k))), ((sDomain_basis 𝔽q β h_ℓ_add_R_rate ⟨↑i + k, ⋯⟩ ⋯).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)

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), ⋯⟩

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 ℓ) (k : Fin (ℓ - (↑i + 1))) : (intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ ⟨↑k, ⋯⟩).comp (qMap 𝔽q β ⟨↑i, ⋯⟩) = intermediateNormVpoly 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ ⟨↑k + 1, ⋯⟩

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 (ℓ + 1)) (j : Fin (2 ^ (ℓ - ↑i))) : Polynomial L

theorem AdditiveNTT.base_intermediateNovelBasisX {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) (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 (ℓ + 1)) : intermediateNovelBasisX 𝔽q β h_ℓ_add_R_rate i ⟨0, ⋯⟩ = 1

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 ℓ) (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, ⋯⟩)

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 ℓ) (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, ⋯⟩)

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 (ℓ + 1)) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : Polynomial L

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 ℓ) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : Polynomial L

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 ℓ) (coeffs : Fin (2 ^ (ℓ - ↑i)) → L) : Polynomial L

theorem AdditiveNTT.evaluation_poly_split_identity {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 ℓ) (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 coeffs; have P_odd_i_plus_1 := oddRefinement 𝔽q β h_ℓ_add_R_rate 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

theorem AdditiveNTT.intermediate_poly_P_base {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) (h_ℓ : ℓ ≤ r) (coeffs : Fin (2 ^ ℓ) → L) : intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate ⟨0, ⋯⟩ coeffs = polynomialFromNovelCoeffs 𝔽q β ℓ h_ℓ coeffs