theorem Hex.FpPoly.ofList_linearConvolution {p : Nat} [ZMod64.Bounds p] (left right : List (ZMod64 p)) : DensePoly.ofList (ZMod64.Ntt.linearConvolution left right) = DensePoly.ofList left * DensePoly.ofList right

The independent NTT coefficient reference normalizes to the existing schoolbook polynomial product.

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

Multiply two finite-field polynomials with a reusable plan for the target modulus. none means that the plan length is not exactly the least power-of-two length covering the ordinary product.

Equations

• Hex.FpPoly.mulNtt? plan left right = Option.map Hex.DensePoly.ofCoeffs (Hex.ZMod64.Ntt.ordinary? plan (Hex.DensePoly.toArray left) (Hex.DensePoly.toArray right))

theorem Hex.FpPoly.mulNtt?_eq {p : Nat} [ZMod64.Bounds p] {n : Nat} [ZMod64.PrimeModulus p] (plan : ZMod64.NttPlan p n) (left right result : FpPoly p) (hresult : mulNtt? plan left right = some result) : result = left * right

Every successful direct NTT multiplication equals schoolbook multiplication. No unchecked root or capacity hypothesis is exposed to the caller: both are carried by the plan and checked operation.

def Hex.FpPoly.nttLength {p : Nat} [ZMod64.Bounds p] (left right : FpPoly p) : Nat

Least radix-two transform capacity covering the ordinary product.

Equations

• left.nttLength right = (Hex.DensePoly.size left + Hex.DensePoly.size right - 1).nextPowerOfTwo

def Hex.FpPoly.nttCrtBound {p : Nat} [ZMod64.Bounds p] (left right : FpPoly p) : Nat

Absolute bound for the integer convolution of canonical representatives.

Equations

• left.nttCrtBound right = min (Hex.DensePoly.size left) (Hex.DensePoly.size right) * ((p - 1) * (p - 1))

def Hex.FpPoly.mulNttCrt? {p : Nat} [ZMod64.Bounds p] (left right : FpPoly p) : Option (FpPoly p)

Multiply canonical coefficient lifts through the fixed auxiliary-prime catalogue, reconstruct over the integers, and reduce back modulo p. none records a catalogue capacity or checked-plan failure.

Equations

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

theorem Hex.FpPoly.mulNttCrt?_eq {p : Nat} [ZMod64.Bounds p] (left right result : FpPoly p) (hresult : left.mulNttCrt? right = some result) : result = left * right

Every successful auxiliary-prime multiplication agrees with the schoolbook finite-field product.

def Hex.FpPoly.nttCrtCutoff : Nat

Shorter-size threshold below which the packed lazy-reduction kernel avoids auxiliary-plan construction. The forced-kernel sweep over F_65537 keeps packed multiplication ahead through 4096 coefficients per operand; CRT-NTT is clearly ahead at 8192 and above. Keeping the policy value named lets modulus-specific sweeps recalibrate it without changing the dispatcher proof.

Equations

• Hex.FpPoly.nttCrtCutoff = 8192

def Hex.FpPoly.karatsubaCutoff : Nat

Leaf cutoff for the generic Karatsuba fallback used when the fixed auxiliary catalogue cannot serve a large request.

Equations

• Hex.FpPoly.karatsubaCutoff = 32

def Hex.FpPoly.mulFast {p : Nat} [ZMod64.Bounds p] (left right : FpPoly p) : FpPoly p

Total finite-field multiplication. Small products use the packed lazy-reduction kernel; large products try auxiliary-prime NTTs and fall back to Karatsuba on normal catalogue exhaustion.

Equations

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

theorem Hex.FpPoly.mulFast_eq {p : Nat} [ZMod64.Bounds p] (left right : FpPoly p) : left.mulFast right = left * right

The total finite-field dispatcher is independent of its crossover constants and agrees with schoolbook multiplication.

def Hex.FpPoly.fastPlan {p : Nat} [ZMod64.Bounds p] : DensePoly.MulPlan (ZMod64 p)

Coefficient-owner multiplication plan for generic fast algorithms. Full products use mulFast, squaring and slices use the proved Karatsuba kernels.

Equations

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

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

Direct cyclic NTT multiplication. Inputs shorter than the quotient length are zero-padded; an input exceeding that length is rejected.

Equations

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

theorem Hex.FpPoly.mulCyclicNtt?_eq {p : Nat} [ZMod64.Bounds p] {n : Nat} [ZMod64.PrimeModulus p] (plan : ZMod64.NttPlan p n) (left right result : FpPoly p) (hresult : mulCyclicNtt? plan left right = some result) : result = DensePoly.ofList (ZMod64.Ntt.cyclicConvolution n (DensePoly.toList left) (DensePoly.toList right))

A successful direct cyclic transform is the independent schoolbook product folded modulo x^n - 1.

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

Direct negacyclic NTT multiplication through a primitive 2nth-root twist. Inputs shorter than n are zero-padded and oversized inputs are rejected.

Equations

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

theorem Hex.FpPoly.mulNegacyclicNtt?_eq {p : Nat} [ZMod64.Bounds p] {n : Nat} [ZMod64.PrimeModulus p] (plan : ZMod64.Ntt.NegacyclicPlan p n) (left right result : FpPoly p) (hresult : mulNegacyclicNtt? plan left right = some result) : result = DensePoly.ofList (ZMod64.Ntt.negacyclicConvolution n (DensePoly.toList left) (DensePoly.toList right))

A successful direct negacyclic transform is the independent schoolbook product folded modulo x^n + 1.