voxelStep_foldMinusOneProgram
plain-language theorem explainer
The lemma states the explicit update performed by one execution of the constant LNAL program foldMinusOneProgram on a single voxel: the nuPhi register component is decremented by 1 and clamped while the auxiliary component is left unchanged. Workers on the LNAL-to-Galerkin bridge in ClassicalBridge.Fluids cite it when checking that discrete coefficient steps commute with decoding. The proof reduces immediately by case split on the voxel pair followed by simplification against the definitions of voxelStep and foldMinusOneProgram.
Claim. Let $v = (r, a)$ with $r$ a Reg6 register and $a$ an Aux5 auxiliary. Execution of the constant program that issues FOLD(-1) produces the updated voxel $(r', a)$ where the nuPhi field of $r'$ equals clampI32(nuPhi(r) - 1).
background
LNALVoxel is the product type Reg6 × Aux5. The function voxelStep runs an LProgram on an initial LState built from the register and auxiliary, then returns the resulting (reg6, aux5) pair. foldMinusOneProgram is the constant program that always emits the instruction LInstr.fold(-1). decodeMag converts an integer to its nonnegative part via Int.toNat so that decrements can saturate at zero. The module Simulation2D at milestone M3 packages the required one-step bridge between the discrete 2D Galerkin model and the independent-voxel LNAL semantics as an explicit SimulationHypothesis without axioms or sorrys.
proof idea
The term proof first performs rcases on the input voxel to obtain the register and auxiliary components. It then invokes simp with the list LNALSemantics.voxelStep, foldMinusOneProgram, lStep, -clampI32, which unfolds the state machine and the constant program to the required clamped update.
why it matters
The lemma is invoked inside the proof of decodeCoeff_voxelStep_foldMinusOne_encodeIndex, which asserts that decoding after a single FOLD(-1) step recovers the corresponding discrete Galerkin coefficient update. It therefore supplies one concrete case of the SimulationHypothesis that links LNAL execution to the Galerkin2D model. The surrounding ClassicalBridge.Fluids development sits inside the larger Recognition Science program that derives classical dynamics from the LNAL forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.