eqvGen_le
plain-language theorem explainer
Any equivalence relation that contains a generating relation also contains that relation's equivalence closure. Cosmology proofs of locked-domain merges cite it when comparing edge-list closures. The argument is induction on the four EqvGen constructors, feeding the target equivalence's refl/symm/trans.
Claim. Let $r,s$ be binary relations on a vertex set $V$. If $s$ is an equivalence and $r\subseteq s$ pointwise, then whenever $a$ and $b$ are related by the equivalence closure of $r$, one has $s(a,b)$.
background
The module proves a dimension-free bound on locked domains in a finite coloured world: monochromatic components are at most the number of bichromatic (interface) edges plus one, once the ambient graph is connected. Vertices form a finite type $V$; an edge list generates a relation whose equivalence closure defines the domains; component count is the cardinality of the quotient.
Relation.EqvGen r is Mathlib's inductive equivalence closure of a relation $r$ (generators, reflexivity, symmetry, transitivity). The local closure clos X is that construction applied to membership in the edge list $X$. Comparing two such closures, or a closure against a hand-built merge relation, needs the universal property: EqvGen is the least equivalence above its generator.
That leastness is exactly this lemma. Downstream monotonicity and merge-characterisation theorems invoke it rather than re-inducting on EqvGen each time.
proof idea
Fix $a,b$ and an EqvGen derivation of $r,a,b$. Induct on that derivation. The generator case applies the inclusion hypothesis $r\subseteq s$. Reflexivity, symmetry, and transitivity cases apply the corresponding fields of the assumed Equivalence s to the inductive hypotheses. No auxiliary lemmas beyond Mathlib's EqvGen induction principle and the Equivalence structure.
why it matters
This is the relational engine under the interface-component bound. clos_mono_cons uses it to show that prepending an edge only enlarges the closure (more edges can only merge domains). clos_cons_iff uses it one direction to identify the closure after adding $(a,b)$ with the explicit merge of the $a$- and $b$-classes.
Those facts feed the atomic merge inequality (adding one edge raises component count by at most one) and its iteration over the bichromatic interface, closing the open connected-graph claim from the 2D/3D domain-coarsening scripts: monochromatic components $\le$ interface size $+1$ on any connected finite world. The lemma itself is pure relation algebra; its place in the chain is what ties it to the cosmology headline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.