comp_congr
plain-language theorem explainer
Component count of a finite graph depends only on the underlying edge set, not list order or multiplicity. Cosmology proofs cite it to rewrite edge lists under membership equivalence before merge bounds. The proof pushes set-equality through the generating relation, its equivalence closure, the induced setoid, and Nat.card of the quotient.
Claim. If $X,Y$ are lists of ordered pairs on a vertex type $V$ and $\forall p,\, p\in X\leftrightarrow p\in Y$, then the number of connected components of the graph with edge list $X$ equals that with edge list $Y$.
background
The module proves a dimension-free bound: on any connected finite world, monochromatic connected components (locked domains) are at most the number of bichromatic interface edges plus one. Vertices form a finite type $V$; an edge list $E:\mathrm{List}(V\times V)$ is the ambient adjacency.
Locally, gen E is membership of ordered pairs in $E$. Its equivalence closure clos E = \mathrm{EqvGen}(\mathrm{gen}\,E)$ is path-connectivity. The setoid cs Epackages that relation;comp Eis $\mathrm{Nat.card}$ of the quotient, so component count needs onlyFinite V`, not decidability of the closure.
Because gen is pure membership, two lists with the same pairs (ignoring order and duplicates) generate identical relations and therefore identical component counts. That invariance is what this lemma records.
proof idea
Four short transports. First, funext on pairs plus propext of the membership hypothesis gives gen X = gen Y. Unfolding clos and rewriting yields clos X = clos Y. Setoid.ext then equates the setoids cs X and cs Y. Finally unfold comp and rewrite: equal setoids give equal quotients, hence equal Nat.card. No external lemmas beyond Mathlib Relation.EqvGen and Setoid infrastructure.
why it matters
Supports the atomic and iterated merge bounds that close the locked-domain inequality left open in the 2D/3D domain-coarsening bridges. Downstream, comp_le_comp_append iterates "adding one edge drops components by at most one" over an interface list; the headline mono_components_le_bichromatic_succ specializes that to monochromatic vs bichromatic filters on a connected world.
Without set-congruence of comp, filter and append rewrites on edge lists would not preserve the count. The result is pure graph bookkeeping inside the cosmology interface bound; it does not itself invoke the forcing chain (T0–T8), RCL, or $\varphi$-ladder constants, but it underwrites the engine's claim that locked-domain count is controlled by recognition-active interface size in any dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.