zFibers_nonempty
plain-language theorem explainer
If every 1D fiber in every plane of a 3D charge grid is nonempty, then every z-fiber of the flattened grid is nonempty. Cosmology proofs that apply the 1D run/boundary identity fiberwise cite this as the nonempty hypothesis transfer. The argument is a short membership chase through list flatten.
Claim. Let $G$ be a 3D grid of charge lists, written as a list of planes, each a list of $z$-fibers. If every fiber of every plane is nonempty, then every member of the flattened list of all $z$-fibers is nonempty.
background
The module develops separable (per-axis) domain coarsening in three dimensions, the spatial dimension forced by the Recognition chain (T8 / D = 3). A 3D charge field is modeled as List (List (List α)) indexed $[x][y][z]$. The $z$-fibers are the charge columns at fixed $(x,y)$: the definition zFibers is simply the double flatten of the grid, so each entry is one 1D fiber along $z$.
Along each fiber the engine counts maximal equal-charge runs (runs) and forced distinctions (boundaries). The 1D identity is runs = boundaries + 1 only for nonempty lists; empty fibers would break the count. The hypothesis here is the natural planewise nonempty assumption on the nested lists; the conclusion is the same statement on the flattened fiber list that later cost lemmas consume.
Module context: the separable $z$-cost equals total $z$-interface plus cross-sectional fiber count, independent of fiber depth, and is the per-axis backbone of the 3D surface law.
proof idea
Tactic proof, four steps. Introduce a fiber $f$ and a membership hypothesis $f \in \mathrm{zFibers}(G)$. Unfold zFibers to grid.flatten and rewrite membership via List.mem_flatten, obtaining a plane in the grid that contains $f$. Discharge by the given planewise nonempty hypothesis on that plane and fiber. No auxiliary lemmas beyond list membership.
why it matters
Feeds zFiber_cost_eq, the main 3D separable cost identity: for grids with all $z$-fibers nonempty,
rowCost(zFibers G) = rowInterface(zFibers G) + length(zFibers G).
That theorem is a one-line application of the rowwise 1D law, and it needs exactly this nonempty transfer. The identity is the per-axis generalization of runs = boundaries + 1 and the backbone of the claim that coarsening cost lives on a surface, not in the volume: deepening the world in $z$ does not raise carried cost. In the broader framework this supports the T8 ($D=3$) cosmogenesis picture where locked domains are 6-connected equal-charge components and recognition work localizes to a 2D interface scaling like $V^{2/3}$. True 3D component coarsening merges across fibers and is at most this separable cost; the present lemma is only the nonempty gate for the separable side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.