gen_cons_le_merged
plain-language theorem explainer
Any edge from the list with a fresh pair (a,b) prepended already sits inside the three-clause merge relation that lumps the a-class with the b-class of the old closure. Domain-coarsening and interface-component arguments cite it as the generator half of the identification "closure after adding one edge = merge of two classes". The proof is a two-case membership split on the cons list, using reflexivity of the old equivalence closure.
Claim. For vertices $a,b$ and an edge list $X$, every ordered pair that belongs to the adjacency of $(a,b)::X$ is related by the merge relation of $a$ and $b$ over $X$: either the pair was already connected in the equivalence closure of $X$, or the two endpoints lie in the $a$-class and $b$-class of that closure (in either order).
background
The module proves a dimension-free bound on locked domains in a finite coloured world: monochromatic components are at most the number of bichromatic interface edges plus one. Vertices form a finite type $V$; an edge list supplies adjacency; gen is membership of an ordered pair in that list; clos is its equivalence closure (paths, ignoring orientation). Component count is the cardinality of the quotient by that setoid.
The atomic step is that adding one edge merges at most two classes. The relation merged a b X encodes exactly that lump: $u\sim v$ under the old closure, or $u$ meets $a$ and $v$ meets $b$, or the swapped cross. Upstream, clos_equiv records that clos X is an equivalence (so reflexivity is available). The ambient story reconstructs a connected world by re-inserting bichromatic edges into the monochromatic graph, each insertion costing at most one component.
proof idea
Introduce $u,v$ and the membership hypothesis that $(u,v)$ lies in $(a,b)::X$. Obtain the equivalence instance clos_equiv X. Case on List.mem_cons: either the pair equals $(a,b)$, or it already belongs to $X$.
In the head case, injectivity of products gives $u=a$ and $v=b$; feed e.refl twice into the middle disjunct of merged. In the tail case, Relation.EqvGen.rel puts $(u,v)$ into clos X, which is the first disjunct of merged. No induction and no further lemmas.
why it matters
This is the generator inclusion half of clos_cons_iff, whose doc-comment states the identification used throughout the module: "The closure after adding edge $(a,b)$ is exactly the merge of the $a$-class and the $b$-class." That biconditional is the algebraic engine behind the atomic merge bound comp_le_comp_cons and its iteration comp_le_comp_append, which close the open connected-graph fact from the 2D/3D domain-coarsening scripts: monochromatic components $\le$ bichromatic edges $+1$ on any connected finite world.
In the Recognition cosmology stack this turns a numeric live-field check into a Lean theorem, dimension-free, with connectivity discharged separately by descent heights on the diamond and octahedron lattices. It does not itself touch T0–T8 or the mass ladder; it is pure graph bookkeeping that locks the interface-component inequality the cosmogenesis engine relies on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.