twoCell_interface_bound
plain-language theorem explainer
Minimal tight case of the locked-domain interface bound: two opposite-charge cells joined by one edge yield two monochromatic components and one bichromatic edge, so 2 ≤ 1+1. Anyone checking the coarsening engine's component inequality on the smallest nontrivial world cites this. Proof is a one-line application of the headline monochromatic-component lemma plus two-cell connectivity.
Claim. On the two-vertex world $V=\{0,1\}$ with edge list $\{(0,1)\}$ and charge coloring the identity map (opposite charges), the number of connected components of the monochromatic subgraph is at most the number of bichromatic edges plus one. Explicitly the bound is tight: $2 \le 1+1$.
background
This module proves a dimension-free fact used by the cosmogenesis domain-coarsening engine: on any finite connected world, the number of locked domains (components of the monochromatic edge graph) is at most the number of bichromatic interface edges plus one. In 1D that is the exact identity runs = boundaries + 1; in higher D an interface can be multiply connected, so equality becomes inequality.
A charge field colours vertices; monochromatic edges (equal charge) generate locked domains, bichromatic edges (unequal charge) form the recognition-active interface. Component count is the cardinality of the quotient by the equivalence closure of the monochromatic edge relation. The classical merge fact is that restoring each interface edge raises the component count by at most one; connectivity of the ambient graph pins the fully restored count at 1.
The present declaration is the smallest nontrivial instance: two cells, opposite charges, single edge. It sits just above the general headline bound and the two-cell connectivity lemma, before the L1 diamond and octahedron specializations the simulation actually evolves.
proof idea
One-line term proof. Apply the headline lemma mono_components_le_bichromatic_succ to the singleton edge list [(0,1)] on Fin 2, with charge coloring the identity map and with connectivity discharged by twoCell_connected. The headline lemma already packages the merge induction (comp_le_comp_cons / comp_le_comp_append) and the connected-endpoint identity (comp_eq_one_of_connected); no further casework is needed.
why it matters
Gives the tight unit check of the locked-domain interface bound that the coarsening engine relies on: two domains, one interface edge, equality in components ≤ interface + 1. The module status note records that this component-counting-under-edge-deletion fact was previously only numeric-discharged in the 2D/3D Python engines and their Lean bridges; proving even the two-cell case in Lean is the first closed instance of that inequality.
No downstream theorems currently depend on it (used_by is empty). Its role is certification and documentation: it shows the bound is sharp before the reusable descent criterion connects the actual simulation lattices (2D L1 diamond, 3D L1 octahedron) at every radius. Framework-wise it supports the cosmogenesis ledger's domain bookkeeping, not the T5–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.