connected_of_descent
plain-language theorem explainer
On a finite vertex set, a height function with a unique zero and a strict descent edge from every other cell forces the undirected edge graph to be connected: every pair of cells lies in one equivalence class of the path closure. Cosmology proofs cite it to discharge the ambient-connectivity hypothesis of the locked-domain bound. The argument is a three-line transitivity through the root after the single-root connectivity lemma.
Claim. Let $V$ be finite, $E$ a list of undirected edges on $V$, $h:V\to\mathbb{N}$, and $\mathrm{root}\in V$. Suppose $h(v)=0$ implies $v=\mathrm{root}$, and every $v$ with $h(v)\neq 0$ has a neighbour $u$ (edge in either orientation) with $h(u)<h(v)$. Then for all $u,v\in V$, $u$ and $v$ are related by the equivalence closure of the edge relation: the whole world is a single connected component.
background
The module proves the dimension-free interface bound: on any finite world, the number of locked (monochromatic) domains is at most the number of bichromatic interface edges plus one. Component count is the cardinality of the quotient by the equivalence closure of monochromatic edges. The headline needs the ambient graph to be connected; this theorem supplies a reusable criterion for that hypothesis.
Connectivity is packaged as clos E, the least equivalence relation containing the generating edge relation of the list $E$ (two vertices related iff a path joins them). Its equivalence property is clos_equiv. The key upstream lemma is clos_root_of_descent: under the same unique-zero and strict-descent hypotheses, every cell is path-connected to the root, by strong induction on height (zero cells are the root; positive cells step down an edge to a lower cell already linked to the root).
In the lattice instantiations, $E$ is the neighbour list of the L1 ball (diamond in 2D, octahedron in 3D), $h$ is L1 distance to the origin, and the root is the centre. Those facts are discharged separately by height, hzero, and descent.
proof idea
Short term-mode argument. Obtain the equivalence instance e := clos_equiv E. For arbitrary $u,v$, apply clos_root_of_descent to get clos E u root and clos E v root. Transitivity of e with symmetry on the second leg yields clos E u v. No induction is redone here; all inductive work lives in the root-connectivity lemma.
why it matters
This is the reusable connectivity criterion that closes the open connected-graph obligation left by the domain-coarsening scripts and their Lean bridges. Downstream, mono_le_interface_of_descent packages it with the headline: any finite world admitting such a height satisfies locked domains $\le$ interface $+1$. That form is what the diamond and octahedron instantiate (L1 height, centre as unique zero), feeding Diamond.mono_le_interface_succ and the 3D analogue.
In Recognition terms the descent height is the recognition law's pull toward the coarsest description, read as graph connectivity: every off-centre cell has an edge toward lower cost, so the ambient lattice is one component and the interface-plus-one bound applies. The module status is fully proved (zero sorry); this lemma is the bridge from lattice geometry to the component-count inequality used in cosmogenesis domain accounting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.