voxelStep_foldPlusOneProgram
The lemma supplies the explicit one-voxel update rule under the fold-plus-one LNAL program: nuPhi increments by 1 and clamps while the auxiliary state is untouched. A researcher verifying the 2D Galerkin-to-LNAL simulation bridge at milestone M3 would cite it when lifting the rule to encoded coefficient fields. The term proof reduces the claim by destructuring the voxel pair and simplifying against the definitions of voxelStep and lStep.
claimFor any LNAL voxel $v = (r, a)$ with $r$ a Reg6 register and $a$ an Aux5 auxiliary, the one-step execution satisfies $voxelStep(foldPlusOneProgram, v) = (r[nuPhi := clampI32(r.nuPhi + 1)], a)$.
background
LNALVoxel is the product type Reg6 × Aux5. voxelStep initializes an LState from the voxel, applies lStep under the supplied LProgram, and returns the resulting register-auxiliary pair. foldPlusOneProgram is the constant program that emits the fold-1 instruction at every index. The module Simulation2D packages the one-step bridge between the discrete 2D Galerkin model and the independent-voxel LNAL semantics; at M3 the required claims are stated explicitly as SimulationHypothesis without axioms.
proof idea
The term proof first applies rcases to split the input voxel into its Reg6 and Aux5 components, then invokes simp on the definitions of voxelStep, foldPlusOneProgram, and lStep while omitting the clampI32 rewrite rule.
why it matters in Recognition Science
The lemma provides the concrete semantics required by the downstream result voxelStep_foldPlusOne_encodeIndex, which shows that the LNAL step on an encoded Galerkin state reproduces foldPlusOneStep. It therefore closes one link in the SimulationHypothesis of the ClassicalBridge.Fluids module. Within the Recognition framework it supports the classical-to-discrete bridge at the M3 milestone without introducing new hypotheses.
scope and limits
- Does not prove analytic equivalence to the continuous Navier-Stokes equations.
- Does not incorporate neighbor interactions between voxels.
- Applies only to foldPlusOneProgram and not to arbitrary LPrograms.
- Does not address multi-step iteration or global consistency checks.
Lean usage
simp [voxelStep_foldPlusOneProgram]formal statement (Lean)
45lemma voxelStep_foldPlusOneProgram (v : LNALVoxel) :
46 voxelStep foldPlusOneProgram v = ({ v.1 with nuPhi := clampI32 (v.1.nuPhi + 1) }, v.2) := by
proof body
Term-mode proof.
47 rcases v with ⟨r6, a5⟩
48 simp [LNALSemantics.voxelStep, foldPlusOneProgram, lStep, -clampI32]
49
50/-- The corresponding discrete step on encoded Galerkin coefficients. -/