coeffSign
plain-language theorem explainer
coeffSign defines the sign of a real coefficient as -1 or 1. It is cited in discrete fluid simulations when encoding Galerkin Fourier states into LNAL voxels and when preserving parity across magnitude updates. The definition is a direct conditional expression on the input real.
Claim. The map $x : {R} mapsto {Z}$ given by $x mapsto -1$ if $x < 0$ and $x mapsto 1$ otherwise.
background
LNALSemantics supplies minimal spatial semantics for LNAL programs over arrays of Reg6 × Aux5 and an explicit encoding of 2D Galerkin Fourier states into LNAL voxels, without neighbor graphs or coupling. The definition supplies the sign/parity component used inside each voxel encoding. Upstream results include the voxel as the fundamental length quantum (RSNativeUnits.voxel) and the unit elements from integers, rationals, spin statistics, and core recognition lemmas.
proof idea
The definition is a direct if-then-else on the input real x that returns -1 when x is negative and 1 otherwise.
why it matters
It is called inside encodeIndex to populate the nuPhi field of each Reg6 voxel and inside the simulation steps foldPlusOneStep, foldMinusOneDecodedStep, coeffSign_foldPlusOneStep, and decide_lt_zero_foldPlusOneStep to keep sign invariant under clamping. The declaration therefore closes the parity half of the M2 encoding bridge from Galerkin states to LNAL voxels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.