def Hex.ZMod64.Ntt.intAddCoeffs : List Int → List Int → List Int

Integer coefficient addition with the same zero-extending shape as the modular convolution reference.

Equations

• Hex.ZMod64.Ntt.intAddCoeffs [] x✝ = x✝
• Hex.ZMod64.Ntt.intAddCoeffs x✝ [] = x✝
• Hex.ZMod64.Ntt.intAddCoeffs (x_2 :: xs) (y :: ys) = (x_2 + y) :: Hex.ZMod64.Ntt.intAddCoeffs xs ys

def Hex.ZMod64.Ntt.intLinearConvolution : List Int → List Int → List Int

Ordinary low-to-high integer schoolbook convolution. This is the coefficient target reconstructed from auxiliary-prime transforms.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.intLinearConvolution [] x✝ = []
• Hex.ZMod64.Ntt.intLinearConvolution (head :: tail) [] = []

def Hex.ZMod64.Ntt.intPadTo (n : Nat) (coefficients : List Int) : List Int

Zero-pad an integer coefficient list to a requested capacity.

Equations

• Hex.ZMod64.Ntt.intPadTo n coefficients = coefficients ++ List.replicate (n - coefficients.length) 0

@[simp]

theorem Hex.ZMod64.Ntt.length_intPadTo (n : Nat) (coefficients : List Int) (hfit : coefficients.length ≤ n) : (intPadTo n coefficients).length = n

theorem Hex.ZMod64.Ntt.linearConvolution_intCast {p : Nat} [Bounds p] (left right : List Int) : linearConvolution (List.map (fun (value : Int) => ↑value) left) (List.map (fun (value : Int) => ↑value) right) = List.map (fun (value : Int) => ↑value) (intLinearConvolution left right)

Reducing an integer convolution modulo p coefficientwise gives the modular convolution of the reduced inputs.

structure Hex.ZMod64.NttPrime : Type

One fixed auxiliary prime and its maximal radix-two root.

• modulus : Nat

  Prime modulus, always below 2^31.

• bounds : Bounds self.modulus

  Word-arithmetic bounds for the modulus.

• prime : PrimeModulus self.modulus

  Kernel-checked primality evidence.

• maxLog : Nat

  Maximum supported transform exponent.

• length_dvd : 2 ^ self.maxLog ∣ self.modulus - 1

  The maximal power-of-two length divides the unit-group order.

• root : ZMod64 self.modulus

  Primitive root of order 2^maxLog.

• root_order : self.root.ExactOrder (2 ^ self.maxLog)

  The stored root has exact maximal power-of-two order.

def Hex.ZMod64.NttPrime.maxLength (prime : NttPrime) : Nat

Maximum supported transform length.

Equations

• prime.maxLength = 2 ^ prime.maxLog

def Hex.ZMod64.NttPrime.rootFor (prime : NttPrime) (n : Nat) : ZMod64 prime.modulus

Derive the root requested for a smaller transform length. The checked builder below rejects lengths that do not divide the maximum.

Equations

• prime.rootFor n = prime.root ^ 2 ^ (prime.maxLog - n.log2)

def Hex.ZMod64.NttPrime.plan? (prime : NttPrime) (n : Nat) : Option (NttPlan prime.modulus n)

Build a reusable plan when n is a supported power-of-two length. A capacity miss or failed validation is normal control flow.

Equations

• prime.plan? n = if n ≤ prime.maxLength then Hex.ZMod64.NttPlan.build? (prime.rootFor n) else none

theorem Hex.ZMod64.NttPrime.rootFor_order (prime : NttPrime) (n : Nat) (hpow : IsPowTwo n) (hcapacity : n ≤ prime.maxLength) : (prime.rootFor n).ExactOrder n

The root derived for an in-capacity power-of-two length has exact order n.

theorem Hex.ZMod64.NttPrime.length_dvd_of_supported (prime : NttPrime) (n : Nat) (hpow : IsPowTwo n) (hcapacity : n ≤ prime.maxLength) : n ∣ prime.modulus - 1

Every supported transform length divides the catalogue modulus's unit group order.

theorem Hex.ZMod64.NttPrime.plan?_isSome_of_supported (prime : NttPrime) (n : Nat) (hpow : IsPowTwo n) (hcapacity : n ≤ prime.maxLength) : (prime.plan? n).isSome = true

Every in-capacity power-of-two request succeeds; the checked runtime failure channel is reserved for invalid lengths and capacity misses.

theorem Hex.ZMod64.NttPrime.plan?_eq_none_of_capacity (prime : NttPrime) (n : Nat) (hcapacity : ¬n ≤ prime.maxLength) : prime.plan? n = none

A request beyond a catalogue entry's capacity returns none.

def Hex.ZMod64.NttPrime.convolution? (prime : NttPrime) (n : Nat) (left right : Array Int) : Option (Array Int)

Run ordinary convolution at one catalogue prime and erase the dependent modular coefficient type to canonical integer residues.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.ZMod64.NttPrime.residue_emod (prime : NttPrime) (value : Int) : Int.ofNat (intCast prime.modulus value).toNat % ↑prime.modulus = value % ↑prime.modulus

Canonicalizing an integer through one catalogue modulus preserves its ordinary integer remainder.

theorem Hex.ZMod64.NttPrime.convolution?_eq_of_some (prime : NttPrime) (n : Nat) (left right result : Array Int) (hresult : prime.convolution? n left right = some result) : result = Array.map (fun (value : Int) => Int.ofNat (intCast prime.modulus value).toNat) (Ntt.intPadTo n (Ntt.intLinearConvolution left.toList right.toList)).toArray

A successful erased transform is the padded integer convolution reduced coefficientwise to canonical representatives at this catalogue prime.

def Hex.ZMod64.nttPrimes : List NttPrime

The finite auxiliary-prime catalogue, ordered by modulus.

Equations

• One or more equations did not get rendered due to their size.