foldMinusOneProgram
plain-language theorem explainer
This definition supplies the constant LNAL program that applies the FOLD instruction with argument -1, decrementing the nuPhi field by one (clamped) while leaving aux5 untouched. Workers on the 2D fluid simulation bridge cite it when assembling one-step updates that link discrete Galerkin states to LNAL voxel execution. The definition is a direct one-line construction returning the fold instruction for any input.
Claim. The constant program $P : LProgram$ given by $P := λ _ ↦ LInstr.fold(-1)$, which decrements the nuPhi component of an LNAL voxel by 1 (clamped) and leaves the auxiliary field unchanged.
background
The Simulation2D module packages the one-step simulation bridge between the discrete 2D Galerkin model and the spatial LNAL execution semantics (independent) applied to an encoded field. LNAL programs are built from instructions that act on voxels, each voxel carrying a 6-tuple of integer fields including nuPhi and an auxiliary aux5. The upstream voxel definition supplies the fundamental length quantum equal to 1 in RS-native units, while the LNALSemantics import provides the LInstr and voxelStep primitives used here.
proof idea
One-line definition that constructs the LProgram as the constant function returning LInstr.fold (-1).
why it matters
The program is invoked by the voxelStep_foldMinusOneProgram lemma to establish the concrete one-voxel update and by decodeCoeff_voxelStep_foldMinusOne_encodeIndex to verify commutation after decoding. It supplies the P component inside the DecodedSimulationHypothesis structure that states the simulation claim for milestone M3. In the Recognition framework this supplies the concrete LNAL program needed for the classical bridge without requiring an analytic correctness proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.