decodeGalerkin2D
plain-language theorem explainer
decodeGalerkin2D converts an LNAL field array of length equal to the mode cardinality times two into the corresponding Galerkin state of real velocity coefficients. Workers on the discrete fluid simulation bridge cite this decoder when assembling the commutation hypothesis between LNAL steps and Galerkin evolution. The definition is a direct construction that applies the per-voxel coefficient decoder after index conversion via finite-type equivalence.
Claim. Let $N$ be a natural number and let $M$ denote the finite set of truncated modes. For an LNAL field array whose length equals $|M|$, the map produces the element of the Euclidean space over $M$ times the two components whose value at each mode-component index is the real coefficient decoded from the corresponding array entry.
background
The module states the one-step simulation bridge between the discrete 2D Galerkin model and spatial LNAL execution semantics at milestone M3. It packages the required claim as an explicit SimulationHypothesis without axioms or sorries. GalerkinState N is the Euclidean space of real coefficients for each truncated mode and each velocity component. The set modes N consists of all integer pairs with absolute value at most N. LNALField is an array of LNAL voxels. decodeCoeff extracts the real coefficient as (sigma times decodeMag nuPhi cast to Int) cast to Real.
proof idea
This is a definition that builds the target Euclidean space element via WithLp.toLp 2 applied to a lambda expression. For each mode-component index the expression converts the index to a Fin via Fintype.equivFin, casts under the size hypothesis, and applies decodeCoeff to the field entry.
why it matters
This decoder is required to state DecodedSimulationHypothesis, which asserts that one LNAL spatial step after encoding and decoding commutes with the discrete Galerkin step map. It supports the M3 milestone for the classical bridge between LNAL semantics and Galerkin dynamics. The parent result decoded_simulation_one_step applies this decoder directly in the commutation statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.