rowwise_cost_eq
plain-language theorem explainer
For any 2D grid of nonempty rows, the separable (row-wise) coarsening cost equals the total horizontal interface plus the number of rows. Cosmologists and lattice-engine auditors cite it for a perimeter-style upper bound on carried super-regions that ignores area. The proof is induction on the row list, applying the 1D law runs = boundaries + 1 on each nonempty row and summing.
Claim. Let the 2D field be a list of rows, each a nonempty finite list of cell labels. Write $C$ for the sum over rows of the number of monochromatic runs in that row, and $I$ for the sum over rows of the number of horizontal boundaries in that row. Then $C = I + N$, where $N$ is the number of rows.
background
This module lifts locked-domain coarsening from the line to a 2D world modeled as List (List α). A locked domain is a maximal 4-connected equal-charge component; the recognition-active interface is a 1D curve, so engine cost should localize to a perimeter rather than area.
In 1D the exact identity is runs = boundaries + 1 on any nonempty list (the row lemma runs_eq_of_ne_nil). Here rowCost is the sum of runs over rows (separable super-region count when each row is coarsened independently), and rowInterface is the sum of boundaries over rows (total horizontal forced distinctions). The true 2D component count also merges vertically, so it is at most this separable cost; the module's headline is the exact separable identity.
Upstream, the cons-unfolding lemmas rowCost_cons and rowInterface_cons reduce both sides to a head row plus the tail sum, and the 1D law supplies one extra super-region per nonempty row.
proof idea
Induction on the list of rows. The empty case is immediate by simp (both sides zero). For r :: rs, rewrite with rowCost_cons and rowInterface_cons, then apply runs_eq_of_ne_nil on the head using the nonempty hypothesis. The inductive hypothesis handles the tail under the restricted membership premise. Finish with List.length_cons and a one-line ring identity: boundaries r + 1 + (rowInterface rs + rs.length) = boundaries r + rowInterface rs + (rs.length + 1).
why it matters
This is the clean proved content of the 2D coarsening module: the exact per-axis lift of the 1D law runs = boundaries + 1, summed over rows. Downstream, rowwise_cost_independent_of_width is a named restatement emphasizing that the cost depends only on interface and row count, never on row widths (area). The 3D module reuses it verbatim as zFiber_cost_eq on the list of z-fibers, giving the surface-law backbone: deeper fibers do not raise the separable carried cost.
In the cosmogenesis engine story, composing with the resolution-work bound (cost per cadence independent of the index type) yields state and work both controlled by interface, not volume. True 2D components merge vertically as well, so components ≤ rowCost; the harder graph fact mono_components_le_bichromatic_succ (components ≤ bichromatic edges + 1 on connected worlds) sits alongside as the dimension-free merge bound. No T0–T8 forcing step is discharged here; the landmark is the sub-extensive coarsening cost that keeps the 2D/3D recognition engine perimeter-bounded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.