The finite-range claim in degree five

The lowest degree, where the exponent (n-4)/2 is 0 + 1/2, so Sendov.R 5 α involves √Q itself.

The informal plan treats this degree separately, on the ground that bound (O) — the tangent line at q = 1 — is too wasteful here, and proposes instead the chord bound Q(t) ≤ 1 - (1-B)t, the resulting formula for ∫ t³ √(1-(1-B)t) dt in half-integer powers of B, and the substitution α = 3r²/(1-r²) needed to make that rational.

None of this is necessary. The waste in (O) comes entirely from the tangent line being taken at q = 1, whereas the values of Q that matter here are small; taking the tangent at q = w² for a smaller rational w fixes it. With w = 1/3, Sendov.integral_rpow_le gives √Q ≤ 3Q/2 + 1/6 and hence

∫ t in 0..1, t³ √Q dt ≤ (3/2) (1/4 - 2c/5 + A/6) + 1/24,

which is already enough. So degree five uses exactly the same machinery as every other odd degree, with only the parameter w changed, and no square roots survive.

With M 5 = 4, A 5 α = 1 - α/2 and c 5 α = (12 - α - α²)/(4(3+α)), the resulting upper bound for R 5 α is 1 - P α / (96 (3+α)²) with

P α = -9α⁴ - 123α³ + 596α² + 30α + 234,

which is positive up to α = 3.912, while feasibility gives α ≤ 2 outright (this is the one degree where Sendov.alpha_le_half_M is exactly the bound A 5 α ≥ 0). For orientation: over the feasible range α ≤ 1.678 the exact maximum of R 5 α is about 0.716, against 0.737 for this upper bound — whereas w = 1 would give 1.063, above 1, and would prove nothing.

theorem Sendov.M_five : M 5 = 4

theorem Sendov.A_five (α : ℝ) : A 5 α = 1 - α / 2

theorem Sendov.c_five (α : ℝ) : c 5 α = 1 - α / 4 - α / (2 * (3 + α))

theorem Sendov.c_five' {α : ℝ} (hα : 0 ≤ α) : c 5 α = (12 - α - α ^ 2) / (4 * (3 + α))

theorem Sendov.integral_five {α : ℝ} (hfeas : c 5 α ^ 2 ≤ A 5 α) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q 5 α t ^ ((↑5 - 4) / 2) ≤ 3 / 2 * (1 / 4 - 2 * c 5 α / 5 + A 5 α / 6) + 1 / 24

The odd-degree bound in degree five, with the tangent line taken at q = 1/9.

theorem Sendov.R_five_le {α : ℝ} (hα : 0 ≤ α) (hfeas : c 5 α ^ 2 ≤ A 5 α) : R 5 α ≤ 1 / 6 + 1 / (4 * (3 + α)) + 1 / 8 + 1 / (16 * (3 + α)) + 60 * A 5 α ^ 2 / (4 * (3 + α)) * (3 / 2 * (1 / 4 - 2 * c 5 α / 5 + A 5 α / 6) + 1 / 24)

The upper bound for R 5 α obtained from Sendov.integral_five.

theorem Sendov.finite_range_five {α : ℝ} (hα : 0 ≤ α) (hfeas : c 5 α ^ 2 ≤ A 5 α) : R 5 α < 1

The finite-range claim in degree five.