decodeMag
decodeMag extracts the nonnegative magnitude from an integer register value by mapping negatives to zero. Fluid simulation code in the ClassicalBridge uses it to recover coefficient magnitudes after executing LNAL steps on encoded voxels. The implementation is a direct one-line composition of the standard Int.toNat and Int.ofNat operations. It enables saturation behavior during decrement steps on the nuPhi register.
claimFor an integer $z$, decodeMag$(z) := z$ if $z >= 0$ and $0$ otherwise.
background
The Simulation2D module implements the one-step simulation bridge between the discrete 2D Galerkin model and LNAL execution semantics on an encoded field. At milestone M3 the analytic correctness claim is packaged explicitly as SimulationHypothesis rather than proved. The voxel is the fundamental length quantum, set to 1 in RS-native units. The nuPhi field inside an LNALVoxel stores the magnitude component of a Galerkin coefficient; sigma supplies the sign.
proof idea
One-line definition that applies Int.toNat to the input integer and then Int.ofNat to the result. This composition yields the nonnegative part of the input while sending every negative value to zero.
why it matters in Recognition Science
decodeMag supplies the magnitude recovery step required by decodeCoeff and foldMinusOneDecodedStep. It appears in the consistency lemmas decodeCoeff_voxelStep_foldMinusOne_encodeIndex and voxelStep_foldMinusOneProgram that verify one-step behavior under the foldMinusOneProgram. The definition therefore closes the saturation requirement inside the M3 simulation bridge between Galerkin2D and LNALSemantics.
scope and limits
- Does not compute absolute value for negative inputs beyond mapping them to zero.
- Does not participate in any analytic proof of simulation correctness.
- Does not depend on phi, the eight-tick octave, or other RS constants.
- Does not apply to non-integer inputs.
Lean usage
noncomputable def decodeCoeff (v : LNALVoxel) : ℝ := ((v.1.sigma * decodeMag v.1.nuPhi : Int) : ℝ)formal statement (Lean)
222def decodeMag (z : Int) : Int :=
proof body
Definition body.
223 Int.ofNat (Int.toNat z)
224
225/-- Decode a single real coefficient from a voxel: sign from `sigma`, magnitude from `nuPhi`. -/