zFiber_cost_eq
plain-language theorem explainer
Separable coarsening along z for a 3D grid equals total z-interface plus the number of z-fibers (the x-y cross-section). Cosmologists and RS auditors cite this as the per-axis backbone of the 3D surface law and of depth-independence. The proof is a one-line application of the 2D row-wise identity to the flattened z-fiber list, under the nonempty-fiber hypothesis.
Claim. For any 3D grid $G$ whose every $z$-fiber is nonempty, the separable coarsening cost along $z$ equals the total $z$-interface plus the number of $z$-fibers: $\mathrm{cost}_z(G) = I_z(G) + N_{xy}(G)$, where $N_{xy}(G)$ is the $x$-$y$ cross-sectional cell count (independent of fiber lengths).
background
This module lifts locked-domain coarsening into three dimensions, the spatial dimension forced by T8. A locked domain is a maximal 6-connected equal-charge component, carried as one coarse super-region; the recognition-active interface is a 2D surface, so engine cost should localize to a surface rather than the volume.
Model a 3D field as a list of planes of 1D fibers, indexed $[x][y][z]$. The list of all $z$-fibers is the double flatten of the grid: each fiber is the charge column at fixed $(x,y)$. The 1D run count runs is the number of maximal equal-charge blocks on a fiber (one super-region per locked domain along that axis). Summing runs over fibers gives the separable cost; summing adjacent distinctions gives the total $z$-interface.
Upstream, the 2D theorem states that for any list of nonempty rows, separable cost equals horizontal interface plus row count: the exact sum of the 1D law $\mathrm{runs} = \mathrm{boundaries} + 1$. The present result is that identity applied to the flattened $z$-fiber list.
proof idea
One-line term wrapper. Apply the 2D row-wise equality to the list of $z$-fibers, discharging the nonempty-row hypothesis with the lemma that every $z$-fiber of a grid satisfying the plane/fiber nonempty assumption is nonempty. No further induction or arithmetic is local to this proof; all content lives in the 2D identity and the nonempty-fiber fact.
why it matters
This is the exact per-axis generalization of the 1D law $\mathrm{runs} = \mathrm{boundaries} + 1$ summed over every fiber of a 3D grid, and the backbone of the 3D surface law in the dimension T8 selects ($D = 3$). 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.
Downstream, depth-independence is the direct corollary (same interface and same fiber count imply same cost). The Phase-15 foam law uses it to show that, at fixed cross-section, strictly more $z$-interface strictly raises separable cost: the engine pays for recognition activity, not volume. True 3D component coarsening also merges across fibers, so it carries at most this many super-regions; together with the volume upper bound from runs-versus-length, cost is bracketed between cross-section and volume and pinned to the interface. Composed with the resolution-work bound (cadence-independent of index type), both state and work of the 3D engine sit on the surface, not in $V$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.