Olympiad problem similar to Sperner's theorem, inspired by OMM 2 ( unproven conjecture of mine) This problem is inspired by problem 2 here.
Consider a set of cubes $F$, such that each corner $(x,y)$ of any given cube of $F$ satisfies $0\leq x,y \leq n$, and each cube has a corner with coordinates $(0,0)$.
What is the maximum number of cubes in $F$ so that no cube of $F$ contains another cube of $F$?
So far I have managed to prove the number is less than $3(n-1)^2+3(n-1)+1$. Since each cube is determined by a triple $(x,y,z)$ and we can split the triples into the equivalence classes given by $(x,y,z)\sim (x+k,y+k,z+k)$. The number of these equivalence classes can be readily counted by noting each has a unique representative triple with at least one coordinate equal to zero.
I conjecture that $F$ can be no larger than the set consisting of all cubes which are represented by triples with sum of coordinates $\lfloor\frac{3n}{2}\rfloor$.
 A: For every $n,k,i\in \mathbb Z$ with $0\leq i\leq nk$ and $n,k>0$ let $F_{n,k,i}$ be the set of all $k$ tuples with elements in $[n]$ and sum $i$.
For every $i<nk$ consider the bipartite graph with vertex sets $F_{n,k,i}$ and $F_{n,k,i+1}$ where $a\in F_{n,k,i}$ is adjacent to $b\in F_{n,k,i+1}$ if $a\leq b$ in each coordinate.
We show that if $i < \frac{nk}{2}$ there is a matching of this graph that saturates $F_{n,k,i}$ (and by symmetry if $i\geq \frac{nk}{2}$ there is a matching that saturates $F_{n,k,i+1}$.
Proof: Proceed by induction on $n$. We will make sure that if two tuples are matched then the coordinates in which they are equal to $n$ coincide (it is not hard that we can then satisfy this by extracting one matching with maximum possible element $n-1$ for each possible subset of coordinates which must be $n$). To make the previous more clear: For every subset $A$ of size $a$ of the $k$ coordinates we must match the subsets in $F_{n,k,i}$ for which those coordinates are $n$ with the ones in $F_{n,k,i+1}$ for which those coordinates are $n$, but that is the same as matching $F_{n-1,k-a,i-an}$ with $F_{n-1,k-a,i-an+1}$, which can be done by the inductive hypothesis.

We can now use the previous lemma to partition the graph in which the vertex set is $\bigcup\limits_{i=1}^{kn} F_{n,k,i}$ and $(x,y,z)\sim (a,b,c)$ if $|x-a| + |y-b| + |z-c|=1$ into a family of paths such that each path contains exactly one vertex of $F_{n,k,\lfloor\frac{nk}{2}\rfloor}$. To do this just take the edges that exist in the matchings, and consider the maximal paths in this graph.
If we are given an antichain in the original partial order then it follows there can be at most one vertex in each path, so the size of the antichain is at most equal to the number of vertices in $F_{n,k,\lfloor \frac{nk}{2} \rfloor}$
