Kummer bridge for the Concrete Mathematics GKP conjecture.

This file owns the central-binomial digit-excess lemmas used by the active GKP attack. Earlier versions imported these lemmas from the retired Erdos117 squarefree-central-binomial scaffold. Keeping them here makes the ConcreteMath module self-contained around its actual open target.

Kummer digit-excess form for central binomial coefficients

theorem Egrs75.ConcreteMath.sub_one_mul_padicValNat_centralBinom (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : (p - 1) * padicValNat p n.centralBinom = 2 * (p.digits n).sum - (p.digits (2 * n)).sum

General p-adic formula for central binomial coefficients.

For any prime p, (p - 1) * ν_p(C(2n,n)) = 2 * S_p(n) - S_p(2n), where S_p is the sum of base-p digits. This is Kummer's theorem specialized to Nat.centralBinom.

theorem Egrs75.ConcreteMath.pow_dvd_centralBinom_of_digit_excess {p n m : ℕ} [hp : Fact (Nat.Prime p)] (h : (p - 1) * m ≤ 2 * (p.digits n).sum - (p.digits (2 * n)).sum) : p ^ m ∣ n.centralBinom

p^m divides Nat.centralBinom n from a Kummer digit bound.

If 2 * S_p(n) - S_p(2n) ≥ (p - 1) * m, then p^m ∣ C(2n,n). This is the reusable bridge from digit/carry certificates to central-binomial divisibility.

theorem Egrs75.ConcreteMath.two_mul_padicValNat_three_centralBinom (n : ℕ) : 2 * padicValNat 3 n.centralBinom = 2 * (Nat.digits 3 n).sum - (Nat.digits 3 (2 * n)).sum

The ternary specialization of the central-binomial digit-excess formula.