encodeIndex
plain-language theorem explainer
The definition encodeIndex packs one real coefficient from a GalerkinState (indexed by a truncated 2D Fourier mode and a velocity component) into a single LNALVoxel by writing its magnitude, sign, mode indices, and negativity flag into a Reg6 record paired with zero auxiliary data. Workers proving exact commutation between discrete Galerkin time steps and LNAL voxel programs cite this map as the atomic encoding step. The definition directly assembles the voxel record from the supplied coefficient and index pair.
Claim. Let $u$ be a Galerkin state (Euclidean space of real coefficients over the finite set of truncated 2D Fourier modes times two components). For an index $i$ consisting of a mode $k$ and a component index, the map returns the LNAL voxel whose Reg6 component has nuPhi equal to the magnitude of the coefficient at $i$, ell and tau taken from $k$, sigma equal to the sign of the coefficient, kPerp equal to the component index, and phiE true precisely when the coefficient is negative, paired with the zero auxiliary value.
background
The module LNALSemantics supplies a minimal spatial semantics for executing LNAL programs on an LNALField (an array of LNALVoxels) together with an explicit encoding of 2D Galerkin Fourier states into such fields. GalerkinState N is the EuclideanSpace ℝ over the finite set (modes N) × Fin 2, where modes N is the finite set of integer pairs (k₁, k₂) with max(|k₁|, |k₂|) ≤ N and Mode2 is simply ℤ × ℤ. LNALVoxel is the product Reg6 × Aux5; the present definition supplies the per-coefficient map that is later lifted to entire fields.
proof idea
The definition extracts the mode k from the first component of i, reads the real coefficient x = u i, then builds a Reg6 record whose fields are set to coeffMag x, k.1, coeffSign x, k.2, Int.ofNat (i.2.val), and decide (x < 0) respectively, finally pairing the record with Aux5.zero.
why it matters
This definition supplies the per-coefficient encoding step that encodeGalerkin2D lifts to entire Galerkin states. It is invoked inside the proofs of voxelStep_foldPlusOne_encodeIndex and decodeCoeff_voxelStep_foldMinusOne_encodeIndex, which establish that single LNAL voxel steps commute with the corresponding discrete Galerkin maps, and it is used to populate the SimulationHypothesis structure that asserts exact one-step equivalence. In the Recognition Science framework the construction belongs to the ClassicalBridge layer that connects the J-cost dynamics and phi-ladder to classical fluid discretizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.