Additive NTT Algorithm

Core Additive NTT data flow: evaluation points, twiddle factors, stage/update definitions, coefficient tiling, and the stage invariant.

noncomputable def AdditiveNTT.evaluationPointω {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 (ℓ + 1)) (x : Fin (2 ^ (ℓ + R_rate - ↑i))) : L

noncomputable def AdditiveNTT.twiddleFactor {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 ℓ) (u : Fin (2 ^ (ℓ + R_rate - ↑i - 1))) : L

theorem AdditiveNTT.evaluationPointω_eq_twiddleFactor_of_div_2 {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 ℓ) (x : Fin (2 ^ (ℓ + R_rate - ↑i))) : evaluationPointω 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ x = twiddleFactor 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ ⟨↑x / 2, ⋯⟩ + ↑(↑x % 2) * Polynomial.eval (β ⟨↑i, ⋯⟩) (normalizedW 𝔽q β ⟨↑i, ⋯⟩)

theorem AdditiveNTT.eval_point_ω_eq_next_twiddleFactor_comp_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 β)] {ℓ R_rate : ℕ} (h_ℓ_add_R_rate : ℓ + R_rate < r) (i : Fin ℓ) (x : Fin (2 ^ (ℓ + R_rate - (↑i + 1)))) : evaluationPointω 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ x = Polynomial.eval (twiddleFactor 𝔽q β h_ℓ_add_R_rate ⟨↑i, ⋯⟩ ⟨↑x, ⋯⟩) (qMap 𝔽q β ⟨↑i, ⋯⟩)

def AdditiveNTT.tileCoeffs {L : Type u} {ℓ R_rate : ℕ} (a : Fin (2 ^ ℓ) → L) : Fin (2 ^ (ℓ + R_rate)) → L

noncomputable def AdditiveNTT.NTTStage {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 ℓ) (b : Fin (2 ^ (ℓ + R_rate)) → L) : Fin (2 ^ (ℓ + R_rate)) → L

noncomputable def AdditiveNTT.additiveNTT {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) (a : Fin (2 ^ ℓ) → L) : Fin (2 ^ (ℓ + R_rate)) → L

def AdditiveNTT.coeffsBySuffix {r : ℕ} {L : Type u} {ℓ R_rate : ℕ} (a : Fin (2 ^ ℓ) → L) (i : Fin (ℓ + 1)) (v : Fin (2 ^ ↑i)) : Fin (2 ^ (ℓ - ↑i)) → L

theorem AdditiveNTT.base_coeffsBySuffix {r : ℕ} {L : Type u} {ℓ R_rate : ℕ} (a : Fin (2 ^ ℓ) → L) : coeffsBySuffix a 0 0 = a

theorem AdditiveNTT.evenRefinement_eq_novel_poly_of_0_leading_suffix {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 ℓ) (v : Fin (2 ^ ↑i)) (original_coeffs : Fin (2 ^ ℓ) → L) : have h_v := ⋯; evenRefinement 𝔽q β h_ℓ_add_R_rate i (coeffsBySuffix original_coeffs ⟨↑i, ⋯⟩ v) = intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ (coeffsBySuffix original_coeffs ⟨↑i + 1, ⋯⟩ ⟨↑v, h_v⟩)

theorem AdditiveNTT.oddRefinement_eq_novel_poly_of_1_leading_suffix {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 ℓ) (v : Fin (2 ^ ↑i)) (original_coeffs : Fin (2 ^ ℓ) → L) : have h_v := ⋯; oddRefinement 𝔽q β h_ℓ_add_R_rate i (coeffsBySuffix original_coeffs ⟨↑i, ⋯⟩ v) = intermediateEvaluationPoly 𝔽q β h_ℓ_add_R_rate ⟨↑i + 1, ⋯⟩ (coeffsBySuffix original_coeffs ⟨↑i + 1, ⋯⟩ ⟨↑v ||| 1 <<< ↑i, h_v⟩)

def AdditiveNTT.additiveNTTInvariant {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) (evaluation_buffer : Fin (2 ^ (ℓ + R_rate)) → L) (original_coeffs : Fin (2 ^ ℓ) → L) (i : Fin (ℓ + 1)) : Prop