merged_equiv
plain-language theorem explainer
The relation that closes an edge list and simultaneously identifies the classes of two vertices a and b is an equivalence. Cosmology proofs that bound locked-domain counts by interface size plus one cite this when treating a single added bichromatic edge as a class merge. The proof unpacks reflexivity, symmetry, and transitivity by case analysis on the three disjuncts of the merge, reducing each case to the known equivalence of the ordinary connectivity closure.
Claim. For any vertices $a,b$ and any edge list $X$ on a finite vertex set $V$, the relation $R$ given by $u\,R\,v$ iff either $u$ and $v$ lie in the same class of the equivalence closure of $X$, or one lies in the $a$-class and the other in the $b$-class of that closure, is an equivalence relation on $V$.
background
The InterfaceComponentBound module proves a dimension-free bound on locked domains: on any connected finite world, the number of monochromatic components is at most the number of bichromatic (interface) edges plus one. A world is a finite vertex type $V$ with an edge list; monochromatic edges generate locked domains via their equivalence closure, and component count is the cardinality of the quotient by that closure.
The ordinary connectivity closure of an edge list is already an equivalence (clos_equiv, via Relation.EqvGen.is_equivalence). The merged relation lumps the classes of two distinguished vertices $a$ and $b$: $u$ relates to $v$ if they are already connected under the old closure, or if they sit on opposite sides of the pair ${a,b}$. By design this is exactly connectivity after adjoining the single edge $(a,b)$.
That merge view is the classical mechanism behind "adding one edge raises the component count by at most one," which the module iterates over the full interface.
proof idea
Invoke clos_equiv X to obtain reflexivity, symmetry, and transitivity of the ordinary closure. Build the three Equivalence fields with refine.
Reflexivity: every vertex relates to itself via the pure-closure disjunct.
Symmetry: on the pure-closure case apply old symmetry; on a cross term swap the two sides $(u\sim a\land v\sim b)$ versus $(u\sim b\land v\sim a)$.
Transitivity: nine-way case split on which disjunct holds for $u\sim v$ and for $v\sim w$. Each branch either chains old closures or rewrites through the identified $a$/$b$ classes, using old symmetry and transitivity to reconnect the free endpoints.
why it matters
This lemma is the equivalence half of the identification between "add edge $(a,b)$" and "merge the $a$-class with the $b$-class." Downstream, clos_cons_iff applies it (with gen_cons_le_merged and eqvGen_le) to prove the two relations coincide pointwise: "the closure after adding edge $(a,b)$ is exactly the merge of the $a$-class and the $b$-class."
That identification is the atomic step in the classical edge-merge argument. It feeds the component-count inequalities (comp_le_comp_cons, then comp_le_comp_append) and the headline mono_components_le_bichromatic_succ.
The module closes an OPEN fact left numeric-only in the cosmogenesis domain-coarsening scripts and their 2D/3D Lean bridges: locked-domain count $\le$ interface size $+1$ in any dimension. The proof needs no Mathlib component-counting library; this equivalence is part of the hand-rolled merge machinery that replaces it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.