decodeGalerkin2D
plain-language theorem explainer
The decoder reconstructs a Galerkin velocity coefficient vector from an LNAL voxel array whose length matches twice the mode cardinality. Workers on the discrete fluid simulation bridge cite it when stating the post-decoding commutation hypothesis. The definition is a direct term that indexes the array via Fintype equivalence and applies the single-coefficient decoder to each entry.
Claim. Let $N$ be a natural number. For an LNAL field whose length equals the cardinality of the product of the truncated mode set with two components, the map that sends each mode-component index to the real value decoded from the corresponding voxel (sign from sigma, magnitude from nuPhi) defines an element of the Euclidean space of velocity coefficients.
background
GalerkinState N is the Euclidean space of real coefficients indexed by the product of the finite mode set with the two velocity components. The mode set itself is the integer grid from -N to N in each coordinate. LNALField is an array of voxels, each carrying a sign bit and a phi-based magnitude. decodeCoeff extracts a real from one voxel by integer multiplication of sign and decoded magnitude. The module packages a one-step simulation claim between the discrete Galerkin dynamics and an LNAL spatial execution without asserting analytic correctness of the fluid model.
proof idea
Term-mode definition. It applies WithLp.toLp 2 to the function that, for each index i in the mode-component product, casts the index via Fintype.equivFin, reads the voxel at the cast position under the size hypothesis, and calls decodeCoeff on that voxel.
why it matters
This definition supplies the decoding map required by DecodedSimulationHypothesis and appears directly in the statement of decoded_simulation_one_step. The latter equates the decoded result of one LNAL step on an encoded Galerkin state to the discrete step map. It closes the round-trip leg of the encoding-decoding pair inside Milestone M3, where the simulation hypothesis is stated explicitly rather than axiomatized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.