The antichain trace conjecture

Let $[n]=\{1,2,\ldots,n\}$, let $2^{[n]}$ be its powerset, and for a family $\mathcal{F}\subset 2^{[n]}$ and $Y\subset[n]$ write $\mathcal{F}_{\mid Y}=\{F\cap Y:F\in\mathcal{F}\}$. An antichain is a family in which no distinct members contain one another. The notation $\mathcal{F}\not\rightarrow(k+1,2^{k+1})$ means that no $(k+1)$-element subset $Y\subset[n]$ has $|\mathcal{F}_{\mid Y}|\geq 2^{k+1}$.

The antichain trace conjecture. Let $k$ be a non-negative integer and let $n\geq 2k$. If $\mathcal{F}\subset 2^{[n]}$ is an antichain satisfying $\mathcal{F}\not\rightarrow(k+1,2^{k+1})$, then

$$|\mathcal{F}|\leq \binom{n}{k}.$$

This is presented as an old conjecture. The surrounding results relate trace conditions for down-sets to forbidden complete uniform hypergraphs, but do not resolve this antichain bound.