Central-binomial consequence of the bounded C3 certificate

The bounded prefix computation supplies a secondary application of the general Kummer carry theorem: divisibility by nine for a finite family of central binomial coefficients indexed by powers of four.

theorem GKPCarry.nine_dvd_centralBinom_four_pow_in_finite_range {m : ℕ} (hlower : 27 ≤ m) (hupper : m ≤ 6560) : 9 ∣ (4 ^ m).centralBinom

The bounded C3 certificate implies divisibility by nine for Nat.centralBinom (4 ^ m) throughout 27 ≤ m ≤ 6560.

theorem GKPCarry.nine_dvd_centralBinom_two_pow_even_in_finite_range {m : ℕ} (hlower : 27 ≤ m) (hupper : m ≤ 6560) : 9 ∣ (2 ^ (2 * m)).centralBinom

Equivalent power-of-two form of the bounded central-binomial theorem.