roots
plain-language theorem explainer
For diamond radius $t\ge 1$, the three roots are the lattice cells $(1,0)$, $(-1,0)$, and $(0,0)$. Cosmology proofs that bound polarized locked domains by three cite this list as the finite root set. The body is a three-element list with ball-membership discharged by the L1 ball criterion and omega.
Claim. For every natural number $t\ge 1$, the roots of the polarized diamond of radius $t$ are the three vertices $(1,0)$, $(-1,0)$, and $(0,0)$ of the L1 ball $\{(x,y)\in\mathbb{Z}^2:|x|+|y|\le t\}$.
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$. Phase 48 bounded locked domains by interface size for arbitrary charges; here the goal is sharper: for this birth field the monochromatic component count is at most 3, independent of radius.
Vertices Vtx t are lattice points in the diamond ball of radius $t$, i.e. pairs $(x,y)$ with $|x|+|y|\le t$ (via mem_ball_iff). The ordinary L1 height is $|x|+|y|$. The polarized descent height used downstream is $(|x|-[x\ne 0])+|y|$, which is designed to vanish exactly at the three cells listed here.
The proof strategy generalizes single-root descent: if height vanishes only on a finite root list and every positive-height cell steps down a monochromatic edge, then every cell connects to some root, so the component count is at most the length of that list.
proof idea
Pure definitional construction. The list is the three subtype values $(1,0)$, $(-1,0)$, $(0,0)$ in Vtx t. Each membership proof rewrites with mem_ball_iff (L1 ball criterion $|x|+|y|\le t$) and closes by omega under the hypothesis $t\ge 1$, which is exactly what puts the $\pm 1$ halves inside the ball.
why it matters
This list is the finite root set that makes the North-Star claim "carry each region at the coarsest rung" exact for birth: three monochromatic super-regions (fine half, coarse half, spine) cover a world of $\Theta(t^2)$ cells, so components/volume $\to 0$.
Downstream, hzero proves the polarized height vanishes only on these roots; hdesc and Fmono supply monochromatic descent; clos_someRoot_of_descent then connects every cell to some root; comp_le_of_roots yields components $\le 3$, feeding polarized_components_le_three. The same root set is reused in BIT-kernel shape forcing arguments that need the birth configuration's O(1) carried state.
Honest scope from the module: this is the birth field only. Live diffusion of the spine creates extra interface components bounded by Phase 48, not counted here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.