encodeGalerkin2D
plain-language theorem explainer
The mapping from a Galerkin velocity coefficient array over truncated Fourier modes to an array of LNAL voxels is defined by deterministic indexing of the mode-component pairs followed by per-coefficient encoding. Researchers simulating fluids via LNAL programs cite this step when constructing simulation hypotheses. The construction relies on a finite-type equivalence to order the coefficients and applies the single-index encoder at each position.
Claim. Let $u$ be a vector of real coefficients indexed by pairs consisting of a truncated 2D Fourier mode and a velocity component. The encoded field is the array whose $j$-th entry is the voxel obtained by encoding the coefficient of the $j$-th pair under the standard enumeration of the finite set of such pairs.
background
GalerkinState N is the Euclidean space of real coefficients over the product of the finite mode set and two velocity components. The modes function returns the finite set of 2D wavevectors whose integer indices range from -N to N in each direction. LNALField is an array of voxels, each carrying a register structure whose magnitude field stores a quantized version of the coefficient value.
proof idea
The definition first constructs the equivalence from the initial segment of naturals to the product set of modes and components via Fintype.equivFin. It then populates the output array with Array.ofFn, sending each position through the single-coefficient encoder applied to the corresponding pair.
why it matters
This definition supplies the forward map required by SimulationHypothesis and DecodedSimulationHypothesis in the Simulation2D module. Those structures encode the claim that an LNAL program step commutes with a discrete Galerkin step after encoding or decoding. The construction realizes the explicit encoding step of the LNALSemantics module for Milestone M2, which remains minimal by omitting voxel coupling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.