voxelStep
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not model neighbor interactions or spatial coupling between voxels.
- Does not enforce global conservation or thermodynamic constraints beyond single-step register updates.
- Does not perform Galerkin encoding or decoding of coefficients.
- Does not expose the full window budgeting state to the caller.
Lean usage
field.map (voxelStep P)formal statement (Lean)
26def voxelStep (P : LProgram) (v : LNALVoxel) : LNALVoxel :=
proof body
Definition body.
27 let s0 : LState := LState.init v.1 v.2
28 let s1 : LState := lStep P s0
29 (s1.reg6, s1.aux5)
30
31/-- Minimal spatial semantics: voxels evolve independently (no neighbor interaction yet). -/