theorem Hex.ZPoly.ofList_intLinearConvolution (left right : List Int) : DensePoly.ofList (ZMod64.Ntt.intLinearConvolution left right) = DensePoly.ofList left * DensePoly.ofList right

The independent integer coefficient convolution normalizes to the existing schoolbook polynomial product.

def Hex.ZPoly.nttLength (left right : ZPoly) : 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.ZPoly.mulNttCrt? (left right : ZPoly) : Option ZPoly

Multiply through the fixed auxiliary NTT-prime catalogue and balanced batch CRT. Failure records catalogue exhaustion or a failed checked plan; callers that need a total operation can fall back to a Kronecker kernel.

Equations

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

theorem Hex.ZPoly.mulNttCrt?_eq (left right result : ZPoly) (hresult : left.mulNttCrt? right = some result) : result = left * right

Every successful auxiliary-prime NTT multiplication is the existing schoolbook integer polynomial product.

inductive Hex.ZPoly.MulKernel : Type

Integer multiplication kernels represented in the crossover table. The constructor is observable for benchmark and fixture reporting.

• schoolbook : MulKernel
• ks1 : MulKernel
• ks2 : MulKernel
• ks3 : MulKernel
• ks4 : MulKernel
• crtNtt : MulKernel

def Hex.ZPoly.instBEqMulKernel.beq : MulKernel → MulKernel → Bool

Equations

• Hex.ZPoly.instBEqMulKernel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Hex.ZPoly.instBEqMulKernel : BEq MulKernel

Equations

• Hex.ZPoly.instBEqMulKernel = { beq := Hex.ZPoly.instBEqMulKernel.beq }

def Hex.ZPoly.instReprMulKernel.repr : MulKernel → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZPoly.instReprMulKernel.repr Hex.ZPoly.MulKernel.ks1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ZPoly.MulKernel.ks1")).group prec✝
• Hex.ZPoly.instReprMulKernel.repr Hex.ZPoly.MulKernel.ks2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ZPoly.MulKernel.ks2")).group prec✝
• Hex.ZPoly.instReprMulKernel.repr Hex.ZPoly.MulKernel.ks3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ZPoly.MulKernel.ks3")).group prec✝
• Hex.ZPoly.instReprMulKernel.repr Hex.ZPoly.MulKernel.ks4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ZPoly.MulKernel.ks4")).group prec✝
• Hex.ZPoly.instReprMulKernel.repr Hex.ZPoly.MulKernel.crtNtt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.ZPoly.MulKernel.crtNtt")).group prec✝

@[instance_reducible]

instance Hex.ZPoly.instReprMulKernel : Repr MulKernel

Equations

• Hex.ZPoly.instReprMulKernel = { reprPrec := Hex.ZPoly.instReprMulKernel.repr }

def Hex.ZPoly.MulKernel.name : MulKernel → String

Stable JSON-facing name for an integer multiplication kernel.

Equations

• Hex.ZPoly.MulKernel.schoolbook.name = "schoolbook"
• Hex.ZPoly.MulKernel.ks1.name = "ks1"
• Hex.ZPoly.MulKernel.ks2.name = "ks2"
• Hex.ZPoly.MulKernel.ks3.name = "ks3"
• Hex.ZPoly.MulKernel.ks4.name = "ks4"
• Hex.ZPoly.MulKernel.crtNtt.name = "crt_ntt"

def Hex.ZPoly.useCrtNtt (_shorter _ratio _width : Nat) : Bool

Whether the measured integer table contains a winning CRT-NTT cell. The balanced 64-bit sweep keeps KS1 roughly an order of magnitude ahead through 16384 coefficients per operand, while wider coefficients exhaust the present seven-prime catalogue. The forced CRT benchmark remains available; a future expanded sweep can replace this empty table without touching correctness.

Equations

• Hex.ZPoly.useCrtNtt _shorter _ratio _width = false

def Hex.ZPoly.selectKernel (left right : ZPoly) : MulKernel

Integer crossover policy, indexed by shorter size, operand ratio, and maximum coefficient width. The forced-kernel benchmarks can recalibrate these isolated boundaries without affecting any correctness theorem.

Equations

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

def Hex.ZPoly.mulFast (left right : ZPoly) : ZPoly

Total integer multiplication. A selected CRT-NTT capacity miss falls back to KS4; every other table cell names a total forced kernel directly.

Equations

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

theorem Hex.ZPoly.mulFast_eq (left right : ZPoly) : left.mulFast right = left * right

The integer dispatcher agrees with schoolbook multiplication independently of every crossover-table entry and of catalogue availability.

def Hex.ZPoly.fastPlan : DensePoly.MulPlan Int

Coefficient-owner multiplication plan for generic fast algorithms.

Equations

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