of
plain-language theorem explainer
Packages the one-dimensional locked-domain cost law at row level: a nonempty charge row coarsens into exactly (horizontal interfaces) + 1 super-regions. Cosmology and domain-coarsening arguments cite it when lifting the 1D identity into separable 2D row sums. As an instance/definition it is pure wiring of that identity for the 2D module, with no separate proof body.
Claim. For a nonempty row $r$ of charges (with decidable equality), the number of maximal equal-charge runs equals the number of adjacent charge changes plus one: $\mathrm{runs}(r)=\mathrm{boundaries}(r)+1$. Equivalently, independent row coarsening of a nonempty row carries exactly one super-region more than its horizontal interface count.
background
The ambient setting is two-dimensional locked-domain coarsening: a locked domain is a maximal equal-charge region, carried as one coarse super-region, so recognition cost should localize to interfaces rather than area. The parent 1D module defines two list functionals on a charge field. boundaries counts forced distinctions (adjacent positions with unequal charge). runs counts maximal equal-charge runs, i.e. the super-regions the coarsening engine carries; a locked block of any length counts once.
In one dimension those functionals obey the exact identity $\mathrm{runs}=\mathrm{boundaries}+1$ on nonempty lists, because a 1D interface is a single cut point. The 2D module models a grid as List (List α) and builds separable (row-wise) cost by summing the 1D functionals over rows: total separable cost is the sum of runs, total horizontal interface is the sum of boundaries.
The module doc stresses that full 2D component counting also merges vertically and is controlled by a dimension-free connected-graph bound (monochromatic components $\le$ bichromatic edges $+1$). What this module proves cleanly is the separable row law, which needs the 1D identity available as a row lemma.
proof idea
Definitional instance with an empty separate proof body: it exposes the 1D nonempty-row cost identity in the 2D namespace so row-wise lemmas can rewrite with it. Upstream, runs and boundaries are the recursive list functionals from DomainCoarsening; the identity they satisfy on nonempty rows is the fact being wired. Downstream row induction (as in the headline separable cost theorem) applies this at the head row, then uses the cons lemmas for separable cost and interface and inducts on the tail.
why it matters
Without the row-level 1D law, the separable 2D identity cannot close. The headline result of the module states that for any grid of nonempty rows, separable coarsening cost equals total horizontal interface plus number of rows: an exact per-axis sum of $\mathrm{runs}=\mathrm{boundaries}+1$. True 2D flood-fill also merges across rows, so the component count is at most that separable cost, yielding a fully proved upper bound on carried 2D state in terms of horizontal interface and row count, independent of row widths (area).
Composed with the recognition work bound (resolution cost per cadence cycle bounded by cadence, independent of index type), both 2D engine state and work are interface-bounded rather than area-bounded. That is the cosmogenesis point of the 2D coarsening scripts: active cost lives on a 1D perimeter curve. The fuller graph-theoretic component bound under edge deletion lives in the interface-component module; wiring the diamond lattice as a connected ambient instance is recorded there as routine. Spatial $D=3$ from the forcing chain is the physical ambient dimension; this file is the 2D separable slice used to control planar sections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.