encodeIndex
plain-language theorem explainer
The definition maps one coefficient from a truncated 2D Fourier velocity field, indexed by mode and component, to a single LNAL voxel. Workers on the discrete-to-LNAL fluid bridge cite it as the atomic encoding step inside SimulationHypothesis. It assembles the voxel by direct record construction from coeffMag, coeffSign, and the supplied mode data.
Claim. Let $u$ be a Galerkin state over $N$ modes and let $i=((k_1,k_2),c)$ with $c$ a component index. Then encodeIndex$(u,i)$ yields the LNAL voxel whose Reg6 record has magnitude coeffMag$(u_i)$, sign coeffSign$(u_i)$, wave numbers $k_1,k_2$, perpendicular index $c$, and phase flag decide$(u_i<0)$, paired with the zero auxiliary value.
background
Module LNALSemantics supplies minimal spatial semantics for LNAL programs acting on an LNALField (an Array of LNALVoxel) together with an explicit encoding of 2D Galerkin states into those voxels; no neighbor graph or inter-voxel coupling is present. GalerkinState $N$ is the EuclideanSpace of real coefficients indexed by (modes $N$) × Fin 2; modes $N$ is the finite set of integer pairs $(k_1,k_2)$ with max$(|k_1|,|k_2|)$ ≤ $N$; Mode2 is simply ℤ × ℤ. LNALVoxel is the product Reg6 × Aux5, where Reg6 carries the six fields nuPhi, ell, sigma, tau, kPerp, phiE.
proof idea
The definition is a direct record construction: extract mode $k$ from the first component of $i$, read real value $x$ from $u$ at $i$, then build Reg6 with nuPhi := coeffMag $x$, ell := $k.1$, sigma := coeffSign $x$, tau := $k.2$, kPerp := Int.ofNat (second component of $i$), phiE := decide $(x<0)$, and pair the result with Aux5.zero.
why it matters
encodeIndex supplies the per-coefficient map required by encodeGalerkin2D and is invoked inside the lemmas voxelStep_foldPlusOne_encodeIndex and decodeCoeff_voxelStep_foldMinusOne_encodeIndex that verify commutation with LNAL steps. It therefore realizes the atomic half of the SimulationHypothesis structure, which asserts that one LNAL spatial step exactly reproduces one discrete Galerkin step. The construction sits inside ClassicalBridge milestone M2 and supplies the concrete translation between Fourier coefficients and the Reg6 voxel format used by the Recognition Science LNAL layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.