LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Central binomial coefficient bounds

Statement

For every natural number $n$ ,

\frac{4^{n}}{2 n + 1} \leq (\binom{2 n}{n}) \leq 4^{n} .

Facts & Assumptions

Given: A natural number $n$ .

[L1]

The binomial theorem gives

\sum_{k = 0}^{2 n} (\binom{2 n}{k}) = (1 + 1)^{2 n} = 4^{n}

(The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$ , The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L2]

The binomial coefficients in the $2 n$ th row are symmetric and unimodal, so their maximum occurs at the central term $(\binom{2 n}{n})$ (The binomial coefficients are symmetric and increase to the middle level before decreasing).

Proof

technique · direct

1.1

The upper bound is immediate from [L1], since $(\binom{2 n}{n})$ is one nonnegative term in a sum equal to $4^{n}$ .

1.2

There are exactly $2 n + 1$ terms in the sum of [L1], and [L2] says that each of them is at most the central term $(\binom{2 n}{n})$ . Therefore $4^{n} = \sum_{k = 0}^{2 n} (\binom{2 n}{k}) \leq (2 n + 1) (\binom{2 n}{n}) .$

L1L2algebra

2.1

Rearranging step 1.2 gives the lower bound $\frac{4^{n}}{2 n + 1} \leq (\binom{2 n}{n}) .$ Together with step 1.1 this proves the lemma.

step 1.1step 1.2algebra∎

Depends on

Used by

Factoring a central binomial coefficient to detect interval primes Example
Bertrand's postulate Theorem
Chebyshev's theta function has linear lower and upper bounds Theorem

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Victor Shoup, A Computational Introduction to Number Theory and Algebra, Version 2 (standard reference, not scraped)