NTT Domain

This file defines the radix-2 NTT domain parameters and basic raw-polynomial shape helpers used by forward/inverse NTT.

structure CompPoly.CPolynomial.NTT.Domain (R : Type u_2) [Field R] : Type u_2

Parameters for a radix-2 NTT domain of size 2 ^ logN.

• logN : ℕ
• omega : R
• primitive : IsPrimitiveRoot self.omega (2 ^ self.logN)

@[implicit_reducible]

def CompPoly.CPolynomial.NTT.Domain.n {R : Type u_1} [Field R] (D : Domain R) : ℕ

Domain size.

@[reducible, inline]

abbrev CompPoly.CPolynomial.NTT.Domain.Idx {R : Type u_1} [Field R] (D : Domain R) : Type

Index type for vectors over the domain.

@[inline]

def CompPoly.CPolynomial.NTT.Domain.node {R : Type u_1} [Field R] (D : Domain R) (i : D.Idx) : R

The i-th evaluation node omega^i.

@[inline]

def CompPoly.CPolynomial.NTT.Domain.omegaInv {R : Type u_1} [Field R] (D : Domain R) : R

Inverse root of unity.

def CompPoly.CPolynomial.NTT.Domain.inverse {R : Type u_1} [Field R] (D : Domain R) : Domain R

The domain with the inverse root, used by inverse NTT butterflies.

@[inline]

def CompPoly.CPolynomial.NTT.Domain.nInv {R : Type u_1} [Field R] (D : Domain R) : R

Multiplicative inverse of the domain size in R.

@[simp]

theorem CompPoly.CPolynomial.NTT.Domain.n_pos {R : Type u_1} [Field R] (D : Domain R) : 0 < D.n

@[simp]

theorem CompPoly.CPolynomial.NTT.Domain.n_ne_zero {R : Type u_1} [Field R] (D : Domain R) : D.n ≠ 0

theorem CompPoly.CPolynomial.NTT.Domain.natCast_ne_zero {R : Type u_1} [Field R] (D : Domain R) : ↑D.n ≠ 0

The size of an NTT domain is nonzero in its coefficient field.

def CompPoly.CPolynomial.NTT.Domain.requiredLength {R : Type u_1} [Field R] [BEq R] (p q : Raw R) : ℕ

Required convolution length for multiplying p and q.

theorem CompPoly.CPolynomial.NTT.Domain.requiredLength_eq_zero_of_left_trim_size_zero {R : Type u_1} [Field R] [BEq R] (p q : Raw R) (hp : Array.size p.trim = 0) : requiredLength p q = 0

theorem CompPoly.CPolynomial.NTT.Domain.requiredLength_eq_zero_of_right_trim_size_zero {R : Type u_1} [Field R] [BEq R] (p q : Raw R) (hq : Array.size q.trim = 0) : requiredLength p q = 0

theorem CompPoly.CPolynomial.NTT.Domain.requiredLength_eq_of_trim_size_pos {R : Type u_1} [Field R] [BEq R] (p q : Raw R) (hp : 0 < Array.size p.trim) (hq : 0 < Array.size q.trim) : requiredLength p q = Array.size p.trim + Array.size q.trim - 1

def CompPoly.CPolynomial.NTT.Domain.fits {R : Type u_1} [Field R] [BEq R] (D : Domain R) (p q : Raw R) : Prop

Whether domain D is large enough for multiplying p and q.

def CompPoly.CPolynomial.NTT.Domain.truncate {R : Type u_1} (m : ℕ) (p : Raw R) : Raw R

Truncate a polynomial to at most m coefficients.

def CompPoly.CPolynomial.NTT.bestLogN (requiredLen : ℕ) : ℕ

The smallest radix-2 exponent that can cover a requested convolution length.

@[inline]

def CompPoly.CPolynomial.NTT.loadNaturalArray {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : Array R

Load an array in natural order and pad it to a domain-sized array.

@[simp]

theorem CompPoly.CPolynomial.NTT.size_loadNaturalArray {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : (loadNaturalArray D a).size = D.n

@[simp]

theorem CompPoly.CPolynomial.NTT.getElem_loadNaturalArray {R : Type u_1} [Field R] (D : Domain R) (a : Array R) (i : ℕ) (hi : i < (loadNaturalArray D a).size) : (loadNaturalArray D a)[i] = a.getD i 0

@[inline]

def CompPoly.CPolynomial.NTT.loadNaturalVector {R : Type u_1} [Field R] (D : Domain R) (a : Array R) : Vector R D.n

Load an array in natural order and pad it to a domain-sized vector.

@[reducible, inline]

abbrev CompPoly.CPolynomial.NTT.FittingDomain (R : Type u_2) [Field R] (requiredLen : ℕ) : Type u_2

An NTT domain bundled with proof that it covers the requested convolution length.

def CompPoly.CPolynomial.NTT.bestDomainForLength? {R : Type u_1} [Field R] (maxLogN : ℕ) (domainOfLogN : (logN : ℕ) → logN ≤ maxLogN → Domain R) (domainOfLogN_logN : ∀ (logN : ℕ) (hlogN : logN ≤ maxLogN), (domainOfLogN logN hlogN).logN = logN) (requiredLen : ℕ) : Option (FittingDomain R requiredLen)

Generic adapter from field-specific radix-2 domain tables to a best-fitting domain lookup.

The adapter chooses logN = Nat.clog 2 requiredLen, then returns none if that exponent is outside the supported table.