voxelStep_foldMinusOneProgram
The lemma establishes that the one-voxel execution of the fold-minus-one program decrements the nu-phi register by one under clamping while leaving the auxiliary state fixed. Workers verifying the discrete update rules inside the 2D Galerkin-LNAL bridge cite it to confirm that encoded program steps match the intended register mutation. The proof reduces by destructuring the voxel pair and invoking the definitions of voxelStep together with lStep.
claimLet $v = (r_6, a_5)$ be an LNAL voxel. Execution of the constant program issuing a fold instruction with argument $-1$ satisfies voxelStep(foldMinusOneProgram, $v$) = $((r_6$ with nuPhi replaced by clampI32$(r_6$.nuPhi $- 1)), a_5)$.
background
LNALVoxel is the product type Reg6 × Aux5. The function voxelStep initializes an LState from the voxel components and applies a single lStep under the supplied program; its doc-comment states it performs one-voxel execution by running a single LNAL step on a (Reg6 × Aux5) voxel. foldMinusOneProgram is the constant LProgram that returns the fold instruction with argument $-1$. The lemma lives in the Simulation2D module, whose module doc describes the one-step simulation bridge between the discrete 2D Galerkin model and the independent LNAL voxel evolution, packaged without axioms or sorries as an explicit SimulationHypothesis.
proof idea
The term proof begins with rcases on the voxel to expose the register-6 and auxiliary-5 components, then applies simp using the definitions of voxelStep, foldMinusOneProgram, and lStep while suppressing the clampI32 rule.
why it matters in Recognition Science
This supplies the concrete one-voxel update rule required by the downstream lemma decodeCoeff_voxelStep_foldMinusOne_encodeIndex, whose doc-comment states that decoding after a single FOLD (-1) step matches the corresponding decoded discrete step. It advances the M3 milestone of the ClassicalBridge by making the LNAL execution semantics explicit for the decrement program, supporting the larger claim that discrete fluid steps can be realized inside the Recognition monolith.
scope and limits
- Does not prove global multi-step or multi-voxel simulation correctness.
- Does not incorporate neighbor interactions from the CellularAutomata layer.
- Does not address analytic convergence of the Galerkin discretization.
- Does not constrain initial conditions or boundary handling for the 2D field.
Lean usage
simp [voxelStep_foldMinusOneProgram]formal statement (Lean)
321lemma voxelStep_foldMinusOneProgram (v : LNALVoxel) :
322 voxelStep foldMinusOneProgram v = ({ v.1 with nuPhi := clampI32 (v.1.nuPhi + (-1)) }, v.2) := by
proof body
Term-mode proof.
323 rcases v with ⟨r6, a5⟩
324 simp [LNALSemantics.voxelStep, foldMinusOneProgram, lStep, -clampI32]
325
326/-- The corresponding discrete step on **decoded** Galerkin coefficients.
327
328We mimic the VM update on `nuPhi` (via `clampI32`) and then decode a nonnegative magnitude using `decodeMag`. -/