simulation_one_step
The one-step commutation between LNAL spatial execution and discrete Galerkin evolution holds exactly under the packaged SimulationHypothesis. Researchers bridging classical fluid models to LNAL semantics in Recognition Science would cite this to justify replacing Galerkin time-stepping with program execution on encoded fields. The proof is a direct one-line application of the comm field inside the hypothesis structure.
claimLet $H$ be a simulation hypothesis for dimension $N$ and let $u$ be a Galerkin state. Then the independent LNAL step on the encoded state equals the encoding of the stepped state: independent.step$(H.P, $encodeGalerkin2D$(u)) = $encodeGalerkin2D$(H.step$(u))$.
background
Module Simulation2D (Milestone M3) states the one-step simulation bridge between the discrete 2D Galerkin model and spatial LNAL execution semantics. GalerkinState is the type of velocity coefficients for each truncated mode and each component. encodeGalerkin2D maps a Galerkin state to an LNALField by deterministic indexing of the finite coefficient set. independent is the spatial semantics in which voxels evolve independently via voxelStep. SimulationHypothesis bundles an LNAL program P, a discrete step map on Galerkin states, and the exact commutation property.
proof idea
The proof is the one-line term H.comm u, which directly applies the commutation axiom defined inside the SimulationHypothesis structure.
why it matters in Recognition Science
This theorem supplies the core one-step simulation lemma for Milestone M3 in ClassicalBridge.Fluids. It connects the Galerkin model to LNAL semantics by packaging the required claim as an explicit hypothesis rather than an axiom. The result supports the Recognition Science program of deriving classical dynamics from LNAL programs without claiming analytic correctness of the fluid simulation.
scope and limits
- Does not prove analytic correctness or convergence of the LNAL simulation to continuous fluid equations.
- Does not extend the commutation to multi-step evolution or full neighbor interactions.
- Does not address 3D cases or variable grid resolutions beyond fixed N.
formal statement (Lean)
280theorem simulation_one_step {N : ℕ} (H : SimulationHypothesis N) (u : GalerkinState N) :
281 independent.step H.P (encodeGalerkin2D u) = encodeGalerkin2D (H.step u) :=
proof body
Term-mode proof.
282 H.comm u
283
284/-!
285## Decode-based simulation (weaker notion) and a diagonal decay step
286
287For some local operations (e.g. sign-preserving decay of a magnitude register), exact commutation
288`encode(step u) = step(encode u)` can fail due to sign-bit conventions at `0`.
289
290We therefore also provide a **decode-based** simulation notion:
291we compare decoded coefficients after executing the LNAL step.
292-/
293
294/-- Hypothesis: one LNAL spatial step simulates one discrete Galerkin step **after decoding**. -/