simulation_one_step
plain-language theorem explainer
The one-step simulation lemma asserts exact commutation between the discrete Galerkin step and the independent LNAL spatial step on an encoded state. Researchers constructing discrete fluid models within Recognition Science would cite it to confirm the encoding bridge at milestone M3. The proof is a direct one-line application of the commutation field inside the SimulationHypothesis structure.
Claim. Let $N$ be a natural number and let $H$ be a simulation hypothesis for $N$ consisting of an LNAL program $P$, a discrete step map on Galerkin states, and the commutation property. For any Galerkin state $u$, the independent spatial step of $P$ applied to the encoding of $u$ equals the encoding of the discrete step applied to $u$.
background
GalerkinState is the type of velocity coefficients for each truncated mode and each of two components in a 2D discretization. SimulationHypothesis bundles an LNAL program $P$, a discrete step map, and the exact commutation property that independent.step of $P$ on the encoded state recovers the encoding of the stepped state. The module sets the local theoretical setting at milestone M3: it states the one-step simulation bridge between the discrete 2D Galerkin model and spatial LNAL execution semantics without attempting analytic correctness proofs.
proof idea
The proof is a one-line wrapper that applies the commutation property packaged inside the SimulationHypothesis structure.
why it matters
This declaration supplies the exact one-step commutation required for the Simulation2D milestone in the ClassicalBridge. It packages the bridge claim as an explicit hypothesis structure rather than an axiom, directly supporting downstream constructions that link Galerkin discretizations to LNAL semantics. The result touches the open question of extending the bridge to multi-step evolution and analytic correctness of the fluid simulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.