comp_le_comp_append
plain-language theorem explainer
Adding any finite list of edges lowers the monochromatic component count by at most the length of that list. Cosmology and domain-coarsening arguments cite this as the iterated form of the classical one-edge merge bound. The proof is induction on the added list, applying the atomic cons bound at each step and rewriting by list-membership congruence.
Claim. Let $V$ be a finite vertex type and let $X,F$ be finite lists of undirected edges on $V$. Write $\mathrm{comp}(E)$ for the number of connected components of the graph with edge list $E$ (cardinality of the quotient by the equivalence closure of the edge relation). Then $\mathrm{comp}(X) \le \mathrm{comp}(X{+}{+}F) + |F|$.
background
The module proves a dimension-free bound used by the cosmogenesis domain-coarsening engine: on any connected finite world, the number of locked (monochromatic) domains is at most the number of bichromatic interface edges plus one. A finite world is a finite vertex type $V$; an edge list $E : \mathrm{List}(V \times V)$ is the ambient adjacency. Component count is defined as $\mathrm{comp}(E) = \mathrm{Nat.card}$ of the quotient by the equivalence closure of the generating edge relation, so it needs only Finite V and no decidability of the closure.
The classical mechanism is that deleting one edge raises the component count by at most one. The atomic form is already proved as the cons bound: $\mathrm{comp}(X) \le \mathrm{comp}((a,b)::X)+1$, via an Option-valued injection injective away from the single class the new edge can collapse. Component count is also independent of list order and multiplicity (comp_congr). The present lemma iterates the atomic bound over an arbitrary finite interface list $F$.
proof idea
Induction on the appended list $F$.
- Base: $F = []$. Both sides reduce by
simpto $\mathrm{comp}(X) \le \mathrm{comp}(X)$. - Step: $F = (a,b)::F'$. The inductive hypothesis gives $\mathrm{comp}(X) \le \mathrm{comp}(X{+}{+}F') + |F'|$. Membership of $X{+}{+}F'$ and of $X{+}{+}((a,b)::F')$ coincides up to reordering of one cons, so
comp_congrrewrites the atomic boundcomp_le_comp_cons a b (X ++ F')into $\mathrm{comp}(X{+}{+}F') \le \mathrm{comp}(X{+}{+}((a,b)::F')) + 1$. Chaining withomega/ringandList.length_consyields the claim for the longer list.
why it matters
This is the middle step of the module's three-lemma chain. The atomic merge bound handles one edge; this lemma lifts it to a full interface list; the headline mono_components_le_bichromatic_succ then specialises to monochromatic versus bichromatic filters on a connected ambient graph and obtains
$$\mathrm{comp}(\mathrm{mono}) \le |\mathrm{bichromatic}| + 1.$$
That headline closes the connected-graph fact previously left open in the 2D/3D domain-coarsening scripts and their Lean bridges: locked-domain count is at most the recognition-active interface plus one, in any dimension. In 1D it recovers the exact identity runs = boundaries + 1; in higher dimensions multiply-connected interfaces force the inequality. Connectivity of the lattices the engine runs on is discharged separately by a height-descent criterion, so the whole bound is a zero-sorry theorem rather than a numeric check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.