Novel Polynomial Basis

This file defines the components of a novel polynomial basis over a field L with degree r as an algebra over its prime-characteristic subfield 𝔽q, and an 𝔽q-basis β for L.

Main Definitions

• Uᵢ: 𝔽q-linear span of the initial i vectors of our basis β
• Wᵢ(X): subspace vanishing polynomial over Uᵢ, with normalized form Ŵᵢ(X)
• {Xⱼ(X), j ∈ Fin 2^ℓ}: basis vectors of L⦃<2^ℓ⦄[X] over L constructed from Ŵᵢ(X)
• novelPolynomialBasis: the novel polynomial basis for L⦃<2^ℓ⦄[X]
• W_prod_comp_decomposition: decomposition of Wᵢ into a product of compositions Π c ∈ Uᵢ, (Wᵢ₋₁ ∘ (X - c • βᵢ₋₁))
• W_linearity: Wᵢ is 𝔽q-linear and satisfies the recursion formula Wᵢ = (Wᵢ₋₁)^|𝔽q| - ((Wᵢ₋₁)(βᵢ₋₁))^(|𝔽q|-1) * Wᵢ₋₁

TODOs

• Computable novel polynomial basis

References

• [Lin, S., Chung, W., and Han, Y.S, Novel polynomial basis and its application to Reed–Solomon erasure codes][LCH14]
• [Von zur Gathen, J., and Gerhard, J., Arithmetic and factorization of polynomial over F2 (extended abstract)][GGJ96]

theorem AdditiveNTT.fintype_card_gt_one_of_field (K : Type u_1) [Field K] [Fintype K] : 1 < Fintype.card K

def AdditiveNTT.U {r : ℕ} [NeZero r] {L : Type u} [Field L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) : Subspace 𝔽q L

𝔽q-linear subspaces Uᵢ

∀ i ∈ {0, ..., r-1}, we define Uᵢ:= <β₀, ..., βᵢ₋₁>_{𝔽q} as the 𝔽q-linear span of the initial i vectors of our basis β.

NOTE: We might allow i = r in the future if needed.

instance AdditiveNTT.instModuleSubtypeMemSubspaceU {r : ℕ} [NeZero r] {L : Type u} [Field L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {i : Fin r} : Module 𝔽q ↥(U 𝔽q β i)

instance AdditiveNTT.instDecidableEqSubtypeMemSubspaceU {r : ℕ} [NeZero r] {L : Type u} [Field L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {i : Fin r} : DecidableEq ↥(U 𝔽q β i)

noncomputable instance AdditiveNTT.instDecidableMemSetCoeSubspaceU {r : ℕ} [NeZero r] {L : Type u} [Field L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) {i : Fin r} (x : L) : Decidable (x ∈ ↑(U 𝔽q β i))

theorem AdditiveNTT.finrank_U {r : ℕ} [NeZero r] {L : Type u} [Field L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) : Module.finrank 𝔽q ↥(U 𝔽q β i) = ↑i

noncomputable instance AdditiveNTT.fintype_U {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) : Fintype ↥(U 𝔽q β i)

theorem AdditiveNTT.U_card {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) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) : Fintype.card ↥(U 𝔽q β i) = Fintype.card 𝔽q ^ ↑i

theorem AdditiveNTT.U_i_is_union_of_cosets {r : ℕ} [NeZero r] {L : Type u} [Field L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) (hi : 0 < i) : ↑(U 𝔽q β i) = ⋃ (c : 𝔽q), (fun (u : L) => c • β (i - 1) + u) '' ↑(U 𝔽q β (i - 1))

An essential helper lemma showing that Uᵢ is the union of all cosets of Uᵢ₋₁ generated by scaling βᵢ₋₁ by elements of 𝔽q.

theorem AdditiveNTT.βᵢ_not_in_Uᵢ {r : ℕ} [NeZero r] {L : Type u} [Field L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) : β i ∉ U 𝔽q β i

The basis vector βᵢ is not an element of the subspace Uᵢ.

theorem AdditiveNTT.root_U_lift_down {r : ℕ} [NeZero r] {L : Type u} [Field L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) (h_i_add_1 : ↑i + 1 < r) (a : L) : a ∈ U 𝔽q β (i + 1) → ∃! x : 𝔽q, a - x • β i ∈ U 𝔽q β i

theorem AdditiveNTT.root_U_lift_up {r : ℕ} [NeZero r] {L : Type u} [Field L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) (h_i_add_1 : ↑i + 1 < r) (a : L) (x : 𝔽q) : a - x • β i ∈ U 𝔽q β i → a ∈ U 𝔽q β (i + 1)

noncomputable def AdditiveNTT.W {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) : Polynomial L

The subspace vanishing polynomial Wᵢ(X) := ∏_{u ∈ Uᵢ} (X - u), ∀ i ∈ {0, ..., r-1}. The degree of Wᵢ(X) is |Uᵢ| = 2^i.

• [LCH14, Lemma 1]: Wᵢ(X) is an 𝔽q-linearized polynomial, i.e., Wᵢ(x) = ∑_{j=0}^i a_{i, j} x^{2^j} for some constants a_{i, j} ∈ L (Equation (3)).
• The additive property: Wᵢ(x + y) = Wᵢ(x) + Wᵢ(y) for all x, y ∈ L (Equation (4)).
• For all y ∈ Uᵢ, Wᵢ(x + y) = Wᵢ(x) (Equation (14)).

theorem AdditiveNTT.degree_W {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) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) : (W 𝔽q β i).degree = ↑(Fintype.card 𝔽q) ^ ↑i

The degree of the subspace vanishing polynomial Wᵢ(X) is 2ⁱ.

theorem AdditiveNTT.W_monic {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) : (W 𝔽q β i).Monic

The subspace vanishing polynomial Wᵢ(X) is monic.

theorem AdditiveNTT.W_ne_zero {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) : W 𝔽q β i ≠ 0

theorem AdditiveNTT.Wᵢ_eval_βᵢ_neq_zero {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) : Polynomial.eval (β i) (W 𝔽q β i) ≠ 0

The evaluation of Wᵢ(X) at βᵢ is non-zero.

theorem AdditiveNTT.Wᵢ_vanishing {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) (u : L) : u ∈ U 𝔽q β i → Polynomial.eval u (W 𝔽q β i) = 0

theorem AdditiveNTT.W₀_eq_X {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) : W 𝔽q β 0 = Polynomial.X

Formalization of linearity of subspace vanishing polynomials

This section formalizes the key properties of the subspace vanishing polynomials Wᵢ, including their recursive structure and 𝔽q-linearity as described in Lemma 2.3 of [GGJ96]. The proofs are done by simultaneous induction on i.

theorem AdditiveNTT.W_splits {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) : (W 𝔽q β i).Splits

The subspace vanishing polynomial Wᵢ(X) splits into linear factors over L.

theorem AdditiveNTT.roots_W {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) : (W 𝔽q β i).roots = Multiset.map (fun (u : ↥(U 𝔽q β i)) => ↑u) Finset.univ.val

The roots of Wᵢ(X) are precisely the elements of the subspace Uᵢ.

noncomputable def AdditiveNTT.algEquivAevalXSubC {R : Type u_1} [CommRing R] (t : R) : Polynomial R ≃ₐ[R] Polynomial R

@[simp]

theorem AdditiveNTT.algEquivAevalXSubC_symm_apply {R : Type u_1} [CommRing R] (t : R) (a : Polynomial R) : (algEquivAevalXSubC t).symm a = (Polynomial.aeval (Polynomial.X + Polynomial.C t)) a

@[simp]

theorem AdditiveNTT.algEquivAevalXSubC_apply {R : Type u_1} [CommRing R] (t : R) (a : Polynomial R) : (algEquivAevalXSubC t) a = (Polynomial.aeval (Polynomial.X - Polynomial.C t)) a

theorem AdditiveNTT.comp_X_sub_C_eq_zero_iff {L : Type u} [Field L] (p : Polynomial L) (a : L) : p.comp (Polynomial.X - Polynomial.C a) = 0 ↔ p = 0

theorem AdditiveNTT.rootMultiplicity_comp_X_sub_C {L : Type u} [Field L] [DecidableEq L] (p : Polynomial L) (a x : L) : Polynomial.rootMultiplicity x (p.comp (Polynomial.X - Polynomial.C a)) = Polynomial.rootMultiplicity (x - a) p

The multiplicity of a root x in a polynomial p composed with (X - a) is equal to the multiplicity of the root x - a in p.

theorem AdditiveNTT.roots_comp_X_sub_C {L : Type u} [Field L] [DecidableEq L] (p : Polynomial L) (a : L) : (p.comp (Polynomial.X - Polynomial.C a)).roots = Multiset.map (fun (r : L) => r + a) p.roots

theorem AdditiveNTT.Prod_W_comp_X_sub_C_ne_zero {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) : ∏ c : 𝔽q, (W 𝔽q β i).comp (Polynomial.X - Polynomial.C (c • β i)) ≠ 0

theorem AdditiveNTT.rootMultiplicity_W {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) (a : L) : Polynomial.rootMultiplicity a (W 𝔽q β i) = if a ∈ ↑(U 𝔽q β i) then 1 else 0

The polynomial Wᵢ(X) has simple roots (multiplicity 1) for each element in the subspace Uᵢ, and no other roots.

theorem AdditiveNTT.eval_W_eq_zero_iff_in_U {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) (a : L) : Polynomial.eval a (W 𝔽q β i) = 0 ↔ a ∈ U 𝔽q β i

theorem AdditiveNTT.rootMultiplicity_prod_W_comp_X_sub_C {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) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) (h_i_add_1 : ↑i + 1 < r) (a : L) : Polynomial.rootMultiplicity a (∏ c : 𝔽q, (W 𝔽q β i).comp (Polynomial.X - Polynomial.C (c • β i))) = if a ∈ ↑(U 𝔽q β (i + 1)) then 1 else 0

theorem AdditiveNTT.W_prod_comp_decomposition {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) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) (hi : i > 0) : W 𝔽q β i = ∏ c : 𝔽q, (W 𝔽q β (i - 1)).comp (Polynomial.X - Polynomial.C (c • β (i - 1)))

The generic product form of the recursion for Wᵢ. This follows the first line of the proof for (i) in the description. Wᵢ(X) = ∏_{c ∈ 𝔽q} Wᵢ₋₁ ∘ (X - cβᵢ₋₁).

theorem AdditiveNTT.comp_sub_C_of_linear_eval {L : Type u} [Field L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (p : Polynomial L) (h_lin : IsLinearMap 𝔽q fun (inner_p : Polynomial L) => p.comp inner_p) (a : L) : p.comp (Polynomial.X - Polynomial.C a) = p - Polynomial.C (Polynomial.eval a p)

theorem AdditiveNTT.inductive_rec_form_W_comp {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) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) (h_i_add_1 : ↑i + 1 < r) (h_prev_linear_map : IsLinearMap 𝔽q fun (inner_p : Polynomial L) => (W 𝔽q β i).comp inner_p) (p : Polynomial L) : (W 𝔽q β (i + 1)).comp p = (W 𝔽q β i).comp p ^ Fintype.card 𝔽q - Polynomial.C (Polynomial.eval (β i) (W 𝔽q β i)) ^ (Fintype.card 𝔽q - 1) * (W 𝔽q β i).comp p

theorem AdditiveNTT.inductive_linear_map_W {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 β)] (i : Fin r) (h_i_add_1 : ↑i + 1 < r) (h_prev_linear_map : IsLinearMap 𝔽q fun (inner_p : Polynomial L) => (W 𝔽q β i).comp inner_p) : IsLinearMap 𝔽q fun (inner_p : Polynomial L) => (W 𝔽q β (i + 1)).comp inner_p

theorem AdditiveNTT.W_linearity {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 β)] (i : Fin r) : IsLinearMap 𝔽q fun (inner_p : Polynomial L) => (W 𝔽q β i).comp inner_p

Simultaneous Proof of Linearity for Wᵢ from the paper [GGJ96] (Lemma 2.3) Wᵢ is an 𝔽q-linearized polynomial. This means for all polynomials f, g with coefficients in L (i.e. L[X]) and for all c ∈ 𝔽q, we have: Wᵢ(f + g) = Wᵢ(f) + Wᵢ(g) and Wᵢ(c * f) = c * Wᵢ(f). As a corollary of this, Wᵢ is 𝔽q-linear when evaluated on elements of L: Wᵢ(x + y) = Wᵢ(x) + Wᵢ(y) for all x, y ∈ L.

noncomputable def AdditiveNTT.polyEvalLinearMap {L : Type u_1} {𝔽q : Type u_2} [Field L] [Field 𝔽q] [Algebra 𝔽q L] (p : Polynomial L) (hp_add : IsLinearMap 𝔽q fun (x : L) => Polynomial.eval x p) : L →ₗ[𝔽q] L

Helper function to create a linear map from a polynomial whose evaluation is additive.

theorem AdditiveNTT.W_linear_comp_decomposition {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 β)] (i : Fin r) (h_i_add_1 : ↑i + 1 < r) (p : Polynomial L) : (W 𝔽q β (i + 1)).comp p = (W 𝔽q β i).comp p ^ Fintype.card 𝔽q - Polynomial.C (Polynomial.eval (β i) (W 𝔽q β i)) ^ (Fintype.card 𝔽q - 1) * (W 𝔽q β i).comp p

theorem AdditiveNTT.W_is_additive {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 β)] (i : Fin r) : IsLinearMap 𝔽q fun (x : L) => Polynomial.eval x (W 𝔽q β i)

The additive property of Wᵢ: Wᵢ(x + y) = Wᵢ(x) + Wᵢ(y).

theorem AdditiveNTT.kernel_W_eq_U {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 β)] (i : Fin r) : (polyEvalLinearMap (W 𝔽q β i) ⋯).ker = U 𝔽q β i

theorem AdditiveNTT.W_add_U_invariant {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 β)] (i : Fin r) (x y : L) : y ∈ U 𝔽q β i → Polynomial.eval (x + y) (W 𝔽q β i) = Polynomial.eval x (W 𝔽q β i)

For all y ∈ Uᵢ, Wᵢ(x + y) = Wᵢ(x).

Normalized Subspace Vanishing Polynomials Ŵᵢ(X) := Wᵢ(X) / Wᵢ(βᵢ), ∀ i ∈ {0, ..., r-1}

noncomputable def AdditiveNTT.normalizedW {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) : Polynomial L

theorem AdditiveNTT.normalizedWᵢ_eval_βᵢ_eq_1 {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] {i : Fin r} : Polynomial.eval (β i) (normalizedW 𝔽q β i) = 1

The evaluation of the normalized polynomial Ŵᵢ(X) at βᵢ is 1.

theorem AdditiveNTT.normalizedW₀_eq_1_div_β₀ {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) : normalizedW 𝔽q β 0 = Polynomial.X * Polynomial.C (1 / β 0)

theorem AdditiveNTT.eval_normalizedW_succ_at_beta_prev {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) (h_i_add_1 : ↑i + 1 < r) : Polynomial.eval (β i) (normalizedW 𝔽q β (i + 1)) = 0

The evaluation Ŵᵢ₊₁(βᵢ) is 0. This is because Ŵᵢ₊₁ = q⁽ⁱ⁾ ∘ Ŵᵢ and q⁽ⁱ⁾(1) = 0.

theorem AdditiveNTT.degree_normalizedW {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) [hβ_lin_indep : Fact (LinearIndependent 𝔽q β)] (i : Fin r) : (normalizedW 𝔽q β i).degree = ↑(Fintype.card 𝔽q) ^ ↑i

The degree of Ŵᵢ(X) remains |𝔽q|ⁱ.

theorem AdditiveNTT.β_lt_mem_U {r : ℕ} [NeZero r] {L : Type u} [Field L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) (j : Fin ↑i) : β ⟨↑j, ⋯⟩ ∈ U 𝔽q β i

theorem AdditiveNTT.normalizedWᵢ_vanishing {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (i : Fin r) (u : L) : u ∈ U 𝔽q β i → Polynomial.eval u (normalizedW 𝔽q β i) = 0

The normalized polynomial Ŵᵢ(X) vanishes on Uᵢ.

theorem AdditiveNTT.normalizedW_is_linear_map {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 β)] (i : Fin r) : IsLinearMap 𝔽q fun (inner_p : Polynomial L) => (normalizedW 𝔽q β i).comp inner_p

The normalized subspace vanishing polynomial Ŵᵢ(X) is 𝔽q-linear.

theorem AdditiveNTT.normalizedW_is_additive {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 β)] (i : Fin r) : IsLinearMap 𝔽q fun (x : L) => Polynomial.eval x (normalizedW 𝔽q β i)

theorem AdditiveNTT.kernel_normalizedW_eq_U {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 β)] (i : Fin r) : (polyEvalLinearMap (normalizedW 𝔽q β i) ⋯).ker = U 𝔽q β i

noncomputable def AdditiveNTT.Xⱼ {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (j : Fin (2 ^ ℓ)) : Polynomial L

The Novel Polynomial Basis {Xⱼ(X), j ∈ Fin 2^ℓ} for the space L⦃<2^ℓ⦄[X] over L

theorem AdditiveNTT.Xⱼ_zero_eq_one {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : Xⱼ 𝔽q β ℓ h_ℓ ⟨0, ⋯⟩ = 1

The zero-th element of the novel polynomial basis is the constant 1

theorem AdditiveNTT.degree_Xⱼ {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (j : Fin (2 ^ ℓ)) : (Xⱼ 𝔽q β ℓ h_ℓ j).degree = ↑↑j

The degree of Xⱼ(X) is j: deg(Xⱼ(X)) = Σ_{i=0}^{ℓ-1} jᵢ * deg(Ŵᵢ(X)) = Σ_{i=0}^{ℓ-1} jᵢ * 2ⁱ = j

noncomputable def AdditiveNTT.basisVectors {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : Fin (2 ^ ℓ) → ↥(Polynomial.degreeLT L (2 ^ ℓ))

The basis vectors {Xⱼ(X), j ∈ Fin 2^ℓ} forms a basis for L⦃<2^ℓ⦄[X]

@[reducible, inline]

abbrev AdditiveNTT.CoeffVecSpace (L : Type u) (ℓ : ℕ) : Type u

The vector space of coefficients for polynomials of degree < 2^ℓ.

noncomputable instance AdditiveNTT.instAddCommGroupCoeffVecSpace {L : Type u} [Field L] (ℓ : ℕ) : AddCommGroup (CoeffVecSpace L ℓ)

instance AdditiveNTT.finiteDimensionalCoeffVecSpace {L : Type u} [Field L] (ℓ : ℕ) : FiniteDimensional L (CoeffVecSpace L ℓ)

def AdditiveNTT.toCoeffsVec {L : Type u} [Field L] (ℓ : ℕ) : ↥(Polynomial.degreeLT L (2 ^ ℓ)) →ₗ[L] CoeffVecSpace L ℓ

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

theorem AdditiveNTT.linearIndependent_rows_of_lower_triangular_ne_zero_diag {n : ℕ} {R : Type u_1} [Field R] (A : Matrix (Fin n) (Fin n) R) (h_lower_triangular : A.BlockTriangular ⇑OrderDual.toDual) (h_diag : ∀ (i : Fin n), A i i ≠ 0) : LinearIndependent R A

The rows of a square lower-triangular matrix with non-zero diagonal entries are linearly independent.

noncomputable def AdditiveNTT.changeOfBasisMatrix {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : Matrix (Fin (2 ^ ℓ)) (Fin (2 ^ ℓ)) L

The change-of-basis matrix from the novel basis to the monomial basis. Aⱼᵢ = coeff of Xⁱ in novel basis vector 𝕏ⱼ. novel_coeffs * A = monomial_coeffs

theorem AdditiveNTT.changeOfBasisMatrix_lower_triangular {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : (changeOfBasisMatrix 𝔽q β ℓ h_ℓ).BlockTriangular ⇑OrderDual.toDual

theorem AdditiveNTT.changeOfBasisMatrix_diag_ne_zero {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (i : Fin (2 ^ ℓ)) : changeOfBasisMatrix 𝔽q β ℓ h_ℓ i i ≠ 0

theorem AdditiveNTT.changeOfBasisMatrix_det_ne_zero {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : (changeOfBasisMatrix 𝔽q β ℓ h_ℓ).det ≠ 0

The determinant of the change-of-basis matrix is non-zero.

noncomputable instance AdditiveNTT.changeOfBasisMatrix_invertible {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : Invertible (changeOfBasisMatrix 𝔽q β ℓ h_ℓ)

The change-of-basis matrix is invertible, this is required by the proofs of inversion between monomial and novel polynomial basis coefficients.

theorem AdditiveNTT.coeff_vectors_linear_independent {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : LinearIndependent L (⇑(toCoeffsVec ℓ) ∘ basisVectors 𝔽q β ℓ h_ℓ)

The coefficient vectors of the novel basis polynomials are linearly independent. This is proven by showing that the change-of-basis matrix to the monomial basis is lower-triangular with a non-zero diagonal.

theorem AdditiveNTT.basisVectors_linear_independent {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : LinearIndependent L (basisVectors 𝔽q β ℓ h_ℓ)

The basis vectors are linearly independent over L.

theorem AdditiveNTT.basisVectors_span {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : Submodule.span L (Set.range (basisVectors 𝔽q β ℓ h_ℓ)) = ⊤

The basis vectors span the space of polynomials with degree less than 2^ℓ.

noncomputable def AdditiveNTT.novelPolynomialBasis {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : Module.Basis (Fin (2 ^ ℓ)) L ↥(Polynomial.degreeLT L (2 ^ ℓ))

The novel polynomial basis for L⦃<2^ℓ⦄[X]

noncomputable def AdditiveNTT.polynomialFromNovelCoeffs {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] (𝔽q : Type u) [Field 𝔽q] [Algebra 𝔽q L] (β : Fin r → L) (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (a : Fin (2 ^ ℓ) → L) : Polynomial L

The polynomial P(X) derived from coefficients a in the novel polynomial basis (Xⱼ), P(X) := ∑_{j=0}^{2^ℓ-1} aⱼ ⋅ Xⱼ(X)

noncomputable def AdditiveNTT.polynomialFromNovelCoeffsF₂ {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (a : Fin (2 ^ ℓ) → L) : ↥(Polynomial.degreeLT L (2 ^ ℓ))

theorem AdditiveNTT.novelPolynomialBasis_is_basisVectors {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) : ⇑(novelPolynomialBasis 𝔽q β ℓ h_ℓ) = basisVectors 𝔽q β ℓ h_ℓ

Proof that the novel polynomial basis is indeed the indicated basis vectors

noncomputable def AdditiveNTT.monomialToNovelCoeffs {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (monomial_coeffs : Fin (2 ^ ℓ) → L) : Fin (2 ^ ℓ) → L

Convert monomial coefficients to novel polynomial basis coefficients. Using row vectors: n = m * A⁻¹.

noncomputable def AdditiveNTT.novelToMonomialCoeffs {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (novel_coeffs : Fin (2 ^ ℓ) → L) : Fin (2 ^ ℓ) → L

Convert novel polynomial basis coefficients to monomial coefficients. Using row vectors: m = n * A.

theorem AdditiveNTT.monomialToNovel_novelToMonomial_inverse {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (coeffs : Fin (2 ^ ℓ) → L) : novelToMonomialCoeffs 𝔽q β ℓ h_ℓ (monomialToNovelCoeffs 𝔽q β ℓ h_ℓ coeffs) = coeffs

The conversion functions are inverses of each other. (Monomial -> Novel -> Monomial)

theorem AdditiveNTT.novelToMonomial_monomialToNovel_inverse {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq 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 β)] (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (coeffs : Fin (2 ^ ℓ) → L) : monomialToNovelCoeffs 𝔽q β ℓ h_ℓ (novelToMonomialCoeffs 𝔽q β ℓ h_ℓ coeffs) = coeffs

The conversion functions are inverses of each other. (Novel -> Monomial -> Novel)