comp_eq_one_of_connected
plain-language theorem explainer
On a finite nonempty vertex set, any edge list whose equivalence closure relates every pair of vertices has exactly one connected component. Cosmology proofs cite this as the connected-ambient endpoint of the locked-domain bound. The argument equips the quotient with Subsingleton and Nonempty instances, then applies the unique-card criterion for Nat.card.
Claim. Let $V$ be a finite nonempty type and $E$ a list of pairs in $V\times V$. Write $\mathrm{clos}(E)$ for the equivalence closure of the edge relation generated by $E$, and $\mathrm{comp}(E)$ for the number of connected components ($\mathrm{Nat.card}$ of the quotient). If $\mathrm{clos}(E)\,u\,v$ holds for every $u,v\in V$, then $\mathrm{comp}(E)=1$.
background
The module proves a dimension-free bound: on any connected finite world, the number of monochromatic connected components (locked domains) is at most the number of bichromatic edges (the recognition-active interface) plus one. In 1D this recovers the exact identity runs = boundaries + 1; in higher dimensions the interface may be multiply connected, so equality becomes inequality.
A world is a finite vertex type $V$ with adjacency given by an edge list $E$. The generating relation gen E is the undirected edge predicate; clos E is its least equivalence relation (path-connectivity). Components are counted by comp E := Nat.card (Quotient (cs E)), which needs only Finite V and no decidability of the closure.
The headline argument reconstructs the ambient graph by re-adding bichromatic edges to the monochromatic subgraph. Each added edge merges at most two components; the connected ambient world supplies the base count of one component. This theorem is that base count.
proof idea
Term-style tactic proof with two instance constructions. From the hypothesis that every pair is related by clos E, the quotient by the setoid cs E is a subsingleton: any two classes are equal by Quotient.sound. Nonemptiness of the quotient follows from Nonempty V via an arbitrary vertex. Unfolding comp and rewriting with Nat.card_eq_one_iff_unique reduces the goal to uniqueness of the quotient type, discharged by the two inferred instances.
why it matters
Supplies the connected-ambient endpoint for mono_components_le_bichromatic_succ, the module headline: locked domains are at most the interface plus one. That theorem is the dimension-free form of the 1D identity runs = boundaries + 1 from DomainCoarsening, and closes the connected-graph fact previously left open in the 2D/3D domain-coarsening scripts and Lean bridges.
Together with the atomic merge bound (comp_le_comp_cons) and its iteration over the interface (comp_le_comp_append), it turns a numeric engine check into a Lean theorem with zero sorry. Connectivity itself is later discharged for the lattices the engine runs on (diamond, octahedron) via connected_of_descent with L1 height, so the bound applies to the actual cosmogenesis graphs without an extra hypothesis at use sites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.