merged
plain-language theorem explainer
Defines the merged relation on vertices: two points are related after lumping the equivalence classes of a and b together under the connectivity closure of edge list X. Equivalently, it is the connectivity relation obtained by adding the single edge (a,b). Component-counting arguments in the locked-domain bound cite it as the atomic merge step. The body is a three-disjunct propositional definition over the existing closure.
Claim. For vertices $a,b,u,v$ and an edge list $X$, the merged relation holds when either $u$ and $v$ are already connected by the equivalence closure of $X$, or $u$ meets $a$ and $v$ meets $b$ in that closure, or $u$ meets $b$ and $v$ meets $a$. This is the connectivity relation after identifying the classes of $a$ and $b$ (equivalently, after adjoining the edge $(a,b)$).
background
The module proves a dimension-free bound for Recognition cosmology domain coarsening: on any finite connected world, the number of monochromatic locked domains is at most the number of bichromatic interface edges plus one. Vertices form a finite type $V$; an edge list encodes adjacency; a charge field colours vertices. Monochromatic edges generate locked domains; bichromatic edges are the interface.
Connectivity is the least equivalence containing the generated edge relation: clos X is Relation.EqvGen of the generators from $X$, so two vertices are related iff a path joins them. Component count is the cardinality of the quotient by that equivalence (using only Finite V).
The classical mechanism is that adding one edge merges at most two components. The merged relation packages exactly that lumping of the $a$-class with the $b$-class under the prior closure of $X$, matching the closure after prepending $(a,b)$.
proof idea
Pure definitional abbreviation: three disjuncts over the existing closure of $X$. First disjunct keeps prior connections; the other two cross-connect any point already tied to $a$ with any point already tied to $b$ (in either orientation). No tactics or lemmas are invoked at the definition site; downstream lemmas prove it is an equivalence and coincides with clos ((a,b)::X).
why it matters
This is the atomic merge predicate for the edge-addition argument behind the headline bound mono_components_le_bichromatic_succ. Downstream, merged_equiv shows it is an equivalence; gen_cons_le_merged and clos_cons_iff identify it with the closure after adjoining $(a,b)$; clos_mono_cons supplies monotonicity of closure under edge prepending. Those facts feed the Option-valued injection that proves each added interface edge raises component count by at most one (comp_le_comp_cons and its iteration).
In the framework this closes the connected-graph inequality left open in the 2D/3D domain-coarsening engines: locked super-regions $\le$ recognition-active interface $+1$, reducing in 1D to the exact runs $=$ boundaries $+1$ identity. It is pure graph combinatorics supporting the cosmogenesis interface count, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.