The finite range 5 ≤ n ≤ 100

This file does nothing but assemble the individual degree files and the degree batches into a single statement. Its only content is the case split, so it is also where the claim "every degree in the range is covered" gets checked: the branches below are generated from the batch plan, and the file would not compile if a degree were skipped.

Degrees 5 and 7 are handled one at a time (Sendov.finite_range_five, Sendov.finite_range_seven); every other degree is covered by a batch B n₀ n₁, whose proof is a single Bernstein certificate valid simultaneously for all n₀ ≤ n ≤ n₁.

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

The finite range. Every degree from 5 to 100 inclusive.

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

The finite-range claim. The right-hand side of equation stat of the blog post is strictly less than 1 on the range of degrees and of α left open there, that is, on 5 ≤ n ≤ 97, 0 ≤ α ≤ 17, subject to the feasibility constraint c ^ 2 ≤ A.

This is the original challenge statement. It is a special case of finite_range_le_100, which covers three more degrees: the finite certification was pushed from 97 to 100 so that it meets the large-degree argument of Sendov.LargeDegree with room to spare.

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

Equation stat of the blog post is infeasible on the range 5 ≤ n ≤ 97, 0 ≤ α ≤ 17, c ^ 2 ≤ A. This is the form in which the claim is used.