The odd central binomial coefficient is at most 4^m

Identifier: F:nat-choose-two-mul-succ-le-four-pow
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every natural m, the binomial coefficient choose(2m+1, m) is at most 4^m. This is strictly sharper than the row bound this kernel already had: Nat.choose_le_two_pow gives choose(2m+1, m) <= 2^(2m+1) = 2*4^m, and the missing factor of two is exactly what Erdos's induction for the primorial bound cannot afford. The sharpening comes from the row sum carrying the middle coefficient TWICE -- choose(2m+1, m) = choose(2m+1, m+1) -- so twice the coefficient is at most the whole row sum 2^(2m+1) = 4^m + 4^m. This is a kernel term with an empty axiom footprint.

Formal statement

theorem Nat.choose_two_mul_succ_le_four_pow : ((x0 : AxNat) -> AxNat.le (AxNat.choose (AxNat.succ (AxNat.add x0 x0)) x0) (AxNat.pow (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero)))) x0))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

kernel-Nat.choose_two_mul_succ_le_four_pow

Kind: kernel-term
Status: checked

Supports: Nat.choose_two_mul_succ_le_four_pow is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

test "$(cargo run -q --release -p axeyum-lean-kernel --example nat_theorem_inventory -- choose_two_mul_succ_le_four_pow 2>/dev/null | grep -Fc 'Nat.choose_two_mul_succ_le_four_pow	1	((x0 : AxNat) -> AxNat.le (AxNat.choose (AxNat.succ (AxNat.add x0 x0)) x0) (AxNat.pow (AxNat.succ (AxNat.succ (AxNat.succ (AxNat.succ AxNat.zero)))) x0))')" -ge 1

Evidence notes

`build_nat_prelude` admits this only through the trusted `Kernel::add_declaration` gate, which re-derives the type from the proof term. The check matches the FULL RENDERED TYPE rather than the name: a name-only checker survives a weakened statement, and the weakening that matters here is exactly the one this theorem exists to rule out -- `pow 2 (add m m)` replaced by `pow 2 (succ (add m m))`, which is `choose_le_two_pow` and was already available.

instantiate-Nat.choose_two_mul_succ_le_four_pow

Kind: kernel-term
Status: checked

Supports: The bound instantiates at m = 0,1,2,3 with both sides independently evaluated (choose 7 3 = 35, 4^3 = 64), and 4^3 is a DIFFERENT numeral from 2^7 = 128 -- the bound choose_le_two_pow already gave.

Checker command

cargo test --release -p axeyum-lean-kernel --lib -- nat_prelude::central_binomial_tests:: --test-threads=4

Evidence notes

The sharpness check is the reason the suite exists: `the_bound_is_sharper_than_choose_le_two_pow` asserts `4^3` and `2^7` are NOT def-eq, so a 'sharpening' that happened to restate the weaker theorem would fail. The instantiation test asserts the applied type against a hand-rebuilt `Le (choose (2m+1) m) (pow 4 m)` at each m and, separately, that each side reduces to the hand-computed numeral.

footprint-Nat.choose_two_mul_succ_le_four_pow

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- the Nat environment admits no trusted declaration

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free nat

Evidence notes

The suite's own `the_central_binomial_shelf_is_admitted_and_axiom_free` asserts `Environment::contains` FIRST for each of the five names and only then an empty `Kernel::axiom_footprint`: the footprint of a name that is not in the environment is also empty, so the footprint assertion alone would pass for a declaration that was never made. `nat_axiom_inventory` bounds it independently by enumerating the whole trusted surface.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum-lean-kernel build_nat_prelude, lane chebyshev-pi",
  "source": "theorem name and canonical type read directly via nat_theorem_inventory, which prints render_lean of the admitted type. The proof is the standard one: Nat.sum_choose_row for the row sum, Nat.choose_symm_of_eq_add for the middle symmetry, Nat.sumRange_split (with one add_comm, because Nat.add recurses on its RIGHT argument and the split bound is stuck otherwise) and two Nat.sumRange_succ peels for the two-term lower bound, and a new Nat.le_of_add_self_le_add_self for the final cancellation.",
  "prior_art": [
    {
      "who": "Paul Erdos",
      "what": "the central binomial bound used in the elementary proof of Bertrand's postulate and of the primorial bound",
      "year": 1932,
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}