decoded_simulation_one_step
plain-language theorem explainer
The decoded simulation one step theorem states that decoding the result of one independent LNAL spatial step on an encoded Galerkin state recovers the discrete Galerkin step whenever the DecodedSimulationHypothesis holds. Researchers bridging truncated-mode fluid models to LNAL voxel semantics would cite this to verify one-step consistency in 2D simulations. The proof is a direct application of the commutation clause inside the hypothesis after a simp tactic discharges the size condition.
Claim. Let $N$ be a natural number. Let $H$ be a DecodedSimulationHypothesis for $N$, consisting of an LNAL program $P$, a discrete step map on Galerkin states, and a commutation property. For any Galerkin state $u$, decodeGalerkin2D applied to independent.step of $P$ on encodeGalerkin2D of $u$ (with size proof obtained by simplification) equals the discrete step applied to $u$.
background
The Simulation2D module at Milestone M3 packages a bridge between the discrete 2D Galerkin model and LNAL spatial execution. GalerkinState N is the type of velocity coefficients in Euclidean space over the product of truncated modes and two components. The independent semantics evolves each voxel separately by applying voxelStep to an LNALField without neighbor coupling. encodeGalerkin2D maps a GalerkinState to an LNALField array via Fintype.equivFin indexing, while decodeGalerkin2D reverses the map up to coarse quantization by coeffMag and decodeCoeff. The DecodedSimulationHypothesis structure contains the LNAL program P, the discrete step function, and the commutation axiom that decode after independent.step on encode recovers the discrete step.
proof idea
The proof is a one-line wrapper that applies the comm field of the DecodedSimulationHypothesis H to the input u. The hsize argument to decodeGalerkin2D is discharged by a simp tactic using the definitions of independent and encodeGalerkin2D.
why it matters
This theorem supplies the explicit one-step commutation required by the SimulationHypothesis at Milestone M3 in the ClassicalBridge.Fluids setting. It links discrete Galerkin time-stepping to LNAL independent voxel evolution without claiming analytic correctness of the fluid equations. No downstream uses appear yet, leaving open its integration with the Recognition Composition Law or scaling to full interacting simulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.