def Hex.ZMod64.Ntt.addCoeffs {p : Nat} [Bounds p] : List (ZMod64 p) → List (ZMod64 p) → List (ZMod64 p)

Add coefficient lists, treating a missing tail as zero.

Equations

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

theorem Hex.ZMod64.Ntt.evalCoeffs_add {p : Nat} [Bounds p] (point : ZMod64 p) (left right : List (ZMod64 p)) : evalCoeffs point (addCoeffs left right) = evalCoeffs point left + evalCoeffs point right

Coefficientwise addition commutes with polynomial evaluation.

def Hex.ZMod64.Ntt.linearConvolution {p : Nat} [Bounds p] : List (ZMod64 p) → List (ZMod64 p) → List (ZMod64 p)

Ordinary low-to-high schoolbook coefficient convolution.

Equations

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

theorem Hex.ZMod64.Ntt.evalCoeffs_linearConvolution {p : Nat} [Bounds p] (point : ZMod64 p) (left right : List (ZMod64 p)) : evalCoeffs point (linearConvolution left right) = evalCoeffs point left * evalCoeffs point right

Schoolbook convolution evaluates to the product of the two evaluations.

@[simp]

theorem Hex.ZMod64.Ntt.evalCoeffs_replicate_zero {p : Nat} [Bounds p] (point : ZMod64 p) (count : Nat) : evalCoeffs point (List.replicate count 0) = 0

A list of zero coefficients evaluates to zero.

def Hex.ZMod64.Ntt.monomial {p : Nat} [Bounds p] (n degree : Nat) (coefficient : ZMod64 p) : List (ZMod64 p)

A fixed-length coefficient vector containing one nonzero monomial.

Equations

• Hex.ZMod64.Ntt.monomial n degree coefficient = if _hn : n = 0 then [] else List.replicate (degree % n) 0 ++ coefficient :: List.replicate (n - (degree % n + 1)) 0

@[simp]

theorem Hex.ZMod64.Ntt.length_monomial {p : Nat} [Bounds p] (n degree : Nat) (coefficient : ZMod64 p) (hn : 0 < n) : (monomial n degree coefficient).length = n

A positive-length monomial vector has exactly the requested length.

theorem Hex.ZMod64.Ntt.evalCoeffs_monomial {p : Nat} [Bounds p] (point : ZMod64 p) (n degree : Nat) (coefficient : ZMod64 p) (hn : 0 < n) : evalCoeffs point (monomial n degree coefficient) = point ^ (degree % n) * coefficient

Evaluating a monomial vector gives its represented monomial.

theorem Hex.ZMod64.Ntt.length_addCoeffs {p : Nat} [Bounds p] (left right : List (ZMod64 p)) (hlength : left.length = right.length) : (addCoeffs left right).length = left.length

Adding equal-sized coefficient vectors preserves their common length.

theorem Hex.ZMod64.Ntt.length_addCoeffs_eq_max {p : Nat} [Bounds p] (left right : List (ZMod64 p)) : (addCoeffs left right).length = max left.length right.length

The zero-extending coefficient sum has the longer input length.

theorem Hex.ZMod64.Ntt.length_linearConvolution_le {p : Nat} [Bounds p] (left right : List (ZMod64 p)) : (linearConvolution left right).length ≤ left.length + right.length - 1

The schoolbook result fits in the standard ordinary-product length.

def Hex.ZMod64.Ntt.foldCyclicFrom {p : Nat} [Bounds p] (n : Nat) : Nat → List (ZMod64 p) → List (ZMod64 p)

Fold coefficients into a fixed cyclic vector, starting at a supplied absolute degree.

Equations

• Hex.ZMod64.Ntt.foldCyclicFrom n x✝ [] = List.replicate n 0
• Hex.ZMod64.Ntt.foldCyclicFrom n x✝ (coefficient :: coefficients) = Hex.ZMod64.Ntt.addCoeffs (Hex.ZMod64.Ntt.monomial n x✝ coefficient) (Hex.ZMod64.Ntt.foldCyclicFrom n (x✝ + 1) coefficients)

theorem Hex.ZMod64.Ntt.length_foldCyclicFrom {p : Nat} [Bounds p] (n degree : Nat) (coefficients : List (ZMod64 p)) (hn : 0 < n) : (foldCyclicFrom n degree coefficients).length = n

Cyclic folding always produces exactly n coefficients when n is positive.

theorem Hex.ZMod64.Ntt.evalCoeffs_foldCyclicFrom {p : Nat} [Bounds p] (point : ZMod64 p) (n degree : Nat) (coefficients : List (ZMod64 p)) (hn : 0 < n) (hroot : point ^ n = 1) : evalCoeffs point (foldCyclicFrom n degree coefficients) = point ^ degree * evalCoeffs point coefficients

At an nth root of unity, cyclic folding preserves evaluation, including the absolute-degree shift used by the recursive worker.

def Hex.ZMod64.Ntt.foldCyclic {p : Nat} [Bounds p] (n : Nat) (coefficients : List (ZMod64 p)) : List (ZMod64 p)

Fold an ordinary coefficient list modulo x^n - 1.

Equations

• Hex.ZMod64.Ntt.foldCyclic n coefficients = Hex.ZMod64.Ntt.foldCyclicFrom n 0 coefficients

@[simp]

theorem Hex.ZMod64.Ntt.length_foldCyclic {p : Nat} [Bounds p] (n : Nat) (coefficients : List (ZMod64 p)) (hn : 0 < n) : (foldCyclic n coefficients).length = n

A positive-length cyclic fold has exactly the requested length.

theorem Hex.ZMod64.Ntt.evalCoeffs_foldCyclic {p : Nat} [Bounds p] (point : ZMod64 p) (n : Nat) (coefficients : List (ZMod64 p)) (hn : 0 < n) (hroot : point ^ n = 1) : evalCoeffs point (foldCyclic n coefficients) = evalCoeffs point coefficients

Cyclic folding preserves evaluation at every nth root of unity.

def Hex.ZMod64.Ntt.cyclicConvolution {p : Nat} [Bounds p] (n : Nat) (left right : List (ZMod64 p)) : List (ZMod64 p)

Independent coefficient-level cyclic convolution reference.

Equations

• Hex.ZMod64.Ntt.cyclicConvolution n left right = Hex.ZMod64.Ntt.foldCyclic n (Hex.ZMod64.Ntt.linearConvolution left right)

theorem Hex.ZMod64.Ntt.evalCoeffs_cyclicConvolution {p : Nat} [Bounds p] (point : ZMod64 p) (n : Nat) (left right : List (ZMod64 p)) (hn : 0 < n) (hroot : point ^ n = 1) : evalCoeffs point (cyclicConvolution n left right) = evalCoeffs point left * evalCoeffs point right

Cyclic convolution evaluates to the pointwise product at every nth root of unity.

theorem Hex.ZMod64.Ntt.dftCoeff_cyclicConvolution {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right : List (ZMod64 p)) (frequency : Nat) : dftCoeff plan.root (cyclicConvolution n left right) frequency = dftCoeff plan.root left frequency * dftCoeff plan.root right frequency

Every DFT coefficient of a cyclic convolution is the pointwise product of the corresponding input coefficients.

def Hex.ZMod64.Ntt.pointwiseMul {p : Nat} [Bounds p] (left right : List (ZMod64 p)) : List (ZMod64 p)

Pointwise multiplication of equal-order transform values.

Equations

• Hex.ZMod64.Ntt.pointwiseMul left right = List.zipWith (fun (x1 x2 : Hex.ZMod64 p) => x1 * x2) left right

theorem Hex.ZMod64.Ntt.dft_cyclicConvolution {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right : List (ZMod64 p)) : dft plan.root n (cyclicConvolution n left right) = pointwiseMul (dft plan.root n left) (dft plan.root n right)

The DFT of cyclic convolution is pointwise multiplication.

def Hex.ZMod64.Ntt.pointwiseMulArray {p : Nat} [Bounds p] (left right : Array (ZMod64 p)) : Array (ZMod64 p)

Array wrapper for pointwise multiplication.

Equations

• Hex.ZMod64.Ntt.pointwiseMulArray left right = (Hex.ZMod64.Ntt.pointwiseMul left.toList right.toList).toArray

theorem Hex.ZMod64.Ntt.pointwise_forward_eq_cyclic {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right : Array (ZMod64 p)) (hleft : left.size = n) (hright : right.size = n) : pointwiseMulArray (forwardRadixArray plan left) (forwardRadixArray plan right) = forwardRadixArray plan (cyclicConvolution n left.toList right.toList).toArray

Pointwise multiplication of the two executable forward results is the forward result of the independent cyclic-convolution reference.

def Hex.ZMod64.Ntt.cyclic? {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right : Array (ZMod64 p)) : Option (Array (ZMod64 p))

Checked cyclic NTT convolution. Length mismatch is normal failure.

Equations

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

theorem Hex.ZMod64.Ntt.cyclic?_eq_reference {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right : Array (ZMod64 p)) (hleft : left.size = n) (hright : right.size = n) : cyclic? plan left right = some (cyclicConvolution n left.toList right.toList).toArray

Successful cyclic NTT convolution is exactly schoolbook convolution folded modulo x^n - 1.

def Hex.ZMod64.Ntt.padTo {p : Nat} [Bounds p] (n : Nat) (coefficients : List (ZMod64 p)) : List (ZMod64 p)

Append enough zero coefficients to reach a requested capacity. Callers use it only when the input already fits.

Equations

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

@[simp]

theorem Hex.ZMod64.Ntt.length_padTo {p : Nat} [Bounds p] (n : Nat) (coefficients : List (ZMod64 p)) (hfit : coefficients.length ≤ n) : (padTo n coefficients).length = n

Padding a fitting list reaches exactly the requested length.

@[simp]

theorem Hex.ZMod64.Ntt.evalCoeffs_padTo {p : Nat} [Bounds p] (point : ZMod64 p) (n : Nat) (coefficients : List (ZMod64 p)) : evalCoeffs point (padTo n coefficients) = evalCoeffs point coefficients

Appending zero coefficients does not change evaluation.

theorem Hex.ZMod64.Ntt.dftArray_injective {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) {left right : Array (ZMod64 p)} (hleft : left.size = n) (hright : right.size = n) (hequal : dftArray plan.root n left = dftArray plan.root n right) : left = right

The exact-order DFT is injective on arrays of its plan length.

theorem Hex.ZMod64.Ntt.foldCyclic_eq_pad {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (coefficients : List (ZMod64 p)) (hfit : coefficients.length ≤ n) : (foldCyclic n coefficients).toArray = (padTo n coefficients).toArray

When no coefficient reaches degree n, cyclic folding is just zero padding.

theorem Hex.ZMod64.Ntt.cyclicConvolution_eq_linear {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right : List (ZMod64 p)) (hcapacity : left.length + right.length - 1 ≤ n) : (cyclicConvolution n left right).toArray = (padTo n (linearConvolution left right)).toArray

A plan whose length covers the ordinary product turns cyclic convolution into the zero-padded schoolbook result.

theorem Hex.ZMod64.Ntt.dft_padTo {p : Nat} [Bounds p] (root : ZMod64 p) (count n : Nat) (coefficients : List (ZMod64 p)) : dft root count (padTo n coefficients) = dft root count coefficients

Zero padding does not change any requested DFT coefficient.

theorem Hex.ZMod64.Ntt.cyclicConvolution_pad_inputs {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right : List (ZMod64 p)) : (cyclicConvolution n (padTo n left) (padTo n right)).toArray = (cyclicConvolution n left right).toArray

Padding either cyclic-convolution input with zeros does not alter the fixed-length cyclic result.

def Hex.ZMod64.Ntt.ordinary? {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right : Array (ZMod64 p)) : Option (Array (ZMod64 p))

Checked ordinary convolution. The plan length must be the least power of two covering the product, and each input must fit that padded length.

Equations

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

theorem Hex.ZMod64.Ntt.ordinary?_eq_reference {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right : Array (ZMod64 p)) (hnext : n = (left.size + right.size - 1).nextPowerOfTwo) (hleft : left.size ≤ n) (hright : right.size ≤ n) : ordinary? plan left right = some (padTo n (linearConvolution left.toList right.toList)).toArray

Padding to nextPowerOfTwo (left.size + right.size - 1) and running the NTT returns the zero-padded ordinary schoolbook convolution.

theorem Hex.ZMod64.Ntt.ordinary?_eq_of_some {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (left right result : Array (ZMod64 p)) (hresult : ordinary? plan left right = some result) : result = (padTo n (linearConvolution left.toList right.toList)).toArray

A successful checked ordinary convolution has the independent coefficient-level reference value. This packages the length checks performed inside ordinary?, so coefficient-owner adapters need no duplicate unchecked hypotheses.

theorem Hex.ZMod64.Ntt.pow_mod_div {p : Nat} [Bounds p] (point : ZMod64 p) (n degree : Nat) : point ^ degree = point ^ (degree % n) * (point ^ n) ^ (degree / n)

Split an exponent into its residue and quotient contributions.

def Hex.ZMod64.Ntt.foldNegacyclicFrom {p : Nat} [Bounds p] (n : Nat) : Nat → List (ZMod64 p) → List (ZMod64 p)

Fold coefficients into a fixed negacyclic vector, starting at a supplied absolute degree. The quotient by n records the alternating sign.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.foldNegacyclicFrom n x✝ [] = List.replicate n 0

theorem Hex.ZMod64.Ntt.length_foldNegacyclicFrom {p : Nat} [Bounds p] (n degree : Nat) (coefficients : List (ZMod64 p)) (hn : 0 < n) : (foldNegacyclicFrom n degree coefficients).length = n

Negacyclic folding always produces exactly n coefficients when n is positive.

theorem Hex.ZMod64.Ntt.evalCoeffs_foldNegacyclicFrom {p : Nat} [Bounds p] (point : ZMod64 p) (n degree : Nat) (coefficients : List (ZMod64 p)) (hn : 0 < n) (hroot : point ^ n = 0 - 1) : evalCoeffs point (foldNegacyclicFrom n degree coefficients) = point ^ degree * evalCoeffs point coefficients

At a root of x^n = -1, negacyclic folding preserves evaluation, including the absolute-degree shift used by the recursive worker.

def Hex.ZMod64.Ntt.foldNegacyclic {p : Nat} [Bounds p] (n : Nat) (coefficients : List (ZMod64 p)) : List (ZMod64 p)

Fold an ordinary coefficient list modulo x^n + 1.

Equations

• Hex.ZMod64.Ntt.foldNegacyclic n coefficients = Hex.ZMod64.Ntt.foldNegacyclicFrom n 0 coefficients

@[simp]

theorem Hex.ZMod64.Ntt.length_foldNegacyclic {p : Nat} [Bounds p] (n : Nat) (coefficients : List (ZMod64 p)) (hn : 0 < n) : (foldNegacyclic n coefficients).length = n

A positive-length negacyclic fold has exactly the requested length.

theorem Hex.ZMod64.Ntt.evalCoeffs_foldNegacyclic {p : Nat} [Bounds p] (point : ZMod64 p) (n : Nat) (coefficients : List (ZMod64 p)) (hn : 0 < n) (hroot : point ^ n = 0 - 1) : evalCoeffs point (foldNegacyclic n coefficients) = evalCoeffs point coefficients

Negacyclic folding preserves evaluation at every root of x^n = -1.

def Hex.ZMod64.Ntt.negacyclicConvolution {p : Nat} [Bounds p] (n : Nat) (left right : List (ZMod64 p)) : List (ZMod64 p)

Independent coefficient-level negacyclic convolution reference.

Equations

• Hex.ZMod64.Ntt.negacyclicConvolution n left right = Hex.ZMod64.Ntt.foldNegacyclic n (Hex.ZMod64.Ntt.linearConvolution left right)

theorem Hex.ZMod64.Ntt.evalCoeffs_negacyclicConvolution {p : Nat} [Bounds p] (point : ZMod64 p) (n : Nat) (left right : List (ZMod64 p)) (hn : 0 < n) (hroot : point ^ n = 0 - 1) : evalCoeffs point (negacyclicConvolution n left right) = evalCoeffs point left * evalCoeffs point right

Negacyclic convolution evaluates to the pointwise product at every root of x^n = -1.

theorem Hex.ZMod64.Ntt.exactOrder_two_mul_half {p n : Nat} [Bounds p] [PrimeModulus p] (twist : ZMod64 p) (hn : 0 < n) (horder : twist.ExactOrder (2 * n)) : twist ^ n = 0 - 1

A primitive root of exact order 2n has nth power -1.

structure Hex.ZMod64.Ntt.NegacyclicPlan (p n : Nat) [Bounds p] [PrimeModulus p] : Type

Data required by the standard twist adapter from negacyclic convolution of length n to an ordinary cyclic NTT of length n.

• transform : NttPlan p n

  The reusable length-n transform.

• twist : ZMod64 p

  A primitive 2nth root used to twist coefficients.

• twist_order : self.twist.ExactOrder (2 * n)

  The twist has exact order 2n.

• root_eq : self.transform.root = self.twist ^ 2

  Squaring the twist gives the transform root.

theorem Hex.ZMod64.Ntt.NegacyclicPlan.length_pos {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) : 0 < n

A negacyclic plan's transform length is positive.

theorem Hex.ZMod64.Ntt.NegacyclicPlan.twist_pow_length {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) : plan.twist ^ n = 0 - 1

The primitive twist satisfies the defining negacyclic equation.

theorem Hex.ZMod64.Ntt.NegacyclicPlan.twist_ne_zero {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) : plan.twist ≠ 0

The primitive twist is nonzero.

def Hex.ZMod64.Ntt.scalePowersFrom {p : Nat} [Bounds p] (root : ZMod64 p) : Nat → List (ZMod64 p) → List (ZMod64 p)

Multiply coefficient i by root^(degree + i).

Equations

• Hex.ZMod64.Ntt.scalePowersFrom root x✝ [] = []
• Hex.ZMod64.Ntt.scalePowersFrom root x✝ (coefficient :: coefficients) = root ^ x✝ * coefficient :: Hex.ZMod64.Ntt.scalePowersFrom root (x✝ + 1) coefficients

@[simp]

theorem Hex.ZMod64.Ntt.length_scalePowersFrom {p : Nat} [Bounds p] (root : ZMod64 p) (degree : Nat) (coefficients : List (ZMod64 p)) : (scalePowersFrom root degree coefficients).length = coefficients.length

Power scaling preserves the coefficient-list length.

theorem Hex.ZMod64.Ntt.evalCoeffs_scalePowersFrom {p : Nat} [Bounds p] (root point : ZMod64 p) (degree : Nat) (coefficients : List (ZMod64 p)) : evalCoeffs point (scalePowersFrom root degree coefficients) = root ^ degree * evalCoeffs (root * point) coefficients

Evaluation after power scaling is evaluation at the correspondingly scaled point, with the worker's absolute-degree factor.

def Hex.ZMod64.Ntt.scalePowers {p : Nat} [Bounds p] (root : ZMod64 p) (coefficients : List (ZMod64 p)) : List (ZMod64 p)

Multiply coefficient i by root^i.

Equations

• Hex.ZMod64.Ntt.scalePowers root coefficients = Hex.ZMod64.Ntt.scalePowersFrom root 0 coefficients

@[simp]

theorem Hex.ZMod64.Ntt.length_scalePowers {p : Nat} [Bounds p] (root : ZMod64 p) (coefficients : List (ZMod64 p)) : (scalePowers root coefficients).length = coefficients.length

Power scaling preserves list length.

theorem Hex.ZMod64.Ntt.evalCoeffs_scalePowers {p : Nat} [Bounds p] (root point : ZMod64 p) (coefficients : List (ZMod64 p)) : evalCoeffs point (scalePowers root coefficients) = evalCoeffs (root * point) coefficients

Evaluation after coefficient twisting changes the evaluation point.

theorem Hex.ZMod64.Ntt.inv_pow_mul_pow {p : Nat} [Bounds p] [PrimeModulus p] (root : ZMod64 p) (hroot : root ≠ 0) (degree : Nat) : root⁻¹ ^ degree * root ^ degree = 1

Inverse and forward powers of a nonzero residue cancel.

theorem Hex.ZMod64.Ntt.scalePowersFrom_inv {p : Nat} [Bounds p] [PrimeModulus p] (root : ZMod64 p) (hroot : root ≠ 0) (degree : Nat) (coefficients : List (ZMod64 p)) : scalePowersFrom root⁻¹ degree (scalePowersFrom root degree coefficients) = coefficients

Scaling by inverse powers cancels scaling by forward powers.

theorem Hex.ZMod64.Ntt.scalePowers_inv {p : Nat} [Bounds p] [PrimeModulus p] (root : ZMod64 p) (hroot : root ≠ 0) (coefficients : List (ZMod64 p)) : scalePowers root⁻¹ (scalePowers root coefficients) = coefficients

Inverse coefficient twisting cancels forward twisting.

theorem Hex.ZMod64.Ntt.twist_mul_root_pow {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) (frequency : Nat) : plan.twist * plan.transform.root ^ frequency = plan.twist ^ (2 * frequency + 1)

Twisting a transform point selects the corresponding odd power of the primitive 2nth root.

theorem Hex.ZMod64.Ntt.twistPoint_pow_length {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) (frequency : Nat) : (plan.twist * plan.transform.root ^ frequency) ^ n = 0 - 1

Every twisted transform point is a root of x^n = -1.

theorem Hex.ZMod64.Ntt.dftCoeff_cyclic_twist {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) (left right : List (ZMod64 p)) (frequency : Nat) : dftCoeff plan.transform.root (cyclicConvolution n (scalePowers plan.twist left) (scalePowers plan.twist right)) frequency = dftCoeff plan.transform.root (scalePowers plan.twist (negacyclicConvolution n left right)) frequency

At each transform frequency, cyclic convolution of twisted inputs agrees with twisting the independent negacyclic reference.

theorem Hex.ZMod64.Ntt.dft_cyclic_twist {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) (left right : List (ZMod64 p)) : dft plan.transform.root n (cyclicConvolution n (scalePowers plan.twist left) (scalePowers plan.twist right)) = dft plan.transform.root n (scalePowers plan.twist (negacyclicConvolution n left right))

The DFT of cyclic convolution on twisted inputs is the DFT of the twisted negacyclic reference.

theorem Hex.ZMod64.Ntt.dft_scalePowers_padTo {p : Nat} [Bounds p] (root twist : ZMod64 p) (count n : Nat) (coefficients : List (ZMod64 p)) : dft root count (scalePowers twist (padTo n coefficients)) = dft root count (scalePowers twist coefficients)

Zero padding before coefficient twisting does not change the transformed values.

theorem Hex.ZMod64.Ntt.cyclic_twist_eq_negacyclic {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) (left right : List (ZMod64 p)) : (cyclicConvolution n (scalePowers plan.twist left) (scalePowers plan.twist right)).toArray = (scalePowers plan.twist (negacyclicConvolution n left right)).toArray

Cyclic convolution of twisted inputs is exactly the twisted negacyclic coefficient reference.

theorem Hex.ZMod64.Ntt.negacyclicConvolution_pad_inputs {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) (left right : List (ZMod64 p)) : (negacyclicConvolution n (padTo n left) (padTo n right)).toArray = (negacyclicConvolution n left right).toArray

Padding either negacyclic-convolution input with zeros does not alter the fixed-length result.

def Hex.ZMod64.Ntt.negacyclic? {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) (left right : Array (ZMod64 p)) : Option (Array (ZMod64 p))

Checked negacyclic NTT convolution via coefficient twisting. Length mismatch is normal failure.

Equations

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

theorem Hex.ZMod64.Ntt.negacyclic?_eq_reference {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NegacyclicPlan p n) (left right : Array (ZMod64 p)) (hleft : left.size = n) (hright : right.size = n) : negacyclic? plan left right = some (negacyclicConvolution n left.toList right.toList).toArray

A primitive 2nth twist makes the checked adapter return exactly schoolbook convolution folded modulo x^n + 1.