structure Hex.ZMod64.Ntt.CrtSelection (n bound : Nat) : Type

A checked catalogue selection with enough pairwise-coprime modulus product for strict symmetric reconstruction.

• primes : List NttPrime

  Selected catalogue entries, in catalogue order.

• hasPrime : self.primes ≠ []

  At least one transform is run, including at bound zero.

• fits (prime : NttPrime) : prime ∈ self.primes → n ≤ prime.maxLength

  Every selected prime supports the requested transform length.

• enough : 2 * bound < (List.map NttPrime.modulus self.primes).prod

  The selected product is strictly larger than twice the supplied bound.

def Hex.ZMod64.Ntt.CrtSelection.build? (n bound : Nat) : Option (CrtSelection n bound)

Select and validate a sufficient supported catalogue prefix.

Equations

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

def Hex.ZMod64.Ntt.CrtSelection.moduli {n bound : Nat} (selection : CrtSelection n bound) : Array Nat

Selected moduli in the same order expected by batch CRT.

Equations

• selection.moduli = (List.map Hex.ZMod64.NttPrime.modulus selection.primes).toArray

@[simp]

theorem Hex.ZMod64.Ntt.CrtSelection.moduli_toList {n bound : Nat} (selection : CrtSelection n bound) : selection.moduli.toList = List.map NttPrime.modulus selection.primes

@[simp]

theorem Hex.ZMod64.Ntt.CrtSelection.moduli_size {n bound : Nat} (selection : CrtSelection n bound) : selection.moduli.size = selection.primes.length

theorem Hex.ZMod64.Ntt.CrtSelection.enough_moduli {n bound : Nat} (selection : CrtSelection n bound) : 2 * bound < selection.moduli.toList.prod

inductive Hex.ZMod64.Ntt.CrtMatches (reference : List Int) {n : Nat} : List NttPrime → List (Vector Int n) → Prop

Coefficientwise congruence between a prime list and its erased residue vectors.

• nil {reference : List Int} {x✝ : Nat} : CrtMatches reference [] []
• cons {reference : List Int} {n : Nat} {prime : NttPrime} {primes : List NttPrime} {residue : Vector Int n} {residues : List (Vector Int n)} : (∀ (j : Fin n), reference.getD (↑j) 0 % ↑prime.modulus = residue[j] % ↑prime.modulus) → CrtMatches reference primes residues → CrtMatches reference (prime :: primes) (residue :: residues)

structure Hex.ZMod64.Ntt.CrtImages {n bound : Nat} (selection : CrtSelection n bound) (left right : Array Int) : Type

Erased NTT residues paired with their coefficientwise congruence proof.

• residues : List (Vector Int n)
• sound : CrtMatches (intPadTo n (intLinearConvolution left.toList right.toList)) selection.primes self.residues
• referenceSize : (intPadTo n (intLinearConvolution left.toList right.toList)).length = n

theorem Hex.ZMod64.Ntt.CrtMatches.length_eq {n : Nat} {reference : List Int} {primes : List NttPrime} {residues : List (Vector Int n)} (h : CrtMatches reference primes residues) : residues.length = primes.length

theorem Hex.ZMod64.Ntt.CrtMatches.getElem {n : Nat} {reference : List Int} {primes : List NttPrime} {residues : List (Vector Int n)} (h : CrtMatches reference primes residues) (i : Nat) (hi : i < primes.length) (j : Fin n) : reference.getD (↑j) 0 % ↑primes[i].modulus = residues[i][j] % ↑primes[i].modulus

def Hex.ZMod64.Ntt.CrtSelection.images? {n bound : Nat} (selection : CrtSelection n bound) (left right : Array Int) : Option (CrtImages selection left right)

Run an integer convolution at every prime in a checked selection.

Equations

• selection.images? left right = do let images ← Hex.ZMod64.Ntt.runPrimes?✝ n left right selection.primes pure { residues := images.val, sound := ⋯, referenceSize := ⋯ }

@[simp]

theorem Hex.ZMod64.Ntt.CrtImages.residues_length {n bound : Nat} {selection : CrtSelection n bound} {left right : Array Int} (images : CrtImages selection left right) : images.residues.length = selection.primes.length

def Hex.ZMod64.Ntt.CrtImages.residueArray {n bound : Nat} {selection : CrtSelection n bound} {left right : Array Int} (images : CrtImages selection left right) : Array (Vector Int n)

Residue vectors in batch-CRT input form.

Equations

• images.residueArray = images.residues.toArray

@[simp]

theorem Hex.ZMod64.Ntt.CrtImages.residueArray_size {n bound : Nat} {selection : CrtSelection n bound} {left right : Array Int} (images : CrtImages selection left right) : images.residueArray.size = selection.moduli.size

theorem Hex.ZMod64.Ntt.CrtImages.congr {n bound : Nat} {selection : CrtSelection n bound} {left right : Array Int} (images : CrtImages selection left right) (i : Fin selection.moduli.size) (j : Fin n) : (intPadTo n (intLinearConvolution left.toList right.toList)).getD (↑j) 0 % ↑selection.moduli[i] = (images.residueArray.getD (↑i) (Vector.replicate n 0))[j] % ↑selection.moduli[i]

Each erased residue lane is congruent to the reference integer convolution at the corresponding selected modulus.