voxelStep_foldPlusOneProgram
plain-language theorem explainer
The lemma supplies the explicit one-voxel update rule under the fold-plus-one LNAL program: nuPhi increments by one with clamping while the auxiliary component is left fixed. Authors constructing the M3 bridge between Galerkin discretizations and LNAL execution would cite it when tracking coefficient evolution in encoded fields. The proof reduces by case split on the voxel pair followed by targeted simplification against the voxelStep and lStep definitions.
Claim. Let $v = (r_6, a_5)$ be a voxel consisting of a Reg6 register file and an Aux5 auxiliary state. Execution of the fold-plus-one program satisfies $voxelStep(foldPlusOneProgram, v) = (r_6', a_5)$ where the nuPhi field of $r_6'$ equals clampI32 of the original nuPhi value plus one.
background
LNALVoxel is the product type Reg6 × Aux5 that represents one simulation cell. voxelStep executes a single LNAL program on such a cell by initializing an LState from the registers and auxiliaries, applying lStep, and returning the updated pair. foldPlusOneProgram is the constant function that returns the fold-1 instruction at every program counter.
proof idea
The term proof first performs rcases to split the input voxel into its Reg6 and Aux5 components. It then applies simp using the definitions of LNALSemantics.voxelStep, foldPlusOneProgram, and lStep while suppressing the clampI32 rule.
why it matters
This lemma provides the concrete voxel semantics required by the downstream voxelStep_foldPlusOne_encodeIndex result, which relates the program step to foldPlusOneStep on Galerkin states. It thereby supports the explicit one-step simulation bridge packaged in the M3 milestone of ClassicalBridge.Fluids. The module states that analytic correctness of the full simulation is not attempted here and is instead left as an explicit SimulationHypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.