LNALField
plain-language theorem explainer
LNALField is the type of spatial states realized as arrays of LNAL voxels, each voxel a product of Reg6 register state and Aux5 auxiliary data. Fluid modelers working in the Recognition Science to Navier-Stokes bridge cite it as the discrete carrier for executing LNAL programs over fields. The declaration is a one-line type alias with no computation or additional axioms.
Claim. Let $LNALField$ denote the type of arrays whose elements are voxels, where each voxel is the product of a 6-register state $Reg6$ and a 5-auxiliary state $Aux5$ drawn from the LNAL virtual machine.
background
The fluids bridge module supplies a minimal spatial interface on top of the single-voxel LNAL core. Spatial state is realized as an array of voxels, each voxel the pair $(Reg6, Aux5)$ taken directly from the LNAL.VM definitions. This choice keeps the bridge independent of any experimental multi-voxel infrastructure while still allowing one-step updates driven by an LProgram.
proof idea
The declaration is a direct type abbreviation that aliases Array over the sibling LNALVoxel definition. No lemmas, tactics, or reductions are invoked; the body simply re-exports the voxel product type.
why it matters
LNALField supplies the spatial state type required by SpatialSemantics.step and the run iterator, which in turn feed the RSNSBridgeSpec structure and the Galerkin encoders encodeGalerkin2D and encodeIndex. It therefore closes the spatial layer of the LNAL-to-fluids bridge while inheriting the phi-forcing and spectral-emergence structures from upstream ledger factorization and Q3 emergence. The definition touches the open question of how discrete voxel steps converge to continuous fluid equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.