clos_someRoot_of_descent
plain-language theorem explainer
On a finite vertex set, if a natural-valued height vanishes only on a listed root set and every positive-height vertex has an undirected edge to a strictly lower vertex, then every vertex is path-connected to some root. Cosmology proofs cite it to bound monochromatic components by the number of roots. The argument is strong induction on height, using that connectivity closure is an equivalence.
Claim. Let $V$ be finite, $E$ a list of undirected edges on $V$, $h:V\to\mathbb{N}$, and $\mathrm{roots}$ a list of vertices. Suppose $h(v)=0$ implies $v\in\mathrm{roots}$, and whenever $h(v)\neq 0$ there is a neighbor $u$ (edge either way) with $h(u)<h(v)$. Then for every $v\in V$ there exists $r\in\mathrm{roots}$ such that $v$ and $r$ lie in the same connected component of $E$.
background
This module treats the forced conjugate-birth (polarized) charge on the diamond/octahedron lattice ball: $+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 field is carried as $O(1)$ locked monochromatic regions independent of radius, so components over volume tends to zero.
Connectivity is the equivalence closure clos E of the edge relation: the least equivalence containing the generators of $E$, so two vertices are related iff a path joins them. Phase 48 already used single-root descent on a height function; here the same idea is stated for a finite list of roots, matching the three charge levels of the polarized field.
The local height on the diamond is essentially $(|x|-[x\neq 0])+|y|$ (plus $|z|$ in 3D). It vanishes only at the three roots $(1,0)$, $(-1,0)$, $(0,0)$ (for $t\ge 1$), and monochromatic edges step toward the root of each charge class.
proof idea
Fix the equivalence package clos_equiv E (reflexivity, symmetry, transitivity of path-connectivity). Prove by strong induction on $n$ that every vertex of height $n$ reaches some root.
Base: if $h(v)=0$, the zero-height hypothesis puts $v$ in roots, and reflexivity gives the connection. Inductive step: if $h(v)>0$, the descent hypothesis supplies a neighbor $u$ with $h(u)<h(v)$; the edge (either orientation) yields a one-step clos link, the IH connects $u$ to a root $r$, and transitivity connects $v$ to $r$.
Instantiate at $n=h(v)$ to finish. No lattice geometry is used; only finiteness of $V$ (for the ambient type) and the two height axioms.
why it matters
This is the multi-root descent lemma that turns the polarized height into a component bound. Downstream, polarized_components_le_three applies it to the monochromatic edge list of the birth field with the three roots and the polarized height, then feeds the covering into comp_le_of_roots to conclude at most three locked domains for every radius $t\ge 1$.
In the module narrative this is the exact, non-numeric form of "carry each region at the coarsest $\varphi$-rung its recognition allows" for the shell-birth configuration: a $\Theta(t^d)$ world is carried as three super-regions. It generalizes the single-root descent of Phase 48 (InterfaceComponentBound) so the three charge levels (fine, coarse, spine) can each keep their own root.
Scope honesty from the module: live diffusion later splits the spine and creates small interface components bounded by Phase 48, not by this lemma. The $O(1)$ claim here is only for the forced birth field itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.