simulation_one_step
plain-language theorem explainer
The one-step simulation lemma asserts exact commutation between an LNAL spatial step on an encoded 2D Galerkin state and the discrete Galerkin step map. Researchers establishing discrete fluid bridges in Recognition Science would cite this when verifying that LNAL programs replicate Galerkin evolution. The proof reduces directly to the commutation clause inside the supplied SimulationHypothesis structure.
Claim. Let $H$ be a SimulationHypothesis for natural number $N$, consisting of an LNAL program $P$ and a discrete step map on Galerkin states. For any Galerkin state $u$, the independent step of $P$ applied to the encoding of $u$ equals the encoding of the result of applying the step map to $u$.
background
Module Simulation2D (Milestone M3) packages the one-step simulation bridge between the discrete 2D Galerkin model and LNAL execution semantics without attempting analytic correctness proofs. A GalerkinState N is the Euclidean space of velocity coefficients over truncated modes and two components. The encodeGalerkin2D function maps a GalerkinState to an LNALField by deterministic indexing of coefficients into voxels. The independent semantics evolves each voxel separately via voxelStep with no neighbor coupling. The SimulationHypothesis structure for N bundles a program P, a step map on Galerkin states, and the commutation property that independent.step P (encodeGalerkin2D u) equals encodeGalerkin2D (step u). Upstream, CostAlgebra.H supplies the shifted cost H(x) = J(x) + 1 that converts the Recognition Composition Law into d'Alembert form, while CPM2D.Hypothesis supplies the projection-defect and energy-control conditions required to build a CPM model for the Galerkin state.
proof idea
The proof is a one-line wrapper that applies the comm field of the supplied SimulationHypothesis H to the input state u.
why it matters
This theorem supplies the exact one-step commutation required for the ClassicalBridge between Galerkin fluid models and LNAL semantics at Milestone M3. It directly instantiates the commutation clause of SimulationHypothesis and thereby closes the simulation interface for further development of decode-based or multi-step extensions. No downstream uses are recorded yet, leaving open how this bridge will be invoked in larger fluid or astrophysical simulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.