twoCell_connected
plain-language theorem explainer
On the two-point vertex set with the single edge joining 0 to 1, every pair of vertices is related by the equivalence closure of that edge: the graph is connected. Cosmology proofs cite it as the connectivity hypothesis when the monochromatic-component bound is instantiated on the minimal opposite-charge pair. The argument is a short Fin-2 case split using reflexivity, symmetry of the generating edge, and transitivity.
Claim. Let $V = \{0,1\}$ and let $E$ be the edge list containing only the pair $(0,1)$. Then for every $u,v \in V$, $u$ and $v$ are related by the least equivalence relation containing the adjacency of $E$ (i.e., the two-cell graph is path-connected).
background
The module proves a dimension-free bound: on any finite connected world, the number of locked domains (components of the monochromatic subgraph) is at most the number of bichromatic interface edges plus one. Connectivity of the ambient edge list is a hypothesis of the headline theorem and must be discharged on each concrete world.
Here the world is the smallest nontrivial certificate: two cells joined by one edge. Adjacency gen E holds when the ordered pair lies in the edge list; clos E is its equivalence closure (Relation.EqvGen), so two vertices are related exactly when a path joins them. The theorem clos_equiv records that this closure is an equivalence relation.
The empty-edge component count comp_nil later pins that the monochromatic graph on this world has exactly two locked domains; connectivity of the full edge list is the missing half of the tight bound.
proof idea
Obtain that clos of the singleton edge list is an equivalence via clos_equiv. The generating edge gives clos 0 1 by Relation.EqvGen.rel and gen. A lemma then shows every u : Fin 2 is related to 0: case-split on u, using reflexivity at 0 and symmetry of the edge at 1. For arbitrary u,v, case-split on v: if v = 0 apply the lemma; if v = 1 compose the lemma with the edge by transitivity.
why it matters
This is the concrete connectivity certificate for the two-cell world used immediately by twoCell_interface_bound, which applies the headline monochromatic bound and obtains the tight inequality $2 \le 1+1$. The module doc frames that pair as the non-vacuity check: two locked domains, one interface edge, bound saturated.
Downstream the same pattern scales to the engine lattices (2D diamond, 3D octahedron) via the descent criterion, closing the connected-graph obligation left open in the domain-coarsening scripts. In Recognition terms the bound is the graph-theoretic reading of locked domains versus recognition-active interface distinctions; the two-cell case shows the $+1$ is sharp already in the smallest opposite-charge configuration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.