rowInterface_nil
plain-language theorem explainer
The total horizontal interface of an empty list of rows is zero. Anyone simplifying separable 2D coarsening costs on grids written as lists of rows needs this base case. The proof is pure definitional equality: the sum of boundary counts over the empty list is zero by reflexivity.
Claim. For any type $\alpha$, the total horizontal interface of the empty collection of rows is zero: if $I$ denotes the sum of within-row boundary counts, then $I([]) = 0$.
background
This module treats a 2D charge field as a list of rows (List (List α)). Locked domains are maximal equal-charge components; the recognition-active cost localizes to interfaces. The separable (row-wise) model coarsens each row independently in 1D.
The total horizontal interface is defined as the sum, over rows, of the forced distinctions within each row: map each row to its 1D boundary count and sum. That is the quantity whose empty-list value is fixed here. The companion total row cost is the sum of 1D run counts over rows.
The module headline is the exact identity that, for nonempty rows, total row cost equals total horizontal interface plus the number of rows: the per-axis lift of the 1D law runs = boundaries + 1. Empty-list base cases anchor the simp normal form for those sums.
proof idea
One-line definitional proof. Unfold the interface as the sum of the list of per-row boundary counts; the empty list maps to the empty list of naturals, whose sum is definitionally 0, so rfl closes.
why it matters
Base case for the horizontal-interface accumulator in separable 2D coarsening. Together with the cons recurrence and the matching cost lemmas, it supports the proved identity that row-wise cost equals horizontal interface plus row count, independent of row widths (area).
That identity supplies a fully discharged upper bound on true 2D component cost (vertical merges only reduce the count) in terms of interface plus row count. Composed with the recognition-work bound (resolution cost per cadence independent of index type), the 2D engine's state and work stay interface-bounded, not area-bounded: the cosmogenesis story that perimeter, not volume, drives cost.
No downstream uses are wired yet in the graph; the lemma is infrastructure for the row-wise simp set and for any induction on the list of rows.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.