The numerical claim, for every degree

This is the top of the development. Sendov.Defs fixes the notation of equation stat of the blog post; everything else establishes that its right-hand side R n α is below 1. Two arguments meet here.

• Sendov.finite_range_le_100 certifies 5 ≤ n ≤ 100 by explicit polynomial arithmetic: the integral is a finite sum of moments, the moments come from a packed recurrence, and each of 31 batches of degrees carries one Bernstein certificate in α.
• Sendov.large_degree covers n ≥ 101 analytically: the integral is bounded by a Beta integral plus a geometric tail, the resulting elementary bound U is shown decreasing in the degree, and its value at n = 101 is below 1 by one more Bernstein certificate.

The two ranges overlap in intent but not in method, and the seam is at 100/101 rather than at the 97/98 of the blog post: the finite side was pushed three degrees further so that the analytic side would start with margin 0.122 instead of 0.048.

Main statements

• Sendov.stat_lt_one: R n α < 1 for every n ≥ 5, 0 ≤ α ≤ 17 with c ^ 2 ≤ A;
• Sendov.stat_contradiction: equation stat of the blog post is therefore unsatisfiable.

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

The numerical claim. The right-hand side of equation stat of the blog post is strictly less than 1 for every degree n ≥ 5 and every 0 ≤ α ≤ 17 satisfying the feasibility constraint c ^ 2 ≤ A.

theorem Sendov.stat_contradiction {α : ℝ} {n : ℕ} (hn : 5 ≤ n) (hα : 0 ≤ α) (hα' : α ≤ 17) (hfeas : c n α ^ 2 ≤ A n α) (hstat : 1 ≤ R n α) : False

Equation stat is unsatisfiable. This is the form in which the blog post uses the claim: the polynomial argument there produces 1 ≤ R n α under exactly these hypotheses, so the assumed counterexample to Sendov's conjecture cannot exist.