CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

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.

The central binomial coefficient is asymptotic to 4^n divided by the square root of pi n

Statement

For $n \geq 1$ , put $a_{n} : = (\binom{2 n}{n}) / 4^{n}$ . Then

$\sqrt{π n} a_{n} ⟶ 1.$

Equivalently,

$(\binom{2 n}{n}) \sim \frac{4^{n}}{\sqrt{π n}},$

where the asymptotic notation means that the ratio of the two sides tends to $1$ .

Facts & Assumptions

Given: A natural $n \geq 1$ and the positive real $a_{n} = (\binom{2 n}{n}) / 4^{n}$ .

[L1]

For $k \leq n$ , $(\binom{n}{k}) k! (n - k)! = n!$ , so the usual factorial quotient equals the binomial coefficient ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ , The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L2]

For $n \in N$ , $W_{n} = \prod_{k = 1}^{n} (2 k)^{2} / ((2 k - 1) (2 k + 1))$ , with $W_{0} = 1$ , and $W_{n} \to π / 2$ (Wallis's product: pi over two is the limit of the finite Wallis products).

[L3]

A finite product in a monoid has empty product equal to the identity and satisfies the recursion that adjoins its last factor (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity).

[L4]

Products and quotients of convergent real sequences have the corresponding limits when the limiting denominator is nonzero (Algebra of limits: sums, scalar multiples, products and quotients).

[L5]

Every nonnegative real has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[L6]

For every $ε > 0$ there is a natural $N \geq 1$ with $1 / N < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L7]

The constant $π$ is positive (Pi as twice the smallest positive zero of cosine).

Proof

technique · direct

1.1givenL1L3algebra

By [L1] and [L3], $a_{n} = \frac{(2 n)!}{(n!)^{2} 4^{n}} = \prod_{k = 1}^{n} \frac{2 k - 1}{2 k} .$

2.1step 1.1L2L3algebra

Comparing step 1.1 with the factors in $W_{n}$ gives $W_{n} = \frac{1}{(2 n + 1) a_{n}^{2}} .$

3.1step 2.1L2L4L6algebra

By [L2], [L4], and step 2.1, $((π / 2) (2 n + 1) a_{n}^{2}) \to 1$ . Also $2 n / (2 n + 1) \to 1$ by [L6], so $π n a_{n}^{2} = \frac{2 n}{2 n + 1} \cdot \frac{π}{2} (2 n + 1) a_{n}^{2} ⟶ 1.$

4.1step 3.1L5L7algebra

Let $b_{n} : = \sqrt{π n} a_{n} \geq 0$ , which is defined by [L5] and [L7]. Then $b_{n}^{2} = π n a_{n}^{2} \to 1$ by step 3.1, and $∣ b_{n} - 1 ∣ = \frac{∣ b_{n}^{2} - 1 ∣}{b_{n} + 1} \leq ∣ b_{n}^{2} - 1 ∣,$ so $b_{n} \to 1$ .

5.1givenstep 4.1algebra

For every $n \geq 1$ , the ratio of $(\binom{2 n}{n})$ to $4^{n} / \sqrt{π n}$ is exactly $\sqrt{π n} a_{n}$ . Thus either displayed asymptotic formulation implies the other, by the definition of asymptotic equivalence.

6.1givenstep 1.1step 2.1step 3.1step 4.1step 5.1L1L7∎

At $n = 0$ , $a_{0} = 1$ but the comparison term $4^{n} / \sqrt{π n}$ is undefined. The theorem starts at $n = 1$ , where every denominator in steps 1.1 to 5.1 is positive, and steps 4.1 and 5.1 prove its two equivalent formulations.

The central binomial coefficient is asymptotic to 4^n divided by the square root of pi n

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources