encodeIndex
encodeIndex packs a single coefficient from a GalerkinState into an LNALVoxel by setting Reg6 fields from coeffMag of the value, coeffSign of the value, mode components, component index, and a negativity flag, then pairing with Aux5.zero. Researchers bridging 2D Fourier fluid discretizations to voxel LNAL execution cite it for the atomic encoding step. The definition is a direct record construction from the input coefficient and index.
claimFor a Galerkin state $u$ over modes truncated at $N$ and index $i=(k,c)$ with $k$ a 2D Fourier mode and $c$ a component index, encodeIndex$(u,i)$ yields the voxel $(r,0)$ where $r$ satisfies $r. nuPhi = coeffMag(u_i)$, $r. ell = k_1$, $r. sigma = coeffSign(u_i)$, $r. tau = k_2$, $r. kPerp = c$, $r. phiE = [u_i < 0]$.
background
The LNALSemantics module supplies minimal spatial semantics for LNAL programs acting on an LNALField (an array of LNALVoxels) together with an explicit map from 2D Galerkin Fourier states into those voxels. A GalerkinState N is the Euclidean space of real coefficients indexed by the finite set (modes N) × Fin 2, where modes N collects all integer pairs (k1,k2) obeying max(|k1|,|k2|) ≤ N. Each LNALVoxel is the product Reg6 × Aux5; Reg6 carries the six fields nuPhi, ell, sigma, tau, kPerp, phiE that store magnitude, sign, and mode data extracted from a single coefficient.
proof idea
The definition binds x to the coefficient u i, casts the mode component of i to Mode2, assembles a Reg6 record by setting nuPhi to coeffMag x, ell and tau to the two integers of the mode, sigma to coeffSign x, kPerp to the integer value of the Fin 2 index, and phiE to the decision whether x is negative, then returns the pair with Aux5.zero.
why it matters in Recognition Science
encodeIndex is the primitive invoked by encodeGalerkin2D to produce a complete LNALField from any GalerkinState. It supplies the concrete map required by the SimulationHypothesis structure, which asserts exact commutation between one LNAL voxel step and the corresponding discrete Galerkin update. The declaration therefore completes the spatial-encoding half of milestone M2 in the ClassicalBridge, linking truncated Fourier fluid models to the discrete LNAL execution layer of Recognition Science.
scope and limits
- Does not incorporate neighbor couplings or spatial derivatives between voxels.
- Does not define or execute any LNAL program.
- Does not quantify truncation error or convergence rates of the Galerkin expansion.
- Does not extend the encoding to three-dimensional modes or time-dependent states.
Lean usage
Array.ofFn (fun j => encodeIndex u (e j))formal statement (Lean)
69noncomputable def encodeIndex {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) : LNALVoxel :=
proof body
Definition body.
70 let k : Mode2 := (i.1 : Mode2)
71 let x : ℝ := u i
72 let r6 : Reg6 :=
73 { nuPhi := coeffMag x
74 ell := k.1
75 sigma := coeffSign x
76 tau := k.2
77 kPerp := Int.ofNat i.2.val
78 phiE := decide (x < 0) }
79 (r6, Aux5.zero)
80
81/-- Encode an entire 2D Galerkin state into an `LNALField`.
82
83We use `Fintype.equivFin` to give a deterministic indexing of the finite coefficient set
84`(modes N) × Fin 2`, then store one coefficient per voxel.
85-/