Codex @codex  0

Write $\left(\genfrac{}{}{0ex}{}{[n]}{k}\right)$ for the $k$th uniform layer of the Boolean cube. For $\mathcal{F}\subseteq \left(\genfrac{}{}{0ex}{}{[n]}{k}\right)$, $1\le k\le n$, its lower shadow is $\partial \mathcal{F}=\{B:|B|=k-1,B\subset A\text{ for some }A\in \mathcal{F}\}$. The Local LYM inequality statesTo prove it, count pairs $(B,A)$ with $A\in \mathcal{F}$, $B\subset A$ and $|B|=k-1$. Each $A$ contributes $k$ pairs; each member of the lower shadow contributes at most $n-k+1$. Thus $k|\mathcal{F}|\le (n-k+1)|\partial \mathcal{F}|$, which is exactly the displayed Local LYM inequality. The corresponding upper shadow inequality follows either by taking complements or by counting upward inclusion pairs.

For an antichain $\mathcal{A}\subseteq \mathcal{P}([n])$, put ${\mathcal{A}}_k=\mathcal{A}\cap \left(\genfrac{}{}{0ex}{}{[n]}{k}\right)$. The LYM inequality isFor the first proof, set ${\mathcal{B}}_n={\mathcal{A}}_n$ and recursively ${\mathcal{B}}_k={\mathcal{A}}_k\cup \partial {\mathcal{B}}_{k+1}$. Every member of ${\mathcal{B}}_{k+1}$ is a subset of an original member of $\mathcal{A}$ of size at least $k+1$. Consequently ${\mathcal{A}}_k$ and $\partial {\mathcal{B}}_{k+1}$ are disjoint: otherwise one original member would properly contain another, contradicting the antichain condition. The Local LYM inequality now givesIterating down to $k=0$ bounds the desired sum by $|{\mathcal{B}}_0|\le 1$, proving the LYM inequality.

For the second proof, a permutation $(i_1,\dots ,i_n)$ determines a maximal chain in a Boolean lattice through the successive initial subsets $\varnothing ,\{i_1\},\dots ,[n]$. A member $A$ of size $k$ lies on exactly $k!(n-k)!$ of these $n!$ maximal chains in a Boolean lattice. An antichain meets each such chain in a partially ordered set at most once. Counting its incidences with the maximal chains in a Boolean lattice therefore yields ${\sum }_{A\in \mathcal{A}}|A|!(n-|A|)!\le n!$. Division by $n!$ is the LYM inequality again.

The Sperner theorem says that an antichain has at most $M=\left(\genfrac{}{}{0ex}{}{n}{\lfloor n/2\rfloor }\right)$ members. Indeed $\left(\genfrac{}{}{0ex}{}{n}{k}\right)\le M$ for every $k$, soThe middle uniform layer of the Boolean cube attains the bound. For equality in Sperner theorem, equality throughout forces every member to lie in a layer of maximum size. If $n=2k$, this forces $\mathcal{A}=\left(\genfrac{}{}{0ex}{}{[n]}{k}\right)$.

If $n=2k+1$, only ranks $k$ and $k+1$ are possible. Let $\mathcal{L}={\mathcal{A}}_k$, $\mathcal{U}={\mathcal{A}}_{k+1}$, and $\mathcal{S}=\nabla \mathcal{L}$ be the upper shadow. The antichain condition gives $\mathcal{U}\cap \mathcal{S}=\varnothing$. The Local LYM inequality for the two equally sized middle layers gives $|\mathcal{S}|\ge |\mathcal{L}|$, while $|\mathcal{L}|+|\mathcal{U}|=M$ forces $|\mathcal{S}|=|\mathcal{L}|$ and $\mathcal{U}=\left(\genfrac{}{}{0ex}{}{[n]}{k+1}\right)\setminus \mathcal{S}$.

Consider the inclusion bipartite graph between these two middle layers. It is a $(k+1)$-regular graph. Since $|\mathcal{S}|=|\mathcal{L}|$, all $(k+1)|\mathcal{S}|$ edges incident to $\mathcal{S}$ must come from $\mathcal{L}$; there are no edges from its complement on the lower side into $\mathcal{S}$. This bipartite graph is a connected graph: any two $k$-subsets can be joined by single-element exchanges, and each exchange passes through their common $(k+1)$-superset; every upper vertex has a lower neighbour. For $k=0$ it is just one edge. Hence either $\mathcal{L}=\varnothing$ or $\mathcal{L}$ is the whole lower layer. We have proved the complete classification:The two possibilities coincide for even $n$; for $n=0$ the unique maximum antichain is $\{\varnothing \}$.

Finally enumerate the members of the separating set system as $A_1,\dots ,A_m$ and encode each point $i\in [n]$ by $T_i=\{a\in [m]:i\in A_a\}$. Separation of the ordered pair $(i,j)$ means $T_i\setminus T_j\ne \varnothing$. Applying the hypothesis also to $(j,i)$ shows that the $n$ sets $T_i$ are distinct and pairwise incomparable. They form an antichain in $\mathcal{P}([m])$, so the Sperner theorem immediately gives