The polar and origin inequalities are incompatible

This is the top of the development. The blog post's argument, after the complex-analytic part that is not formalized here, produces two inequalities about a degree n, a zero 0 < a < 1 and the real part x of the mean of the reciprocal critical-point data:

• the raw polar inequality (1Q), 1 ≤ ∫₀¹ P(t)^((n-1)/2) dt;
• the raw origin inequality (origin-exact).

Sendov.polar_origin_incompatible says they cannot both hold for n ≥ 5. Neither statement mentions a polynomial or a complex number, so the theorem is a self-contained assertion about two real numbers.

The chain

                      polar_exp            beta_le
   (1Q)  ─────────────────────▶  (lt)  ─────────────────▶  β(1) ≤ α/(3+α)
                                   │                            │
                                   │ log_le_alpha_mul           │
                                   ▼                            │
                          log α ≤ α(1-β(1))                     │
                                   │                            │
   (origin-exact) ────────────────────────────────────▶  α ≤ 17 │
          │              alpha_le_seventeen                     │
          │ one_le_of_origin                                    │
          ▼                                                     ▼
        (1le) ───────────────────────────────────────────▶  1 ≤ R n α
                          stat_of_one_le                        │
                                                                │ stat_lt_one
                                                                ▼
                                                              False

Both halves of (beta-bound) are needed, and each is used exactly once: the rational half β(1) ≤ α/(3+α) by Sendov.stat_of_one_le, to substitute for β(1) in (1le), and the logarithmic half by Sendov.alpha_le_seventeen, to bound 1/x².

Main statements

• Sendov.polar_origin_incompatible: the two raw inequalities have no common solution.

theorem Sendov.polar_origin_incompatible {n : ℕ} (hn : 5 ≤ n) {a x α : ℝ} (ha : 0 < a) (ha1 : a < 1) (hx : x ^ 2 ≤ 1) (hα : α = M n * (1 - a ^ 2) / 2) (hpolar : 1 ≤ ∫ (t : ℝ) in 0..1, Ppolar a x t ^ ((↑n - 1) / 2)) (horigin : 2 * α + a * x ≤ (1 - x ^ 2) / (2 * M n) + a ^ 2 * ↑n * M n * ∫ (t : ℝ) in 0..1, t * QQ (a * x) (a ^ 2) t ^ ((↑n - 2) / 2)) : False

The polar and origin inequalities are incompatible. For n ≥ 5 there is no 0 < a < 1 and |x| ≤ 1 satisfying both the raw polar inequality (1Q) and the raw origin inequality (origin-exact).