clos_equiv
plain-language theorem explainer
The connectivity closure of any edge list is an equivalence relation on the vertex type. Cosmology arguments that count locked domains via quotients cite this to build a Setoid and to move paths under edge-list growth. The proof is a one-line appeal to Mathlib: equivalence generation always yields an equivalence.
Claim. For any list $E$ of ordered pairs of vertices, the connectivity closure of $E$ (the least equivalence relation containing the edge relation generated by $E$) is an equivalence relation on the vertex set.
background
This module proves a dimension-free bound on locked domains in Recognition cosmogenesis: on a connected finite world, the number of monochromatic components is at most the number of bichromatic (interface) edges plus one. Vertices form a finite type $V$; an edge list $E : \mathrm{List}(V \times V)$ is the world's adjacency (line, 4-neighbour diamond, or 6-neighbour octahedron). A charge field colours vertices; monochromatic edges generate locked domains, bichromatic edges form the interface.
The connectivity closure of $E$ is defined as the least equivalence relation containing the generating edge relation of $E$. Two vertices are related precisely when a path of edges joins them. Component count is then $\mathrm{Nat.card}$ of the quotient by that relation, which needs only finiteness of $V$ and no decidability of the closure.
The present fact is the elementary structural step: that closure really is an equivalence, so the Setoid and quotient of locked domains are well-defined before any merge or descent argument begins.
proof idea
One-line term proof. The closure is defined as Mathlib's Relation.EqvGen applied to the generating edge relation of $E$. Mathlib already proves that equivalence generation produces an equivalence relation; the underscore supplies the generator, and the result is immediate. No graph-specific reasoning is needed.
why it matters
Every locked-domain construction in the module rests on this fact. It is the second argument of the Setoid whose quotient is the set of locked domains, and therefore underwrites the component-count definition used by the headline inequality (monochromatic components at most bichromatic edges plus one).
Downstream, monotonicity of closure under prepending an edge, the characterisation of closure after adding one edge as the merge of two classes, the descent-to-root connectivity criterion, and full-world connectivity under a unique-zero height function all invoke it to know they are working with a genuine equivalence. Those lemmas discharge the connected-ambient hypothesis for the 2D diamond and 3D octahedron lattices the engine runs on, closing the open connected-graph obligation left by the domain-coarsening scripts and their Lean bridges.
In the Recognition picture this is pure graph infrastructure for the interface-plus-one bound, not a forcing-chain step; it makes the classical "each added edge merges at most two components" argument available without numeric discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.