voxelStep_foldMinusOneProgram
plain-language theorem explainer
The lemma gives the explicit one-voxel update produced by the constant program that decrements the nuPhi register by one with clamping while leaving the auxiliary component untouched. Researchers verifying the discrete-to-decoded equivalence in the 2D Galerkin-LNAL fluid bridge cite it when checking single-step coefficient evolution. The argument reduces by splitting the voxel pair and simplifying against the definitions of voxel execution and the fold program.
Claim. Let $v = (r, a)$ be a voxel consisting of a register state $r$ and auxiliary state $a$. Execution of the fold-minus-one program on $v$ yields the updated voxel $(r', a)$, where $r'$ equals $r$ except that its nuPhi field is replaced by the clamped integer value of $r$.nuPhi minus one.
background
The Simulation2D module packages the one-step bridge between the discrete 2D Galerkin model and LNAL execution semantics as an explicit SimulationHypothesis rather than an axiom or sorry. LNALVoxel is the type alias for the product of a six-register state and a five-auxiliary state. voxelStep initializes an LState from the voxel, applies the single-instruction lStep with the supplied program, and returns the resulting register-auxiliary pair. foldMinusOneProgram is the constant program returning the fold instruction with argument -1. decodeMag converts a register value to a nonnegative magnitude by mapping negatives to zero, allowing saturation under decrement.
proof idea
The term proof splits the input voxel into its register and auxiliary components via rcases, then reduces both sides by simplification against the definitions of voxelStep, foldMinusOneProgram, and lStep while excluding clampI32 from the rewrite set.
why it matters
This lemma supplies the concrete update rule required by the downstream decodeCoeff_voxelStep_foldMinusOne_encodeIndex result, which equates the decoded coefficient after a fold-minus-one step to the corresponding discrete Galerkin update. It advances the M3 milestone in ClassicalBridge.Fluids by making the encoded LNAL step explicit. Within the Recognition framework it supports the classical limit by aligning discrete register operations with expected fluid-coefficient changes, without yet addressing spatial interactions or analytic validation of the full simulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.