DecodedSimulationHypothesis
plain-language theorem explainer
DecodedSimulationHypothesis N packages an LNAL program P together with a discrete step map on Galerkin states of size N and the commutation property that one independent LNAL step on the encoded state decodes back to the direct Galerkin step. Researchers formalizing the classical bridge between discrete fluid models and LNAL semantics cite this structure when stating one-step simulation hypotheses at milestone M3. The declaration is a plain structure definition that bundles the three fields without proof obligations.
Claim. Let $N$ be a natural number. A decoded simulation hypothesis consists of an LNAL program $P$, a map step from Galerkin states of size $N$ to themselves, and the property that for every Galerkin state $u$, decoding the result of applying the independent spatial step of $P$ to the encoding of $u$ equals the direct application of step to $u$.
background
The Simulation2D module states the one-step simulation bridge between the discrete 2D Galerkin model and spatial LNAL execution semantics. GalerkinState N is the Euclidean space of velocity coefficients over the truncated modes and two components. encodeGalerkin2D maps such a state to an LNALField by deterministic indexing of coefficients into voxels. The independent semantics is the spatial map that applies voxelStep to each field element independently, with no neighbor coupling.
proof idea
The declaration is a structure definition. It directly assembles the three fields P, step, and the comm property that encodes the one-step commutation after decoding.
why it matters
This definition supplies the hypothesis used by the theorem decoded_simulation_one_step, which extracts the commutation for any such H. It fills the one-step simulation bridge in the ClassicalBridge.Fluids layer, connecting Galerkin discretizations to LNAL spatial steps at milestone M3 without attempting analytic correctness proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.