A uniform certificate for the finite Moore band

This file proves the SUM side condition on the full range 48 ≤ n ≤ 122 without subdividing the range. The census inequalities imply, for t = n - 4 - X - 3h, v = n - h, and ell = (2n - X) / 12 / 2, that

• 43 ≤ t ≤ v ≤ 122,
• 4 ≤ ell ≤ 10, and
• 5v + 41 ≤ 50ell + 3t.

These bounds give (t - 9) * v ^ ell ≤ (v + 2t) ^ ell. The exponent-four case is an endpoint estimate; the remaining exponents follow from the first three nonconstant binomial terms and an exact chord identity for a cubic polynomial. This replaces the five numerical ratio certificates formerly used by Band.Assembly.

theorem ACMax.binomial_lower_three (v t k : ℕ) : 3 * (v + 2 * t) ^ (k + 3) ≥ 3 * v ^ (k + 3) + 6 * (k + 3) * t * v ^ (k + 2) + 6 * (k + 3) * (k + 2) * t ^ 2 * v ^ (k + 1) + 4 * (k + 3) * (k + 2) * (k + 1) * t ^ 3 * v ^ k

theorem ACMax.uniform_power_four (t v : ℕ) (ht43 : 43 ≤ t) (htv : t ≤ v) (hv122 : v ≤ 122) (hlin : 5 * v + 41 ≤ 200 + 3 * t) : (t - 9) * v ^ 4 ≤ (v + 2 * t) ^ 4

theorem ACMax.uniform_cubic_arith (t v ell : ℕ) (ht43 : 43 ≤ t) (htv : t ≤ v) (hv122 : v ≤ 122) (hell5 : 5 ≤ ell) (hell10 : ell ≤ 10) (hlin : 5 * v + 41 ≤ 50 * ell + 3 * t) : 3 * (t - 10) * v ^ 3 ≤ 6 * ell * t * v ^ 2 + 6 * ell * (ell - 1) * t ^ 2 * v + 4 * ell * (ell - 1) * (ell - 2) * t ^ 3

theorem ACMax.uniform_power_ge_five (t v k : ℕ) (ht43 : 43 ≤ t) (htv : t ≤ v) (hv122 : v ≤ 122) (hk2 : 2 ≤ k) (hk7 : k ≤ 7) (hlin : 5 * v + 41 ≤ 50 * (k + 3) + 3 * t) : (t - 9) * v ^ (k + 3) ≤ (v + 2 * t) ^ (k + 3)

theorem ACMax.uniform_power_certificate (t v ell : ℕ) (ht43 : 43 ≤ t) (htv : t ≤ v) (hv122 : v ≤ 122) (hell4 : 4 ≤ ell) (hell10 : ell ≤ 10) (hlin : 5 * v + 41 ≤ 50 * ell + 3 * t) : (t - 9) * v ^ ell ≤ (v + 2 * t) ^ ell

theorem ACMax.uniform_region_bounds (n X h : ℕ) (hM : 10 * X + 7 * h + 186 ≤ 4 * n) (hHoard : 3 * X + 26 ≤ n) (hhX : h ≤ X) (hn48 : 48 ≤ n) (hn122 : n ≤ 122) : have t := n - 4 - X - 3 * h; have v := n - h; have ell := (2 * n - X) / 12 / 2; 43 ≤ t ∧ t ≤ v ∧ v ≤ 122 ∧ 4 ≤ ell ∧ ell ≤ 10 ∧ 5 * v + 41 ≤ 50 * ell + 3 * t

theorem ACMax.sum_cert_of_power {t v ell : ℕ} (ht10 : 10 ≤ t) (hA : t * (v - 1) + 1 ≤ (t - 10) * (v + t)) (hpower : (t - 9) * v ^ ell ≤ (v + 2 * t) ^ ell) (hv : 0 < v) : t * (v - 1) * v ^ ell < (v + t) * ((v + 2 * t) ^ ell - v ^ ell)

theorem ACMax.band_cert_uniform_48_122 (n X h : ℕ) (hM : 10 * X + 7 * h + 186 ≤ 4 * n) (hHoard : 3 * X + 26 ≤ n) (hhX : h ≤ X) (hn48 : 48 ≤ n) (hn122 : n ≤ 122) : (n - 4 - X - 3 * h) * (n - h - 1) * (n - h) ^ ((2 * n - X) / 12 / 2) < (n - h + (n - 4 - X - 3 * h)) * ((n - h + 2 * (n - 4 - X - 3 * h)) ^ ((2 * n - X) / 12 / 2) - (n - h) ^ ((2 * n - X) / 12 / 2))