The large-degree claim

Sendov.U_le_Ut removed the degree from the bound; what is left is the single inequality Ut α < 1 on 0 ≤ α ≤ 17, and then R n α < 1 for every n ≥ 101.

Ut is a rational function of α times (α/(3+α)) ^ 48, so multiplying by

D = 865200 · (3+α) ^ 49 · γ ^ 4, γ = 300 + 47α - α²,

which is positive on [0,17], turns the claim into positivity of the single polynomial F = D (1 - Ut) of degree 58. The two closed forms used are

c 101 α = γ / (100 (3+α)), T1 101 α = 1600000 (100-2α)² (3+α)³ / (721 γ⁴).

A Bernstein certificate on [0,17] settles it: all 59 coefficients of F in the basis α^m (17-α)^(58-m) are positive, so no subdivision of the α-range is needed. (The informal write-up splits at α = 16 and estimates the two pieces separately; that is not necessary once the sharp Beta constant is used, which is what leaves the margin — Ut peaks at α = 17 with value 0.9229.)

How the identity is checked

D and D · Ut are written as coefficient lists (Sendov.endD, Sendov.endN), using the polynomial arithmetic of Sendov.FiniteRange.Certificate, so that F = endD - endN is a list the kernel can compute, and the Bernstein certificate Sendov.endB is a decidable equality of lists (Sendov.pev_pos_of_bern). The only identity proved by ring is pev endN α = Ut α · pev endD α (Sendov.endN_eq): each of the six terms of Ut cancels against the matching factor of D separately, and (3+α) ^ 48 and γ ^ 4 are generalized away before field_simp, so nothing of degree 48 is ever expanded. Upstream, this identity and the certificate were closed by ring under a twentyfold heartbeat budget.

Main statements

• Sendov.Ut_lt_one: Ut α < 1 on 0 ≤ α ≤ 17;
• Sendov.large_degree: R n α < 1 for n ≥ 101.

def Sendov.gam : List ℤ

γ = 300 + 47α - α², which is 100 (3+α) · c 101 α.

Equations

• Sendov.gam = [300, 47, -1]

theorem Sendov.pev_gam (x : ℝ) : pev gam x = 300 + 47 * x - x ^ 2

def Sendov.endD : List ℤ

The denominator D = 865200 (3+α)^49 γ⁴.

Equations

• Sendov.endD = Sendov.pscale 865200 (Sendov.pmul (Sendov.ppow [3, 1] 49) (Sendov.ppow Sendov.gam 4))

def Sendov.endN : List ℤ

The numerator D · Ut: the six terms of Ut, each multiplied by D.

Equations

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

def Sendov.endF : List ℤ

F = D (1 - Ut), the polynomial certified positive.

Equations

• Sendov.endF = Sendov.psub Sendov.endD Sendov.endN

def Sendov.endB : List ℤ

The Bernstein coefficients of 17 ^ 58 * F on [0, 17].

Equations

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

theorem Sendov.F_pos {α : ℝ} (hα : 0 ≤ α) (hα' : α ≤ 17) : 0 < pev endF α

The Bernstein certificate: F is positive on [0,17].

theorem Sendov.gam_pos {α : ℝ} (hα : 0 ≤ α) (hα' : α ≤ 17) : 0 < 300 + 47 * α - α ^ 2

theorem Sendov.endD_pos {α : ℝ} (hα : 0 ≤ α) (hα' : α ≤ 17) : 0 < pev endD α

theorem Sendov.endN_eq {α : ℝ} (hα : 0 ≤ α) (hα' : α ≤ 17) : pev endN α = Ut α * pev endD α

D · Ut = N, with (3+α) ^ 48 and γ ^ 4 generalized away before clearing denominators.

theorem Sendov.Ut_lt_one {α : ℝ} (hα : 0 ≤ α) (hα' : α ≤ 17) : Ut α < 1

The bound in α alone is below 1.

theorem Sendov.large_degree {α : ℝ} {n : ℕ} (hn : 101 ≤ n) (hα : 0 ≤ α) (hα' : α ≤ 17) (hfeas : c n α ^ 2 ≤ A n α) : R n α < 1

The large-degree claim. Every degree n ≥ 101.