rowInterface_cons
plain-language theorem explainer
The total horizontal interface of a 2D grid, written as a cons of rows, splits as the boundary count of the head row plus the interface of the tail. Anyone proving the separable row-wise coarsening identity cites this. The proof is a one-line simplification of the sum-of-mapped-boundaries definition.
Claim. For any row $r$ and any list of rows $rs$, the total horizontal interface of the grid $r :: rs$ equals the number of forced adjacent distinctions in $r$ plus the total horizontal interface of $rs$: $\mathrm{rowInterface}(r :: rs) = \mathrm{boundaries}(r) + \mathrm{rowInterface}(rs)$.
background
This module lifts locked-domain coarsening from the line to a 2D grid modeled as List (List α). A locked domain is a maximal equal-charge run; the recognition-active interface is the set of adjacent unequal charges. In 1D, boundaries counts those forced distinctions along a row, and runs counts the coarse super-regions.
The 2D separable quantities are defined by summing the 1D ones over rows: rowInterface is (rows.map boundaries).sum, the total horizontal interface, and rowCost is the analogous sum of runs. The module headline is that, for nonempty rows, separable cost equals horizontal interface plus row count, the exact per-axis lift of the 1D law runs = boundaries + 1.
Upstream, boundaries is the recursive count of adjacent unequal charges (zero on empty or singleton lists). The present lemma is the cons-case unfolding of the sum that defines rowInterface.
proof idea
One-line wrapper: simp [rowInterface]. Unfolding the definition replaces rowInterface (r :: rs) by the sum of boundaries over r :: rs, which is definitionally boundaries r + (rs.map boundaries).sum, i.e. boundaries r + rowInterface rs.
why it matters
Feeds the induction step of rowwise_cost_eq, the module headline: for any grid of nonempty rows, rowCost = rowInterface + rows.length. That identity is the exact per-axis generalization of the 1D law runs = boundaries + 1, and it depends only on horizontal interface and row count, never on row widths (area).
In the Recognition cosmology stack this supplies a fully proved upper bound on separable 2D coarsening cost. True 2D component coarsening also merges vertically, so it carries at most this many super-regions. Composed with the resolution-work bound (cadence-independent of the index type), the 2D engine's state and work localize to the interface, not the area: the sub-extensive perimeter cost that the cosmogenesis scripts rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.