comp
plain-language theorem explainer
Counts locked domains: the connected components of a finite graph given by edge list E. Defined as the cardinality of the quotient by the equivalence closure of those edges, so it needs only Finite V (no decidability on the closure). Domain-coarsening and interface bounds in the cosmology stack cite it as the left-hand side of the monochromatic-component inequality.
Claim. For a finite vertex type $V$ and an edge list $E$ of pairs in $V\times V$, $\mathrm{comp}(E)$ is the number of connected components of the graph $(V,E)$: the cardinality of the quotient of $V$ by the equivalence relation generated by identifying endpoints of edges in $E$.
background
The 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 charge field colours vertices; monochromatic edges generate locked domains, bichromatic edges form the recognition-active interface.
Connectivity is packaged as a Setoid: the generating relation from the edge list is closed under the usual reflexive-symmetric-transitive rules, and cs E is that setoid. The quotient of $V$ by cs E is the set of locked domains. Using Nat.card on that quotient avoids needing a decidable equality on the closure, which is the usual obstruction in constructive graph libraries.
This definition is the component counter the rest of the module manipulates. Upstream, the closure and its equivalence proof supply the setoid; the ambient lattices (diamond, octahedron) later instantiate $V$ and $E$.
proof idea
One-line definition: take the connectivity setoid cs E (equivalence closure of the edge list as a Setoid on $V$), form the quotient type, and return its Nat.card. Noncomputable only because Nat.card is; no proof obligations beyond those already discharged for cs.
why it matters
This is the component counter behind the module headline mono_components_le_bichromatic_succ: monochromatic components $\le$ bichromatic edges $+ 1$. That inequality closes the open connected-graph fact from the cosmogenesis domain-coarsening scripts (2D/3D) and their Lean bridges, previously only numeric-discharged on live fields.
The atomic merge step (comp_le_comp_cons: adding one edge raises component count by at most one), its iteration over an interface list, and the connected ambient endpoint all quantify over this comp. In 1D it specialises to the exact identity runs $=$ boundaries $+ 1$; in higher $D$ multiply-connected interfaces force the inequality form. It is pure graph combinatorics supporting Recognition cosmology's locked-domain bookkeeping, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.