encodeGalerkin2D
plain-language theorem explainer
The definition maps a GalerkinState with N modes to an LNALField array by reindexing the finite coefficient set and applying the per-coefficient encoder. Researchers embedding truncated 2D Fourier velocity fields into LNAL voxel arrays for discrete simulation would cite this map. It proceeds by constructing the Fin equivalence for (modes N) times Fin 2 then filling the array via encodeIndex on each entry.
Claim. Let $u$ be a Galerkin state consisting of real coefficients indexed by the truncated modes and the two velocity components. The map produces an LNAL field whose length equals the cardinality of that index set, with the $j$-th voxel holding the encoded magnitude and sign of the coefficient at the corresponding mode-component pair.
background
GalerkinState N is the EuclideanSpace of real coefficients over the product of the finite mode set (modes N) with Fin 2. The auxiliary definition modes N returns the Finset of Mode2 pairs whose integer components range from -N to N. LNALField is the type Array LNALVoxel, each voxel a record carrying nuPhi magnitude, sigma sign, and auxiliary fields.
proof idea
The definition first binds a Fin equivalence e obtained by inverting Fintype.equivFin on the product type (modes N) times Fin 2. It then returns Array.ofFn applied to the function that sends each index j to encodeIndex u (e j).
why it matters
This forward encoding supplies the left half of the commutation required by SimulationHypothesis and DecodedSimulationHypothesis in the Simulation2D module. Those structures assert that one LNAL program step on the encoded field, followed by decoding, recovers the discrete Galerkin step. The declaration therefore completes the explicit spatial translation step of milestone M2, enabling the one-step lemmas such as decoded_simulation_one_step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.