mono_le_interface_of_descent
plain-language theorem explainer
Any finite graph that admits a height function with a unique zero and a strict descent edge from every other vertex has monochromatic component count at most the number of bichromatic edges plus one. Cosmologists and lattice-engine auditors cite it to discharge connectivity before applying the interface bound. The proof is a one-line composition of the headline merge bound with the descent-connectivity lemma.
Claim. Let $V$ be a finite nonempty vertex set, $E$ a list of undirected edges on $V$, $c:V\to\beta$ a charge colouring, and $h:V\to\mathbb{N}$ a height with unique root $r$ (so $h(v)=0$ forces $v=r$) such that every non-root vertex has a neighbour of strictly smaller height. Then the number of connected components of the monochromatic subgraph is at most the number of bichromatic edges plus one: $\mathrm{comp}(E_{\mathrm{mono}})\le |E_{\mathrm{bi}}|+1$.
background
The module proves a dimension-free bound on locked domains: on any connected finite world, monochromatic components (same-charge super-regions the cosmogenesis engine tracks) are at most the bichromatic interface size plus one. In 1D this is the identity runs = boundaries + 1; in higher D the interface may be multiply connected, so equality weakens to inequality.
Component count comp E is Nat.card of the quotient by the equivalence closure of the edge relation, well-defined for any finite $V$ without decidability of the closure. The monochromatic filter keeps edges with equal charge; the bichromatic filter is the recognition-active interface.
The headline mono_components_le_bichromatic_succ already gives the bound under an explicit connectivity hypothesis. Descent connectivity supplies that hypothesis: a height with unique zero and a descent edge from every other cell forces the whole world into one component (every cell reaches the root).
proof idea
One-line term proof. Apply mono_components_le_bichromatic_succ to the edge list $E$ and charge $c$, discharging the connectivity hypothesis by connected_of_descent E h root hzero hdesc. That lemma shows every pair of vertices is related by the equivalence closure of $E$, using the unique-zero and strict-descent assumptions to route every cell to the root. No further algebraic work is done here.
why it matters
This is the reusable bridge from abstract descent to the interface bound, so concrete lattices need only exhibit a height and check two local properties. Downstream, Diamond.mono_le_interface_succ instantiates it on the 2D L1 ball (4-neighbour diamond) with L1 norm as height and the origin as root, obtaining the bound for every radius on the exact lattice the 2D engine runs on. The same pattern covers the 3D octahedron.
In the Recognition framework this closes the connected-graph fact left open in the domain-coarsening scripts and their Lean bridges: the locked-domain count the engine carries is controlled by forced distinctions (the interface) plus one. The descent criterion itself is the recognition law's pull toward the coarsest description, read as graph connectivity. It is dimension-free and needs no Mathlib component-counting library beyond what the module builds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.