comp_le_comp_cons
plain-language theorem explainer
Adding a single undirected edge to a finite graph lowers the number of connected components by at most one. Cosmology and graph-theory arguments that bound locked-domain counts by interface size cite this atomic merge step. The proof builds a quotient map that is injective away from one class and applies the general cardinality-of-merge lemma.
Claim. Let $V$ be a finite vertex type and $X$ a list of edges on $V$. For any vertices $a,b\in V$, if $\mathrm{comp}(E)$ denotes the number of connected components of the undirected graph with edge list $E$ (cardinality of the quotient by the equivalence closure of the edge relation), then $\mathrm{comp}(X)\le \mathrm{comp}((a,b)::X)+1$.
background
The module proves a dimension-free bound used in Recognition cosmology: on any finite connected world, the number of monochromatic locked domains is at most the number of bichromatic interface edges plus one. A finite world is a finite type $V$; an edge list $E:\mathrm{List}(V\times V)$ is the ambient adjacency. Component count is $\mathrm{Nat.card}$ of the quotient by the equivalence closure of the generating edge relation, so no decidability of path-connectivity is required.
Connectivity closure $\mathrm{clos}(E)$ is the least equivalence containing the edge generators. The local component count $\mathrm{comp}(E)$ is the cardinality of that quotient. The companion lemma $\mathrm{clos_cons_iff}$ states that adjoining one edge $(a,b)$ exactly merges the $a$-class with the $b$-class in the old closure. The cardinality engine is $\mathrm{card_le_succ_of_merge}$: any map that is injective except possibly into a single distinguished class loses at most one element of cardinality.
This atomic inequality is the inductive step that turns one-edge merges into a bound linear in interface length.
proof idea
Construct the natural projection from the old quotient $\mathrm{Quotient}(\mathrm{cs},X)$ induced by adjoining $(a,b)$. Prove the merge hypothesis: if two old classes have the same image, then either they were already equal, or one of them is the class of $b$. The argument is by double quotient induction, then $\mathrm{clos_cons_iff}$ on the exactness witness, splitting into the three merge cases (old path; path through $a$ then $b$; path through $b$ then $a$) and re-sounding each into the old quotient.
Feed that projection and the distinguished class of $b$ into $\mathrm{card_le_succ_of_merge}$, which supplies $\mathrm{Nat.card}$ of the old quotient $\le$ $\mathrm{Nat.card}$ of the new quotient plus one, i.e. the claimed inequality.
why it matters
This is the atomic merge bound named in the module doc as the first link of the chain that closes the open connected-graph fact from the 2D/3D domain-coarsening engines. Downstream, $\mathrm{comp_le_comp_append}$ iterates it by induction on the interface list: adjoining $F$ edges lowers component count by at most $F.\mathrm{length}$. That iteration, together with a connectedness endpoint, yields the headline $\mathrm{mono_components_le_bichromatic_succ}$: locked domains $\le$ bichromatic edges $+1$.
In 1D the same counting is the exact identity runs $=$ boundaries $+1$; in higher $D$ interfaces may be multiply connected, so only the inequality survives. The proof is dimension-free and discharges what was previously only numeric-checked on live fields. It sits inside the Recognition cosmology stack that treats monochromatic regions as locked domains and bichromatic edges as the recognition-active interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.