35.2. HexPolyFast: fast dense polynomials🔗

35.2.1. Introduction🔗

HexPolyFast adds proof-carrying fast algorithms to the normalized dense polynomials from HexPoly. The underlying multiplication and Euclidean operations remain the semantic reference. Optimized kernels are selected explicitly, and their laws state exact equality with that reference rather than equality only up to normalization or a unit.

The library covers full and clipped Karatsuba multiplication, Newton reciprocals and division, half-gcd, product and remainder trees, reusable multipoint evaluation and interpolation, and Padé approximation. It is Mathlib-free. Its other direct dependency is HexTruncatedSeries, whose fixed-precision series representation supplies the Newton-inversion boundary.

35.2.2. Multiplication plans🔗

Hex.DensePoly.MulPlan packages full multiplication, specialized squaring, and an arbitrary product slice. Its three proof fields identify all results with the existing DensePoly product. A plan is an ordinary value, not a typeclass instance, so callers can choose a coefficient-specific kernel locally without changing global arithmetic.

def

Hex.DensePoly.schoolbookPlan.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] : Hex.DensePoly.MulPlan R
Hex.DensePoly.schoolbookPlan.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] :
  Hex.DensePoly.MulPlan R

The reference plan backed by the existing allocation-conscious schoolbook multiplication.

def

Hex.DensePoly.karatsubaPlan.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (cutoff : Nat) : Hex.DensePoly.MulPlan R
Hex.DensePoly.karatsubaPlan.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (cutoff : Nat) :
  Hex.DensePoly.MulPlan R

A lawful Karatsuba plan.

def

Hex.DensePoly.mulWith.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R)
  (a b : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.mulWith.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (a b : Hex.DensePoly R) :
  Hex.DensePoly R

Multiply using an explicit plan.

def

Hex.DensePoly.squareWith.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R)
  (a : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.squareWith.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (a : Hex.DensePoly R) : Hex.DensePoly R

Square using an explicit plan.

def

Hex.DensePoly.mulLow.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) (len : Nat)
  (a b : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.mulLow.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (len : Nat) (a b : Hex.DensePoly R) :
  Hex.DensePoly R

Keep the first len coefficients of a planned product.

def

Hex.DensePoly.mulSlice.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R)
  (lo len : Nat) (a b : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.mulSlice.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (lo len : Nat) (a b : Hex.DensePoly R) :
  Hex.DensePoly R

Keep len coefficients beginning at product degree lo.

def

Hex.DensePoly.mulMiddleChecked.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R)
  (a b : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.mulMiddleChecked.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (a b : Hex.DensePoly R) :
  Hex.DensePoly R

Checked middle product. Operands are ordered by size; an empty operand has zero middle product.

The following example selects a small Karatsuba cutoff and checks full and clipped multiplication against the schoolbook semantics.

open Hex Hex.DensePoly

namespace HexPolyFastChapterMul

private def a : DensePoly Int :=
  #p[3, -2, 0, 5, 1]

private def b : DensePoly Int :=
  #p[-1, 6, 2]

private def plan : MulPlan Int :=
  karatsubaPlan 2

#guard mulWith plan a b = a * b
#guard squareWith plan a = a * a
#guard
  mulSlice plan 2 3 a b =
    schoolbookSlice 2 3 a b
#guard mulSlice plan 30 4 a b = 0

end HexPolyFastChapterMul

The projection theorems are the public semantic boundary. Dispatch cutoffs, recursive splits, and clipped allocation do not appear in their statements.

theorem

Hex.DensePoly.mulWith_eq.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R)
  (a b : Hex.DensePoly R) : Hex.DensePoly.mulWith plan a b = a * b
Hex.DensePoly.mulWith_eq.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (a b : Hex.DensePoly R) :
  Hex.DensePoly.mulWith plan a b = a * b

Planned multiplication has the existing dense-polynomial semantics.

theorem

Hex.DensePoly.squareWith_eq.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R)
  (a : Hex.DensePoly R) : Hex.DensePoly.squareWith plan a = a * a
Hex.DensePoly.squareWith_eq.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (a : Hex.DensePoly R) :
  Hex.DensePoly.squareWith plan a = a * a

Planned squaring has the existing dense-polynomial semantics.

theorem

Hex.DensePoly.coeff_mulLow.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) (len i : Nat)
  (a b : Hex.DensePoly R) :
  (Hex.DensePoly.mulLow plan len a b).coeff i =
    if i < len then (a * b).coeff i else 0
Hex.DensePoly.coeff_mulLow.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (len i : Nat) (a b : Hex.DensePoly R) :
  (Hex.DensePoly.mulLow plan len a
          b).coeff
      i =
    if i < len then (a * b).coeff i else 0

Coefficient law for a planned low product.

theorem

Hex.DensePoly.coeff_mulSlice.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R)
  (lo len i : Nat) (a b : Hex.DensePoly R) :
  (Hex.DensePoly.mulSlice plan lo len a b).coeff i =
    if i < len then (a * b).coeff (lo + i) else 0
Hex.DensePoly.coeff_mulSlice.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (lo len i : Nat)
  (a b : Hex.DensePoly R) :
  (Hex.DensePoly.mulSlice plan lo len a
          b).coeff
      i =
    if i < len then (a * b).coeff (lo + i)
    else 0

Coefficient law for an arbitrary planned slice.

35.2.3. Cyclic products and series bridges🔗

Cyclic and negacyclic products fold a planned ordinary product modulo x^n - 1 and x^n + 1. The proof-taking forms require positive length; the checked forms return none for length zero.

def

Hex.DensePoly.mulCyclic.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) (n : Nat)
  (_hn : 0 < n) (a b : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.mulCyclic.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (n : Nat) (_hn : 0 < n)
  (a b : Hex.DensePoly R) :
  Hex.DensePoly R

Cyclic convolution of positive length n.

def

Hex.DensePoly.mulNegacyclic.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) (n : Nat)
  (_hn : 0 < n) (a b : Hex.DensePoly R) : Hex.DensePoly R
Hex.DensePoly.mulNegacyclic.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (n : Nat) (_hn : 0 < n)
  (a b : Hex.DensePoly R) :
  Hex.DensePoly R

Negacyclic convolution of positive length n.

theorem

Hex.DensePoly.mulCyclic_eq_modByMonic.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) (n : Nat)
  (hn : 0 < n) (hone : 1 ≠ 0) (a b : Hex.DensePoly R) :
  Hex.DensePoly.mulCyclic plan n hn a b =
    (a * b).modByMonic (Hex.DensePoly.cyclicModulus n) ⋯
Hex.DensePoly.mulCyclic_eq_modByMonic.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0)
  (a b : Hex.DensePoly R) :
  Hex.DensePoly.mulCyclic plan n hn a b =
    (a * b).modByMonic
      (Hex.DensePoly.cyclicModulus n) ⋯

Planned cyclic multiplication is polynomial remainder modulo x^n - 1.

theorem

Hex.DensePoly.mulNegacyclic_eq_modByMonic.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R) (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0)
  (a b : Hex.DensePoly R) :
  Hex.DensePoly.mulNegacyclic plan n hn a b =
    (a * b).modByMonic (Hex.DensePoly.negacyclicModulus n) ⋯
Hex.DensePoly.mulNegacyclic_eq_modByMonic.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0)
  (a b : Hex.DensePoly R) :
  Hex.DensePoly.mulNegacyclic plan n hn a
      b =
    (a * b).modByMonic
      (Hex.DensePoly.negacyclicModulus n)
      ⋯

Planned negacyclic multiplication is polynomial remainder modulo x^n + 1.

def

Hex.DensePoly.mulCyclic?.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) (n : Nat)
  (a b : Hex.DensePoly R) : Option (Hex.DensePoly R)
Hex.DensePoly.mulCyclic?.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (n : Nat) (a b : Hex.DensePoly R) :
  Option (Hex.DensePoly R)

Checked cyclic convolution; length zero has no quotient-ring meaning.

def

Hex.DensePoly.mulNegacyclic?.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) (n : Nat)
  (a b : Hex.DensePoly R) : Option (Hex.DensePoly R)
Hex.DensePoly.mulNegacyclic?.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (n : Nat) (a b : Hex.DensePoly R) :
  Option (Hex.DensePoly R)

Checked negacyclic convolution; length zero has no quotient-ring meaning.

Reversal converts the leading end of a polynomial to the low end of a fixed series prefix. The guarded coefficient theorem matters because natural-number subtraction saturates below zero.

def

Hex.DensePoly.reverseSeries.{u} {R : Type u} [Zero R] [DecidableEq R]
  (f : Hex.DensePoly R) (n : Nat) : Hex.TSeries R n
Hex.DensePoly.reverseSeries.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  (f : Hex.DensePoly R) (n : Nat) :
  Hex.TSeries R n

Reverse a dense polynomial from its leading end into an exactly n-term truncated series, padding with zeros when n exceeds the polynomial size.

theorem

Hex.DensePoly.coeff_reverseSeries.{u} {R : Type u} [Zero R]
  [DecidableEq R] (f : Hex.DensePoly R) (n i : Nat) (hi : i < n) :
  (f.reverseSeries n).coeff i =
    if i < f.size then f.coeff (f.size - 1 - i) else 0
Hex.DensePoly.coeff_reverseSeries.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  (f : Hex.DensePoly R) (n i : Nat)
  (hi : i < n) :
  (f.reverseSeries n).coeff i =
    if i < f.size then
      f.coeff (f.size - 1 - i)
    else 0

Coefficient law for zero-extending polynomial reversal.

def

Hex.DensePoly.polyOfSeries.{u} {R : Type u} [Zero R] [DecidableEq R]
  {n : Nat} (a : Hex.TSeries R n) : Hex.DensePoly R
Hex.DensePoly.polyOfSeries.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  {n : Nat} (a : Hex.TSeries R n) :
  Hex.DensePoly R

Convert all represented coefficients of a truncated series to a normalized dense polynomial.

def

Hex.DensePoly.seriesMulUpTo.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) {n : Nat}
  (m : Nat) (a b : Hex.TSeries R n) : Hex.TSeries R n
Hex.DensePoly.seriesMulUpTo.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  {n : Nat} (m : Nat)
  (a b : Hex.TSeries R n) :
  Hex.TSeries R n

Multiply two series through degree m - 1 with a polynomial multiplication plan.

def

Hex.DensePoly.reciprocalWith.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) {n : Nat}
  (g : Hex.TSeries R n) (u : R) : Hex.TSeries R n
Hex.DensePoly.reciprocalWith.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  {n : Nat} (g : Hex.TSeries R n)
  (u : R) : Hex.TSeries R n

Newton reciprocal at the full represented precision. Each doubling step uses plan.slice 0 k; no schoolbook TSeries product is executed by this definition.

theorem

Hex.DensePoly.reciprocalWith_eq.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R) {n : Nat}
  (g : Hex.TSeries R n) (u : R) :
  Hex.DensePoly.reciprocalWith plan g u = g.invOfUnit u
Hex.DensePoly.reciprocalWith_eq.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  {n : Nat} (g : Hex.TSeries R n)
  (u : R) :
  Hex.DensePoly.reciprocalWith plan g u =
    g.invOfUnit u

The plan-driven reciprocal has the established truncated-series semantics. The inverse-witness hypothesis is intentionally not needed for algorithmic agreement; it is needed by the defining inverse equation below.

35.2.4. Newton division🔗

Hex.DensePoly.DivPlan caches a divisor and a finite-precision reciprocal. The capacity records the largest quotient prefix the plan can serve. Monic construction works over a commutative ring; field construction uses the inverse of the leading coefficient.

def

Hex.DensePoly.DivPlan.ofMonic.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (mul : Hex.DensePoly.MulPlan R)
  (q : Hex.DensePoly R) (hq : q.Monic) (hqne : q ≠ 0) (capacity : Nat) :
  Hex.DensePoly.DivPlan R
Hex.DensePoly.DivPlan.ofMonic.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (mul : Hex.DensePoly.MulPlan R)
  (q : Hex.DensePoly R) (hq : q.Monic)
  (hqne : q ≠ 0) (capacity : Nat) :
  Hex.DensePoly.DivPlan R

Build a cached plan for a nonzero monic divisor.

def

Hex.DensePoly.DivPlan.ofNonzero.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (mul : Hex.DensePoly.MulPlan F)
  (q : Hex.DensePoly F) (hqne : q ≠ 0) (capacity : Nat) :
  Hex.DensePoly.DivPlan F
Hex.DensePoly.DivPlan.ofNonzero.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (mul : Hex.DensePoly.MulPlan F)
  (q : Hex.DensePoly F) (hqne : q ≠ 0)
  (capacity : Nat) :
  Hex.DensePoly.DivPlan F

Build a cached plan for an arbitrary nonzero divisor over a field.

def

Hex.DensePoly.DivPlan.divMod.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.DivPlan R)
  (p : Hex.DensePoly R)
  (hcap : p.quotientLength plan.divisor ≤ plan.capacity) :
  Hex.DensePoly R × Hex.DensePoly R
Hex.DensePoly.DivPlan.divMod.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.DivPlan R)
  (p : Hex.DensePoly R)
  (hcap :
    p.quotientLength plan.divisor ≤
      plan.capacity) :
  Hex.DensePoly R × Hex.DensePoly R

Divide using a cached reciprocal. The proof ensures the cached precision covers the requested quotient; it is erased from executable code.

def

Hex.DensePoly.DivPlan.mod.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.DivPlan R)
  (p : Hex.DensePoly R)
  (hcap : p.quotientLength plan.divisor ≤ plan.capacity) :
  Hex.DensePoly R
Hex.DensePoly.DivPlan.mod.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.DivPlan R)
  (p : Hex.DensePoly R)
  (hcap :
    p.quotientLength plan.divisor ≤
      plan.capacity) :
  Hex.DensePoly R

Remainder-only cached division.

The one-shot interfaces preserve all existing conventions, including division by zero and a divisor larger than the dividend.

def

Hex.DensePoly.divModMonicWith.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (mul : Hex.DensePoly.MulPlan R)
  (p q : Hex.DensePoly R) (hq : q.Monic) :
  Hex.DensePoly R × Hex.DensePoly R
Hex.DensePoly.divModMonicWith.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (mul : Hex.DensePoly.MulPlan R)
  (p q : Hex.DensePoly R) (hq : q.Monic) :
  Hex.DensePoly R × Hex.DensePoly R

One-shot reciprocal division by a monic polynomial.

def

Hex.DensePoly.divModWith.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (mul : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) : Hex.DensePoly F × Hex.DensePoly F
Hex.DensePoly.divModWith.{u} {F : Type u}
  [DecidableEq F] [Lean.Grind.Field F]
  (mul : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly F × Hex.DensePoly F

One-shot reciprocal division over a field.

theorem

Hex.DensePoly.divModWith_eq.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (mul : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly.divModWith mul p q = p.divMod q
Hex.DensePoly.divModWith_eq.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (mul : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly.divModWith mul p q =
    p.divMod q

One-shot field reciprocal division is extensionally the existing verified long-division operation.

open Hex Hex.DensePoly

namespace HexPolyFastChapterDivision

private def a : DensePoly Rat :=
  #p[3, -2, 0, 5, 1]

private def b : DensePoly Rat :=
  #p[2, -3, 1]

#guard
  divModWith (karatsubaPlan 2) a b =
    divMod a b
#guard
  divModWith (karatsubaPlan 2) a 0 =
    (0, a)
#guard
  divModWith (karatsubaPlan 2) (a * b) b =
    (a, 0)

end HexPolyFastChapterDivision

35.2.5. Half-gcd🔗

Hex.DensePoly.GcdStep is the two-by-two polynomial transformation used by half-gcd. It keeps this library independent of the matrix hierarchy. Recursive high-half calls predict and group the existing Euclidean quotient sequence; a checked fallback preserves exact executable behavior.

def

Hex.DensePoly.gcdWith.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) : Hex.DensePoly F
Hex.DensePoly.gcdWith.{u} {F : Type u}
  [DecidableEq F] [Lean.Grind.Field F]
  (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly F

Gcd projection of the half-gcd engine.

def

Hex.DensePoly.xgcdWith.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) : Hex.DensePoly.XGCDResult F
Hex.DensePoly.xgcdWith.{u} {F : Type u}
  [DecidableEq F] [Lean.Grind.Field F]
  (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly.XGCDResult F

Plan-driven half-gcd extended gcd.

def

Hex.DensePoly.xgcdLeftWith.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) : Hex.DensePoly.XGCDLeftResult F
Hex.DensePoly.xgcdLeftWith.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly.XGCDLeftResult F

One-sided result projection of the half-gcd engine. It shares the full matrix computation with xgcdWith; this API omits the unused result field but does not promise a cheaper algorithm.

theorem

Hex.DensePoly.gcdWith_eq.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) : Hex.DensePoly.gcdWith plan p q = p.gcd q
Hex.DensePoly.gcdWith_eq.{u} {F : Type u}
  [DecidableEq F] [Lean.Grind.Field F]
  (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly.gcdWith plan p q = p.gcd q

Half-gcd returns exactly the established gcd.

theorem

Hex.DensePoly.xgcdWith_eq.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) : Hex.DensePoly.xgcdWith plan p q = p.xgcd q
Hex.DensePoly.xgcdWith_eq.{u} {F : Type u}
  [DecidableEq F] [Lean.Grind.Field F]
  (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly.xgcdWith plan p q =
    p.xgcd q

Half-gcd returns exactly the established extended-gcd result, including the raw gcd scaling and both Bezout coefficients.

theorem

Hex.DensePoly.xgcdLeftWith_eq.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly.xgcdLeftWith plan p q = p.xgcdLeft q
Hex.DensePoly.xgcdLeftWith_eq.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (plan : Hex.DensePoly.MulPlan F)
  (p q : Hex.DensePoly F) :
  Hex.DensePoly.xgcdLeftWith plan p q =
    p.xgcdLeft q

The one-sided half-gcd projection agrees exactly with the established one-sided extended gcd.

35.2.6. Product trees and multipoint operations🔗

Hex.DensePoly.ProductTree caches the root of a balanced tree without retaining its intermediate levels. Its observations expose the original leaves, reconstruct levels on demand, and compute individual node products from their represented leaf blocks.

def

Hex.DensePoly.ProductTree.build.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.MulPlan R)
  (leaves : Array (Hex.DensePoly R)) : Hex.DensePoly.ProductTree R
Hex.DensePoly.ProductTree.build.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.MulPlan R)
  (leaves : Array (Hex.DensePoly R)) :
  Hex.DensePoly.ProductTree R

Build a balanced product tree without retaining intermediate levels. The empty tree has root 1 and one singleton level containing that root.

def

Hex.DensePoly.ProductTree.level?.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (tree : Hex.DensePoly.ProductTree R)
  (i : Nat) : Option (Array (Hex.DensePoly R))
Hex.DensePoly.ProductTree.level?.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (tree : Hex.DensePoly.ProductTree R)
  (i : Nat) :
  Option (Array (Hex.DensePoly R))

A balanced level reconstructed from the leaves, from leaves upward. The empty tree has the singleton level [1].

def

Hex.DensePoly.ProductTree.root.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (tree : Hex.DensePoly.ProductTree R) :
  Hex.DensePoly R
Hex.DensePoly.ProductTree.root.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (tree : Hex.DensePoly.ProductTree R) :
  Hex.DensePoly R

The product represented by the root node.

def

Hex.DensePoly.ProductTree.nodeProduct?.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (tree : Hex.DensePoly.ProductTree R)
  (level index : Nat) : Option (Hex.DensePoly R)
Hex.DensePoly.ProductTree.nodeProduct?.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (tree : Hex.DensePoly.ProductTree R)
  (level index : Nat) :
  Option (Hex.DensePoly R)

Product represented by a valid balanced node. The observation is semantic: it folds exactly that node's leaf block, independently of the internal level layout.

Hex.DensePoly.RemainderTree caches a reciprocal plan at every node for an arbitrary ordered collection of nonzero monic divisors. The caller chooses only the root capacity; proper nodes derive the exact precision they need from their sibling subtree.

structure

Hex.DensePoly.MonicLeaf.{u} (R : Type u) [DecidableEq R]
  [Lean.Grind.CommRing R] : Type u
Hex.DensePoly.MonicLeaf.{u} (R : Type u)
  [DecidableEq R]
  [Lean.Grind.CommRing R] : Type u

A nonzero monic polynomial suitable as a remainder-tree leaf.

Constructor

Hex.DensePoly.MonicLeaf.mk.{u}

Fields

poly : Hex.DensePoly R

Leaf divisor.

monic : self.poly.Monic

The divisor is monic.

ne : self.poly ≠ 0

The divisor is nonzero.

def

Hex.DensePoly.RemainderTree.build.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (mul : Hex.DensePoly.MulPlan R)
  (capacity : Nat) (leaves : Array (Hex.DensePoly.MonicLeaf R))
  (hone : 1 ≠ 0) : Hex.DensePoly.RemainderTree R
Hex.DensePoly.RemainderTree.build.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (mul : Hex.DensePoly.MulPlan R)
  (capacity : Nat)
  (leaves :
    Array (Hex.DensePoly.MonicLeaf R))
  (hone : 1 ≠ 0) :
  Hex.DensePoly.RemainderTree R

Build a cached remainder tree. capacity is the reciprocal capacity of the root; every proper node derives the exact worst-case capacity it needs from its sibling subtree. The empty leaf sequence is represented without an internal root.

def

Hex.DensePoly.RemainderTree.rootDegree.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (tree : Hex.DensePoly.RemainderTree R) : Nat
Hex.DensePoly.RemainderTree.rootDegree.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (tree : Hex.DensePoly.RemainderTree R) :
  Nat

Degree of the root product, computed as the sum of the leaf degrees.

def

Hex.DensePoly.RemainderTree.remainders?.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (tree : Hex.DensePoly.RemainderTree R)
  (p : Hex.DensePoly R) : Option (Array (Hex.DensePoly R))
Hex.DensePoly.RemainderTree.remainders?.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (tree : Hex.DensePoly.RemainderTree R)
  (p : Hex.DensePoly R) :
  Option (Array (Hex.DensePoly R))

Compute all leaf remainders with the cached reciprocal plans. Returns none exactly when the input needs more reciprocal precision than the root capacity. Proper-node capacities are sufficient by construction.

theorem

Hex.DensePoly.RemainderTree.remainders?_isSome_of_capacity.{u}
  {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R]
  (tree : Hex.DensePoly.RemainderTree R) (p : Hex.DensePoly R)
  (hcap : p.size ≤ tree.rootDegree + tree.capacity) :
  (tree.remainders? p).isSome = true
Hex.DensePoly.RemainderTree.remainders?_isSome_of_capacity.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (tree : Hex.DensePoly.RemainderTree R)
  (p : Hex.DensePoly R)
  (hcap :
    p.size ≤
      tree.rootDegree + tree.capacity) :
  (tree.remainders? p).isSome = true

A caller-supplied root capacity covering the input above the root degree makes the entire traversal succeed. Every proper-node guard follows from the sibling-degree capacities recorded by construction.

theorem

Hex.DensePoly.RemainderTree.remainders?_sound.{u} {R : Type u}
  [DecidableEq R] [Lean.Grind.CommRing R]
  (tree : Hex.DensePoly.RemainderTree R) (p : Hex.DensePoly R)
  (results : Array (Hex.DensePoly R))
  (h : tree.remainders? p = some results) :
  p.RemainderSpec tree.entries.toList results.toList
Hex.DensePoly.RemainderTree.remainders?_sound.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (tree : Hex.DensePoly.RemainderTree R)
  (p : Hex.DensePoly R)
  (results : Array (Hex.DensePoly R))
  (h :
    tree.remainders? p = some results) :
  p.RemainderSpec tree.entries.toList
    results.toList

Every successful traversal returns, in leaf order, the canonical-size remainder of the input modulo each leaf polynomial.

Hex.DensePoly.EvalPlan specializes the leaves to x - a and caches the reciprocal plans used by its remainder tree. Evaluation is total: inputs within capacity use the tree, and oversized inputs use direct pointwise evaluation.

def

Hex.DensePoly.EvalPlan.build.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (mul : Hex.DensePoly.MulPlan R)
  (points : Array R) : Hex.DensePoly.EvalPlan R
Hex.DensePoly.EvalPlan.build.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (mul : Hex.DensePoly.MulPlan R)
  (points : Array R) :
  Hex.DensePoly.EvalPlan R

Build the point-product tree and all finite-capacity reciprocal plans.

def

Hex.DensePoly.EvalPlan.treeView.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.EvalPlan R) :
  Hex.DensePoly.ProductTree R
Hex.DensePoly.EvalPlan.treeView.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.EvalPlan R) :
  Hex.DensePoly.ProductTree R

Rebuild the observational leaf-and-root product-tree view. Constructing an evaluation plan does not eagerly recompute this redundant product tree.

def

Hex.DensePoly.EvalPlan.eval.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.EvalPlan R)
  (f : Hex.DensePoly R) : Array R
Hex.DensePoly.EvalPlan.eval.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.EvalPlan R)
  (f : Hex.DensePoly R) : Array R

Specification of multipoint evaluation. The compiled implementation below replaces this direct map by the cached remainder tree.

theorem

Hex.DensePoly.EvalPlan.get_eval.{u} {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R] (plan : Hex.DensePoly.EvalPlan R)
  (f : Hex.DensePoly R) (i : Nat) (hi : i < plan.size) :
  (plan.eval f)[i] = f.eval plan.points[i]
Hex.DensePoly.EvalPlan.get_eval.{u}
  {R : Type u} [DecidableEq R]
  [Lean.Grind.CommRing R]
  (plan : Hex.DensePoly.EvalPlan R)
  (f : Hex.DensePoly R) (i : Nat)
  (hi : i < plan.size) :
  (plan.eval f)[i] = f.eval plan.points[i]

Every output entry is evaluation at the corresponding planned point.

Hex.DensePoly.InterpPlan additionally requires a field and distinct points. Plan construction rejects exactly duplicate points, while interpolation rejects exactly a mismatch between point and value counts.

def

Hex.DensePoly.InterpPlan.build?.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (mul : Hex.DensePoly.MulPlan F)
  (points : Array F) : Option (Hex.DensePoly.InterpPlan F)
Hex.DensePoly.InterpPlan.build?.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (mul : Hex.DensePoly.MulPlan F)
  (points : Array F) :
  Option (Hex.DensePoly.InterpPlan F)

Build a reusable interpolation plan exactly when the points are distinct.

def

Hex.DensePoly.InterpPlan.interpolate?.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.InterpPlan F)
  (values : Array F) : Option (Hex.DensePoly F)
Hex.DensePoly.InterpPlan.interpolate?.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (plan : Hex.DensePoly.InterpPlan F)
  (values : Array F) :
  Option (Hex.DensePoly F)

Interpolate a matching value array, rejecting only a count mismatch.

theorem

Hex.DensePoly.InterpPlan.interpolate?_sound.{u} {F : Type u}
  [DecidableEq F] [Lean.Grind.Field F]
  (plan : Hex.DensePoly.InterpPlan F) (values : Array F)
  (p : Hex.DensePoly F) (hsome : plan.interpolate? values = some p) :
  p.size ≤ plan.size ∧
    ∀ (i : Nat) (hi : i < plan.size),
      p.eval plan.points[i] = values.getD i 0
Hex.DensePoly.InterpPlan.interpolate?_sound.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (plan : Hex.DensePoly.InterpPlan F)
  (values : Array F) (p : Hex.DensePoly F)
  (hsome :
    plan.interpolate? values = some p) :
  p.size ≤ plan.size ∧
    ∀ (i : Nat) (hi : i < plan.size),
      p.eval plan.points[i] =
        values.getD i 0

A successful interpolation has the requested values and no more coefficients than there are points.

theorem

Hex.DensePoly.InterpPlan.interpolate?_unique.{u} {F : Type u}
  [DecidableEq F] [Lean.Grind.Field F]
  (plan : Hex.DensePoly.InterpPlan F) (values : Array F)
  (p q : Hex.DensePoly F) (hsome : plan.interpolate? values = some p)
  (hqsize : q.size ≤ plan.size)
  (hqvalues :
    ∀ (i : Nat) (hi : i < plan.size),
      q.eval plan.points[i] = values.getD i 0) :
  q = p
Hex.DensePoly.InterpPlan.interpolate?_unique.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (plan : Hex.DensePoly.InterpPlan F)
  (values : Array F)
  (p q : Hex.DensePoly F)
  (hsome :
    plan.interpolate? values = some p)
  (hqsize : q.size ≤ plan.size)
  (hqvalues :
    ∀ (i : Nat) (hi : i < plan.size),
      q.eval plan.points[i] =
        values.getD i 0) :
  q = p

The successful interpolation is the unique polynomial of size at most the point count with the supplied values.

open Hex Hex.DensePoly

namespace HexPolyFastChapterPoints

private def points : Array Rat :=
  #[-1, 0, 2]

private def values : Array Rat :=
  #[6, 3, 3]

private def expected : DensePoly Rat :=
  #p[3, -2, 1]

private def interpolated : Option (DensePoly Rat) :=
  (InterpPlan.build?
    (karatsubaPlan 2) points).bind
      (fun plan => plan.interpolate? values)

#guard interpolated = some expected

#guard
  (InterpPlan.build? (karatsubaPlan 2)
    (#[1, 2, 1] : Array Rat)).isNone

end HexPolyFastChapterPoints

35.2.7. Padé approximation🔗

Hex.DensePoly.PadeApproximant carries a homogeneous numerator and denominator, their degree bounds, nontriviality, and the required low-order congruence. Hex.DensePoly.NormalizedPade strengthens the denominator's constant coefficient to one.

def

Hex.DensePoly.padeHomogeneous.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.MulPlan F) {k : Nat}
  (s : Hex.TSeries F k) (m n : Nat) :
  Hex.DensePoly.PadeApproximant s m n
Hex.DensePoly.padeHomogeneous.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (plan : Hex.DensePoly.MulPlan F)
  {k : Nat} (s : Hex.TSeries F k)
  (m n : Nat) :
  Hex.DensePoly.PadeApproximant s m n

Compute a homogeneous Padé approximant with the selected multiplication plan. The half-gcd prefix stops precisely when the remainder crosses the numerator-size boundary.

def

Hex.DensePoly.pade?.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.MulPlan F) {k : Nat}
  (s : Hex.TSeries F k) (m n : Nat) :
  Option (Hex.DensePoly.NormalizedPade s m n)
Hex.DensePoly.pade?.{u} {F : Type u}
  [DecidableEq F] [Lean.Grind.Field F]
  (plan : Hex.DensePoly.MulPlan F)
  {k : Nat} (s : Hex.TSeries F k)
  (m n : Nat) :
  Option
    (Hex.DensePoly.NormalizedPade s m n)

Compute the normalized rational-series Padé form when its denominator can be made a unit at the origin.

theorem

Hex.DensePoly.pade?_eq_none_iff.{u} {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F] (plan : Hex.DensePoly.MulPlan F) {k : Nat}
  (s : Hex.TSeries F k) (m n : Nat) :
  Hex.DensePoly.pade? plan s m n = none ↔
    ¬Nonempty (Hex.DensePoly.NormalizedPade s m n)
Hex.DensePoly.pade?_eq_none_iff.{u}
  {F : Type u} [DecidableEq F]
  [Lean.Grind.Field F]
  (plan : Hex.DensePoly.MulPlan F)
  {k : Nat} (s : Hex.TSeries F k)
  (m n : Nat) :
  Hex.DensePoly.pade? plan s m n = none ↔
    ¬Nonempty
        (Hex.DensePoly.NormalizedPade s m
          n)

Normalized Padé construction fails exactly when no denominator with constant coefficient one satisfies the requested bounds and congruence.

The homogeneous result is total. The normalized operation returns none exactly when no admissible denominator is invertible at the origin.

open Hex Hex.DensePoly

namespace HexPolyFastChapterPade

private def series : TSeries Rat 3 :=
  TSeries.ofFn fun _ => 1

private def approximant :
    Option (DensePoly Rat × DensePoly Rat) :=
  (pade? (karatsubaPlan 2) series 1 1).map
    (fun approx => (approx.p, approx.q))

#guard approximant = some (C 1, #p[1, -1])

end HexPolyFastChapterPade

35.2.8. Computational boundary and cross-references🔗

All algorithms and correctness theorems in this chapter are Mathlib-free and run natively in Lean. There is no separate Mathlib companion: the operations reduce to the existing DensePoly semantics, which the HexPoly chapter and its companion already connect to Mathlib polynomials.

Coefficient-specific callers construct plans above this dependency boundary. HexPolyZ supplies Kronecker and CRT-NTT integer kernels, while HexPolyFp supplies direct and auxiliary-prime NTT multiplication. The generic algorithms here remain their independent semantic fallback.