independent_step_listenNoopProgram
plain-language theorem explainer
The lemma establishes invariance of any LNAL field under the independent spatial semantics when the program is the trivial listen-noop variant. Workers on minimal LNAL execution models for fluid discretizations cite it as the base invariance case before adding coupling. The proof reduces the claim to an array identity map after unfolding the independent definition and simplifying the voxel step.
Claim. Let $F$ be an LNAL field (an array of voxels). Then the step operation of the independent spatial semantics applied to the listen-noop program on $F$ returns $F$ unchanged.
background
The LNALSemantics module supplies a minimal spatial semantics for executing LNAL programs over an LNALField, defined as an Array of LNALVoxel pairs (Reg6, Aux5). The independent semantics is the SpatialSemantics whose step function maps each voxel independently via voxelStep, with no neighbor graph or coupling. The listenNoopProgram is the constant LProgram that issues LInstr.listen ListenMode.noop at every index. voxelStep initializes an LState from the voxel, applies lStep under the program, and extracts the updated registers. This setup is explicitly minimal, as stated in the module documentation, and precedes the Galerkin2D encoding section.
proof idea
The proof is a one-line tactic wrapper. It unfolds the independent definition to expose the array map of voxelStep listenNoopProgram, then invokes Array.map_id'' after a local simp that shows voxelStep listenNoopProgram acts as the identity on each voxel.
why it matters
The result supplies the invariance base case for the noop program inside the minimal LNAL spatial semantics of the ClassicalBridge.Fluids layer. It supports the M2 milestone by confirming that the listen-noop program induces no change, which is a prerequisite for later encoding steps from Galerkin2D. No direct downstream uses are recorded, but the simp attribute indicates it is intended for rewriting in larger LNAL execution arguments. It sits outside the core T0-T8 forcing chain and RCL but provides the classical semantics bridge needed to connect LNAL programs to fluid models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.