Additive NTT Domains

Domain-level constructions for the Additive NTT: quotient maps, intermediate domains, and the finite-domain bijections used by the algorithm.

theorem AdditiveNTT.𝔽q_element_eq_zero_or_eq_one (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽q] [hF₂ : Fact (Fintype.card 𝔽q = 2)] (c : 𝔽q) : c = 0 ∨ c = 1

noncomputable def AdditiveNTT.sDomain {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) : Subspace 𝔽q L

noncomputable def AdditiveNTT.qMap {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) : Polynomial L

theorem AdditiveNTT.qMap_eval_𝔽q_eq_0 {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) : Polynomial.eval ((algebraMap 𝔽q L) c) (qMap 𝔽q β i) = 0

theorem AdditiveNTT.qMap_comp_normalizedW {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) : (qMap 𝔽q β i).comp (normalizedW 𝔽q β i) = normalizedW 𝔽q β (i + 1)

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

theorem AdditiveNTT.qMap_maps_sDomain {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) (h_i_add_1 : ↑i + 1 < r) : have q_comp_linear_map := ⋯; have q_eval_linear_map := ⋯; have q_i_map := polyEvalLinearMap (qMap 𝔽q β i) q_eval_linear_map; have S_i := sDomain 𝔽q β h_ℓ_add_R_rate i; have S_i_plus_1 := sDomain 𝔽q β h_ℓ_add_R_rate (i + 1); Submodule.map q_i_map S_i = S_i_plus_1

@[irreducible]

noncomputable def AdditiveNTT.qCompositionChain {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 : ℕ} (i : Fin r) : Polynomial L

theorem AdditiveNTT.qCompositionChain_eq_foldl {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 : ℕ} (i : Fin r) : qCompositionChain 𝔽q β i = Fin.foldl (↑i) (fun (acc : Polynomial L) (j : Fin ↑i) => (qMap 𝔽q β ⟨↑j, ⋯⟩).comp acc) Polynomial.X

theorem AdditiveNTT.normalizedW_eq_qMap_composition {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 : ℕ) (i : Fin r) : normalizedW 𝔽q β i = qCompositionChain 𝔽q β i

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

theorem AdditiveNTT.sDomainBasisVectors_mem_sDomain {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) (k : Fin (ℓ + R_rate - ↑i)) : sDomainBasisVectors 𝔽q β h_ℓ_add_R_rate i k ∈ sDomain 𝔽q β h_ℓ_add_R_rate i

def AdditiveNTT.sBasis {r : ℕ} {L : Type u} (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ + R_rate) : Fin (ℓ + R_rate - ↑i) → L

theorem AdditiveNTT.sBasis_range_eq {r : ℕ} {L : Type u} (β : Fin r → L) {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin r) (h_i : ↑i < ℓ + R_rate) : β '' Set.Ico i ⟨ℓ + R_rate, h_ℓ_add_R_rate⟩ = Set.range (sBasis β h_ℓ_add_R_rate i h_i)

theorem AdditiveNTT.sDomain_eq_image_of_upper_span {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) (h_i : ↑i < ℓ + R_rate) : have V_i := Submodule.span 𝔽q (Set.range (sBasis β h_ℓ_add_R_rate i h_i)); have W_i_map := polyEvalLinearMap (normalizedW 𝔽q β i) ⋯; sDomain 𝔽q β h_ℓ_add_R_rate i = Submodule.map W_i_map V_i

noncomputable def AdditiveNTT.sDomain_basis {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) (h_i : ↑i < ℓ + R_rate) : Module.Basis (Fin (ℓ + R_rate - ↑i)) 𝔽q ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)

theorem AdditiveNTT.get_sDomain_basis {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) (h_i : ↑i < ℓ + R_rate) (k : Fin (ℓ + R_rate - ↑i)) : ↑((sDomain_basis 𝔽q β h_ℓ_add_R_rate i h_i) k) = Polynomial.eval (β ⟨↑i + ↑k, ⋯⟩) (normalizedW 𝔽q β i)

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

@[implicit_reducible]

noncomputable instance AdditiveNTT.fintype_sDomain {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) : Fintype ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)

theorem AdditiveNTT.sDomain_card {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) (h_i : ↑i < ℓ + R_rate) : Fintype.card ↥(sDomain 𝔽q β h_ℓ_add_R_rate i) = Fintype.card 𝔽q ^ (ℓ + R_rate - ↑i)

noncomputable def AdditiveNTT.splitPointIntoCoeffs {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽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) (h_i : ↑i < ℓ + R_rate) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)) : Fin (ℓ + R_rate - ↑i) → ℕ

noncomputable def AdditiveNTT.sDomainToFin {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽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) (h_i : ↑i < ℓ + R_rate) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)) : Fin (2 ^ (ℓ + R_rate - ↑i))

def AdditiveNTT.finToBinaryCoeffs {r : ℕ} (𝔽q : Type u) [Field 𝔽q] {ℓ R_rate : ℕ} (i : Fin r) (idx : Fin (2 ^ (ℓ + R_rate - ↑i))) : Fin (ℓ + R_rate - ↑i) → 𝔽q

theorem AdditiveNTT.finToBinaryCoeffs_sDomainToFin {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽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 < ℓ + R_rate) (x : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)) : have pointFinIdx := sDomainToFin 𝔽q β h_ℓ_add_R_rate i h_i x; finToBinaryCoeffs 𝔽q i pointFinIdx = ⇑((sDomain_basis 𝔽q β h_ℓ_add_R_rate i h_i).repr x)

noncomputable def AdditiveNTT.finToSDomain {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) (h_i : ↑i < ℓ + R_rate) (idx : Fin (2 ^ (ℓ + R_rate - ↑i))) : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i)

noncomputable def AdditiveNTT.sDomainFinEquiv {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽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 < ℓ + R_rate) : ↥(sDomain 𝔽q β h_ℓ_add_R_rate i) ≃ Fin (2 ^ (ℓ + R_rate - ↑i))

theorem AdditiveNTT.sDomainFin_bijective {r : ℕ} [NeZero r] {L : Type u} [Field L] [Fintype L] [DecidableEq L] (𝔽q : Type u) [Field 𝔽q] [Fintype 𝔽q] [DecidableEq 𝔽q] [h_Fq_char_prime : Fact (Nat.Prime (ringChar 𝔽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 < ℓ + R_rate) : Function.Bijective ⇑(sDomainFinEquiv 𝔽q β h_ℓ_add_R_rate i h_i)