[proofplan]
We count maximal chains in the regular graded poset. Regularity forces every element at level $k$ to lie in the same number of maximal chains, namely $m(k) = \prod_{i=1}^{k} r_i \cdot \prod_{i=k}^{n-1} s_i$. Since every maximal chain passes through a unique element of each level, we obtain $M = |S_k| \cdot m(k)$, giving $m(k) = M / |S_k|$. The antichain property ensures each maximal chain contributes at most one element of $\mathcal{A}$, so summing the chain counts over $\mathcal{A}$ and dividing by $M$ yields $w(\mathcal{A}) \leq 1$.
[/proofplan]
[step:Compute the number of maximal chains through an element at level $k$]
Let $M$ denote the total number of maximal chains of length $n + 1$ in the poset $(S, <)$ with levels $S_0, S_1, \ldots, S_n$. For each $x \in S_k$, let $m(x)$ denote the number of maximal chains passing through $x$.
By regularity, every element of $S_i$ lies above exactly $r_i$ elements of $S_{i-1}$ and below exactly $s_i$ elements of $S_{i+1}$. A maximal chain through $x \in S_k$ consists of a chain from $S_0$ up to $x$ concatenated with a chain from $x$ up to $S_n$. The number of chains descending from $x$ to $S_0$ is $\prod_{i=1}^{k} r_i$: at each step from level $i$ to level $i - 1$, there are exactly $r_i$ choices. The number of chains ascending from $x$ to $S_n$ is $\prod_{i=k}^{n-1} s_i$: at each step from level $i$ to level $i + 1$, there are exactly $s_i$ choices. By independence of the descending and ascending portions:
\begin{align*}
m(x) = \prod_{i=1}^{k} r_i \cdot \prod_{i=k}^{n-1} s_i.
\end{align*}
This quantity depends only on the level $k$, not on the particular element $x \in S_k$.
[guided]
Why does regularity make $m(x)$ depend only on the level? Consider building a maximal chain through $x \in S_k$. Going downward from $x$: at level $k$, the element $x$ lies above exactly $r_k$ elements of $S_{k-1}$, so we choose one. From that chosen element at level $k - 1$, we have exactly $r_{k-1}$ elements below it at level $k - 2$, and so on. The regularity hypothesis guarantees that the branching factor at each level is the same regardless of which specific element we are at — every element of $S_i$ has exactly $r_i$ elements below it. So the total number of downward chains from level $k$ to level $0$ is $r_k \cdot r_{k-1} \cdots r_1 = \prod_{i=1}^{k} r_i$.
The same reasoning applies going upward: from $x$ at level $k$, there are $s_k$ elements above at level $k + 1$, then $s_{k+1}$ above each of those at level $k + 2$, and so on. The upward chain count is $s_k \cdot s_{k+1} \cdots s_{n-1} = \prod_{i=k}^{n-1} s_i$.
Since the downward path from $x$ to $S_0$ and the upward path from $x$ to $S_n$ are determined independently (they involve disjoint portions of the poset), the total count is the product $\prod_{i=1}^{k} r_i \cdot \prod_{i=k}^{n-1} s_i$.
Without regularity this argument fails: the number of chains through $x$ could depend on which specific element $x \in S_k$ we choose, and the level-uniform cancellation in the next step would not hold.
[/guided]
[/step]
[step:Express $M$ in terms of $|S_k|$ and $m(k)$]
Every maximal chain passes through exactly one element of each level $S_k$ (since the levels partition $S$ and consecutive elements of a maximal chain lie in consecutive levels). Summing the chain counts over all elements of $S_k$:
\begin{align*}
M = \sum_{x \in S_k} m(x) = |S_k| \cdot m(k),
\end{align*}
where $m(k) = \prod_{i=1}^{k} r_i \cdot \prod_{i=k}^{n-1} s_i$ is the common value of $m(x)$ for $x \in S_k$. Rearranging:
\begin{align*}
m(k) = \frac{M}{|S_k|}.
\end{align*}
[/step]
[step:Bound the weighted sum using the antichain property]
Since $\mathcal{A}$ is an antichain and each maximal chain is a chain, a maximal chain can contain at most one element of $\mathcal{A}$. Therefore the total number of (maximal chain, element of $\mathcal{A}$) incidences satisfies:
\begin{align*}
\sum_{x \in \mathcal{A}} m(x) \leq M.
\end{align*}
Substituting $m(x) = M / |S_k|$ for each $x \in \mathcal{A} \cap S_k$ and summing over all levels:
\begin{align*}
\sum_{k=0}^{n} |\mathcal{A} \cap S_k| \cdot \frac{M}{|S_k|} \leq M.
\end{align*}
Dividing both sides by $M > 0$:
\begin{align*}
\sum_{k=0}^{n} \frac{|\mathcal{A} \cap S_k|}{|S_k|} \leq 1.
\end{align*}
The left-hand side is $w(\mathcal{A})$, so $w(\mathcal{A}) \leq 1$.
[guided]
The logic mirrors the double-counting proof of the [LYM Inequality](/theorems/2586). There, we counted pairs $(\mathcal{C}, A)$ with $\mathcal{C}$ a maximal chain and $A \in \mathcal{A} \cap \mathcal{C}$. Summing over chains first: each chain meets the antichain $\mathcal{A}$ in at most one element, so the total is at most $M$. Summing over elements of $\mathcal{A}$ first: each $x \in \mathcal{A} \cap S_k$ contributes $m(x) = M / |S_k|$ pairs.
Combining:
\begin{align*}
M \geq \sum_{x \in \mathcal{A}} m(x) = \sum_{k=0}^{n} |\mathcal{A} \cap S_k| \cdot \frac{M}{|S_k|} = M \sum_{k=0}^{n} \frac{|\mathcal{A} \cap S_k|}{|S_k|} = M \cdot w(\mathcal{A}).
\end{align*}
Since $M > 0$ (the poset has at least one maximal chain), we divide to obtain $w(\mathcal{A}) \leq 1$.
The regularity hypothesis is used in a single but essential place: it guarantees that $m(x)$ depends only on the level of $x$, which allows us to factor $m(x)$ out of the sum over $\mathcal{A} \cap S_k$ and express the result in terms of the weight function. In a non-regular poset, elements at the same level could lie in different numbers of maximal chains, and this factoring would fail.
[/guided]
[/step]
[step:Deduce the antichain size bound]
Since $|S_k| \leq \max_i |S_i|$ for every $k$, we have $\frac{1}{|S_k|} \geq \frac{1}{\max_i |S_i|}$. Therefore:
\begin{align*}
\frac{|\mathcal{A}|}{\max_i |S_i|} = \sum_{k=0}^{n} \frac{|\mathcal{A} \cap S_k|}{\max_i |S_i|} \leq \sum_{k=0}^{n} \frac{|\mathcal{A} \cap S_k|}{|S_k|} = w(\mathcal{A}) \leq 1.
\end{align*}
Hence $|\mathcal{A}| \leq \max_i |S_i|$.
[/step]
