of
plain-language theorem explainer
Definitional instance in the 3D domain-coarsening module that wires the ambient typeclass data for charge grids with decidable equality. Cosmology and forcing-chain readers cite the surrounding module for the surface-vs-volume cost law in D = 3. There is no proof body: it is pure instance packaging consumed by the fiber and foam lemmas.
Claim. On a type $\alpha$ of charges with decidable equality, the 3D coarsening setup is available as an instance: a field is a list of planes of $z$-fibers (type $\mathrm{List}(\mathrm{List}(\mathrm{List}\,\alpha))$, indexed $[x][y][z]$), and the separable cost infrastructure (run counts, row cost, row interface) applies fiberwise along $z$.
background
The module treats locked domains in the dimension selected by the forcing chain (T8 / AlphaDerivation: $D = 3$). A locked domain is a maximal equal-charge region; the recognition-active interface is a 2D surface, so engine cost should localize to that surface rather than the volume.
Upstream 1D and 2D primitives are reused. runs counts maximal equal-charge blocks on a 1D fiber (each locked block costs one super-region). rowCost sums runs over a list of fibers; rowInterface sums the within-fiber boundaries. Flattening the $x$ and $y$ levels yields the list of all $z$-fibers, so the same separable cost applies in 3D along one axis.
The exact 1D identity $\mathrm{runs} = \mathrm{boundaries} + 1$ becomes, in higher D, an inequality on monochromatic components versus bichromatic edges. The dimension-free graph fact lives in InterfaceComponentBound; this module's clean content is the separable per-axis cost and its depth independence.
proof idea
No tactic or term proof: claim status is definitional instance packaging (def_or_abbrev style, zero body lines). It supplies the typeclass/ambient data (decidable equality on charges, 3D list-of-planes grid shape) so that sibling lemmas can quote rowCost, rowInterface, and runs on grid.flatten without repeating setup. Downstream reasoning in the module is carried by the real theorems (zFiber_cost_eq, zFiber_cost_le_volume, foam_cost_tracks_interface), not by this instance.
why it matters
Sits at the entry of Cosmology.DomainCoarsening3D, the Lean backing for the 3D locked-domain coarsener and the Phase-15 recognition-foam picture. The forcing chain fixes $D = 3$; here the engine is told how to see a 3D charge field so that cost can be proved to live on the interface.
Parent results in-module (not external used_by edges) are the depth-free identity rowCost(zFibers) = rowInterface(zFibers) + |zFibers|, the volume bracket, and foam_cost_tracks_interface: at fixed cross-section, strictly more $z$-interface yields strictly more separable cost, while changing only fiber length is free. Composed with RecognitionWorkBound (cadence-bounded resolution cost, index-type independent), state and work stay interface-bounded, not volume-bounded. That is the sub-extensive $\sim V^{2/3}$ surface law endpoint in the dimension reality has.
No external consumers are recorded yet; the instance is local scaffolding for those 3D cost theorems and the numeric foam driver they upper-bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.