coeffMag
plain-language theorem explainer
coeffMag quantizes a real coefficient to an integer by returning the floor of its absolute value. It is referenced when encoding Galerkin Fourier coefficients into LNAL voxels for the fluid simulation bridge. The definition is realized by a direct one-line application of the floor function to the absolute value.
Claim. Define the quantization map by $coeffMag(x) := floor(|x|)$ for $x in mathbb{R}$.
background
The LNALSemantics module supplies minimal spatial semantics for LNAL programs over an LNALField (Array of Reg6 times Aux5) and an explicit encoding of 2D Galerkin Fourier states into LNAL voxels, kept intentionally without neighbor graphs or coupling. This definition supplies the magnitude component of that encoding. Upstream results include the active edge count per tick A from IntegrationGap and Masses.Anchor, which fix the per-tick structure in the unified forcing chain.
proof idea
One-line definition that applies Int.floor to the absolute value of the input real number.
why it matters
It is invoked by encodeIndex to populate the nuPhi field of Reg6 in LNAL voxels and by the foldPlusOneStep family of lemmas in Simulation2D. It implements the coarse quantization placeholder in the M2 milestone doc. It advances the classical fluids bridge but leaves open refinement against the phi-ladder and J-cost from T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.