Proposition: Joint spectral Gram

For the joint spectral projection ${\Pi }_{m,\lambda }$, where $\lambda =-m,-m+2,\dots ,m$,

Every projected-code rank is $r_m$.

Proof. For a fixed occupied-pair set, each exchange has eigenvalues $\pm 1$; the all-boundary state has overlap squared $1/2$ with each. The sum has the binomial law. Different pair sets are orthogonal and invariant. Every allowed binomial weight is positive.