foldMinusOneProgram
plain-language theorem explainer
This definition supplies a fixed LNAL program consisting of a single FOLD instruction with argument -1. Researchers constructing the one-step simulation bridge between discrete Galerkin states and LNAL voxel execution cite it when building the DecodedSimulationHypothesis. The definition is introduced by a direct one-line abbreviation that maps every input to the decrement instruction.
Claim. Define the constant LNAL program $P$ by $P(x) = $ FOLD$(-1)$ for arbitrary input $x$.
background
The Simulation2D module states the one-step simulation bridge between the discrete 2D Galerkin model and spatial LNAL execution semantics applied to an encoded field. At milestone M3 the analytic correctness claim is packaged explicitly as DecodedSimulationHypothesis without axioms or sorries. Upstream, voxel is the fundamental length quantum (one voxel equals unit length in RS-native units) and the for structure records the meta-realization properties required by self-reference axioms.
proof idea
One-line definition that constructs the program by returning the fold instruction with constant argument -1.
why it matters
This definition supplies the program component inside DecodedSimulationHypothesis, which asserts that one LNAL spatial step simulates one discrete Galerkin step after decoding. It supports the M3 goal of stating the simulation bridge between Galerkin2D and LNALSemantics without proving analytic correctness. The program participates in the classical bridge that connects Recognition Science forcing chain steps to concrete fluid models, though the full commutation remains a packaged hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.