listenNoopProgram
plain-language theorem explainer
The declaration defines a constant LProgram that returns the listen instruction with noop mode at every step. Researchers verifying discrete fluid simulations cite it as the identity baseline for LNAL spatial steps. The definition is a direct one-line construction of the constant function.
Claim. The constant program $P$ such that $P(i) = $ LISTEN(noop) for every instruction pointer $i$.
background
The LNALSemantics module supplies minimal spatial semantics for executing an LNAL program on an LNALField, defined as an Array of (Reg6 × Aux5) voxels. An LProgram is a function from instruction pointers to LInstr values; here the listen constructor is used with ListenMode.noop. The module also encodes 2D Galerkin Fourier states into these voxels without neighbor coupling or inter-voxel interactions.
proof idea
Direct definition: the program is constructed as the constant function that returns LInstr.listen ListenMode.noop regardless of the input pointer.
why it matters
This definition supplies the program component P inside the SimulationHypothesis structure, which requires that one LNAL spatial step commutes with the Galerkin encoding. It is invoked by the lemmas voxelStep_listenNoopProgram and independent_step_listenNoopProgram to establish that the step acts as the identity on the field. In the Recognition framework it provides the trivial case for the classical bridge to fluid dynamics before introducing coupling or nontrivial instructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.