The terminology "$n$-cell" is made up by me, and I'd love to hear if this has an official name.
Given a poset $(X,\le)$, define the set $A_n$ of $n$-cells of $X$ recursively as follows:
- An element is a $0$-cell iff it is the bottom element: $x\in A_0\iff\forall y,x\le y$.
- An element is an $n+1$-cell iff it covers some $n$-cell: $x\in A_{n+1}\iff\exists y\in A_n,y<:x$.
(Recall that $x<:y$, read "$x$ covers $y$", if $x<y$ and $\lnot\exists z:x<z<y$.) Note that a $1$-cell is the same thing as an atom, so this is a generalization to "higher-dimensional atoms".
One curious property of the Hilbert lattice, or any other vector subspace lattice for that matter, is that $A_n$ is an antichain for each $n$ (because $A_n$ is the set of subspaces of dimension $n$). On the other hand, this is not always the case for an arbitrary lattice. For example, in the pentagon lattice $N_5$ with atoms $a,x$ and coatoms $a,b$, we have $A_2=\{b,1\}$ which is not an antichain since $b\le 1$.
Does this property (which I will call "cell-graded" for lack of a better term) follow from the assumption that the lattice is modular?
Edit: I've now beat myself over the head with several failed classification theorems for modular lattices in attempt to prove that a modular lattice is cell-graded, with no luck. However, these attempts and the counterexamples that are generated halfway during the "proof" have only made me more sure that I was correct with my original claim:
Claim: The $n$-cells of a modular lattice are antichains.
(This answer has been cleaned up from the earlier stream-of-consciousness style now that the proof is complete, see the revision log.)
Edit: Amazingly, it turns out that these theorems, up to and including the main theorem in the OP, can be generalized still further, from modular lattices to weakly semimodular lattices.
A lattice is said to be a Birkhoff lattice or weakly semimodular lattice if $a:>a\land b<:b$ implies $a<:a\lor b:>b$. (In other words, both sides of the diamond must be covering before it can be "pushed up".) By contrast, an upper semimodular lattice satisfies $a\land b<:b\to a<:a\lor b$ (only one side is needed to push the relation up), and a modular lattice has isomorphisms between $[a\land b,b]$ and $[a,a\lor b]$, so the arrow goes in both directions.
Let $a<:^nb$ denote that there is a covering sequence of length $n$ from $a$ to $b$. Obvious properties of this relation include:
The Birkhoff law also generalizes to weak covering $a\le:b$ (which means $a<:b$ or $a=b$): if $a:\ge c\le:b$, then $a\le:a\lor b:\ge b$. Furthermore, by an induction in first $m$ then $n$, we have that if $a:>^mc<:^nb$, then $a<:^ia\lor b:>^jb$ for some $i\le m$, $j\le n$.
Proof: By induction. If $n=0$, then $a=b$ is the only possible chain. Suppose it is true for chains of length $<n$, and $a<:^nb$ and $a<:^mb$. We must have $m>0$ because $n>0$ iff $a<b$ iff $m>0$, so separate off the first elements as $a<:x<:^{n-1}b$ and $a<:y<:^{m-1}b$. If $x=y$, then the induction hypothesis implies that $n-1=m-1$, so we are done. Otherwise, $x\land y=a$, so the Birkhoff law implies that $x<:x\lor y:>y$. The Birkhoff law also implies that $x\lor y<:^kb\lor y=b$ for some $k\le n-1$. Then $x<:^{n-1}b$ and $x<:^{k+1}b$, and $y<:^{m-1}b$ and $y<:^{k+1}b$, so $n-1=k+1=m-1$ by the induction hypothesis. $$\tag*{$\blacksquare$}$$
This generalizes a bit:
The Birkhoff law gives $b=a\lor b<:^kc\lor b=c$ for some $k\le n$, so $a<:^{m+k}c$. Then Theorem 1 gives $m+k=n$, so $m\le n$ and $b<:^{n-m}c$.
With this result in hand, the original question is simple:
Suppose $a<:^n b$, $a<:^n c$, and $b\le c$. Then the corollary gives $b<:^{n-n}c$, so $b=c$. $$\tag*{$\blacksquare$}$$
All of the results that hold for $A_n$ also hold for the more general $\{x\mid a<:^nx\}$, which is simply a matter of looking at $A_n$ within the sublattice $[a,\infty)$. In particular, $\bigcup_n A_n$ is downward closed, and there is at least one covering sequence of the appropriate length between comparable elements. It is also closed under joins, because if $a\in A_m$ and $b\in A_n$, then $a<:^ka\lor b$ for some $k\le n$, hence $a\lor b\in A_i$ for some $i=m+k\le m+n$. Thus $\bigcup_n A_n$ is an ideal and a sublattice.
We can also prove that $\bigcup_n A_n$ has no bounded infinite chains, using theorem 2. Suppose that there is an infinite chain $C$ in $\bigcup_n A_n$ with a top element $a\in A_n$. Then $C\cap A_i$ must be infinite for some $i$ (because the union up to $i=n$ gives $C$), so in particular there is an $A_i$ that is not an antichain.