encodeGalerkin2D
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not introduce neighbor coupling or spatial interaction rules between voxels.
- Does not specify or execute any particular LNAL program for time evolution.
- Does not guarantee exact inversion by decodeGalerkin2D beyond the quantization performed by coeffMag.
- Does not extend the encoding to three-dimensional or time-dependent Galerkin truncations.
Lean usage
let field := encodeGalerkin2D u; independent.step H.P fieldformal statement (Lean)
86noncomputable def encodeGalerkin2D {N : ℕ} (u : GalerkinState N) : LNALField :=
proof body
Definition body.
87 let e : Fin (Fintype.card ((modes N) × Fin 2)) ≃ ((modes N) × Fin 2) :=
88 (Fintype.equivFin ((modes N) × Fin 2)).symm
89 Array.ofFn (fun j => encodeIndex u (e j))
90
91end Encoding
92
93end IndisputableMonolith.ClassicalBridge.Fluids