DecodedSimulationHypothesis
plain-language theorem explainer
DecodedSimulationHypothesis packages an LNAL program P together with a discrete step map on Galerkin states such that one independent LNAL spatial step, after encoding and decoding, equals the supplied step. Researchers citing the M3 milestone in the ClassicalBridge would reference this record to make the simulation hypothesis explicit. The declaration is a plain structure whose commutation field is witnessed by a simp on the independent semantics and the encodeGalerkin2D map.
Claim. A structure consisting of an LNAL program $P$, a map $step : GalerkinState_N → GalerkinState_N$, and the commutation property that for every $u$, decoding the result of the independent spatial step of $P$ applied to the encoded $u$ equals $step(u)$, where the size hypothesis is discharged by simplification.
background
The Simulation2D module at milestone M3 states the one-step simulation bridge between the discrete 2D Galerkin model and the spatial LNAL execution semantics, packaging the required claim as an explicit structure rather than an axiom or sorry. GalerkinState N is the EuclideanSpace of velocity coefficients over the truncated modes and two components. encodeGalerkin2D converts such a state into an LNALField by deterministic indexing via Fintype.equivFin. independent is the SpatialSemantics whose step applies voxelStep independently to every voxel.
proof idea
Structure definition. The commutation field is witnessed directly by the displayed equality whose size hypothesis is obtained by simp on LNALSemantics.independent and encodeGalerkin2D.
why it matters
The structure is consumed by decoded_simulation_one_step, which extracts the one-step commutation lemma directly from its comm field. It supplies the explicit hypothesis required by the M3 milestone in ClassicalBridge.Fluids, connecting Galerkin2D discrete dynamics to the independent LNAL semantics while avoiding axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.