clos_nil
plain-language theorem explainer
With an empty edge list, the connectivity closure relates two vertices if and only if they are identical. Component-counting arguments cite this as the empty-graph base case: every vertex is its own locked domain. The proof is a short induction on the equivalence generators, with the adjacency case ruled out by emptiness.
Claim. For any vertices $u,v$ of the world $V$, the least equivalence relation containing the empty edge list relates $u$ and $v$ if and only if $u=v$.
background
This module proves a dimension-free bound: on any connected finite world, the number of locked (monochromatic) domains is at most the number of bichromatic interface edges plus one. A world is a finite vertex type $V$ with an edge list $E$ as adjacency; a charge field colours vertices, monochromatic edges generate locked domains, and bichromatic edges form the interface.
Base adjacency holds when an ordered pair sits in $E$. Connectivity closure is the least equivalence containing that relation: two vertices are related exactly when a path of edges joins them. The empty list supplies no generating pairs, so the closure must reduce to equality. Component count is then the cardinality of the quotient by that equivalence (needing only Finite V).
proof idea
Split the biconditional. Forward: induct on the EqvGen derivation. The generating-pair case is absurd, since membership in the empty list is false after unfolding base adjacency. Reflexivity yields equality on the nose; symmetry and transitivity transport equality by the inductive hypotheses. Backward: substitute $u=v$ and apply reflexivity of the equivalence generator.
why it matters
Direct input to the empty-list component identity: with no edges the quotient map is bijective, so the component count equals the number of cells. That base case anchors the merge induction used throughout the module (each added edge collapses at most two classes). The chain ends at the headline bound that locked-domain count is at most interface size plus one, closing the connected-graph fact left open in the cosmogenesis domain-coarsening scripts and their 2D/3D Lean bridges. The argument is classical graph theory read in Recognition units: deleting interface edges raises components by at most one, and a connected ambient world supplies the unit endpoint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.