polarized_components_eq_three
plain-language theorem explainer
On the 2-D L1 diamond of any radius t≥1, the polarized birth charge field (+1 / −1 / 0) has exactly three monochromatic locked domains: fine half, coarse half, and spine. Sub-extensivity theorems cite this to pin the carried state at 3 while the world is Θ(t²). The proof is antisymmetry of the descent upper bound ≤3 and the three-charge lower bound ≥3 at the roots (1,0), (−1,0), (0,0).
Claim. For every integer radius $t \ge 1$, the number of connected components of the monochromatic adjacency graph of the polarized charge field on the 2-D diamond $\{(x,y)\in\mathbb{Z}^2 : |x|+|y|\le t\}$ equals exactly $3$.
background
The module studies the forced conjugate-birth (polarized) field on the 2-D diamond: charge $+1$ on the fine half $x>0$, $-1$ on the coarse half $x<0$, and $0$ on the spine $x=0$. The diamond itself is the L1 ball of radius $t$ (Phase 48/49 geometry). Monochromatic edges are adjacent same-charge pairs; their connected components are the locked domains that must be carried as super-regions.
Phase 48 (InterfaceComponentBound) already bounds components by interface size plus one for arbitrary charge fields. Here the charge field is fixed to the birth configuration, so a sharper count is available. A height function $(|x|-[x\ne 0])+|y|$ vanishes exactly at the three roots $(1,0)$, $(-1,0)$, $(0,0)$ and descends along monochromatic steps within each charge class. Descent toward a finite root list implies every cell meets one root, hence at most three components; the three distinct root charges give the matching lower bound.
The North-Star slogan is that each region is carried at the coarsest rung its recognition allows. Exact component count $3$, independent of $t$, is the sharpest form of that claim for the birth field.
proof idea
Term-mode antisymmetry. The upper bound is the sibling polarized_components_le_three (descent of the polarized height to the three roots, via clos_someRoot_of_descent and comp_le_of_roots). The lower bound is three_le_comp_of_three_charges applied to the full edge list and the polarized charge map, with explicit witnesses $(1,0)$, $(-1,0)$, $(0,0)$ shown to lie in the ball (by the L1 membership criterion and omega) and to carry charges $+1$, $-1$, $0$ respectively (decide on the polarized definition). Charge is a closure invariant, so three distinct root charges force at least three components. le_antisymm glues the two sides to equality.
why it matters
This is the exact-count half of Phase-50 carried-state sub-extensivity. Downstream, polarized_carried_subextensive packages it with the volume inequality $3t\le\mathrm{card}(\mathrm{ball},t)$ (using the Phase-49 closed form $2t^2+2t+1$), so the carried cost is $O(1)$ while the world is $\Theta(t^2)$. The Phase-51 capstone birth_field_subextensive further pairs the count with spine-incident interface support, making both the domain fraction and the interface support vanish relative to area.
In the Recognition framework this is the birth configuration the shell installs each cadence cycle: three locked domains (fine, coarse, spine) rather than a proliferating interface. It is the sharpest possible sub-extensivity for that field, stated as a theorem with no sorry. Honest scope (module doc): the live engine later diffuses the spine and creates small interface components bounded by Phase 48, not counted here; the $O(1)$ claim is exact for the forced conjugate birth only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.