zFibers
plain-language theorem explainer
Extracts every one-dimensional z-column from a three-dimensional charge grid by flattening the outer two list levels. Cosmology proofs that bound separable coarsening cost by interface plus cross-section cite this projection. The body is the standard list flatten, so the fibers are exactly the charge runs at fixed (x,y).
Claim. Given a 3D grid $G$ as a nested list indexed $[x][y][z]$, the collection of all $z$-fibers is the list of 1D columns obtained by flattening the $x$ and $y$ levels. Each fiber is the charge sequence along $z$ at a fixed lattice site $(x,y)$.
background
The module treats locked domains in three spatial dimensions (the dimension forced by T8 of the unified forcing chain). A 3D field is modeled as List (List (List α)) with indices $[x][y][z]$: outer lists are planes, middle lists are rows of fibers, and the innermost lists are the charge columns along $z$.
Coarsening along an axis collapses each fiber into maximal equal-charge runs. The separable (per-axis) cost is the sum of those run counts over all fibers. To state that cost, one first needs the flat list of every $z$-fiber. That list is exactly the double flatten of the outer two levels: every charge column at fixed $(x,y)$ appears once.
The 2D predecessor module already used the same flatten pattern for rows; here it is lifted one dimension so that later identities can quote the 1D law runs = boundaries + 1 fiberwise and sum.
proof idea
Pure definition: the body is grid.flatten, which concatenates the list of planes into a single list of fibers. No lemmas are applied. Downstream simp lemmas (zFibers_nil) and nonempty transport (zFibers_nonempty) unfold this equality and rewrite with List.mem_flatten.
why it matters
This projection is the data spine for the 3D surface-cost story. zFiber_cost_eq rewrites separable cost as total $z$-interface plus number of $z$-fibers (the $x$-$y$ cross-section), independent of fiber lengths. zFiber_cost_depth_independent and foam_cost_tracks_interface compare two grids at fixed cross-section and show cost tracks interface, not depth or volume: the Phase-15 recognition-foam claim. zFiber_cost_le_volume brackets the cost between cross-section and volume, giving the sub-extensive $\sim V^{2/3}$ surface scaling once true 3D components merge across fibers.
Together these feed the claim that recognition work in $D=3$ localizes to the interface surface, matching the forcing-chain selection of three spatial dimensions and the engine bound from RecognitionWorkBound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.