def Hex.ZPoly.bitLen (n : Nat) : Nat

The number of bits in n: the least k with n < 2 ^ k.

Equations

• Hex.ZPoly.bitLen n = if n = 0 then 0 else n.log2 + 1

theorem Hex.ZPoly.lt_two_pow_bitLen (n : Nat) : n < 2 ^ bitLen n

n fits in bitLen bits.

def Hex.ZPoly.ceilLog2 (n : Nat) : Nat

The least k with n ≤ 2 ^ k.

Equations

• Hex.ZPoly.ceilLog2 n = Hex.ZPoly.bitLen (n - 1)

theorem Hex.ZPoly.le_two_pow_ceilLog2 (n : Nat) : n ≤ 2 ^ ceilLog2 n

n is at most 2 ^ ceilLog2 n.

def Hex.ZPoly.maxAbs (p : ZPoly) : Nat

The largest absolute value of a stored coefficient.

Equations

• p.maxAbs = Array.foldl (fun (m : Nat) (c : Int) => max m c.natAbs) 0 (Hex.DensePoly.toArray p)

theorem Hex.ZPoly.natAbs_coeff_le_maxAbs (p : ZPoly) (i : Nat) : (DensePoly.coeff p i).natAbs ≤ p.maxAbs

Every coefficient is bounded in absolute value by maxAbs.

theorem Hex.ZPoly.natAbs_coeff_mul_le (p q : ZPoly) (A : Nat) (hp : ∀ (i : Nat), (DensePoly.coeff p i).natAbs ≤ A) (hq : ∀ (j : Nat), (DensePoly.coeff q j).natAbs ≤ A) (n : Nat) : (DensePoly.coeff (p * q) n).natAbs ≤ DensePoly.size p * (A * A)

A product coefficient is bounded by the number of diagonal terms times the square of the coefficient bound. This is the no-overlap budget: it is what the slot width has to accommodate.

theorem Hex.ZPoly.natAbs_coeff_mul_le_min (p q : ZPoly) (A : Nat) (hp : ∀ (i : Nat), (DensePoly.coeff p i).natAbs ≤ A) (hq : ∀ (j : Nat), (DensePoly.coeff q j).natAbs ≤ A) (n : Nat) : (DensePoly.coeff (p * q) n).natAbs ≤ min (DensePoly.size p) (DensePoly.size q) * (A * A)

The min-symmetric form of natAbs_coeff_mul_le.

theorem Hex.ZPoly.natAbs_mulCoeff_le (p q : ZPoly) (A C : Nat) (hp : ∀ (i : Nat), (DensePoly.coeff p i).natAbs ≤ A) (hq : ∀ (j : Nat), (DensePoly.coeff q j).natAbs ≤ C) (n : Nat) : (DensePoly.coeff (p * q) n).natAbs ≤ DensePoly.size p * (A * C)

A product coefficient is bounded using the two operands' separate coefficient bounds. Keeping A * C rather than first replacing both by their maximum is important for strongly asymmetric inputs.

theorem Hex.ZPoly.natAbs_mulCoeff_le_min (p q : ZPoly) (A C : Nat) (hp : ∀ (i : Nat), (DensePoly.coeff p i).natAbs ≤ A) (hq : ∀ (j : Nat), (DensePoly.coeff q j).natAbs ≤ C) (n : Nat) : (DensePoly.coeff (p * q) n).natAbs ≤ min (DensePoly.size p) (DensePoly.size q) * (A * C)

The symmetric diagonal-length form of natAbs_mulCoeff_le, while retaining separate coefficient bounds for the two operands.

def Hex.ZPoly.packSpec (b : Nat) (f : Nat → Int) : Nat → Int

∑_{i < len} f i * (2 ^ b) ^ i, as an integer.

Equations

• Hex.ZPoly.packSpec b f 0 = 0
• Hex.ZPoly.packSpec b f len.succ = f 0 + 2 ^ b * Hex.ZPoly.packSpec b (fun (i : Nat) => f (i + 1)) len

def Hex.ZPoly.natEval (b : Nat) (c : Nat → Nat) : Nat → Nat

∑_{i < len} c i * (2 ^ b) ^ i, as a natural number.

Equations

• Hex.ZPoly.natEval b c 0 = 0
• Hex.ZPoly.natEval b c len.succ = c 0 + 2 ^ b * Hex.ZPoly.natEval b (fun (i : Nat) => c (i + 1)) len

theorem Hex.ZPoly.packSpec_add (b : Nat) (f : Nat → Int) (m k : Nat) : packSpec b f (m + k) = packSpec b f m + 2 ^ (b * m) * packSpec b (fun (i : Nat) => f (m + i)) k

Splitting a packed range at m.

theorem Hex.ZPoly.natEval_add (b : Nat) (c : Nat → Nat) (m k : Nat) : natEval b c (m + k) = natEval b c m + 2 ^ (b * m) * natEval b (fun (i : Nat) => c (m + i)) k

Splitting a Nat-valued packed range at m.

theorem Hex.ZPoly.natEval_lt (b : Nat) (c : Nat → Nat) (len : Nat) : (∀ (i : Nat), c i < 2 ^ b) → natEval b c len < 2 ^ (b * len)

A packed range of len digits below 2 ^ b stays below 2 ^ (b * len).

theorem Hex.ZPoly.packSpec_natCast (b : Nat) (c : Nat → Nat) (len : Nat) : packSpec b (fun (i : Nat) => ↑(c i)) len = ↑(natEval b c len)

The Nat and Int packed evaluations agree on nonnegative digits.

theorem Hex.ZPoly.packSpec_add_fun (b : Nat) (f g : Nat → Int) (len : Nat) : packSpec b (fun (i : Nat) => f i + g i) len = packSpec b f len + packSpec b g len

Adding a constant to every slot adds the constant's packed range.

theorem Hex.ZPoly.packSpec_eq_eval (b : Nat) (p : ZPoly) (len : Nat) (hlen : DensePoly.size p ≤ len) : packSpec b (DensePoly.coeff p) len = DensePoly.eval p (2 ^ b)

Packing a polynomial's coefficients is Horner evaluation at 2 ^ b.

@[irreducible]

def Hex.ZPoly.packAux (b : Nat) (f : Nat → Int) (lo len : Nat) : Int

Balanced packing of len slots of width b starting at index lo. Halving keeps the running integers balanced, so the shifts cost O(n log n) limb operations instead of the O(n²) a sequential Horner scan would pay.

Equations

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

theorem Hex.ZPoly.packAux_eq (b len : Nat) (f : Nat → Int) (lo : Nat) : packAux b f lo len = packSpec b (fun (i : Nat) => f (lo + i)) len

The divide-and-conquer packing computes the packed range.

@[irreducible]

def Hex.ZPoly.constPack (b : Nat) (c : Int) (len : Nat) : Int

Packing a constant slot value. The recursion doubles rather than walking the slots, so the bias repunit costs O(log n) big-integer operations instead of the O(n) a general packAux would pay for it — which measured as the single largest cost in the Kronecker path before it was split out.

Equations

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

theorem Hex.ZPoly.constPack_eq (b : Nat) (c : Int) (len : Nat) : constPack b c len = packSpec b (fun (x : Nat) => c) len

The doubling recursion computes the constant packed range.

@[irreducible]

def Hex.ZPoly.unpackAux (b n len : Nat) : Array Nat

Balanced base-2 ^ b digit extraction of n into len slots.

Equations

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

theorem Hex.ZPoly.unpackAux_natEval (len b : Nat) (c : Nat → Nat) : (∀ (i : Nat), c i < 2 ^ b) → unpackAux b (natEval b c len) len = (List.map c (List.range len)).toArray

Digit extraction inverts packing, given digits that fit their slots.

theorem Hex.ZPoly.kronecker_identity (p q : ZPoly) (b slots : Nat) (hb : 0 < b) (hsize : DensePoly.size (p * q) ≤ slots) (hbudget : ∀ (n : Nat), (DensePoly.coeff (p * q) n).natAbs < 2 ^ (b - 1)) : DensePoly.ofCoeffs (Array.map (fun (d : Nat) => ↑d - ↑(2 ^ (b - 1))) (unpackAux b (packAux b (DensePoly.coeff p) 0 (DensePoly.size p) * packAux b (DensePoly.coeff q) 0 (DensePoly.size q) + constPack b (↑(2 ^ (b - 1))) slots).toNat slots)) = p * q

The substitution identity. Given a slot width b whose half-range strictly dominates every coefficient of the product, packing both operands at 2 ^ b, multiplying once, biasing every slot and reading the base-2 ^ b digits back off recovers the schoolbook product exactly.

hbudget is the no-overlap bound; Hex.ZPoly.mulKroneckerAt discharges it from a runtime scan of the actual coefficients rather than assuming it.

def Hex.ZPoly.kroneckerSizeCutoff : Nat

The measured size cutoff: the shorter operand must store at least this many coefficients before the substitution pays for its packing, single GMP multiplication and unpacking.

Equations

• Hex.ZPoly.kroneckerSizeCutoff = 24

def Hex.ZPoly.kroneckerBitCutoff : Nat

The measured coefficient-width cutoff, in bits. Schoolbook cost per coefficient pair steps twice as coefficients widen — about 9 ns up to 12 bits, about 53 ns at 16, about 120 ns at 20 — and packing only amortises against the widest regime at the size cutoff. Below 20 bits the schoolbook loop is what runs, at any degree.

Equations

• Hex.ZPoly.kroneckerBitCutoff = 20

def Hex.ZPoly.mulKroneckerAt (sizeCutoff bitCutoff : Nat) (p q : ZPoly) : ZPoly

Kronecker substitution with explicit cutoffs, so the kernel benchmark can sweep them. Production uses Hex.ZPoly.mulKronecker, which fixes them to the measured Hex.ZPoly.kroneckerSizeCutoff and Hex.ZPoly.kroneckerBitCutoff.

Both guards are checked before the coefficient scan is used, and the size guard is checked before the scan is run at all, so a product that stays on the schoolbook path for its size pays nothing for the test.

Equations

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

theorem Hex.ZPoly.mulKroneckerAt_eq (sizeCutoff bitCutoff : Nat) (p q : ZPoly) : mulKroneckerAt sizeCutoff bitCutoff p q = p * q

The Kronecker kernel computes the schoolbook product, at every cutoff.

def Hex.ZPoly.mulKronecker (p q : ZPoly) : ZPoly

Kronecker substitution at the measured cutoffs.

Equations

• p.mulKronecker q = Hex.ZPoly.mulKroneckerAt Hex.ZPoly.kroneckerSizeCutoff Hex.ZPoly.kroneckerBitCutoff p q

theorem Hex.ZPoly.mulKronecker_eq (p q : ZPoly) : p.mulKronecker q = p * q

The production kernel computes the schoolbook product.