foldMinusOneProgram
foldMinusOneProgram supplies the constant LNAL program that executes a single FOLD instruction with argument -1. Workers on the discrete Galerkin to LNAL bridge at milestone M3 cite it when assembling the elementary operations inside DecodedSimulationHypothesis. The definition is a direct one-line abbreviation returning the fixed LInstr.fold(-1) term for any input.
claimLet $P$ be the LNAL program defined by $P := fun _ => LInstr.fold(-1)$. Execution of $P$ on a voxel decrements the nuPhi field by 1 subject to clamping while leaving the auxiliary register unchanged.
background
The Simulation2D module constructs the one-step simulation bridge between the discrete 2D Galerkin model (Galerkin2D) and the spatial LNAL execution semantics (LNALSemantics.independent) applied to an encoded field. At milestone M3 the analytic correctness of the full simulation is not proved; instead the required commutation is packaged explicitly as the DecodedSimulationHypothesis structure. The upstream voxel definition supplies the fundamental length quantum (set to 1 in RS-native units), while the for structure from UniversalForcingSelfReference records the meta-realization properties required by the forcing chain.
proof idea
This is a direct definition. The body is the explicit term fun _ => LInstr.fold(-1), which ignores its argument and returns the constant fold instruction. No lemmas or tactics are invoked; the declaration is simply an abbreviation marked with @[simp].
why it matters in Recognition Science
The definition supplies one of the elementary programs required by the DecodedSimulationHypothesis structure and is invoked inside the commutation lemma decodeCoeff_voxelStep_foldMinusOne_encodeIndex. It therefore participates in the classical bridge that connects the phi-ladder mass formulas and eight-tick octave semantics to fluid simulations. The module leaves open the question of full analytic correctness for the simulation, which is recorded as an explicit hypothesis rather than an axiom.
scope and limits
- Does not prove analytic correctness of the full simulation.
- Does not derive the program from the Recognition Composition Law.
- Does not assign numerical values to physical constants such as alpha or G.
Lean usage
lemma voxelStep_foldMinusOneProgram (v : LNALVoxel) : voxelStep foldMinusOneProgram v = ({ v.1 with nuPhi := clampI32 (v.1.nuPhi + (-1)) }, v.2) := by simp [foldMinusOneProgram]formal statement (Lean)
317@[simp] def foldMinusOneProgram : LProgram :=
proof body
Definition body.
318 fun _ => LInstr.fold (-1)
319
320/-- One-voxel semantics for `foldMinusOneProgram`: decrement `nuPhi` by `1` (clamped); leave `aux5` unchanged. -/