foam_cost_tracks_interface
plain-language theorem explainer
At fixed x-y cross-section (equal number of z-fibers), a 3D grid with strictly more z-interface carries strictly more separable coarsening cost. Cosmologists and RS auditors cite this as the Phase-15 foam law: finer multi-domain structure costs more than a coarser one of the same extent. The proof rewrites both sides via the depth-independent cost identity and finishes by linear arithmetic.
Claim. Let $g_1,g_2$ be 3D grids (lists of planes of nonempty z-fibers). If the flattened z-fiber lists have equal length and the total z-interface of $g_1$ is strictly less than that of $g_2$, then the separable coarsening cost of $g_1$ is strictly less than that of $g_2$: $\mathrm{rowCost}(z\mathrm{Fibers}(g_1)) < \mathrm{rowCost}(z\mathrm{Fibers}(g_2))$.
background
This module formalizes separable coarsening cost in three dimensions, the dimension forced by T8 of the UnifiedForcingChain. A 3D field is modeled as List (List (List α)) indexed $[x][y][z]$. The z-fibers are the charge columns at fixed $(x,y)$, obtained by flattening the outer two levels. Each fiber is coarsened into maximal equal-charge runs.
From the 2D layer, rowCost is the sum of run counts over a list of 1D rows (total separable super-regions), and rowInterface is the sum of within-row boundaries (total forced distinctions). The key upstream identity zFiber_cost_eq states that for any grid with nonempty fibers, rowCost(zFibers(grid)) = rowInterface(zFibers(grid)) + (zFibers(grid)).length. The right-hand side depends only on interface and cross-section, never on fiber lengths: deepening the world in $z$ does not raise carried cost.
The module thesis is that recognition cost lives on a surface, not in the volume. True 3D component coarsening merges across fibers as well, so it is bounded above by this separable cost and pinned to the interface.
proof idea
Term-mode proof in three steps. Rewrite the left cost by zFiber_cost_eq g₁ h₁ and the right by zFiber_cost_eq g₂ h₂, so each side becomes interface plus fiber count. Substitute the hypothesis that the two z-fiber lists have equal length (hcross). The goal reduces to comparing two sums that share the same additive constant; the strict interface inequality then yields the strict cost inequality by omega.
why it matters
This is the strict companion to depth-independence and the formal Phase-15 multi-domain ("recognition foam") claim: at fixed cross-section, strictly more z-interface costs strictly more. A finely recognized foam with more domain walls is strictly more expensive to carry than a coarser structure of the same extent, while changing fiber lengths with interface fixed changes nothing (zFiber_cost_depth_independent). The engine pays for recognition activity, not volume.
It feeds the module's packaging instance of and sits inside the 3D surface-law backbone: separable cost scales with interface plus cross-section, true components are at most that cost, and composed with RecognitionWorkBound both state and work stay interface-bounded. Framework landmark: T8 forces $D=3$, so the recognition-active interface is a 2D surface and a single domain of volume $V$ is carried at cost $\sim V^{2/3}$, the sharpest sub-extensive scaling. The remaining open wiring is identifying flood-fill components with the 6-neighbour lattice graph for the full component bound; the separable foam law itself is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.