comp_nil
plain-language theorem explainer
On a finite vertex set with the empty edge list, the locked-domain count equals the number of vertices. Cosmology proofs cite it as the base case when the monochromatic graph has no edges (every cell is its own domain). The argument shows the quotient map is bijective via the empty-closure lemma, then transports cardinality.
Claim. Let $V$ be a finite type of vertices. The number of connected components of the graph with empty edge list equals the cardinality of $V$: if $\mathrm{comp}(E)$ denotes $\mathrm{Nat.card}$ of the quotient by the equivalence closure of $E$, then $\mathrm{comp}(\emptyset)=|V|$.
background
The module proves a dimension-free bound on locked domains in Recognition cosmology: on any connected finite world, monochromatic components are at most the number of bichromatic (interface) edges plus one. A world is a finite vertex type $V$ with an edge list $E$; a charge field colours vertices, monochromatic edges generate locked domains, and bichromatic edges form the interface.
Component count is defined without decidability of the closure: cs E is the setoid whose relation is the equivalence closure of the generating edge relation, and comp E is Nat.card of the quotient. The empty-list lemma clos_nil states that this closure collapses to equality: two vertices are related under the empty edge list if and only if they are identical. That is the algebraic input here.
The setting is classical graph connectivity under edge deletion/addition, formalized so the engine's 1D/2D/3D domain-coarsening counts become theorems rather than numeric checks.
proof idea
Build a bijection between $V$ and the quotient by the empty setoid. Surjectivity of Quotient.mk is standard. Injectivity: if two vertices map to the same class, Quotient.exact yields a closure witness, and clos_nil forces them equal. Unfold comp and apply Nat.card_congr to the equivalence from that bijection (symmetry gives the stated orientation).
why it matters
This is the empty-graph base case for the interface-component calculus. Downstream, twoCell_comp_nil specializes it to the two-cell world (comp [] = 2), which pins the tight instance of the bound (two locked domains, one interface edge). The same module's connectivity and merge lemmas (comp_le_comp_cons, comp_eq_one_of_connected, headline mono_components_le_bichromatic_succ) sit on top of this counting infrastructure.
In the broader Recognition story the module closes an OPEN fact from the cosmogenesis domain-coarsening scripts: locked-domain count $\le$ interface size $+1$ on connected worlds in any dimension. The empty case is the extreme where every cell is a separate domain, matching $|V|$ before any monochromatic edges glue them. It does not itself invoke T0–T8 or the mass ladder; it is pure finite-graph bookkeeping that the cosmology layer needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.