coeffMag
plain-language theorem explainer
coeffMag maps a real coefficient to the floor of its absolute value as a coarse integer magnitude. It is referenced by encodeIndex for populating LNAL voxels from Galerkin states and by the fold lemmas in Simulation2D. The definition is realized by a direct one-line application of Int.floor to the absolute value.
Claim. For a real coefficient $x$, the magnitude is defined by $m = |x|$ and then $m = floor(m)$.
background
The LNALSemantics module supplies minimal spatial semantics for an LNAL program over an LNALField (an Array of Reg6 × Aux5 pairs) and an explicit encoding of 2D Galerkin Fourier states into LNAL voxels, with no neighbor graph or inter-voxel coupling. Upstream results include the active-edge count A (defined as 1) from IntegrationGap and Masses.Anchor, the parity abbrev from LedgerPostingAdjacency, and the actualization operator A from Modal.Actualization that maps a configuration to its J-minimizing image.
proof idea
The definition is a one-line wrapper that applies Int.floor to the absolute value of the input real.
why it matters
coeffMag supplies the nuPhi component inside encodeIndex when mapping Galerkin coefficients to LNAL voxels. It is invoked by the Simulation2D lemmas coeffMag_foldPlusOneStep, coeffSign_foldPlusOneStep, decide_lt_zero_foldPlusOneStep, decodeCoeff, foldMinusOneDecodedStep and foldPlusOneStep that track discrete updates. It serves as the placeholder quantization step before any phi-ladder refinement in the classical-bridge encoding of fluid states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.