def Hex.ZPoly.signedUnpack (b : Nat) (packed : Int) (slots : Nat) : Array Int

Recover slots signed base-2 ^ b digits from a packed integer.

Every digit is biased by 2 ^ (b - 1) before extraction. If each true digit lies strictly inside the signed half-range, the bias makes every extracted digit nonnegative without allowing a carry into the next slot.

Equations

• Hex.ZPoly.signedUnpack b packed slots = Array.map (fun (d : Nat) => ↑d - ↑(2 ^ (b - 1))) (Hex.ZPoly.unpackAux b (packed + Hex.ZPoly.constPack b (↑(2 ^ (b - 1))) slots).toNat slots)

theorem Hex.ZPoly.signedUnpack_packSpec (b slots : Nat) (f : Nat → Int) (hb : 0 < b) (hbudget : ∀ (i : Nat), (f i).natAbs < 2 ^ (b - 1)) : signedUnpack b (packSpec b f slots) slots = (List.map f (List.range slots)).toArray

Signed recovery inverts a packed range when every digit fits strictly in the signed half-range.

def Hex.ZPoly.evalRange (x : Int) (f : Nat → Int) : Nat → Int

Horner evaluation of the first len values of f at an arbitrary integer point. packSpec is the specialization to 2 ^ b.

Equations

• Hex.ZPoly.evalRange x f 0 = 0
• Hex.ZPoly.evalRange x f len.succ = f 0 + x * Hex.ZPoly.evalRange x (fun (i : Nat) => f (i + 1)) len

theorem Hex.ZPoly.evalRange_twoPow (b : Nat) (f : Nat → Int) (len : Nat) : evalRange (2 ^ b) f len = packSpec b f len

packSpec is range evaluation at the positive power of two.

theorem Hex.ZPoly.evalRange_coeff_eq_eval (x : Int) (p : ZPoly) (len : Nat) (hlen : DensePoly.size p ≤ len) : evalRange x (DensePoly.coeff p) len = DensePoly.eval p x

Range evaluation agrees with polynomial evaluation once the requested range covers all stored coefficients.

def Hex.ZPoly.alternate (f : Nat → Int) (i : Nat) : Int

Alternate coefficient signs, so positive-base packing represents evaluation at the corresponding negative base.

Equations

• Hex.ZPoly.alternate f i = if i % 2 = 0 then f i else -f i

theorem Hex.ZPoly.evalRange_alternate (x : Int) (f : Nat → Int) (len : Nat) : evalRange x (alternate f) len = evalRange (-x) f len

Packing alternating coefficients at B is evaluation of the original coefficient stream at -B.

theorem Hex.ZPoly.evalRange_split (x : Int) (f : Nat → Int) (pairs : Nat) : evalRange x f (2 * pairs) = evalRange (x * x) (fun (i : Nat) => f (2 * i)) pairs + x * evalRange (x * x) (fun (i : Nat) => f (2 * i + 1)) pairs

An even-length evaluation splits into its even and odd coefficient streams, each evaluated at the squared point.

theorem Hex.ZPoly.evalRange_add_neg (x : Int) (f : Nat → Int) (pairs : Nat) : evalRange x f (2 * pairs) + evalRange (-x) f (2 * pairs) = 2 * evalRange (x * x) (fun (i : Nat) => f (2 * i)) pairs

Adding evaluations at opposite points isolates the even coefficient stream.

theorem Hex.ZPoly.evalRange_sub_neg (x : Int) (f : Nat → Int) (pairs : Nat) : evalRange x f (2 * pairs) - evalRange (-x) f (2 * pairs) = 2 * x * evalRange (x * x) (fun (i : Nat) => f (2 * i + 1)) pairs

Subtracting evaluations at opposite points isolates the odd coefficient stream, with one factor of the evaluation point.

theorem Hex.ZPoly.packAlternate_eq_eval (b : Nat) (p : ZPoly) : packAux b (alternate (DensePoly.coeff p)) 0 (DensePoly.size p) = DensePoly.eval p (-2 ^ b)

Alternating-sign balanced packing evaluates a polynomial at -2 ^ b.

theorem Hex.ZPoly.pack_eq_eval (b : Nat) (p : ZPoly) : packAux b (DensePoly.coeff p) 0 (DensePoly.size p) = DensePoly.eval p (2 ^ b)

Balanced positive packing evaluates a polynomial at 2 ^ b.

def Hex.ZPoly.mergeParity (even odd : Array Int) (slots : Nat) : Array Int

Interleave equal-length even and odd coefficient channels, retaining only the requested number of output slots.

Equations

• Hex.ZPoly.mergeParity even odd slots = Array.ofFn fun (i : Fin slots) => if ↑i % 2 = 0 then even.getD (↑i / 2) 0 else odd.getD (↑i / 2) 0

def Hex.ZPoly.KS2.recover (b pairs slots : Nat) (p q : ZPoly) : ZPoly

The two-point reconstruction at an explicit half-width and output shape. The only large products are the evaluations at 2 ^ b and -2 ^ b.

Equations

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

theorem Hex.ZPoly.KS2.recover_eq (p q : ZPoly) (b pairs slots : Nat) (hb : 0 < b) (hsize : DensePoly.size (p * q) ≤ slots) (hslots : slots ≤ 2 * pairs) (hbudget : ∀ (i : Nat), (DensePoly.coeff (p * q) i).natAbs < 2 ^ (2 * b - 1)) : recover b pairs slots p q = p * q

Two evaluations at opposite points recover the schoolbook product when the doubled slots contain every signed coefficient.

def Hex.ZPoly.coeffBudget (p q : ZPoly) : Nat

The exact maximum product-coefficient budget used by the multipoint kernels: diagonal length times the two separate coefficient maxima.

Equations

• p.coeffBudget q = min (Hex.DensePoly.size p) (Hex.DensePoly.size q) * (p.maxAbs * q.maxAbs)

def Hex.ZPoly.ks2Width (p q : ZPoly) : Nat

Half-width used by KS2. Two adjacent result coefficients share a 2 * ks2Width-bit packed slot after the opposite-point evaluations are combined.

Equations

• p.ks2Width q = (Hex.ZPoly.bitLen (p.coeffBudget q) + 2) / 2

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

Forced two-point Kronecker substitution. Every nonzero input uses exactly the two packed integer products at B and -B; there is no size or width fallback in this entry point.

Equations

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

theorem Hex.ZPoly.mulKS2_eq (p q : ZPoly) : p.mulKS2 q = p * q

Forced KS2 agrees with the schoolbook polynomial product.

def Hex.ZPoly.KS3.reversePack (b : Nat) (p : ZPoly) : Int

Pack an operand in descending coefficient order. Multiplying two such values is the reciprocal product used by KS3.

Equations

• Hex.ZPoly.KS3.reversePack b p = Hex.ZPoly.packAux b (fun (i : Nat) => Hex.DensePoly.coeff p (Hex.DensePoly.size p - 1 - i)) 0 (Hex.DensePoly.size p)

theorem Hex.ZPoly.KS3.reversePack_eq_eval (b : Nat) (p : ZPoly) : reversePack b p = (DensePoly.polyOfSeries (DensePoly.reverseSeries p (DensePoly.size p))).eval (2 ^ b)

Descending packing is evaluation of the normalized reversed polynomial.

theorem Hex.ZPoly.KS3.reversePoly_extend (p : ZPoly) (slots : Nat) (hsize : DensePoly.size p ≤ slots) : DensePoly.polyOfSeries (DensePoly.reverseSeries p (DensePoly.size p)) = DensePoly.polyOfSeries (DensePoly.reverseSeries p slots)

Extending the precision of a reversed polynomial merely appends zero coefficients, which normalization removes.

def Hex.ZPoly.KS3.headDigit (b remaining forward reverse : Nat) : Nat

Recover one coefficient from the low end of a forward packed residual and the high end of its reciprocal packed residual.

Equations

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

def Hex.ZPoly.KS3.digits (b : Nat) : Nat → Nat → Nat → List Nat

Sequential reciprocal recovery. Each step removes the coefficient just recovered from both packed residuals; the forward residual is then shifted by one base digit.

Equations

• One or more equations did not get rendered due to their size.
• Hex.ZPoly.KS3.digits b 0 x✝¹ x✝ = []

def Hex.ZPoly.KS3.unpack (b forward reverse slots : Nat) : Array Nat

Array-valued wrapper around digits.

Equations

• Hex.ZPoly.KS3.unpack b forward reverse slots = (Hex.ZPoly.KS3.digits b slots forward reverse).toArray

def Hex.ZPoly.KS3.bias (b : Nat) : Nat

Per-slot translation used by signed reciprocal recovery. It is exactly half of B * (B - 1) for B = 2 ^ b.

Equations

• Hex.ZPoly.KS3.bias b = 2 ^ (b - 1) * (2 ^ b - 1)

def Hex.ZPoly.KS3.recover (b slots : Nat) (p q : ZPoly) : ZPoly

Reciprocal recovery at an explicit half-width and output shape. The only large products are the forward and reversed operand packings.

Equations

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

theorem Hex.ZPoly.KS3.digits_natEval (b slots : Nat) (f : Nat → Nat) : (∀ (i : Nat), f i < 2 ^ b * (2 ^ b - 1)) → digits b slots (natEval b f slots) (natEval b (fun (i : Nat) => f (slots - 1 - i)) slots) = List.map f (List.range slots)

Reciprocal recovery inverts a forward packing and its reversed packing when every coefficient fits in two base digits with one spare high value for carry disambiguation.

theorem Hex.ZPoly.KS3.coeff_reverseProduct (p q : ZPoly) (slots t : Nat) (hp : 0 < DensePoly.size p) (hq : 0 < DensePoly.size q) (hslots : slots = DensePoly.size p + DensePoly.size q - 1) (ht : t < slots) : (DensePoly.polyOfSeries (DensePoly.reverseSeries p slots) * DensePoly.polyOfSeries (DensePoly.reverseSeries q slots)).coeff t = DensePoly.coeff (p * q) (slots - 1 - t)

The product of two reversed operands lists the schoolbook product coefficients in descending order.

theorem Hex.ZPoly.KS3.reversePack_mul_eq_packSpec (b slots : Nat) (p q : ZPoly) (hp : 0 < DensePoly.size p) (hq : 0 < DensePoly.size q) (hslots : slots = DensePoly.size p + DensePoly.size q - 1) : reversePack b p * reversePack b q = packSpec b (fun (i : Nat) => DensePoly.coeff (p * q) (slots - 1 - i)) slots

Multiplying descending operand packings yields the descending coefficient packing of their schoolbook product.

theorem Hex.ZPoly.KS3.unpack_packSpec (b slots : Nat) (f : Nat → Int) (hb : 0 < b) (hbudget : ∀ (i : Nat), (f i).natAbs < bias b) : Array.map (fun (x : Nat) => ↑x - ↑(bias b)) (unpack b (packSpec b f slots + constPack b (↑(bias b)) slots).toNat (packSpec b (fun (i : Nat) => f (slots - 1 - i)) slots + constPack b (↑(bias b)) slots).toNat slots) = (List.map f (List.range slots)).toArray

Biasing a signed forward stream and its reversal, then applying reciprocal recovery, returns the original coefficient array.

theorem Hex.ZPoly.KS3.recover_eq (p q : ZPoly) (b slots : Nat) (hb : 0 < b) (hp : 0 < DensePoly.size p) (hq : 0 < DensePoly.size q) (hslots : slots = DensePoly.size p + DensePoly.size q - 1) (hbudget : ∀ (i : Nat), (DensePoly.coeff (p * q) i).natAbs < bias b) : recover b slots p q = p * q

Forward and reciprocal packing recover the schoolbook product whenever every signed coefficient fits strictly inside the reciprocal bias range.

def Hex.ZPoly.ks3Width (p q : ZPoly) : Nat

Half-width used by reciprocal Kronecker substitution. Each recovered coefficient may occupy two adjacent base digits.

Equations

• p.ks3Width q = (Hex.ZPoly.bitLen (p.coeffBudget q) + 3) / 2

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

Forced reciprocal Kronecker substitution. Every nonzero input uses exactly the forward and reversed packed integer products; there is no size or width fallback in this entry point.

Equations

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

theorem Hex.ZPoly.mulKS3_eq (p q : ZPoly) : p.mulKS3 q = p * q

Forced KS3 agrees with the schoolbook polynomial product.

def Hex.ZPoly.KS4.reverseAlternatePack (b : Nat) (p : ZPoly) : Int

Descending coefficient packing at the negative evaluation point.

Equations

• Hex.ZPoly.KS4.reverseAlternatePack b p = Hex.ZPoly.packAux b (Hex.ZPoly.alternate fun (i : Nat) => Hex.DensePoly.coeff p (Hex.DensePoly.size p - 1 - i)) 0 (Hex.DensePoly.size p)

def Hex.ZPoly.KS4.recover (b slots : Nat) (p q : ZPoly) : ZPoly

Four-point reconstruction at an explicit quarter-width. The four large products evaluate the operands at B, -B, and the corresponding two reciprocal points represented by descending coefficient packings.

Equations

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

theorem Hex.ZPoly.KS4.recover_eq (p q : ZPoly) (b slots : Nat) (hb : 0 < b) (hp : 0 < DensePoly.size p) (hq : 0 < DensePoly.size q) (hslots : slots = DensePoly.size p + DensePoly.size q - 1) (hbudget : ∀ (i : Nat), (DensePoly.coeff (p * q) i).natAbs < KS3.bias (2 * b)) : recover b slots p q = p * q

Four-point reconstruction recovers the schoolbook product whenever every coefficient fits the reciprocal range of either parity channel.

def Hex.ZPoly.ks4Width (p q : ZPoly) : Nat

Quarter-width used by the four-point kernel. Opposite-point splitting first doubles the base exponent, after which reciprocal recovery uses two adjacent channel digits.

Equations

• p.ks4Width q = (Hex.ZPoly.bitLen (p.coeffBudget q) + 5) / 4

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

Forced four-point Kronecker substitution. Every nonzero input uses the four packed integer products at the positive, negative, and two reciprocal evaluation points; there is no fallback in this entry point.

Equations

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

theorem Hex.ZPoly.mulKS4_eq (p q : ZPoly) : p.mulKS4 q = p * q

Forced KS4 agrees with the schoolbook polynomial product.