hzero
plain-language theorem explainer
On the 2D diamond of radius t≥1, polarized height zero forces the cell to be one of the three birth roots (1,0), (−1,0), (0,0). Anyone proving multi-root monochromatic descent or the O(1) locked-domain bound for the conjugate-birth field cites this. The proof is a short case split on the first coordinate, discharging the height formula by omega.
Claim. Fix $t\ge 1$. For every diamond vertex $v$ in the $\ell_1$-ball of radius $t$, if the polarized height $h(v)=(|x|-[x\ne 0])+|y|$ vanishes, then $v$ is one of the three roots $(1,0)$, $(-1,0)$, $(0,0)$.
background
The module studies the forced conjugate-birth (polarized) charge field on the 2D diamond: $+1$ on the fine half $x>0$, $-1$ on the coarse half $x<0$, and $0$ on the spine $x=0$. Vertices Vtx t are lattice points in the $\ell_1$-ball of radius $t$.
The polarized height is $h(v)=(|x|-[x\ne 0])+|y|$. Unlike the ordinary L1 height of InterfaceComponentBound (which vanishes only at the centre), this height is engineered to vanish exactly at the three charge-level roots $(1,0)$, $(-1,0)$, $(0,0)$, and to decrease along monochromatic steps toward the root of the cell's own charge.
Upstream, InterfaceComponentBound.hzero is the single-root analogue: zero ordinary height implies the centre. Here the same role is played for a finite root list, feeding the multi-root descent lemmas that bound locked domains.
proof idea
Unpack $v=\langle x,y\rangle$ and the definition of polarized height at the hypothesis $h(v)=0$. Case on $x=0$.
- If $x=0$, the height formula collapses to $|y|=0$, so $y=0$; the point $(0,0)$ is in the root list by definition.
- If $x\ne 0$, the formula forces $|x|=1$ and $y=0$. Then $x=\pm 1$ by the integer absolute-value dichotomy, and both $(\pm 1,0)$ sit in the root list.
All arithmetic steps are discharged by omega after simplifying the conditional in the height definition. No external lemmas beyond the local definitions of height and roots.
why it matters
This is the zero-set half of the multi-root descent package for the birth field. Together with the monochromatic step-down lemma, it discharges the hypotheses of clos_someRoot_of_descent / the multi-root form of clos_root_of_descent: every cell connects to one of the three roots. comp_le_of_roots then yields at most three locked domains, independent of radius.
That bound is the module's North-Star claim: a world of $\Theta(t^2)$ cells is carried as $O(1)$ monochromatic super-regions (fine half, coarse half, spine), so the carried-state fraction tends to zero. It makes exact, for the forced conjugate-birth configuration, the Recognition slogan "carry each region at the coarsest $\varphi$-rung its recognition allows." Downstream consumers include polarized_components_le_three and the graded-rung identity that total cost equals interface cost (bulk contributes nothing).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.