rowInterface
plain-language theorem explainer
The total horizontal interface of a 2D charge grid is the sum, over every row, of adjacent charge mismatches in that row. Cosmology and Recognition-Science auditors cite it when bounding separable coarsening cost by perimeter rather than area. The definition is a one-line map-and-sum of the 1D boundary count.
Claim. For a 2D grid given as a list of rows $(r_i)$, the total horizontal interface is $\sum_i B(r_i)$, where $B(r)$ is the number of positions at which consecutive entries of row $r$ carry unequal charges.
background
In the 1D coarsening module, boundaries counts forced distinctions: adjacent list entries with different charges. Within a locked domain of equal charge there is no distinction. For nonempty 1D lists the identity runs = boundaries + 1 holds exactly, because a 1D interface between domains is a single point.
This module lifts locked-domain coarsening to two dimensions by modeling a field as a list of rows. Separable (row-wise) coarsening treats each row independently: the total number of 1D super-regions is the sum of runs over rows, and the total horizontal interface is the sum of boundaries over rows. True 2D components also merge vertically, so they never exceed the separable count. The module's headline identity then rewrites that count as horizontal interface plus number of rows, independent of row widths (area).
proof idea
One-line definition: apply the 1D boundaries function to every row via list map, then sum the resulting naturals. No separate proof body; the equation is the definition.
why it matters
This quantity is the interface half of the separable cost law. Downstream, rowInterface_cons and rowInterface_nil feed the induction in rowwise_cost_eq, which states that for grids with nonempty rows the separable cost equals horizontal interface plus row count; the width-independence corollary is the same identity under a clearer name. DomainCoarsening3D reuses it on z-fibers so foam_cost_tracks_interface can assert that a finer domain-wall structure costs strictly more while changing fiber depth at fixed interface costs nothing. Composed with RecognitionWorkBound (resolution cost bounded by cadence, independent of index type), the 2D engine's state and work are pinned to the interface, not the area, matching the cosmogenesis domain-coarsen script and the sub-extensive perimeter picture in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.