Kronecker packing of dense polynomials

Sendov.qrow computes the coefficients of (g₀ + g₁t + g₂t²) ^ k as a List (List ℤ). That is correct but the kernel evaluates list recursion by interpretation, which costs Θ(k³) interpreted steps: measured, k = 24 takes two minutes and k = 32 over twenty.

Kernel Nat arithmetic, by contrast, is GMP-backed and fast — a 4000-digit multiplication and a 50th power are milliseconds. So the fix is to change the representation, not the algorithm: pack a dense polynomial into a single natural number by evaluating it at a base b = 2 ^ B larger than every coefficient. Multiplication of polynomials then becomes multiplication of naturals, and the whole recurrence collapses to base ^ k, one exponentiation. Measured on the real shapes, k = 46 drops from hours to about half a second.

This file provides the arithmetic core: evaluation Sendov.npev, the digit extraction Sendov.unpackN, and the round trip Sendov.unpackN_npev saying that packing is faithful exactly when every coefficient is below the base. The bound hypothesis is what the caller must supply, and it is the only genuinely new obligation the packing introduces.

Everything here is about ℕ; signed coefficients are handled downstream by splitting a ℤ-polynomial into its positive and negative parts.

Main statements

• Sendov.npev_cons, Sendov.npev_append: how evaluation behaves;
• Sendov.unpackN_npev: unpackN b p.length (npev p b) = p for coefficients below b.

def Sendov.npev : List ℕ → ℕ → ℕ

Evaluate a dense ℕ-polynomial (lowest degree first) at b, by Horner's rule. This is the packing map: npev p b is the single natural number representing p.

Equations

• Sendov.npev [] x✝ = 0
• Sendov.npev (a :: p) x✝ = a + x✝ * Sendov.npev p x✝

@[simp]

theorem Sendov.npev_nil (b : ℕ) : npev [] b = 0

@[simp]

theorem Sendov.npev_cons (a : ℕ) (p : List ℕ) (b : ℕ) : npev (a :: p) b = a + b * npev p b

def Sendov.unpackN (b : ℕ) : ℕ → ℕ → List ℕ

Recover the first m coefficients of a packed polynomial.

Equations

• Sendov.unpackN b 0 x✝ = []
• Sendov.unpackN b m.succ x✝ = x✝ % b :: Sendov.unpackN b m (x✝ / b)

@[simp]

theorem Sendov.unpackN_zero (b x : ℕ) : unpackN b 0 x = []

@[simp]

theorem Sendov.unpackN_succ (b m x : ℕ) : unpackN b (m + 1) x = x % b :: unpackN b m (x / b)

theorem Sendov.unpackN_npev (b : ℕ) (hb : 0 < b) (p : List ℕ) : (∀ a ∈ p, a < b) → unpackN b p.length (npev p b) = p

Packing is faithful. If every coefficient is smaller than the base, evaluation at the base loses nothing: the coefficients can be read back off by division with remainder.

This is the standard Kronecker-substitution correctness statement, and the hypothesis ∀ a ∈ p, a < b is exactly the overflow condition the caller must discharge.

theorem Sendov.npev_append (p q : List ℕ) (b : ℕ) : npev (p ++ q) b = npev p b + b ^ p.length * npev q b

Evaluation of a concatenation: the second block is shifted by b ^ (length of the first). This is what makes the two-dimensional packing work.

Packing is a ring homomorphism

def Sendov.paddN : List ℕ → List ℕ → List ℕ

Addition of dense ℕ-polynomials.

Equations

• Sendov.paddN [] x✝ = x✝
• Sendov.paddN (a :: p) [] = a :: p
• Sendov.paddN (a :: p) (c :: q) = (a + c) :: Sendov.paddN p q

def Sendov.pmulN : List ℕ → List ℕ → List ℕ

Multiplication of dense ℕ-polynomials.

Equations

• Sendov.pmulN [] x✝ = []
• Sendov.pmulN (a :: p) x✝ = Sendov.paddN (List.map (fun (c : ℕ) => a * c) x✝) (0 :: Sendov.pmulN p x✝)

def Sendov.ppowN (p : List ℕ) : ℕ → List ℕ

The k-th power of a dense ℕ-polynomial.

Equations

• Sendov.ppowN p 0 = [1]
• Sendov.ppowN p k.succ = Sendov.pmulN p (Sendov.ppowN p k)

theorem Sendov.npev_paddN (p q : List ℕ) (b : ℕ) : npev (paddN p q) b = npev p b + npev q b

theorem Sendov.npev_map_mul (a : ℕ) (q : List ℕ) (b : ℕ) : npev (List.map (fun (c : ℕ) => a * c) q) b = a * npev q b

theorem Sendov.npev_pmulN (p q : List ℕ) (b : ℕ) : npev (pmulN p q) b = npev p b * npev q b

theorem Sendov.npev_ppowN (p : List ℕ) (b k : ℕ) : npev (ppowN p k) b = npev p b ^ k

The overflow bound

theorem Sendov.mem_le_npev_one (q : List ℕ) (a : ℕ) : a ∈ q → a ≤ npev q 1

Every coefficient is at most the sum of the coefficients, which is the value at 1.

theorem Sendov.unpackN_pow (b : ℕ) (hb : 0 < b) (p : List ℕ) (k : ℕ) (hbound : npev p 1 ^ k < b) : unpackN b (ppowN p k).length (npev p b ^ k) = ppowN p k

Kronecker substitution. The coefficients of p ^ k are recovered from the single natural number (npev p b) ^ k, provided the base b exceeds every coefficient of p ^ k — for which (npev p 1) ^ k < b suffices, npev p 1 being the sum of the coefficients.

This is the statement that lets the kernel replace Θ(k³) interpreted list steps by one GMP-backed exponentiation.

Signed coefficients

The recurrence's middle coefficient g₁ = -2Dc is negative, so the polynomials that have to be packed have coefficients in ℤ. Packing is still evaluation at the base — the same homomorphism — but reading the coefficients back needs balanced digits: the representative of x % b taken in (-b/2, b/2) rather than [0, b). The overflow condition becomes 2 * |c| < b.

def Sendov.pevZ : List ℤ → ℤ → ℤ

Evaluate a dense ℤ-polynomial at an integer. This is the signed packing map.

Equations

• Sendov.pevZ [] x✝ = 0
• Sendov.pevZ (a :: p) x✝ = a + x✝ * Sendov.pevZ p x✝

@[simp]

theorem Sendov.pevZ_nil (b : ℤ) : pevZ [] b = 0

@[simp]

theorem Sendov.pevZ_cons (a : ℤ) (p : List ℤ) (b : ℤ) : pevZ (a :: p) b = a + b * pevZ p b

def Sendov.bdig (b x : ℤ) : ℤ

The balanced representative of x modulo b, lying in (-b/2, b/2) when b is positive and x is a balanced digit.

Equations

• Sendov.bdig b x = if 2 * (x % b) < b then x % b else x % b - b

def Sendov.unpackZ (b : ℤ) : ℕ → ℤ → List ℤ

Recover the first m balanced digits of a packed ℤ-polynomial.

Equations

• Sendov.unpackZ b 0 x✝ = []
• Sendov.unpackZ b m.succ x✝ = Sendov.bdig b x✝ :: Sendov.unpackZ b m ((x✝ - Sendov.bdig b x✝) / b)

@[simp]

theorem Sendov.unpackZ_zero (b x : ℤ) : unpackZ b 0 x = []

@[simp]

theorem Sendov.unpackZ_succ (b : ℤ) (m : ℕ) (x : ℤ) : unpackZ b (m + 1) x = bdig b x :: unpackZ b m ((x - bdig b x) / b)

theorem Sendov.bdig_add_mul (b c N : ℤ) (hb : 0 < b) (hc : 2 * |c| < b) : bdig b (c + b * N) = c

The balanced digit of c + b * N is c, provided 2 * |c| < b.

theorem Sendov.unpackZ_pevZ (b : ℤ) (hb : 0 < b) (p : List ℤ) : (∀ a ∈ p, 2 * |a| < b) → unpackZ b p.length (pevZ p b) = p

Signed packing is faithful. If 2 * |c| < b for every coefficient c, the coefficients are recovered from the single integer pevZ p b by balanced-digit extraction.