An exact Moore certificate for every order at least 48

The existing power estimate handles exponents four through seven. For exponent at least eight, the fourth nonconstant term of the binomial expansion gives a uniform certificate with no upper bound on the order.

theorem ACMax.small_exponent_power_growth (t v ell : ℕ) (ht43 : 43 ≤ t) (htv : t ≤ v) (hv107 : v ≤ 107) (hell4 : 4 ≤ ell) (hell7 : ell ≤ 7) (hlin : 5 * v + 41 ≤ 50 * ell + 3 * t) : (t - 9) * v ^ ell ≤ (v + 2 * t) ^ ell

The small-exponent power estimate in the parameter range used by the paper.

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

The binomial expansion through its fourth nonconstant term.

theorem ACMax.fourth_term_corner_t43 (v ell : ℕ) (hell8 : 8 ≤ ell) (hlin : 5 * v + 41 ≤ 50 * ell + 3 * 43) : 3 * v ^ 4 ≤ 2 * ell * (ell - 1) * (ell - 2) * (ell - 3) * 43 ^ 3

At t = 43, the fourth-term inequality is minimized at ell = 8.

theorem ACMax.fourth_term_ratio_step (t A C : ℕ) (ht : 1 ≤ t) (hAt : 5 * t ≤ A) (hbase : 3 * A ^ 4 ≤ C * t ^ 3) : 3 * (A + 3) ^ 4 ≤ C * (t + 1) ^ 3

Increasing t by one cannot worsen the scaled fourth-term ratio when A ≥ 5t.

theorem ACMax.fourth_term_corner_ge44 (ell a : ℕ) (hell8 : 8 ≤ ell) : 2 * (44 + a) + 41 ≤ 50 * ell → 3 * (50 * ell + 91 + 3 * a) ^ 4 ≤ 1250 * ell * (ell - 1) * (ell - 2) * (ell - 3) * (44 + a) ^ 3

The scaled corner inequality for t ≥ 44.

theorem ACMax.fourth_term_region (t v ell : ℕ) (ht43 : 43 ≤ t) (htv : t ≤ v) (hell8 : 8 ≤ ell) (hlin : 5 * v + 41 ≤ 50 * ell + 3 * t) : 3 * v ^ 4 ≤ 2 * ell * (ell - 1) * (ell - 2) * (ell - 3) * t ^ 3

The census region implies the fourth-term inequality whenever ell ≥ 8.

theorem ACMax.sum_cert_of_fourth {t v ell : ℕ} (ht : 0 < t) (hv : 0 < v) (hell8 : 8 ≤ ell) (hfourth : 3 * v ^ 4 ≤ 2 * ell * (ell - 1) * (ell - 2) * (ell - 3) * t ^ 3) : t * (v - 1) * v ^ ell < (v + t) * ((v + 2 * t) ^ ell - v ^ ell)

The fourth binomial term implies the exact Moore side condition.

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

The order-free parameter bounds supplied by the strengthened census.

theorem ACMax.band_cert_uniform_ge_48 (n X h : ℕ) (hM : 10 * X + 7 * h + 186 ≤ 4 * n) (hhX : h ≤ X) (hn48 : 48 ≤ n) : (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))

The exact non-backtracking side condition holds throughout the full census region n ≥ 48.