clos_mono_cons
plain-language theorem explainer
Adding one undirected edge to a finite graph cannot destroy existing path-connections: if u and v are already joined by the equivalence closure of X, they remain joined after prepending (a,b). Cosmology proofs that track locked-domain merges under interface edges cite this monotonicity. The argument is a one-shot appeal to the universal property of EqvGen against the larger generating relation.
Claim. Let $V$ be a finite vertex type and $X$ a list of undirected edges on $V$. Write $\mathrm{clos}(X)$ for the least equivalence relation containing the edge relation of $X$. For any $a,b,u,v\in V$, if $\mathrm{clos}(X)\,u\,v$ holds, then $\mathrm{clos}(((a,b)::X))\,u\,v$ holds.
background
The module proves a dimension-free bound on locked domains in Recognition cosmogenesis: on any finite connected world, the number of monochromatic components is at most the number of bichromatic (interface) edges plus one. Vertices are a finite type $V$; an edge list $E:\mathrm{List}(V\times V)$ is the ambient adjacency; a charge field colours vertices. Monochromatic edges generate locked domains; bichromatic edges form the interface.
Connectivity is formalized by clos: the equivalence closure Relation.EqvGen of the generating edge relation of a list. Two vertices are related precisely when a path of listed edges joins them. The setoid of that closure has quotient equal to the set of locked domains; component count is Nat.card of the quotient (only Finite V is required).
Upstream, clos_equiv records that clos E is an equivalence, and eqvGen_le is the universal property: any equivalence containing the generators already contains the full EqvGen. The merged relation (classes of $a$ and $b$ lumped) is defined next and will be identified with the enlarged closure.
proof idea
Term-mode via the universal property. Apply eqvGen_le with target relation clos ((a,b)::X), which is an equivalence by clos_equiv. It remains only to check that every generator of the old list $X$ is already a generator of the cons-list: if $(x,y)\in X$, then $(x,y)\in (a,b)::X$ by List.mem_cons_of_mem, so Relation.EqvGen.rel places $(x,y)$ in the new closure. The old witness $h:\mathrm{clos},X,u,v$ therefore transfers.
why it matters
This is the atomic monotonicity step for edge-addition in the locked-domain count. Downstream, clos_cons_iff uses it (with the converse merge direction) to identify clos ((a,b)::X) with the explicit merge of the $a$- and $b$-classes. That identification feeds proj, the canonical surjection from the finer quotient (fewer edges) onto the coarser one (one more edge), whose almost-injectivity yields the atomic bound that each added interface edge drops cardinality by at most one.
Iterating that bound over the bichromatic list and using ambient connectivity recovers the headline mono_components_le_bichromatic_succ: components of the monochromatic graph $\le$ interface size $+1$. The module thereby closes the open connected-graph fact left numeric in the 2D/3D domain-coarsening engines. The argument is pure finite-graph combinatorics; it does not invoke the forcing chain T0–T8, but it supplies the component arithmetic those cosmogenesis runs rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.