Computing the recurrence by a single exponentiation

Sendov.rev_qrow says that qrow computes the coefficients of (g₀ + g₁t + g₂t²) ^ k. Evaluating that identity at integer points turns it into a statement about packed values, and the packing is nothing but the same Horner evaluation read in ℤ instead of ℝ. So the forward direction needs no new theory at all: Sendov.pevZ_rowZ_qrow follows from rev_qrow by casting.

Two bases are involved:

• β packs a coefficient polynomial in α into one integer (Sendov.pevZ);
• τ packs the resulting row, a polynomial in t, into one integer.

Together they are the two-dimensional Kronecker substitution, and the whole recurrence becomes G ^ k for the single integer G = pevZ g₀ β + pevZ g₁ β * τ + pevZ g₂ β * τ². Sendov.unpackZ_pevZ then reads the row back off, given the overflow bounds — which is where the numerical parameters β and τ have to be chosen, one per degree.

Main statements

• Sendov.pev_intCast, Sendov.rev_intCast: evaluation over ℝ at an integer point agrees with the packed evaluation over ℤ;
• Sendov.pevZ_rowZ_qrow: the recurrence as one integer exponentiation.

def Sendov.rowZ (r : List (List ℤ)) (β : ℤ) : List ℤ

The row with each coefficient polynomial packed at the base β.

Equations

• Sendov.rowZ r β = List.map (fun (p : List ℤ) => Sendov.pevZ p β) r

@[simp]

theorem Sendov.rowZ_nil (β : ℤ) : rowZ [] β = []

@[simp]

theorem Sendov.rowZ_cons (p : List ℤ) (r : List (List ℤ)) (β : ℤ) : rowZ (p :: r) β = pevZ p β :: rowZ r β

@[simp]

theorem Sendov.rowZ_length (r : List (List ℤ)) (β : ℤ) : (rowZ r β).length = r.length

theorem Sendov.pev_intCast (p : List ℤ) (b : ℤ) : pev p ↑b = ↑(pevZ p b)

Evaluating a coefficient polynomial over ℝ at an integer point is the packed evaluation over ℤ.

theorem Sendov.rev_intCast (r : List (List ℤ)) (β τ : ℤ) : rev r ↑β ↑τ = ↑(pevZ (rowZ r β) τ)

Evaluating a row over ℝ at integer points is the packed evaluation over ℤ.

theorem Sendov.pevZ_rowZ_qrow (g₀ g₁ g₂ : List ℤ) (k : ℕ) (β τ : ℤ) : pevZ (rowZ (qrow g₀ g₁ g₂ k) β) τ = (pevZ g₀ β + pevZ g₁ β * τ + pevZ g₂ β * τ ^ 2) ^ k

The recurrence as one exponentiation. The two-dimensionally packed row is the k-th power of a single integer. In the kernel this replaces Θ(k³) interpreted list steps by one GMP-backed exponentiation; measured at k = 46, hours become about half a second.

theorem Sendov.rowZ_qrow_eq (g₀ g₁ g₂ : List ℤ) (k : ℕ) (β τ : ℤ) (hτ : 0 < τ) (hbound : ∀ a ∈ rowZ (qrow g₀ g₁ g₂ k) β, 2 * |a| < τ) : unpackZ τ (qrow g₀ g₁ g₂ k).length ((pevZ g₀ β + pevZ g₁ β * τ + pevZ g₂ β * τ ^ 2) ^ k) = rowZ (qrow g₀ g₁ g₂ k) β

Reading the packed row back, given the overflow bound on the packed coefficients. The bound is a hypothesis: it is discharged per degree from explicit numerical parameters.

The moment as a single integer polynomial

Sendov.irow has rational weights 1/(j+4). Scaling by a common multiple L of the denominators clears them, turning the moment into one ℤ-polynomial in α.

def Sendov.wsum (L : ℤ) : ℕ → List (List ℤ) → List ℤ

∑ⱼ (L/(i+j+4)) • rⱼ: the moment numerator, scaled by L to clear denominators.

Equations

• Sendov.wsum L x✝ [] = []
• Sendov.wsum L x✝ (p :: r) = Sendov.padd (List.map (fun (c : ℤ) => L / (↑x✝ + 4) * c) p) (Sendov.wsum L (x✝ + 1) r)

@[simp]

theorem Sendov.wsum_nil (L : ℤ) (i : ℕ) : wsum L i [] = []

@[simp]

theorem Sendov.wsum_cons (L : ℤ) (i : ℕ) (p : List ℤ) (r : List (List ℤ)) : wsum L i (p :: r) = padd (List.map (fun (c : ℤ) => L / (↑i + 4) * c) p) (wsum L (i + 1) r)

theorem Sendov.pev_wsum (L : ℤ) (r : List (List ℤ)) (i : ℕ) (α : ℝ) : (∀ j < r.length, ↑i + ↑j + 4 ∣ L) → pev (wsum L i r) α = ↑L * irow r i α

The scaled moment is an integer polynomial. Given that L clears every denominator i+j+4 occurring, wsum computes L times Sendov.irow.

Coefficient bounds

Injectivity of packing needs a bound on the coefficients of both lists compared — including the true row, which is precisely the object we must not compute. So the bound has to be proved rather than checked. The L¹ norm does it: it is submultiplicative, so a coefficient of the k-th power is at most (l1 g₀ + l1 g₁ + l1 g₂) ^ k.

def Sendov.l1 : List ℤ → ℤ

Sum of absolute values of the coefficients.

Equations

• Sendov.l1 [] = 0
• Sendov.l1 (a :: p) = |a| + Sendov.l1 p

@[simp]

theorem Sendov.l1_nil : l1 [] = 0

@[simp]

theorem Sendov.l1_cons (a : ℤ) (p : List ℤ) : l1 (a :: p) = |a| + l1 p

theorem Sendov.l1_nonneg (p : List ℤ) : 0 ≤ l1 p

theorem Sendov.abs_le_l1 (p : List ℤ) (a : ℤ) : a ∈ p → |a| ≤ l1 p

theorem Sendov.l1_padd (p q : List ℤ) : l1 (padd p q) ≤ l1 p + l1 q

theorem Sendov.l1_map_mul (c : ℤ) (q : List ℤ) : l1 (List.map (fun (x : ℤ) => c * x) q) = |c| * l1 q

theorem Sendov.l1_pmul (p q : List ℤ) : l1 (pmul p q) ≤ l1 p * l1 q

def Sendov.l1row : List (List ℤ) → ℤ

The L¹ norm of a row: the total of its coefficients' absolute values.

Equations

• Sendov.l1row [] = 0
• Sendov.l1row (p :: r) = Sendov.l1 p + Sendov.l1row r

@[simp]

theorem Sendov.l1row_nil : l1row [] = 0

@[simp]

theorem Sendov.l1row_cons (p : List ℤ) (r : List (List ℤ)) : l1row (p :: r) = l1 p + l1row r

theorem Sendov.l1row_nonneg (r : List (List ℤ)) : 0 ≤ l1row r

theorem Sendov.l1row_radd (r s : List (List ℤ)) : l1row (radd r s) ≤ l1row r + l1row s

theorem Sendov.l1row_rscale (g : List ℤ) (r : List (List ℤ)) : l1row (rscale g r) ≤ l1 g * l1row r

theorem Sendov.l1row_qstep (g₀ g₁ g₂ : List ℤ) (r : List (List ℤ)) : l1row (qstep g₀ g₁ g₂ r) ≤ (l1 g₀ + l1 g₁ + l1 g₂) * l1row r

theorem Sendov.l1row_qrow (g₀ g₁ g₂ : List ℤ) (k : ℕ) : l1row (qrow g₀ g₁ g₂ k) ≤ (l1 g₀ + l1 g₁ + l1 g₂) ^ k

The coefficients of the k-th power are bounded by the k-th power of the L¹ norm. This is the bound that the packing base must exceed.

Lengths, and the magnitude of a packed value

theorem Sendov.padd_length (p q : List ℤ) : (padd p q).length = max p.length q.length

theorem Sendov.radd_length (r s : List (List ℤ)) : (radd r s).length = max r.length s.length

@[simp]

theorem Sendov.rscale_length (g : List ℤ) (r : List (List ℤ)) : (rscale g r).length = r.length

@[simp]

theorem Sendov.qrow_length (g₀ g₁ g₂ : List ℤ) (k : ℕ) : (qrow g₀ g₁ g₂ k).length = 2 * k + 1

The row of the k-th power has 2k+1 entries, whatever the multiplier.

theorem Sendov.abs_pevZ_le (b : ℤ) (hb : 1 ≤ b) (p : List ℤ) : |pevZ p b| ≤ l1 p * b ^ p.length

A packed value is bounded by the L¹ norm times a power of the base.

The verification step

The generator supplies the moment numerator; Lean checks it with one integer comparison. Lengths need not match exactly: a shorter list is compared against its zero-padding, which has the same value as a polynomial.

theorem Sendov.pev_append_zeros (p : List ℤ) (j : ℕ) (α : ℝ) : pev (p ++ List.replicate j 0) α = pev p α

Evaluation ignores trailing zeros.

theorem Sendov.unpackZ_pevZ_le (β : ℤ) (hβ : 0 < β) (m : ℕ) (p : List ℤ) : p.length ≤ m → (∀ a ∈ p, 2 * |a| < β) → unpackZ β m (pevZ p β) = p ++ List.replicate (m - p.length) 0

The round trip, tolerating extra room: unpacking to length m ≥ p.length returns p zero-padded.

def Sendov.wsumZ (L : ℤ) : ℕ → List ℤ → ℤ

The weighted sum computed directly on the α-packed row.

Equations

• Sendov.wsumZ L x✝ [] = 0
• Sendov.wsumZ L x✝ (a :: s) = L / (↑x✝ + 4) * a + Sendov.wsumZ L (x✝ + 1) s

@[simp]

theorem Sendov.wsumZ_nil (L : ℤ) (i : ℕ) : wsumZ L i [] = 0

@[simp]

theorem Sendov.wsumZ_cons (L : ℤ) (i : ℕ) (a : ℤ) (s : List ℤ) : wsumZ L i (a :: s) = L / (↑i + 4) * a + wsumZ L (i + 1) s

theorem Sendov.pevZ_padd (p q : List ℤ) (b : ℤ) : pevZ (padd p q) b = pevZ p b + pevZ q b

theorem Sendov.pevZ_map_mul (c : ℤ) (q : List ℤ) (b : ℤ) : pevZ (List.map (fun (x : ℤ) => c * x) q) b = c * pevZ q b

theorem Sendov.pevZ_wsum (L : ℤ) (r : List (List ℤ)) (i : ℕ) (β : ℤ) : pevZ (wsum L i r) β = wsumZ L i (rowZ r β)

The packed weighted sum agrees with packing the weighted sum: this is what makes the check a single integer comparison.

theorem Sendov.pevZ_inj (β : ℤ) (hβ : 0 < β) (p q : List ℤ) (hp : ∀ a ∈ p, 2 * |a| < β) (hq : ∀ a ∈ q, 2 * |a| < β) (hlen : p.length = q.length) (h : pevZ p β = pevZ q β) : p = q

Packing is injective on lists of the same length with coefficients below β/2.

theorem Sendov.wsum_eq_of_packed (g₀ g₁ g₂ : List ℤ) (k : ℕ) (L β τ : ℤ) (Nmom : List ℤ) (hβ : 0 < β) (hτ : 0 < τ) (hbτ : ∀ a ∈ rowZ (qrow g₀ g₁ g₂ k) β, 2 * |a| < τ) (hbN : ∀ a ∈ Nmom, 2 * |a| < β) (hbW : ∀ a ∈ wsum L 0 (qrow g₀ g₁ g₂ k), 2 * |a| < β) (hlen : Nmom.length = (wsum L 0 (qrow g₀ g₁ g₂ k)).length) (hcheck : wsumZ L 0 (unpackZ τ (qrow g₀ g₁ g₂ k).length ((pevZ g₀ β + pevZ g₁ β * τ + pevZ g₂ β * τ ^ 2) ^ k)) = pevZ Nmom β) : Nmom = wsum L 0 (qrow g₀ g₁ g₂ k)

Verification of a supplied moment numerator. Given the overflow bounds, checking a generator-supplied Nmom is one integer comparison against the packed computation — which is a single exponentiation and 2k+1 digit extractions.

Entry lengths

qrow_length counts the entries of a row; bounding the α-packed values also needs each entry's length. Multiplying by a g of length at most G lengthens an entry by at most G, so after k steps an entry has length at most 1 + G*k. This is what lets the hypotheses of wsum_eq_of_packed be discharged by arithmetic instead of by computing qrow.

theorem Sendov.pmul_length_le (p q : List ℤ) : (pmul p q).length ≤ p.length + q.length

theorem Sendov.mem_radd_length_le {m : ℕ} (r s : List (List ℤ)) : (∀ p ∈ r, p.length ≤ m) → (∀ q ∈ s, q.length ≤ m) → ∀ x ∈ radd r s, x.length ≤ m

theorem Sendov.mem_rscale_length_le {m : ℕ} (g : List ℤ) (r : List (List ℤ)) (hr : ∀ p ∈ r, p.length ≤ m) (x : List ℤ) : x ∈ rscale g r → x.length ≤ g.length + m

theorem Sendov.qrow_entry_length_le (g₀ g₁ g₂ : List ℤ) (G : ℕ) (h0 : g₀.length ≤ G) (h1 : g₁.length ≤ G) (h2 : g₂.length ≤ G) (k : ℕ) (p : List ℤ) : p ∈ qrow g₀ g₁ g₂ k → p.length ≤ 1 + G * k

Each entry of the k-th row has length at most 1 + G*k, where G bounds the lengths of the multipliers.

theorem Sendov.l1_le_l1row (r : List (List ℤ)) (p : List ℤ) : p ∈ r → l1 p ≤ l1row r

l1 of an entry is at most l1row of the row.

theorem Sendov.wsum_length_le {m : ℕ} (L : ℤ) (r : List (List ℤ)) (i : ℕ) : (∀ p ∈ r, p.length ≤ m) → (wsum L i r).length ≤ m

The weighted sum is no longer than the entries it combines.

theorem Sendov.l1_wsum_le (L : ℤ) (hL : 0 ≤ L) (r : List (List ℤ)) (i : ℕ) : l1 (wsum L i r) ≤ L * l1row r

The weighted sum's L¹ norm is at most L times the row's.

The bounds in usable form

Each hypothesis of Sendov.wsum_eq_of_packed reduces to an inequality between explicit numbers, so a degree file never computes qrow.

theorem Sendov.rowZ_bound (g₀ g₁ g₂ : List ℤ) (k G : ℕ) (β τ : ℤ) (hβ : 1 ≤ β) (h0 : g₀.length ≤ G) (h1 : g₁.length ≤ G) (h2 : g₂.length ≤ G) (hτ : 2 * ((l1 g₀ + l1 g₁ + l1 g₂) ^ k * β ^ (1 + G * k)) < τ) (a : ℤ) : a ∈ rowZ (qrow g₀ g₁ g₂ k) β → 2 * |a| < τ

The τ bound: the α-packed row entries are bounded by the L¹ norm times a power of β, the exponent coming from Sendov.qrow_entry_length_le.

theorem Sendov.wsum_bound (g₀ g₁ g₂ : List ℤ) (k : ℕ) (L β : ℤ) (hL : 0 ≤ L) (hβ : 2 * (L * (l1 g₀ + l1 g₁ + l1 g₂) ^ k) < β) (a : ℤ) : a ∈ wsum L 0 (qrow g₀ g₁ g₂ k) → 2 * |a| < β

The β bound for the moment numerator.

theorem Sendov.pev_wsum_eq_of_packed (g₀ g₁ g₂ : List ℤ) (k m : ℕ) (L β τ : ℤ) (Nmom : List ℤ) (hβ : 0 < β) (hτ : 0 < τ) (hbτ : ∀ a ∈ rowZ (qrow g₀ g₁ g₂ k) β, 2 * |a| < τ) (hbN : ∀ a ∈ Nmom, 2 * |a| < β) (hbW : ∀ a ∈ wsum L 0 (qrow g₀ g₁ g₂ k), 2 * |a| < β) (hlenN : Nmom.length ≤ m) (hlenW : (wsum L 0 (qrow g₀ g₁ g₂ k)).length ≤ m) (hcheck : wsumZ L 0 (unpackZ τ (qrow g₀ g₁ g₂ k).length ((pevZ g₀ β + pevZ g₁ β * τ + pevZ g₂ β * τ ^ 2) ^ k)) = pevZ Nmom β) (α : ℝ) : pev Nmom α = pev (wsum L 0 (qrow g₀ g₁ g₂ k)) α

Pad-tolerant verification. Concludes equality of the polynomial functions, which is all the moment needs, and so requires only length bounds rather than an exact match.

theorem Sendov.integral_moment_packed (n k : ℕ) (hn : 2 ≤ n) (α : ℝ) (hα : 0 ≤ α) (L : ℤ) (hL : 0 < L) (Nmom : List ℤ) (hdvd : ∀ j < 2 * k + 1, ↑0 + ↑j + 4 ∣ L) (hNmom : pev Nmom α = pev (wsum L 0 (qrow (gg0 n) (gg1 n) (gg2 n) k)) α) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q n α t ^ k = pev Nmom α / (↑L * (2 * M n * (3 + α)) ^ k)

The moment from a verified numerator. Combining Sendov.integral_moment_of with Sendov.pev_wsum, the integral is an explicit integer polynomial over an explicit denominator. Everything on the right is either supplied by the generator or a kernel computation on integers.

theorem Sendov.abs_le_l1row (r : List (List ℤ)) (p : List ℤ) : p ∈ r → ∀ a ∈ p, |a| ≤ l1row r

Every coefficient of every entry of a row is bounded by the row's L¹ norm.