LNALVoxel
plain-language theorem explainer
LNALVoxel is the type of one LNAL voxel, formed as the product of a Reg6 register and an Aux5 auxiliary state. Fluids-bridge authors cite it when building spatial fields or one-step voxel updates. The declaration is a direct type abbreviation with no further content.
Claim. $LNALVoxel := Reg_6 × Aux_5$, where $Reg_6$ and $Aux_5$ are the register and auxiliary types supplied by the LNAL virtual machine.
background
The LNAL core supplies a single-voxel virtual machine whose states are built from Reg6 and Aux5. The fluids bridge requires a spatial semantics over an entire field of such voxels while remaining separate from experimental multi-voxel infrastructure. LNALVoxel therefore packages the state of one voxel as the ordered pair (Reg6, Aux5).
proof idea
Direct type abbreviation that aliases the product IndisputableMonolith.LNAL.Reg6 × IndisputableMonolith.LNAL.Aux5.
why it matters
LNALVoxel is the atomic unit for LNALField (an array of voxels) and is used by voxelStep, encodeIndex, decodeCoeff, and the fold lemmas that implement one-step LNAL execution on Galerkin coefficients. It supplies the minimal spatial interface that lets the fluids bridge evolve voxels independently under LProgram steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.