clos
plain-language theorem explainer
The connectivity closure of an edge list is the least equivalence relation generated by those edges: two vertices are related exactly when a path joins them. Cosmology proofs that count locked domains cite this as the relation whose quotient is the set of monochromatic components. It is a one-line definition wrapping Mathlib's equivalence generation on the base adjacency.
Claim. For an edge list $E$ of ordered pairs on a vertex type $V$, let $\mathrm{clos}(E)$ be the least equivalence relation on $V$ containing the base adjacency of $E$. Two vertices $u,v$ satisfy $\mathrm{clos}(E)\,u\,v$ if and only if a (possibly empty) path of edges from $E$ joins them.
background
The module proves a dimension-free bound: on any connected finite world, the number of locked domains (monochromatic components) is at most the number of bichromatic interface edges plus one. A world is a finite vertex type $V$ with a charge colouring and an adjacency list $E$; monochromatic edges generate the locked domains, bichromatic edges form the interface. Component count is the cardinality of the quotient by the equivalence closure of the edge relation.
The base adjacency gen E holds of $(a,b)$ exactly when that ordered pair appears in $E$. Orientation is irrelevant once the relation is closed under symmetry. The present definition packages Mathlib's Relation.EqvGen applied to that base relation, so path-connectedness becomes an equivalence.
Upstream, the same edge-list pattern appears in lattice constructions (diamond and octahedron adjacency) that later discharge connectivity of the ambient world via a height-descent criterion.
proof idea
One-line definitional wrapper: set the binary relation equal to Mathlib's Relation.EqvGen applied to the base adjacency of the edge list. No tactics or lemmas are invoked at the definition site; all structure (reflexivity, symmetry, transitivity, and the universal property of the least equivalence) is inherited from EqvGen.
why it matters
This is the relation whose quotient is the set of locked domains, so almost every component-counting lemma in the module is stated in terms of it. Immediate dependents include the proof that the closure is an equivalence, monotonicity under prepending edges, the empty-list characterisation (closure is equality), the merge characterisation after adding one edge, congruence of component count under list reordering, and the descent criterion that every cell reaches a unique root.
Those lemmas feed the atomic merge bound (adding one edge raises component count by at most one), its iteration over the interface, and the connected ambient endpoint. The headline inequality then closes the open connected-graph fact left numeric-only in the 2D/3D domain-coarsening engines: monochromatic components are at most bichromatic edges plus one. The construction is the graph-theoretic reading of recognition's pull toward the coarsest description.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.