When Sharp Layer Bounds Cannot Coexist: Exact Antichain Saturation via Symbolic Search

Can separately optimal layers be assembled into a minimum saturated set family? Exact search exposes an obstruction in a published tightness question for antichain saturation. We prove that, for every integer $r\ge3$ and $r+1\le h\le2r-1$, the minimum size of a $\bigl(\binom{2r}{r}-h+1\bigr)$-antichain-saturated family on $2r$ points is $2^{2r}-h-1$, exactly one above the existing recursive lower bound. This resolves $r-1$ near-central values at each even boundary, and we classify all minimum families. The discovery proceeds from exact matching checks and symmetry-reduced enumeration to a symbolic incompatibility proof. Explicit chain covers and saturation witnesses make the finite constructions independently checkable. The result illustrates how failed assembly of sharp local bounds can guide computational mathematical discovery.