decoded_simulation_one_step
plain-language theorem explainer
The decoded simulation one-step lemma states that, under a packaged hypothesis linking an LNAL program to a discrete Galerkin step map, decoding after one independent voxel evolution on an encoded state recovers exactly the discrete step. Researchers establishing one-step fidelity between discrete fluid models and LNAL execution semantics cite it at Milestone M3. The proof is a direct one-line application of the commutation field inside the hypothesis structure, after a size-simplification tactic.
Claim. Let $N$ be a natural number and let $H$ be a DecodedSimulationHypothesis for $N$, consisting of an LNAL program $P$, a discrete step map on Galerkin states, and a commutation property. For any Galerkin state $u$, decoding the LNAL field obtained by applying one independent spatial step of $P$ to the encoded $u$ equals the result of the discrete step map applied to $u$.
background
GalerkinState $N$ is the type of velocity coefficient vectors indexed by truncated Fourier modes and two spatial components. encodeGalerkin2D maps such a state to an LNALField by deterministic indexing of the finite coefficient set. decodeGalerkin2D performs the inverse map, recovering coefficients up to the coarse quantization of coeffMag. independent is the spatial semantics in which each voxel evolves separately by applying voxelStep to the program $P$ with no neighbor coupling. DecodedSimulationHypothesis packages the claim that one LNAL step, after encoding and decoding, reproduces the discrete Galerkin step map. The module sets this up at Milestone M3 as an explicit hypothesis rather than an axiom, to bridge the discrete 2D Galerkin model with LNAL execution without yet proving analytic correctness.
proof idea
The proof is a one-line wrapper that applies the comm field of the supplied DecodedSimulationHypothesis. A preceding simp tactic discharges the size hypothesis on the decode call by unfolding LNALSemantics.independent and encodeGalerkin2D.
why it matters
This theorem supplies the one-step commutation bridge required by the Simulation2D module at Milestone M3. It directly implements the commutation property stated in the DecodedSimulationHypothesis structure and thereby closes the explicit hypothesis interface for the discrete-to-LNAL link. No downstream results are recorded yet, but the lemma is the base case for any future multi-step simulation fidelity argument. It sits inside the ClassicalBridge layer and does not invoke the cost algebra H or the phi-ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.