CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-04 (gpt-5.6-sol-codex-subscription)

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.

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

Statement

Let $A$ be an $n$ -element set. Every antichain $F \subseteq P (A)$ satisfies

$∣ F ∣ \leq (\binom{n}{⌊ n / 2 ⌋}) .$

Equality holds exactly for a complete middle level. If $n$ is even, the unique maximum antichain is $[A]^{n / 2}$ . If $n$ is odd, the maximum antichains are exactly the two complete middle levels $[A]^{(n - 1) / 2}$ and $[A]^{(n + 1) / 2}$ .

Facts & Assumptions

Given: An $n$ -element set $A$ and an antichain $F \subseteq P (A)$ .

[L1]

The LYM inequality gives $\sum_{S \in F} 1 / (\binom{n}{∣ S ∣}) \leq 1$ (Lubell-Yamamoto-Meshalkin inequality for antichains in a Boolean lattice).

[L2]

The binomial coefficients have their maximum at the middle rank, uniquely for even $n$ and at the two middle ranks for odd $n$ (The binomial coefficients are symmetric and increase to the middle level before decreasing).

[L3]

For $k < n$ and $G \subseteq [A]^{k}$ , local LYM gives $∣ G ∣ / (\binom{n}{k}) \leq ∣ \nabla G ∣ / (\binom{n}{k + 1})$ , with equality exactly when every set in the upper shadow contains all its $k$ -subsets in $G$ ; the hypothesis $k < n$ is needed, since at $k = n$ the right-hand denominator $(\binom{n}{n + 1})$ is zero (Local LYM inequality comparing a uniform family with its upper shadow).

[F1]

The rank- $k$ level of the Boolean lattice is $[A]^{k}$ and has cardinality $(\binom{n}{k})$ (The Boolean lattice of subsets of a finite set and its rank levels, The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

Proof

technique · direct

1.1

Put $M : = (\binom{n}{⌊ n / 2 ⌋})$ . By [L2], every $(\binom{n}{∣ S ∣}) \leq M$ , so [L1] gives $∣ F ∣ / M \leq \sum_{S \in F} 1 / (\binom{n}{∣ S ∣}) \leq 1$ . Hence $∣ F ∣ \leq M$ .

givenL1L2

2.1

If equality holds, then every member of $F$ lies on a rank whose binomial coefficient equals $M$ ; otherwise the first inequality in step 1.1 would be strict.

step 1.1L2

3.1

If $n$ is even, [L2] leaves only rank $n / 2$ . Thus $F \subseteq [A]^{n / 2}$ , and equality of cardinalities forces $F = [A]^{n / 2}$ .

step 2.1L2F1

3.2

Suppose $n = 2 k + 1$ is odd. Write $G : = F \cap [A]^{k}$ and $H : = F \cap [A]^{k + 1}$ . Since $F$ is an antichain, $H$ is disjoint from $\nabla G$ . The two middle levels both have cardinality $M$ , and [L3] gives $∣ \nabla G ∣ \geq ∣ G ∣$ . Therefore $∣ F ∣ = ∣ G ∣ + ∣ H ∣ \leq ∣ G ∣ + M - ∣ \nabla G ∣ \leq M$ .

step 2.1L2L3F1

4.1

Equality in step 3.2 forces $∣ \nabla G ∣ = ∣ G ∣$ and $H = [A]^{k + 1} ∖ \nabla G$ . By the equality clause of [L3], whenever $S \in G$ , $x \notin S$ , and $y \in S$ , the set $(S ∖ {y}) \cup {x}$ also lies in $G$ : it is a $k$ -subset of $S \cup {x} \in \nabla G$ .

step 3.2L3

5.1

Any two $k$ -subsets can be joined by repeatedly replacing an element not in the target by an element of the target not yet present. Thus the closure in step 4.1 implies that $G$ is either empty or all of $[A]^{k}$ . In the first case equality forces $H = [A]^{k + 1}$ ; in the second, $\nabla G = [A]^{k + 1}$ and equality forces $H = \emptyset$ .

step 4.1F1

6.1

Complete levels are antichains and the middle ones have cardinality $M$ . Steps 3.1 and 5.1 therefore give all equality cases and complete the proof.

step 3.1step 5.1F1∎

Depends on

Used by

The Boolean lattice on four elements: ranks, width, shadows, and a symmetric chain decomposition Example

Dependency tree · two levels

23 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

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