[proofplan] We induct on the span of the antichain $\mathcal{A}$ (the difference between its highest and lowest occupied levels). The base case — $\mathcal{A}$ contained in a single level — gives $w(\mathcal{A}) \leq 1$ immediately. For the inductive step, we replace the top-level portion $\mathcal{A} \cap S_h$ by its shadow $\partial(\mathcal{A} \cap S_h)$ at level $h - 1$. The downward-expanding property guarantees that this shadow replacement does not increase the weight, while the antichain property ensures the replacement is still an antichain with strictly smaller span. [/proofplan] [step:Establish the base case: antichains contained in a single level have weight at most $1$] If $\operatorname{span}(\mathcal{A}) = 0$, then $\mathcal{A} \subseteq S_i$ for some level $i$. Since $\mathcal{A}$ is a subset of $S_i$, we have $|\mathcal{A}| \leq |S_i|$, so \begin{align*} w(\mathcal{A}) = \frac{|\mathcal{A}|}{|S_i|} \leq 1. \end{align*} [/step] [step:Define the shadow replacement and verify it reduces span] Suppose $\operatorname{span}(\mathcal{A}) \geq 1$. Let $h = \max\{i : \mathcal{A} \cap S_i \neq \varnothing\}$ be the highest occupied level. Define \begin{align*} \mathcal{A}' = \bigl(\mathcal{A} \setminus (\mathcal{A} \cap S_h)\bigr) \cup \partial(\mathcal{A} \cap S_h), \end{align*} where $\partial(\mathcal{A} \cap S_h) \subseteq S_{h-1}$ is the shadow of the top-level portion. Since $\mathcal{A}'$ has no elements at level $h$ and may have new elements at level $h - 1$ (but no higher), we have $\operatorname{span}(\mathcal{A}') < \operatorname{span}(\mathcal{A})$. [guided] The idea is a "shadow replacement": we remove the elements of $\mathcal{A}$ at the top level $h$ and replace them with their shadow one level below. This strictly decreases the span because: - The set $\mathcal{A}'$ contains no elements of $S_h$ (we removed $\mathcal{A} \cap S_h$ and the shadow $\partial(\mathcal{A} \cap S_h)$ lies in $S_{h-1}$). - The set $\mathcal{A}'$ contains no elements above level $h$ (since $\mathcal{A}$ had none above $h$). - The lowest occupied level of $\mathcal{A}'$ is at most the lowest occupied level of $\mathcal{A}$ (removing top elements and adding elements at $h-1$ cannot raise the minimum). Therefore $\max\{i : \mathcal{A}' \cap S_i \neq \varnothing\} \leq h - 1$ while $\min\{i : \mathcal{A}' \cap S_i \neq \varnothing\} \leq \min\{i : \mathcal{A} \cap S_i \neq \varnothing\}$, giving $\operatorname{span}(\mathcal{A}') < \operatorname{span}(\mathcal{A})$. [/guided] [/step] [step:Verify that $\mathcal{A}'$ is an antichain] We must check that no two distinct elements of $\mathcal{A}'$ are comparable. The set $\mathcal{A}'$ consists of two parts: $\mathcal{A} \setminus (\mathcal{A} \cap S_h)$ (the elements of $\mathcal{A}$ below level $h$) and $\partial(\mathcal{A} \cap S_h)$ (the shadow at level $h - 1$). **Within $\mathcal{A} \setminus (\mathcal{A} \cap S_h)$:** These elements are all in $\mathcal{A}$, which is an antichain, so no two are comparable. **Within $\partial(\mathcal{A} \cap S_h)$:** All elements lie in the single level $S_{h-1}$. Since the levels of a graded poset are antichains, no two elements of $S_{h-1}$ are comparable. **Between the two parts:** Let $x \in \mathcal{A} \setminus (\mathcal{A} \cap S_h)$ and $y \in \partial(\mathcal{A} \cap S_h)$. Since $y \in \partial(\mathcal{A} \cap S_h)$, there exists $z \in \mathcal{A} \cap S_h$ with $y < z$. If $x \leq y$, then by transitivity $x \leq y < z$, so $x < z$, contradicting the fact that $x$ and $z$ are both in the antichain $\mathcal{A}$. If $y \leq x$, then $y \in S_{h-1}$ and $x \in S_j$ for some $j \leq h - 1$ (since $x \notin S_h$). In a graded poset, $y \leq x$ with $y \in S_{h-1}$ forces $x \in S_j$ with $j \geq h - 1$, so $j = h - 1$. But $S_{h-1}$ is an antichain, so $y \leq x$ with both in $S_{h-1}$ forces $y = x$, contradicting distinctness. Therefore $\mathcal{A}'$ is an antichain. [guided] The critical case is cross-comparability between old elements of $\mathcal{A}$ (below level $h$) and new shadow elements at level $h - 1$. Could some $x \in \mathcal{A}$ at level $j < h$ be comparable with some $y \in \partial(\mathcal{A} \cap S_h)$ at level $h - 1$? **Case $x < y$:** Since $y$ is in the shadow, there exists $z \in \mathcal{A} \cap S_h$ with $y < z$. Then $x < y < z$, giving $x < z$. But $x, z \in \mathcal{A}$ and $\mathcal{A}$ is an antichain — contradiction. **Case $y < x$:** We have $y \in S_{h-1}$ and $x \in S_j$ for some $j \leq h - 1$ (since $x$ is below level $h$). In a graded poset, $y < x$ means $y$ is at a strictly lower level than $x$, i.e., $h - 1 < j$. But $j \leq h - 1$, so this is impossible unless $y = x$, which contradicts distinctness. To confirm: could $y \leq x$ with both at level $h-1$? In a graded poset, elements at the same level are incomparable (each level is an antichain), so $y \leq x$ with both in $S_{h-1}$ forces $y = x$. And if $j < h - 1$, then $y < x$ would require $y$ at a level below $x$, i.e., $h - 1 < j$, contradicting $j < h - 1$. No new comparabilities are introduced, and $\mathcal{A}'$ is an antichain. [/guided] [/step] [step:Use the downward-expanding property to bound the weight change] The weight of $\mathcal{A}'$ relates to the weight of $\mathcal{A}$ as follows. At every level other than $h$ and $h - 1$, the two families agree. At level $h$, we removed $\mathcal{A} \cap S_h$, contributing $-|\mathcal{A} \cap S_h|/|S_h|$ to the weight change. At level $h - 1$, we added $\partial(\mathcal{A} \cap S_h)$ and the original $\mathcal{A} \cap S_{h-1}$ is still present. More precisely: \begin{align*} w(\mathcal{A}') &= w(\mathcal{A}) - \frac{|\mathcal{A} \cap S_h|}{|S_h|} + \frac{|\partial(\mathcal{A} \cap S_h)|}{|S_{h-1}|} - \frac{|(\mathcal{A} \cap S_{h-1}) \cap \partial(\mathcal{A} \cap S_h)|}{|S_{h-1}|}. \end{align*} Since $\mathcal{A}$ is an antichain and every element of $\partial(\mathcal{A} \cap S_h)$ is below some element of $\mathcal{A} \cap S_h$, no element of $\mathcal{A} \cap S_{h-1}$ can lie in $\partial(\mathcal{A} \cap S_h)$ (otherwise it would be comparable to an element of $\mathcal{A}$ at level $h$, contradicting the antichain property). So $(\mathcal{A} \cap S_{h-1}) \cap \partial(\mathcal{A} \cap S_h) = \varnothing$, and the expression simplifies to: \begin{align*} w(\mathcal{A}') = w(\mathcal{A}) - \frac{|\mathcal{A} \cap S_h|}{|S_h|} + \frac{|\partial(\mathcal{A} \cap S_h)|}{|S_{h-1}|}. \end{align*} Since $P$ is downward-expanding, applying the expansion condition to $\mathcal{A} \cap S_h \subseteq S_h$: \begin{align*} \frac{|\partial(\mathcal{A} \cap S_h)|}{|S_{h-1}|} \geq \frac{|\mathcal{A} \cap S_h|}{|S_h|}. \end{align*} Therefore: \begin{align*} w(\mathcal{A}') \geq w(\mathcal{A}). \end{align*} Equivalently, $w(\mathcal{A}) \leq w(\mathcal{A}')$. [guided] We need to track how the weight changes when we perform the shadow replacement. The weight function is additive over levels: \begin{align*} w(\mathcal{A}) = \sum_{i=0}^{n} \frac{|\mathcal{A} \cap S_i|}{|S_i|}. \end{align*} When forming $\mathcal{A}'$, the only levels that change are $h$ and $h - 1$: - At level $h$: $|\mathcal{A}' \cap S_h| = 0$ (we removed everything), whereas $|\mathcal{A} \cap S_h| > 0$. - At level $h - 1$: $|\mathcal{A}' \cap S_{h-1}| = |(\mathcal{A} \cap S_{h-1}) \cup \partial(\mathcal{A} \cap S_h)|$. A key point is that the union at level $h-1$ is disjoint. Why? If some $y$ were in both $\mathcal{A} \cap S_{h-1}$ and $\partial(\mathcal{A} \cap S_h)$, then $y \in \mathcal{A}$ and $y < z$ for some $z \in \mathcal{A} \cap S_h$, making $y$ and $z$ comparable — contradicting the antichain property of $\mathcal{A}$. With the disjointness established: \begin{align*} w(\mathcal{A}') &= w(\mathcal{A}) - \frac{|\mathcal{A} \cap S_h|}{|S_h|} + \frac{|\partial(\mathcal{A} \cap S_h)|}{|S_{h-1}|}. \end{align*} Now the downward-expanding hypothesis enters. It states that for any $\mathcal{B} \subseteq S_i$: \begin{align*} \frac{|\partial \mathcal{B}|}{|S_{i-1}|} \geq \frac{|\mathcal{B}|}{|S_i|}. \end{align*} Applying this with $\mathcal{B} = \mathcal{A} \cap S_h$ and $i = h$: \begin{align*} \frac{|\partial(\mathcal{A} \cap S_h)|}{|S_{h-1}|} \geq \frac{|\mathcal{A} \cap S_h|}{|S_h|}. \end{align*} This means the weight contributed by the new shadow elements at level $h - 1$ is at least as large as the weight we removed from level $h$. Therefore $w(\mathcal{A}') \geq w(\mathcal{A})$, or equivalently $w(\mathcal{A}) \leq w(\mathcal{A}')$. This is the heart of the proof: the expanding property ensures that pushing elements downward does not decrease the weight, so any upper bound on the weight of the simpler antichain $\mathcal{A}'$ applies to $\mathcal{A}$ as well. [/guided] [/step] [step:Complete the induction to conclude $w(\mathcal{A}) \leq 1$] Since $\mathcal{A}'$ is an antichain with $\operatorname{span}(\mathcal{A}') < \operatorname{span}(\mathcal{A})$, the induction hypothesis gives $w(\mathcal{A}') \leq 1$. Combined with $w(\mathcal{A}) \leq w(\mathcal{A}')$: \begin{align*} w(\mathcal{A}) \leq w(\mathcal{A}') \leq 1. \end{align*} This completes the induction. For the "in particular" statement: since $\frac{1}{|S_i|} \geq \frac{1}{\max_j |S_j|}$ for all $i$, we have \begin{align*} \frac{|\mathcal{A}|}{\max_i |S_i|} = \sum_{i=0}^{n} \frac{|\mathcal{A} \cap S_i|}{\max_j |S_j|} \leq \sum_{i=0}^{n} \frac{|\mathcal{A} \cap S_i|}{|S_i|} = w(\mathcal{A}) \leq 1, \end{align*} giving $|\mathcal{A}| \leq \max_i |S_i|$. [/step]