The odd-degree bound

For odd n the exponent (n-4)/2 is the half-integer k + 1/2 with k = (n-5)/2, and Sendov.R involves a genuine square root. Writing Q ^ (k+1/2) = Q ^ k * √Q and bounding √Q by a tangent line to the square root replaces it by polynomial moments:

∫ t in 0..1, t ^ 3 * Q ^ (k+1/2) ≤ ∫ t in 0..1, t ^ 3 * (Q ^ k * (Q/(2w) + w/2))

for any w > 0 (Sendov.integral_rpow_le). This is the only place where Real.sqrt appears; the statement above is already free of it.

The tangent line √q ≤ q/(2w) + w/2 touches at q = w², so w should be chosen near the values of Q that matter. Taking w = 1 recovers 2√u ≤ 1 + u, which is bound (O) of the informal plan and is sharp enough for every odd n ≥ 7. Degree five needs a smaller w: there the relevant values of Q are small, w = 1 overshoots (it gives an upper bound exceeding 1, so it proves nothing), and w = 1/3 works comfortably. This is what lets degree five avoid the chord bound and the substitution α = 3r²/(1-r²) proposed in the plan.

Note that only 0 ≤ Q is needed, never Q ≤ 1: the tangent-line inequality is just (√q - w)² ≥ 0.

theorem Sendov.sqrt_le_tangent {q w : ℝ} (hq : 0 ≤ q) (hw : 0 < w) : √q ≤ q / (2 * w) + w / 2

The tangent line to √· at q = w²: √q ≤ q/(2w) + w/2.

theorem Sendov.rpow_add_half_le {q w : ℝ} (hq : 0 ≤ q) (k : ℕ) (hw : 0 < w) : q ^ (↑k + 1 / 2) ≤ q ^ k * (q / (2 * w) + w / 2)

The half-integer power bound q ^ (k + 1/2) ≤ q ^ k * (q/(2w) + w/2).

theorem Sendov.integral_rpow_le {n : ℕ} {α w : ℝ} (hfeas : c n α ^ 2 ≤ A n α) (k : ℕ) (hk : (↑n - 4) / 2 = ↑k + 1 / 2) (hw : 0 < w) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q n α t ^ ((↑n - 4) / 2) ≤ ∫ (t : ℝ) in 0..1, t ^ 3 * (Q n α t ^ k * (Q n α t / (2 * w) + w / 2))

The odd-degree bound. The square root is eliminated in favour of polynomial moments, at the cost of a free parameter w > 0.