voxelStep
plain-language theorem explainer
voxelStep supplies the atomic one-voxel update rule that executes an LNAL program on a single (Reg6, Aux5) pair. Researchers building discrete fluid simulations or proving commutation between LNAL steps and Galerkin coefficient maps cite it when assembling spatial semantics. The definition is a direct wrapper that initializes an augmented VM state, applies one wrapped program step, and projects the resulting registers.
Claim. Let $P$ be an LNAL program and let $v=(r_6,a_5)$ be a voxel in $Reg_6×Aux_5$. Define voxelStep$(P,v)$ to be the pair $(s_1.reg_6,s_1.aux_5)$, where $s_0$ is the LState obtained by initializing from $r_6$ and $a_5$, and $s_1$ is the result of applying one step of $P$ to $s_0$.
background
LNALVoxel is the type alias Reg6 × Aux5 that carries the minimal state of each spatial cell. LState is the VM wrapper that augments the legacy LNAL state with monotone window counters for vNext budgeting. The init constructor builds an LState from legacy registers, while lStep performs a single wrapped execution that preserves legacy semantics and updates window indices on eight-tick boundaries.
proof idea
The definition is a direct one-line wrapper: it calls LState.init on the two components of the input voxel, feeds the result to lStep, and returns the updated (reg6, aux5) pair.
why it matters
voxelStep is the primitive building block for the independent spatial semantics map, which in turn supports the SimulationHypothesis that one LNAL spatial step exactly reproduces one discrete Galerkin step. It supplies the minimal spatial semantics required by milestone M2 in the classical bridge to fluids, relying on the J-descent iteration from the Second Law module and the window-tracked VM state from the core VM layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.