voxelStep
plain-language theorem explainer
voxelStep defines the atomic update that applies one LNAL program step to a single voxel consisting of a Reg6 register tuple and Aux5 auxiliary state. Workers on the LNAL-to-Galerkin bridge cite it as the building block for spatial field evolution. The definition initializes an LState wrapper, invokes the wrapped lStep, and projects the resulting registers back to voxel form.
Claim. For an LNAL program $P$ and voxel $v = (r_6, a_5)$, the map returns the registers and auxiliary values after initializing the VM state from $v$, executing one wrapped step of $P$, and extracting the updated components.
background
The LNALSemantics module supplies minimal spatial semantics for LNAL programs acting on an LNALField (an array of voxels) together with an encoding of 2D Galerkin Fourier states into those voxels; the setting is deliberately local with no neighbor graph or inter-voxel coupling. LNALVoxel is the product type Reg6 × Aux5. LState augments the legacy LNAL state with a monotone window counter and J-budget accumulator that increments every eight ticks. The upstream lStep wraps the legacy small-step while preserving its semantics and updating the window index on boundary crossings.
proof idea
One-line definition: initialize LState from the voxel components via init, apply lStep to the program and state, then return the pair of updated reg6 and aux5 fields.
why it matters
voxelStep supplies the step function inside the independent SpatialSemantics, which in turn supports the SimulationHypothesis that one LNAL spatial step commutes with the discrete Galerkin map. It fills the M2 milestone for minimal spatial semantics and the explicit Galerkin-to-voxel encoding. The window tracking inside the underlying LState links directly to the eight-tick octave of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.