encodeIndex
plain-language theorem explainer
Encodes one Fourier coefficient from a truncated 2D Galerkin velocity field into a single LNAL voxel. Researchers bridging discrete fluid steps to LNAL execution cite this atomic map. The definition directly assembles a Reg6 record from magnitude and sign extractors, mode indices, and a zero auxiliary field.
Claim. Let $u$ be a Galerkin state for truncation $N$ and let $i=(k,c)$ index a mode $k$ together with a component $c$. Then encodeIndex$(u,i)$ returns the voxel $(r_6,0)$ whose register $r_6$ stores the magnitude of the coefficient $u_i$, its sign, the mode integers, the component index, and a negativity flag.
background
The module supplies a minimal spatial semantics for LNAL programs acting on an array of voxels (LNALField) together with an explicit map from the 2D Galerkin Fourier representation into those voxels. GalerkinState $N$ is the Euclidean space of velocity coefficients indexed by the finite set of truncated modes crossed with two components. Each mode is an integer pair $(k_1,k_2)$ obeying the truncation predicate max$(|k_1|,|k_2|)$ ≤ $N$. LNALVoxel is the product of a Reg6 register (nuPhi, ell, sigma, tau, kPerp, phiE) and an Aux5 auxiliary field.
proof idea
Direct construction. The body casts the mode index to Mode2, reads the real coefficient, builds the Reg6 record by calling coeffMag and coeffSign on that value, populates the remaining fields from the mode and component indices, sets the negativity flag by a decide expression, and pairs the result with the zero auxiliary value.
why it matters
This supplies the per-coefficient step required by encodeGalerkin2D to produce a full LNALField from any GalerkinState. It is invoked inside the commutation lemmas voxelStep_foldPlusOne_encodeIndex and decodeCoeff_voxelStep_foldMinusOne_encodeIndex that discharge the SimulationHypothesis. The construction therefore closes one link in the ClassicalBridge layer that embeds fluid dynamics inside the LNAL execution model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.