clos_cons_iff
plain-language theorem explainer
Two vertices are connected after prepending edge (a,b) to list X exactly when they lie in the merged a/b classes of the prior connectivity. Domain-count arguments that track how one interface edge collapses locked regions cite this. Proof is a two-way equivalence: EqvGen's universal property against the merge relation one way; case split on the three merge disjuncts with monotonicity and the new edge the other.
Claim. For vertices $a,b,u,v$ and edge list $X$, the equivalence closure of the edge relation after prepending $(a,b)$ relates $u$ to $v$ if and only if $u$ and $v$ are related under the merge of the $a$-class and $b$-class of the prior closure: either already connected under $X$, or one is $X$-connected to $a$ and the other to $b$ (in either order).
background
The module proves a dimension-free bound: locked domains (monochromatic components of a charge field on a finite world $V$) number at most the bichromatic interface size plus one, once the ambient edge graph is connected. Connectivity is the equivalence closure of the generating edge relation: clos E is the least equivalence containing the generators of list $E$, so two vertices are related precisely when an undirected path of listed edges joins them.
The merge relation packages the classical effect of identifying the class of $a$ with the class of $b$. Upstream, clos_mono_cons records that prepending an edge only enlarges the closure; eqvGen_le is the universal property that the equivalence closure sits below any equivalence containing the generators; gen_cons_le_merged places every generator of the extended list inside the merge relation; and merged_equiv confirms the merge is itself an equivalence.
proof idea
Bidirectional constructor.
Forward: feed eqvGen_le the facts that the merge is an equivalence (merged_equiv) and that every generator of the cons-list lies in the merge (gen_cons_le_merged). That pushes the whole EqvGen of the extended generators into the merge.
Reverse: introduce a merge witness and rcases on its three disjuncts. The already-connected case is immediate from clos_mono_cons. For the two bridge cases, build a path $u\to a\to b\to v$ (or $u\to b\to a\to v$) by lifting the old connections via clos_mono_cons, inserting the new edge as EqvGen.rel from List.mem_cons_self, and reassembling with trans/symm of clos_equiv on the extended list.
why it matters
Direct input to comp_le_comp_cons, the atomic merge bound: adding one edge lowers the component count by at most one (equivalently, the count without the edge is at most the count with it, plus one). That bound iterates over the interface list and, with ambient connectivity, yields the headline mono_components_le_bichromatic_succ.
The module closes the connected-graph fact left open in the cosmogenesis domain-coarsening scripts and their 2D/3D Lean bridges: locked-domain count $\le$ recognition-active interface $+1$ on any connected finite world. In 1D this is the exact identity runs $=$ boundaries $+1$; in higher dimensions multiply-connected interfaces force the inequality. The characterization here is the relational engine of the Option-valued injection that proves the atomic step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.