decoded_simulation_one_step
The one-step decoded simulation result shows that decoding an LNAL independent step applied to an encoded Galerkin state recovers the discrete step map, whenever the DecodedSimulationHypothesis holds. Researchers modeling 2D fluid dynamics via discrete Galerkin methods bridged to LNAL would cite this lemma for single-step consistency. The proof consists of a direct application of the commutation property stored inside the hypothesis.
claimLet $N$ be a natural number. Let $H$ be a structure containing an LNAL program $P$, a discrete step map on Galerkin states, and a commutation property. For any Galerkin state $u$, the decoding of the LNAL field obtained by applying the independent spatial step with program $P$ to the encoding of $u$ equals the discrete step map applied to $u$, where the size condition holds by construction.
background
In the Simulation2D module at Milestone M3 the goal is to connect the discrete 2D Galerkin model to LNAL spatial semantics without proving full analytic correctness. GalerkinState N is the type of velocity coefficients for each truncated mode and each of two components. encodeGalerkin2D maps such a state to an LNALField by deterministic indexing of the finite coefficient set. The independent semantics applies a voxelStep to each element of the field independently, with no neighbor interaction. DecodedSimulationHypothesis packages a program P, a discrete step map, and the key commutation that decode after independent.step equals the discrete step.
proof idea
The proof is a one-line wrapper that applies the comm field of the supplied DecodedSimulationHypothesis H to the input state u. The size hypothesis is discharged by a single simp tactic using the definitions of independent and encodeGalerkin2D.
why it matters in Recognition Science
This declaration supplies the one-step consistency bridge required by the Simulation2D milestone. It directly instantiates the commutation property from DecodedSimulationHypothesis, enabling downstream verification that LNAL execution reproduces discrete Galerkin dynamics after encoding and decoding. In the Recognition framework it supports the classical bridge from discrete models to LNAL without introducing axioms. No parent theorems appear in the current dependency graph, indicating it serves as a foundational interface for further simulation results.
scope and limits
- Does not establish convergence or stability of the simulation over multiple steps.
- Does not incorporate neighbor interactions in the LNAL semantics.
- Does not prove that the discrete step approximates the continuous Navier-Stokes equations.
- Does not address quantization errors beyond the coarse coeffMag decoding.
formal statement (Lean)
309theorem decoded_simulation_one_step {N : ℕ} (H : DecodedSimulationHypothesis N) (u : GalerkinState N) :
310 decodeGalerkin2D (N := N)
proof body
Tactic-mode proof.
311 (field := independent.step H.P (encodeGalerkin2D u))
312 (hsize := by simp [LNALSemantics.independent, encodeGalerkin2D])
313 = H.step u :=
314 H.comm u
315
316/-- A constant LNAL program: decrement `nuPhi` by `1` (via `FOLD (-1)`). -/