cs
plain-language theorem explainer
Packages the path-connectivity relation of an edge list into a Setoid on the vertex type. Its quotient is the set of locked domains (monochromatic connected components). Downstream component-count lemmas cite it as the equivalence used by Nat.card. Construction is the pair of the EqvGen closure and the Mathlib fact that EqvGen is an equivalence.
Claim. For an edge list $E$ on a vertex type $V$, let $\sim_E$ be the least equivalence relation containing the undirected edge relation generated by $E$. Then $\mathrm{cs}(E)$ is the setoid $(V,\sim_E)$; the quotient $V/\sim_E$ is the set of locked domains of the graph.
background
The module proves a dimension-free bound on locked domains in Recognition cosmogenesis: on any finite connected world, the number of monochromatic connected components is at most the number of bichromatic (interface) edges plus one. A world is a finite vertex type $V$ with adjacency given as a list $E$ of pairs; a charge field colours vertices, monochromatic edges lock domains, and bichromatic edges form the interface.
Upstream, clos E is the connectivity closure: Relation.EqvGen of the generating edge relation, so two vertices are related iff a path of edges joins them. The companion fact clos_equiv records that this relation is an equivalence. The setoid packages that pair so Lean quotients and Nat.card apply without a decidability hypothesis on the closure.
Component count is then the cardinality of the quotient by this setoid. That is the quantity bounded by the headline inequality and used for 2D diamonds and 3D octahedra once ambient connectivity is discharged by a height-descent criterion.
proof idea
One-line definitional packaging: the setoid is the structure whose relation is clos E and whose equivalence proof is clos_equiv E (Mathlib's Relation.EqvGen.is_equivalence). No further reasoning.
why it matters
This is the setoid that makes locked-domain counting well-typed. Immediate consumers include comp (component count as Nat.card of the quotient), the atomic merge bound comp_le_comp_cons, the connected-world endpoint comp_eq_one_of_connected, list-order invariance comp_congr, the empty-graph identity comp_nil, and the finer-to-coarser surjection proj used in the merge argument.
Outside the module, PolarizedBirthDomains uses it for root and charge bounds on component counts. Together these close the connected-graph fact previously left open in the 2D/3D domain-coarsening bridges: components of the monochromatic graph are at most interface size plus one. The construction is pure graph theory; it sits under the Recognition interface story rather than under T0–T8 forcing, but it is what turns the engine's numeric domain count into a Lean theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.