foldPlusOneProgram
plain-language theorem explainer
foldPlusOneProgram defines a fixed LNAL program that applies a single fold instruction with argument 1 to increment nuPhi by one at each voxel. Researchers building the discrete-to-LNAL bridge in the ClassicalBridge module cite it as the executable realizing the one-step simulation claim. The definition is a direct one-line wrapper returning the fold-1 instruction for any input.
Claim. Let $P$ be the LNAL program defined by $P(x) = $ LInstr.fold$(1)$ for any input $x$. This program increments the nuPhi coefficient by $+1$ (clamped) while leaving the auxiliary value unchanged.
background
The Simulation2D module at milestone M3 packages the one-step bridge between the discrete 2D Galerkin model and spatial LNAL execution semantics applied to an encoded field. LNAL programs consist of instructions operating on voxels, where each voxel holds a 6-tuple of coefficients together with an auxiliary value. The voxel itself is the fundamental length quantum, defined as length 1 in RS-native units.
proof idea
The definition is a one-line wrapper that maps every input to the LInstr.fold 1 instruction.
why it matters
This definition supplies the concrete program component required by the SimulationHypothesis structure, which asserts that one LNAL spatial step on an encoded Galerkin state commutes with the discrete step map. It fills the executable slot in the M3 classical-bridge milestone. In the Recognition Science framework it supports the discrete simulation layer that precedes analytic limits, using the phi-ladder and eight-tick octave for scaling while leaving full commutation as an explicit hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.