coeffMag
plain-language theorem explainer
This definition quantizes a real coefficient x to the integer floor of its absolute value. It acts as a coarse placeholder in the LNAL voxel encoding of Galerkin Fourier states for 2D fluid simulations. The implementation is a direct one-line application of the floor function to the absolute value. Researchers working on the classical bridge from continuous Galerkin models to discrete LNAL programs would cite it when tracing coefficient updates through encodeIndex and fold steps.
Claim. The magnitude quantization maps a real number $x$ to the integer $m = |x|$ rounded down, written $m = floor(|x|)$.
background
The LNALSemantics module supplies minimal spatial semantics for executing an LNAL program on an LNALField (an array of Reg6 × Aux5 pairs) together with an explicit encoding of a 2D Galerkin Fourier state into LNAL voxels. The construction is deliberately minimal: no neighbor graph and no inter-voxel coupling are present yet. Upstream results supply the active-edge count A (equal to 1) from IntegrationGap and Masses.Anchor, the parity pattern from LedgerPostingAdjacency, and the actualization operator A from Modal.Actualization that selects the configuration minimizing J-cost.
proof idea
One-line definition that applies the floor function to the absolute value of the input real.
why it matters
The definition supplies the nuPhi component inside encodeIndex, which packs a Galerkin coefficient into an LNAL voxel. It is invoked by the foldPlusOneStep, coeffSign_foldPlusOneStep, decodeCoeff, and foldMinusOneDecodedStep lemmas in Simulation2D. These steps close the encode-decode loop for the M2 milestone that bridges continuous fluid models to the discrete LNAL semantics. The coarse quantization is the first concrete link between real Fourier coefficients and the integer registers of the LNAL machine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.