voxelStep_listenNoopProgram
plain-language theorem explainer
The lemma establishes that the voxel-step operator applied to the listen-noop program acts as the identity on any LNAL voxel. Researchers formalizing minimal LNAL execution semantics or Galerkin encodings would cite it to discharge trivial cases during simplification. The proof reduces directly by unpacking the voxel pair and invoking simplification on the definitions of voxelStep, listenNoopProgram, and lStep.
Claim. For any voxel $v = (r_6, a_5)$ of type Reg6 × Aux5, executing the constant listen-noop program via the one-voxel step operator returns the original voxel unchanged.
background
LNALVoxel is defined as the product type Reg6 × Aux5. listenNoopProgram is the constant LProgram that maps every instruction pointer to a LISTEN noop instruction. voxelStep initializes an LState from the voxel registers, applies the wrapped small-step lStep, and projects the resulting Reg6 and Aux5 components back out. The module supplies minimal spatial semantics for LNAL programs over an array of such voxels, with no neighbor graph or coupling yet; it also encodes 2D Galerkin Fourier states into this voxel representation. Upstream lStep wraps the base LNAL step while tracking window indices and boundary conditions.
proof idea
The proof performs rcases to split the voxel into its Reg6 and Aux5 fields, then applies simp using the definitions of voxelStep, listenNoopProgram, and lStep; the reduction is immediate and yields the original voxel.
why it matters
This simp lemma anchors the base case for the trivial program inside the LNAL spatial semantics layer. It supports simplification in any downstream argument that invokes voxelStep on listenNoopProgram before neighbor interactions or full Galerkin encoding are introduced. The declaration closes a basic identity in the minimal execution model that precedes coupling and classical fluid bridging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.