mono_components_le_bichromatic_succ
plain-language theorem explainer
On any finite connected graph with a vertex colouring, the number of monochromatic connected components is at most the number of bichromatic edges plus one. Cosmologists and domain-coarsening theorists cite it as the dimension-free bound on locked domains versus the recognition-active interface. The proof splits the edge list, applies the merge bound under edge append, and uses ambient connectivity to pin the component count at one.
Claim. Let $V$ be a nonempty finite vertex set, $E$ a list of undirected edges on $V$, and $c : V \to \beta$ a colouring with decidable equality on colours. If the equivalence closure of $E$ connects every pair of vertices, then the number of connected components of the monochromatic subgraph (edges with $c(u)=c(v)$) is at most the length of the bichromatic edge list (edges with $c(u)\neq c(v)$) plus one.
background
This module proves a dimension-free graph fact used by the Recognition Science domain-coarsening engine: locked domains (monochromatic super-regions) cannot outnumber the recognition-active interface by more than one, on any connected finite world. In 1D the identity is exact (runs = boundaries + 1); in higher dimensions the interface may be multiply connected, so only the inequality survives.
A world is a finite type $V$ with edge list $E$. Connectivity is the equivalence closure clos E of the generating edge relation. Component count comp E is Nat.card of the quotient by that closure, well-defined from Finite V alone. A charge field $c$ splits $E$ into monochromatic edges (same colour ends: the locked-domain generators) and bichromatic edges (unequal ends: the interface).
The classical mechanism is that deleting an edge raises the component count by at most one. Adding the interface edges back reconstructs the ambient connected graph, and each added edge merges at most two monochromatic components. Upstream lemmas package this: the atomic merge bound, its iteration under list append, and the fact that a fully connected edge list has comp = 1.
proof idea
Name the monochromatic filter mono and the bichromatic filter bi. First show that membership in mono ++ bi is equivalent to membership in $E$ (case split on whether the two endpoints share a colour). Apply the append merge bound: comp mono ≤ comp (mono ++ bi) + bi.length. Congruence of component count under edge-list membership equivalence rewrites comp (mono ++ bi) to comp E. Ambient connectivity (clos E total) forces comp E = 1. Substitute and finish with omega: monochromatic components $\le 1 + |\mathrm{bi}|$.
why it matters
This is the headline of the module: the connected-graph fact previously left open in the 2D/3D domain-coarsening scripts and their Lean bridges, discharged only by numeric checks on the live field. It upgrades that check to a theorem with zero sorry.
Downstream, mono_le_interface_of_descent composes it with the potential-descent connectivity criterion (unique root of height zero, every other cell has a strict descent edge), yielding the form instantiated on the engine lattices. twoCell_interface_bound checks tightness on two opposite-charge cells ($2 \le 1+1$). Those feed the 2D diamond and 3D octahedron bounds used by cosmogenesis.
In framework terms it is the higher-dimensional shadow of the 1D run/boundary identity that controls how many locked domains the coarsening engine may carry relative to forced distinctions. Connectivity itself is later read as the recognition law's pull toward the coarsest description (descent toward a root).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.