LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

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 binomial coefficients are symmetric and increase to the middle level before decreasing

Statement

For every $n$ and $0\le k\le n$ ,

$\binom nk=\binom n{n-k}.$

For $0\le k<n$ ,

$\binom n{k+1}\ge\binom nk\quad\Longleftrightarrow\quad k+1\le n-k.$

Consequently the binomial coefficients increase up to the middle rank and decrease after it. Their maximum is attained only at $k=n/2$ when $n$ is even, and at the two ranks $k=(n-1)/2$ and $k=(n+1)/2$ when $n$ is odd.

Facts & Assumptions

Given: Natural numbers $n$ and $k$ with $0\le k\le n$ .

[F1]

$\binom nk$ is the number of $k$ -element subsets of an $n$ -element set (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$ ).

[L1]

The binomial closed formula gives symmetry and, for $k<n$ , the identity $\binom nk(n-k)=\binom n{k+1}(k+1)$ ( $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le 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}$ ).

[L2]

The product rule licenses the usual double count of a set together with a chosen element outside or inside it (The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$ , and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$ ).

Proof

technique · direct

1.1

The symmetry $\binom nk=\binom n{n-k}$ is the symmetry clause of [L1].

1.2

For $k<n$ , count pairs $(S,x)$ with $|S|=k$ and $x\notin S$ by first choosing $S$ , or by first choosing the $(k+1)$ -set $S\cup\{x\}$ and then the deleted element. This gives $\binom nk(n-k)=\binom n{k+1}(k+1)$ , in agreement with [L1].

F1L1L2

2.1

Since both $n-k$ and $k+1$ are positive, step 1.2 shows that $\binom n{k+1}\ge\binom nk$ exactly when $n-k\ge k+1$ , with equality exactly when $n-k=k+1$ .

step 1.2algebra

3.1

Reading step 2.1 as $k$ increases gives strict increase before the middle, equality between the two middle ranks only when $n$ is odd, and strict decrease afterward; symmetry from step 1.1 identifies the stated maximizing ranks.

step 1.1step 2.1∎

Depends on

Used by

Sperner's theorem and its equality cases: a largest antichain is a complete middle level Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 69 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

M. Keller and W. T. Trotter, Applied Combinatorics, §6.2 (standard reference, not scraped)