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

A transform plan always has positive length.

theorem Hex.ZMod64.NttPlan.length_eq_pow_log2 {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) : n = 2 ^ n.log2

Recover the executable power-of-two exponent used by the transform loop.

theorem Hex.ZMod64.NttPlan.length_lt_modulus {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) : n < p

A valid transform length is strictly smaller than its prime modulus.

theorem Hex.ZMod64.NttPlan.length_ne_zero {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) : ↑n ≠ 0

The transform length is nonzero as a prime-field residue.

theorem Hex.ZMod64.NttPlan.invLength_mul_length {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) : plan.invLength * ↑n = 1

The stored inverse-length scale cancels the transform length.

def Hex.ZMod64.NttPlan.forwardTwiddle {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (i : Nat) : NttTwiddle p

Read a forward twiddle, wrapping the requested exponent into the plan.

Equations

• plan.forwardTwiddle i = plan.forwardTwiddles[i % n]

def Hex.ZMod64.NttPlan.inverseTwiddle {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (i : Nat) : NttTwiddle p

Read an inverse twiddle, wrapping the requested exponent into the plan.

Equations

• plan.inverseTwiddle i = plan.inverseTwiddles[i % n]

theorem Hex.ZMod64.NttPlan.forwardTwiddle_value {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (i : Nat) : (plan.forwardTwiddle i).value = plan.root ^ (i % n)

A forward twiddle is the corresponding wrapped root power.

theorem Hex.ZMod64.NttPlan.inverseTwiddle_value {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (i : Nat) : (plan.inverseTwiddle i).value = plan.invRoot ^ (i % n)

An inverse twiddle is the corresponding wrapped inverse-root power.

theorem Hex.ZMod64.NttPlan.root_ne_zero {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) : plan.root ≠ 0

An exact-order transform root is nonzero.

theorem Hex.ZMod64.NttPlan.invRoot_pow_mul_root_pow {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (e : Nat) : plan.invRoot ^ e * plan.root ^ e = 1

Matching inverse and forward root powers cancel.

theorem Hex.ZMod64.NttPlan.root_half_eq_neg_one {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (hn : 1 < n) : plan.root ^ (n / 2) = 0 - 1

For a nontrivial power-of-two plan, the half-order root power is -1.

theorem Hex.ZMod64.NttPlan.root_stride_half {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride fuel : Nat) (hscale : n = stride * 2 ^ (fuel + 1)) : (plan.root ^ stride) ^ 2 ^ fuel = 0 - 1

At every recursive radix depth, the effective root raised to half the current transform length is minus one.

def Hex.ZMod64.Ntt.interleave {α : Type u} : List α → List α → List α

Interleave two frequency classes. Equal-length inputs produce the usual even/odd merge; the trailing clauses make the helper total.

Equations

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

def Hex.ZMod64.Ntt.deinterleave {α : Type u} : List α → List α × List α

Split a list into its even- and odd-indexed entries.

Equations

• Hex.ZMod64.Ntt.deinterleave [] = ([], [])
• Hex.ZMod64.Ntt.deinterleave [x_1] = ([x_1], [])
• Hex.ZMod64.Ntt.deinterleave (x_1 :: y :: rest) = (x_1 :: (Hex.ZMod64.Ntt.deinterleave rest).fst, y :: (Hex.ZMod64.Ntt.deinterleave rest).snd)

theorem Hex.ZMod64.Ntt.deinterleave_interleave {α : Type u} (left right : List α) (hlength : left.length = right.length) : deinterleave (interleave left right) = (left, right)

Deinterleaving reverses an equal-length interleave.

def Hex.ZMod64.Ntt.forwardStage {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride : Nat) : Nat → List (NttRaw2 p) → List (NttRaw2 p) → List (NttRaw2 p) × List (NttRaw2 p)

One forward DIF stage over two equal-sized halves.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.forwardStage plan stride x✝¹ [] x✝ = ([], [])
• Hex.ZMod64.Ntt.forwardStage plan stride x✝¹ x✝ [] = ([], [])

def Hex.ZMod64.Ntt.inverseStage {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride : Nat) : Nat → List (NttRaw4 p) → List (NttRaw4 p) → List (NttRaw4 p) × List (NttRaw4 p)

One inverse DIT stage over two equal-sized recursive results.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.inverseStage plan stride x✝¹ [] x✝ = ([], [])
• Hex.ZMod64.Ntt.inverseStage plan stride x✝¹ x✝ [] = ([], [])

def Hex.ZMod64.Ntt.forwardStageSpec {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride : Nat) : Nat → List (ZMod64 p) → List (ZMod64 p) → List (ZMod64 p) × List (ZMod64 p)

Canonical-residue specification of one forward DIF stage.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.forwardStageSpec plan stride x✝¹ [] x✝ = ([], [])
• Hex.ZMod64.Ntt.forwardStageSpec plan stride x✝¹ x✝ [] = ([], [])

def Hex.ZMod64.Ntt.inverseStageSpec {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride : Nat) : Nat → List (ZMod64 p) → List (ZMod64 p) → List (ZMod64 p) × List (ZMod64 p)

Canonical-residue specification of one inverse DIT stage.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.inverseStageSpec plan stride x✝¹ [] x✝ = ([], [])
• Hex.ZMod64.Ntt.inverseStageSpec plan stride x✝¹ x✝ [] = ([], [])

theorem Hex.ZMod64.Ntt.eval_forwardStageSpec_fst {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (point : ZMod64 p) (left right : List (ZMod64 p)) (hlength : left.length = right.length) : evalCoeffs point (forwardStageSpec plan stride i left right).fst = evalCoeffs point left + evalCoeffs point right

Evaluating the sum half of a forward DIF stage adds the evaluations of the two input halves.

theorem Hex.ZMod64.Ntt.eval_forwardStageSpec_snd {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (point : ZMod64 p) (left right : List (ZMod64 p)) (hlength : left.length = right.length) : evalCoeffs point (forwardStageSpec plan stride i left right).snd = plan.root ^ (i * stride) * (evalCoeffs (plan.root ^ stride * point) left - evalCoeffs (plan.root ^ stride * point) right)

Evaluating the difference half of a forward DIF stage absorbs its coefficient twiddles into the evaluation point.

theorem Hex.ZMod64.Ntt.normalize_forwardStage {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (left right : List (NttRaw2 p)) : have raw := forwardStage plan stride i left right; (List.map NttRaw2.normalize raw.fst, List.map NttRaw2.normalize raw.snd) = forwardStageSpec plan stride i (List.map NttRaw2.normalize left) (List.map NttRaw2.normalize right)

Normalizing a raw forward stage gives its residue-level specification.

theorem Hex.ZMod64.Ntt.normalize_inverseStage {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (left right : List (NttRaw4 p)) : have raw := inverseStage plan stride i left right; (List.map NttRaw4.normalize raw.fst, List.map NttRaw4.normalize raw.snd) = inverseStageSpec plan stride i (List.map NttRaw4.normalize left) (List.map NttRaw4.normalize right)

Normalizing a raw inverse stage gives its residue-level specification.

theorem Hex.ZMod64.Ntt.inverse_forwardStageSpec {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (left right : List (ZMod64 p)) (hlength : left.length = right.length) : have forward := forwardStageSpec plan stride i left right; inverseStageSpec plan stride i forward.fst forward.snd = (List.map (fun (value : ZMod64 p) => value + value) left, List.map (fun (value : ZMod64 p) => value + value) right)

Applying the inverse stage to one forward stage doubles both original halves.

theorem Hex.ZMod64.Ntt.inverseStageSpec_scale {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (c : ZMod64 p) (left right : List (ZMod64 p)) (hlength : left.length = right.length) : inverseStageSpec plan stride i (List.map (fun (value : ZMod64 p) => c * value) left) (List.map (fun (value : ZMod64 p) => c * value) right) = have output := inverseStageSpec plan stride i left right; (List.map (fun (value : ZMod64 p) => c * value) output.fst, List.map (fun (value : ZMod64 p) => c * value) output.snd)

Inverse stages commute with a common scalar on both halves.

theorem Hex.ZMod64.Ntt.forwardStageSpec_lengths {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (left right : List (ZMod64 p)) (hlength : left.length = right.length) : have output := forwardStageSpec plan stride i left right; output.fst.length = left.length ∧ output.snd.length = right.length

A residue-level forward stage preserves both equal half lengths.

theorem Hex.ZMod64.Ntt.inverseStageSpec_lengths {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (left right : List (ZMod64 p)) (hlength : left.length = right.length) : have output := inverseStageSpec plan stride i left right; output.fst.length = left.length ∧ output.snd.length = right.length

A residue-level inverse stage preserves both equal half lengths.

def Hex.ZMod64.Ntt.forwardGo {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride : Nat) : Nat → List (NttRaw2 p) → List (NttRaw2 p)

Recursive DIF forward transform. fuel is the remaining radix-two depth and stride is the root-power stride at this level.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.forwardGo plan stride 0 x✝ = x✝

def Hex.ZMod64.Ntt.inverseGo {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride : Nat) : Nat → List (NttRaw4 p) → List (NttRaw4 p)

Recursive DIT inverse transform. Its input is in ordinary DFT order, so the even and odd frequency classes are separated before recursion.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.inverseGo plan stride 0 x✝ = x✝

def Hex.ZMod64.Ntt.forwardRadix {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride : Nat) : Nat → List (ZMod64 p) → List (ZMod64 p)

Residue-level recursive specification of the forward radix-two loop.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.forwardRadix plan stride 0 x✝ = x✝

def Hex.ZMod64.Ntt.inverseRadix {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride : Nat) : Nat → List (ZMod64 p) → List (ZMod64 p)

Residue-level recursive specification of the inverse radix-two loop.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZMod64.Ntt.inverseRadix plan stride 0 x✝ = x✝

theorem Hex.ZMod64.Ntt.length_interleave {α : Type u} (left right : List α) : (interleave left right).length = left.length + right.length

Interleaving preserves the combined input length.

theorem Hex.ZMod64.Ntt.getElem_interleave_even {α : Type u} (left right : List α) (hlength : left.length = right.length) (k : Nat) (hk : k < left.length) : (interleave left right)[2 * k] = left[k]

An even position of an equal-length interleave comes from the left list.

theorem Hex.ZMod64.Ntt.getElem_interleave_odd {α : Type u} (left right : List α) (hlength : left.length = right.length) (k : Nat) (hk : k < right.length) : (interleave left right)[2 * k + 1] = right[k]

An odd position of an equal-length interleave comes from the right list.

theorem Hex.ZMod64.Ntt.forwardStage_lengths {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (left right : List (NttRaw2 p)) (hlength : left.length = right.length) : have output := forwardStage plan stride i left right; output.fst.length = left.length ∧ output.snd.length = right.length

A forward stage preserves both equal half lengths.

theorem Hex.ZMod64.Ntt.inverseStage_lengths {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride i : Nat) (left right : List (NttRaw4 p)) (hlength : left.length = right.length) : have output := inverseStage plan stride i left right; output.fst.length = left.length ∧ output.snd.length = right.length

An inverse stage preserves both equal half lengths.

theorem Hex.ZMod64.Ntt.deinterleave_lengths {α : Type u} (values : List α) (m : Nat) (hlength : values.length = 2 * m) : have halves := deinterleave values; halves.fst.length = m ∧ halves.snd.length = m

Deinterleaving an even list produces two equal halves.

theorem Hex.ZMod64.Ntt.length_forwardGo {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride fuel : Nat) (values : List (NttRaw2 p)) (hlength : values.length = 2 ^ fuel) : (forwardGo plan stride fuel values).length = 2 ^ fuel

The raw forward loop preserves a power-of-two input length.

theorem Hex.ZMod64.Ntt.length_inverseGo {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride fuel : Nat) (values : List (NttRaw4 p)) (hlength : values.length = 2 ^ fuel) : (inverseGo plan stride fuel values).length = 2 ^ fuel

The raw inverse loop preserves a power-of-two input length.

theorem Hex.ZMod64.Ntt.normalize_forwardGo {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride fuel : Nat) (values : List (NttRaw2 p)) : List.map NttRaw2.normalize (forwardGo plan stride fuel values) = forwardRadix plan stride fuel (List.map NttRaw2.normalize values)

The raw forward loop represents its residue-level radix specification at every recursive depth.

theorem Hex.ZMod64.Ntt.normalize_inverseGo {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride fuel : Nat) (values : List (NttRaw4 p)) : List.map NttRaw4.normalize (inverseGo plan stride fuel values) = inverseRadix plan stride fuel (List.map NttRaw4.normalize values)

The raw inverse loop represents its residue-level radix specification at every recursive depth.

theorem Hex.ZMod64.Ntt.length_forwardRadix {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride fuel : Nat) (values : List (ZMod64 p)) (hlength : values.length = 2 ^ fuel) : (forwardRadix plan stride fuel values).length = 2 ^ fuel

The residue-level forward radix recurrence preserves a power-of-two length.

theorem Hex.ZMod64.Ntt.length_inverseRadix {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride fuel : Nat) (values : List (ZMod64 p)) (hlength : values.length = 2 ^ fuel) : (inverseRadix plan stride fuel values).length = 2 ^ fuel

The residue-level inverse radix recurrence preserves a power-of-two length.

theorem Hex.ZMod64.Ntt.forwardRadix_eq_dft {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride fuel : Nat) (values : List (ZMod64 p)) (hlength : values.length = 2 ^ fuel) (hscale : n = stride * 2 ^ fuel) : forwardRadix plan stride fuel values = dft (plan.root ^ stride) (2 ^ fuel) values

At every recursive depth, the residue-level forward recurrence is the coefficientwise DFT for the effective root at that depth.

theorem Hex.ZMod64.Ntt.inverse_forwardRadix {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (stride fuel : Nat) (values : List (ZMod64 p)) (hlength : values.length = 2 ^ fuel) : inverseRadix plan stride fuel (forwardRadix plan stride fuel values) = List.map (fun (value : ZMod64 p) => ↑(2 ^ fuel) * value) values

The unscaled inverse radix recurrence cancels the forward recurrence and multiplies every coefficient by the transform length.

def Hex.ZMod64.Ntt.forwardRadixArray {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) : Array (ZMod64 p)

Residue-level forward result computed by the radix specification.

Equations

• Hex.ZMod64.Ntt.forwardRadixArray plan values = (Hex.ZMod64.Ntt.forwardRadix plan 1 n.log2 values.toList).toArray

def Hex.ZMod64.Ntt.inverseRadixArray {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) : Array (ZMod64 p)

Residue-level inverse result, including the final n⁻¹ scaling.

Equations

• Hex.ZMod64.Ntt.inverseRadixArray plan values = Array.map (fun (value : Hex.ZMod64 p) => plan.invLength * value) (Hex.ZMod64.Ntt.inverseRadix plan 1 n.log2 values.toList).toArray

theorem Hex.ZMod64.Ntt.forwardArray_eq_dft {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) (hsize : values.size = n) : forwardRadixArray plan values = dftArray plan.root n values

The residue-level forward array is exactly the coefficientwise DFT.

theorem Hex.ZMod64.Ntt.inverse_forwardArray {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) (hsize : values.size = n) : inverseRadixArray plan (forwardRadixArray plan values) = values

The scaled residue-level inverse exactly cancels the forward transform on an array of the plan length.

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

Forward radix-two transform. A length mismatch is normal checked failure; successful execution reuses every root power from plan.

Equations

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

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

Inverse radix-two transform, including multiplication by n⁻¹ after the raw inverse loop.

Equations

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

theorem Hex.ZMod64.Ntt.forward?_eq_radix {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) (hsize : values.size = n) : forward? plan values = some (forwardRadixArray plan values)

Successful forward execution is exactly its residue-level radix specification.

theorem Hex.ZMod64.Ntt.forward?_eq_dft {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) (hsize : values.size = n) : forward? plan values = some (dftArray plan.root n values)

Successful public forward execution is the coefficientwise DFT.

theorem Hex.ZMod64.Ntt.inverse?_eq_radix {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) (hsize : values.size = n) : inverse? plan values = some (inverseRadixArray plan values)

Successful inverse execution is exactly its residue-level radix specification.

theorem Hex.ZMod64.Ntt.forward?_eq_none_iff {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) : forward? plan values = none ↔ values.size ≠ n

Forward execution rejects exactly a length mismatch.

theorem Hex.ZMod64.Ntt.inverse?_eq_none_iff {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) : inverse? plan values = none ↔ values.size ≠ n

Inverse execution rejects exactly a length mismatch.

theorem Hex.ZMod64.Ntt.forward?_size {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values result : Array (ZMod64 p)) (hrun : forward? plan values = some result) : result.size = n

Every successful forward transform has the plan length.

theorem Hex.ZMod64.Ntt.inverse?_size {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values result : Array (ZMod64 p)) (hrun : inverse? plan values = some result) : result.size = n

Every successful inverse transform has the plan length.

theorem Hex.ZMod64.Ntt.inverse?_forward? {p n : Nat} [Bounds p] [PrimeModulus p] (plan : NttPlan p n) (values : Array (ZMod64 p)) (hsize : values.size = n) : (forward? plan values).bind (inverse? plan) = some values

On an array of the plan length, public forward execution followed by public inverse execution returns the original array.