mono_le_interface_succ
plain-language theorem explainer
On the 2D diamond lattice of any radius, any vertex colouring has at most one more monochromatic 4-connected component than there are bichromatic edges. Domain-coarsening and cosmogenesis arguments cite this as the locked-domain bound the 2D engine needs at every radius. The proof is a one-line specialisation of the descent-based interface lemma to the diamond's L1 height, unique centre, and neighbour-descent facts.
Claim. For every radius $t\in\mathbb{N}$ and every colouring $c$ of the vertices of the 2D L1 diamond $|x|+|y|\le t$ by a type with decidable equality, the number of connected components of the monochromatic 4-neighbour graph is at most the number of bichromatic edges plus one: $\mathrm{comp}(E_{\mathrm{mono}})\le |E_{\mathrm{bi}}|+1$.
background
This module closes a connected-graph fact left open in the 2D/3D domain-coarsening scripts: locked monochromatic domains are at most the bichromatic interface size plus one. In 1D the identity is exact (runs = boundaries + 1); in higher dimensions multiply-connected interfaces force the inequality. Component count is the cardinality of the quotient by equivalence closure of the monochromatic edge relation on a finite vertex type.
The 2D diamond of radius $t$ is the L1 ball $|x|+|y|\le t$ carved from a bounding box Finset, with 4-neighbour adjacency (L1 distance exactly one). Vertices are lattice points in that ball. Height is the L1 norm; the unique zero-height vertex is the origin. From every off-centre vertex there is a 4-neighbour of strictly smaller height.
Ambient connectivity is discharged by the reusable criterion that a finite world with a height function, a unique zero, and a descent edge from every other cell is one component. That criterion is the recognition pull toward the coarsest description, read as graph connectivity.
proof idea
One-line wrapper. Applies the general descent-based interface bound to the diamond edge list, the given colouring, L1 height, the origin as centre, the unique-zero lemma, and the neighbour-descent lemma.
That general result reconstructs the connected ambient graph by re-adding bichromatic edges to the monochromatic graph: each added edge merges at most two components (atomic merge bound, iterated over the interface), and the ambient endpoint is a single component by the descent criterion. No further diamond-specific algebra is needed beyond feeding those five witnesses.
why it matters
Gives the exact locked-domain bound on the lattice the 2D engine runs on, for every radius, with zero sorry. Previously the count was only numeric-discharged each cycle; here it is a theorem. It instantiates the module headline (monochromatic components ≤ bichromatic edges + 1) after connectivity is discharged by L1 descent.
Downstream it is consumed in PolarizedBirthInterface (including spine analysis of bichromatic endpoints). The same pattern yields the 3D octahedron bound under six-neighbour adjacency, aligning with the forced spatial dimension D = 3. Together these close the open interface-component gap in the cosmogenesis coarsening bridges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.