Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck 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≤k≤n,

(nk)=(nn−k).

For 0≤k<n,

(nk+1)≥(nk)⟺k+1≤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≤k≤n.

[F1]

(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 (nk):=∣[n]k∣).

[L1]
[L2]

The product rule licenses the usual double count of a set together with a chosen element outside or inside it (The product rule: ∣A×B∣=∣A∣ ∣B∣, and ∣∏i<mAi∣=∏i<m∣Ai∣).

Proof

technique · direct
1.1

The symmetry (nk)=(nn−k) is the symmetry clause of [L1].

L1
1.2

For k<n, count pairs (S,x) with ∣S∣=k and x∉S by first choosing S, or by first choosing the (k+1)-set S∪{x} and then the deleted element. This gives (nk)(n−k)=(nk+1)(k+1), in agreement with [L1].

F1L1L2
2.1

Since both n−k and k+1 are positive, step 1.2 shows that (nk+1)≥(nk) exactly when n−k≥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

Dependency tree · two levels

30 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