The low-degree branch: degrees 2 ≤ n ≤ 5

The high-degree argument relaxes the branch point (⋆),

1 ≤ ∫₀¹ ∏ⱼ ‖a + t(1-a²)qⱼ‖ dt,

by AM–GM to the raw polar inequality (1Q), and then needs the origin channel as well. In low degree none of that is necessary: bounding each factor of (⋆) by the scalar X(t) = a + (1-a²)t already contradicts itself.

Writing m = n - 1 for the number of non-distinguished zeroes and J_m(a) = ∫₀¹ X(t)^m dt, the branch point gives 1 ≤ J_m(a) while a direct computation gives J_m(a) < 1 for 0 < a < 1 and 1 ≤ m ≤ 4. The computation is done once, at m = 4:

1 - J₄(a) = ((1-a)³(1+a)/5)(a⁴ - 3a³ + 3a + 4),

whose last factor is 2 + 3a + (1-a)(2 + 2a + a²(2-a)) > 0; the smaller exponents are dominated by X^m ≤ 1 - m/4 + (m/4)X⁴, four instances of weighted AM–GM that factor as squares.

Note the off-by-one: m ≤ 4 is degree n ≤ 5, so this branch covers degree five as well. All strictness comes from a < 1; at a = 1 one has J_m(1) = 1, matching the regular-polygon equality examples.

Main statements

• Sendov.low_degree_contradiction: (⋆) is contradictory for 2 ≤ n ≤ 5;
• Sendov.lowJ_lt_one: J_m(a) < 1 for 0 < a < 1 and 1 ≤ m ≤ 4.

The scalar chord and its moments

noncomputable def Sendov.lowX (a t : ℝ) : ℝ

X(t) = a + (1-a²)t, the pointwise majorant of ‖a + t(1-a²)qⱼ‖.

Equations

• Sendov.lowX a t = a + (1 - a ^ 2) * t

noncomputable def Sendov.lowJ (m : ℕ) (a : ℝ) : ℝ

J_m(a) = ∫₀¹ X(t)^m dt.

Equations

• Sendov.lowJ m a = ∫ (t : ℝ) in 0..1, Sendov.lowX a t ^ m

theorem Sendov.lowX_nonneg {a t : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (ht0 : 0 ≤ t) : 0 ≤ lowX a t

theorem Sendov.continuous_lowX_pow (a : ℝ) (m : ℕ) : Continuous fun (t : ℝ) => lowX a t ^ m

The branch point, bounded factor by factor

theorem Sendov.norm_le_lowX {a t : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (ht0 : 0 ≤ t) {v : ℂ} (hv : ‖v‖ ≤ 1) : ‖↑a + ↑t * (1 - ↑a ^ 2) * v‖ ≤ lowX a t

theorem Sendov.prod_norm_le_lowX_pow {a t : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (ht0 : 0 ≤ t) (q : Multiset ℂ) : (∀ v ∈ q, ‖v‖ ≤ 1) → (Multiset.map (fun (v : ℂ) => ‖↑a + ↑t * (1 - ↑a ^ 2) * v‖) q).prod ≤ lowX a t ^ q.card

theorem Sendov.one_le_lowJ {n : ℕ} {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a ≤ 1) {q : Multiset ℂ} (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (hstar : 1 ≤ ∫ (t : ℝ) in 0..1, (Multiset.map (fun (v : ℂ) => ‖↑a + ↑t * (1 - ↑a ^ 2) * v‖) q).prod) : 1 ≤ lowJ (n - 1) a

The branch point (⋆), with every factor replaced by the scalar X(t).

The fourth moment

theorem Sendov.lowJ_four (a : ℝ) : lowJ 4 a = a ^ 4 + 2 * a ^ 3 * (1 - a ^ 2) + 2 * a ^ 2 * (1 - a ^ 2) ^ 2 + a * (1 - a ^ 2) ^ 3 + (1 - a ^ 2) ^ 4 / 5

J₄(a), by the fundamental theorem of calculus against an explicit antiderivative. The antiderivative is written without dividing by 1 - a², so no side condition on a appears.

theorem Sendov.lowJ_four_identity (a : ℝ) : 1 - lowJ 4 a = (1 - a) ^ 3 * (1 + a) / 5 * (a ^ 4 - 3 * a ^ 3 + 3 * a + 4)

theorem Sendov.quartic_aux_pos {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) : 0 < a ^ 4 - 3 * a ^ 3 + 3 * a + 4

theorem Sendov.lowJ_four_lt_one {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) : lowJ 4 a < 1

Dominating exponents one through four by the fourth

theorem Sendov.pow_le_quartic_average {x : ℝ} (hx : 0 ≤ x) {m : ℕ} (hm0 : 1 ≤ m) (hm4 : m ≤ 4) : x ^ m ≤ 1 - ↑m / 4 + ↑m / 4 * x ^ 4

X^m ≤ 1 - m/4 + (m/4)X⁴ for 0 ≤ X and 1 ≤ m ≤ 4: weighted AM–GM, but at these four exponents each instance factors as a square times a positive quadratic.

theorem Sendov.lowJ_lt_one {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) {m : ℕ} (hm0 : 1 ≤ m) (hm4 : m ≤ 4) : lowJ m a < 1

The contradiction

theorem Sendov.low_degree_contradiction {n : ℕ} (hn : 2 ≤ n) (hn5 : n ≤ 5) {a : ℝ} (ha0 : 0 < a) (ha1 : a < 1) {q : Multiset ℂ} (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (hstar : 1 ≤ ∫ (t : ℝ) in 0..1, (Multiset.map (fun (v : ℂ) => ‖↑a + ↑t * (1 - ↑a ^ 2) * v‖) q).prod) : False

The low-degree branch. The branch point (⋆) is already contradictory for 2 ≤ n ≤ 5, with no recourse to the origin channel.