voxelStep
plain-language theorem explainer
voxelStep supplies the atomic one-voxel transition that executes a single wrapped LNAL step on a (Reg6 × Aux5) pair and returns the updated pair. Workers on the LNAL-to-Galerkin bridge cite it when building spatial maps or proving commutation with discrete Fourier steps. The definition is a direct three-line wrapper that initializes an augmented LState, advances it via lStep, and projects the registers back out.
Claim. Let $P$ be an LNAL program and let $v = (r_6, a_5)$ be a voxel of type Reg6 × Aux5. Then voxelStep$(P, v)$ equals $(s_1.reg6, s_1.aux5)$, where $s_0 :=$ init$(r_6, a_5)$ and $s_1 :=$ lStep$(P, s_0)$.
background
LNALVoxel is the abbreviation Reg6 × Aux5. LState wraps the base LNAL state with a monotone window counter and J-budget accumulator that increments every eight ticks. lStep is the wrapped small-step that preserves legacy semantics while updating the window index on boundary crossings. init constructs an LState from legacy registers with zeroed window fields. The module supplies minimal spatial semantics for running LNAL programs over an LNALField (an array of voxels) with no neighbor graph or coupling, as part of milestone M2 for encoding 2D Galerkin states.
proof idea
Direct definition that composes LState.init on the input voxel, applies lStep to the resulting augmented state, and projects the reg6 and aux5 fields back to the voxel type.
why it matters
It supplies the atomic step used by the independent spatial semantics (which maps voxelStep over an entire field) and by the SimulationHypothesis structure that requires one LNAL spatial step to commute with a discrete Galerkin step. The declaration therefore closes the minimal encoding leg of the M2 milestone that bridges LNAL voxels to Galerkin2D coefficients without neighbor interactions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.