N=2 integer steps live below level 3

At $N=2$, every integer entropy step lives below level $3$. The length field $L \cdot 2^{lower-1} = 2$ is unsatisfiable for $lower \ge 3$, so only levels $0$, $1$ and $2$ (with $L = 2$, $2$ and $1$) can occur. This pins all $N=2$ step data, including the level-two case used by the regional construction, to finitely many levels. Formalization Note Lean states the bound over an arbitrary step with a trivial predicate.