voxelStep_foldPlusOneProgram
plain-language theorem explainer
The lemma states the one-voxel execution rule for the fold-plus-one program on an LNAL voxel pair: the nuPhi register increments by one under clamping while the auxiliary component stays fixed. Workers on the M3 discrete-to-continuous bridge cite it when closing the encoding map from Galerkin coefficients to LNAL states. The proof reduces by destructuring the pair and simplifying against the definitions of voxelStep and lStep.
Claim. Let $v = (r_6, a_5)$ be a voxel consisting of a Reg6 register and an Aux5 auxiliary state. One-step execution of the constant fold-1 program on $v$ returns the updated voxel $(r_6', a_5)$, where $r_6'$ equals $r_6$ except that its $nuPhi$ field is replaced by $clampI32(r_6.nuPhi + 1)$.
background
Module Simulation2D supplies the one-step simulation bridge at milestone M3 between the discrete 2D Galerkin model and the spatial LNAL execution semantics, packaging the overall claim as an explicit SimulationHypothesis rather than an axiom. LNALVoxel is the product type Reg6 × Aux5. The function voxelStep initializes an LState from the voxel components, applies the wrapped small-step lStep to the supplied program, and returns the resulting (reg6, aux5) pair. The program foldPlusOneProgram is the constant function returning the single instruction fold 1. The upstream voxelStep definition states: 'One-voxel execution: run a single LNAL step on a (Reg6 × Aux5) voxel.'
proof idea
The term proof first destructures the input voxel into its Reg6 and Aux5 components via rcases, then invokes simplification on the definitions of voxelStep, foldPlusOneProgram, and lStep while suppressing the clampI32 unfolding.
why it matters
This lemma supplies the concrete one-voxel semantics required by the downstream voxelStep_foldPlusOne_encodeIndex, which rewrites the encoded Galerkin state under the same program. It therefore closes the encoding step inside the M3 SimulationHypothesis that links Galerkin2D to LNALSemantics. The result sits inside the classical bridge without touching analytic correctness of the fluid simulation or neighbor coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.