clos_root_of_descent
plain-language theorem explainer
On a finite vertex set, a unique-zero height function with a strict descent edge from every positive-height cell forces every vertex into the connectivity class of the root. Cosmologists and graph theorists working the locked-domain bound cite it to discharge ambient connectivity. The argument is strong induction on height, stepping down one edge and transporting along the equivalence closure.
Claim. Let $V$ be finite, $E$ a list of undirected edges on $V$, and $h:V\to\mathbb{N}$ a height with unique zero $\mathrm{root}$ (i.e. $h(v)=0\Rightarrow v=\mathrm{root}$). Suppose every $v$ with $h(v)\neq 0$ has a neighbour $u$ (edge in either orientation) with $h(u)<h(v)$. Then for every $v\in V$, $v$ lies in the equivalence closure of $E$ with $\mathrm{root}$.
background
The module proves a dimension-free bound on locked domains: on any finite connected world, the number of monochromatic components is at most the number of bichromatic (interface) edges plus one. Connectivity of the ambient graph is an input to the headline inequality and must be discharged for the lattices the cosmogenesis engine actually runs.
Here clos E is the least equivalence relation containing the edge relation generated by the list $E$: two vertices are related exactly when a path of edges joins them. The theorem clos_equiv records that this relation is an equivalence, so reflexivity, symmetry, and transitivity are available as e.refl, e.symm, e.trans.
The descent package is the recognition-law reading of connectivity: a height $h$ with unique zero (the root) and a strict step-down edge from every other cell. Concrete instances (diamond L1 ball, octahedron) take the L1 norm as height and the origin as root; sibling lemmas such as hzero and hdesc discharge those geometric hypotheses.
proof idea
Obtain the equivalence structure e := clos_equiv E. Prove the stronger claim that every vertex of height $n$ is connected to the root, by strong induction on $n$.
For fixed $n$ and $v$ with $h(v)=n$, split on whether $h(v)=0$. If zero, hzero forces $v=\mathrm{root}$, and reflexivity gives the link. If positive, hdesc supplies a neighbour $u$ of strictly smaller height; one edge (or its reverse via e.symm) yields clos E v u. The induction hypothesis at height $h(u)$ connects $u$ to the root; transitivity closes the path.
The original statement is the special case $n=h(v)$.
why it matters
This lemma is the root-reaching half of descent connectivity. Its sole consumer is connected_of_descent, which upgrades root-links to full pairwise connectivity: any two cells meet through the root, so the ambient world is one component.
That connectivity hypothesis is exactly what the headline bound mono_components_le_bichromatic_succ needs. Closing it here finishes the open connected-graph fact left numeric-only in the 2D/3D domain-coarsening scripts and their Lean bridges: locked-domain count $\le$ interface size $+1$ on any connected finite world.
In the Recognition reading, the height descent is the pull toward the coarsest description, rephrased as graph connectivity. Instantiations on the diamond and octahedron (L1 height, origin root) feed Diamond.mono_le_interface_succ and the 3D analogue, tying the interface-component bound to the engine's actual lattices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.