three_le_comp_of_three_charges
plain-language theorem explainer
Three cells with pairwise-distinct charges force at least three monochromatic locked domains: charge is constant on connectivity classes, so the induced map on the quotient hits three values. Cosmologists proving exact component counts for the polarized birth field cite this as the lower bound. The proof is a short card-chain through the charge lift on the monochromatic quotient.
Claim. Let $E$ be a finite edge list on vertex set $V$, and let $c : V \to \beta$ be a charge assignment. If $a,b,d \in V$ satisfy $c(a) \neq c(b)$, $c(a) \neq c(d)$, and $c(b) \neq c(d)$, then the number of connected components of the monochromatic subgraph (edges of $E$ with equal endpoint charges) is at least $3$.
background
This module studies the forced conjugate-birth (polarized) charge field on lattice balls: $+1$ on the fine half $x>0$, $-1$ on the coarse half $x<0$, and $0$ on the spine $x=0$. The North-Star claim is that this birth configuration is carried at $O(1)$ cost: the locked-domain count stays bounded while volume grows as $\Theta(t^d)$.
From InterfaceComponentBound, comp E is the number of locked domains, defined as $\mathrm{Nat.card}$ of the quotient by the connectivity closure cs E of the edge list. Filtering $E$ to edges whose endpoints share a charge yields the monochromatic graph whose components are the locked domains of a charge field.
The sibling lemma clos_mono_charge records that charge is a closure invariant: if two vertices are connected by a monochromatic path, they carry the same charge. That fact lets charge descend to a well-defined map on the monochromatic quotient.
proof idea
Work classically. Let $F$ be the monochromatic filter of $E$. Charge $c$ lifts along clos_mono_charge to a map $q$ from the quotient of cs F into $\beta$. The three vertices $a,b,d$ give three quotient classes whose $q$-images are exactly $c(a),c(b),c(d)$.
The three-element finset ${c(a),c(b),c(d)}$ therefore sits inside the image of $q$ on the whole quotient (pairwise distinctness gives card $3$). Card monotonicity and the image bound yield
$$3 = |{c(a),c(b),c(d)}| \le |\mathrm{im}, q| \le |\mathrm{Quotient}(\mathrm{cs}, F)| = \mathrm{comp}, F.$$
The last step is the definition of comp via Nat.card equals Fintype.card.
why it matters
This is the lower-bound half of the exact count for the polarized birth field. Downstream, polarized_components_eq_three antisymmetrizes it against polarized_components_le_three (descent to the three roots $(1,0)$, $(-1,0)$, $(0,0)$) to conclude that the monochromatic component count equals $3$ for every radius $t \ge 1$ in 2-D.
In the module's language, the fine half, coarse half, and spine are three distinct locked domains and cannot collapse further because they carry distinct charges. That pins the carried-state fraction $\mathrm{components}/\mathrm{volume} \to 0$ at the sharpest possible constant $3$, making the North-Star "carry each region at the coarsest $\varphi$-rung its recognition allows" exact for the birth configuration installed each cadence cycle.
It does not address post-birth spine diffusion (bounded separately by the Phase-48 interface bound).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.