encodeGalerkin2D
plain-language theorem explainer
Encodes a 2D Galerkin velocity state, given as real coefficients over the finite set of truncated Fourier modes times two components, into an LNALField array of voxels. Simulation researchers cite the map to connect discrete spectral dynamics to LNAL voxel execution in the classical bridge. The definition obtains a deterministic bijection of the index set via Fintype.equivFin and applies the single-coefficient encoder to each entry.
Claim. Let $u$ be a vector in Euclidean space over the product of the finite mode set $M_N$ (integer pairs with components in $[-N,N]$) and the two velocity components. The encoding produces the array whose $j$-th entry is the voxel obtained by applying the single-coefficient encoder to the pair indexed by the standard enumeration of $M_N$ times Fin 2.
background
GalerkinState N is the Euclidean space of real coefficients indexed by (modes N) × Fin 2. The definition modes N returns the Finset of Mode2 pairs whose components range from -N to N. LNALField is the type Array LNALVoxel, each voxel carrying a Reg6 record (including nuPhi magnitude and ell index) together with Aux5 auxiliary data. The sibling encodeIndex maps one coefficient at a given mode-component pair to a voxel by extracting its magnitude via coeffMag and storing the mode indices directly.
proof idea
Obtains the equivalence e as the symmetric of Fintype.equivFin applied to the product type (modes N) × Fin 2. Constructs the output array by Array.ofFn, feeding each natural-number index j through e to select the corresponding pair and then calling encodeIndex on u at that pair.
why it matters
Supplies the forward encoding required by SimulationHypothesis and DecodedSimulationHypothesis in Simulation2D, which assert one-step commutation between an LNAL program and a discrete Galerkin step (exact or after decoding). Realizes the explicit Galerkin-to-voxel map of Milestone M2 in the LNALSemantics module. Supports the classical bridge layer without reference to the T0-T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.