decodeMag
plain-language theorem explainer
decodeMag extracts the nonnegative magnitude from an integer register by mapping negatives to zero. It is cited inside the 2D fluid simulation bridge when recovering Galerkin coefficients after an LNAL voxel step. The definition is a one-line wrapper that applies the natural-number projection followed by its integer embedding.
Claim. The map sending an integer register value $z$ to its nonnegative magnitude, realized as the composition of the natural-number truncation with the integer embedding of that natural number.
background
The module packages a one-step simulation bridge between the discrete 2D Galerkin model and an LNAL execution semantics applied to an encoded field. Milestone M3 states the required claim explicitly as SimulationHypothesis without axioms or sorry. The definition appears inside the coefficient-decoding layer that separates sign (taken from the sigma register) from magnitude (taken from the nuPhi register). Upstream, voxel supplies the fundamental length quantum, while toNat from ArithmeticFromLogic supplies the forward iteration-count map used in related register handling.
proof idea
One-line wrapper that applies Int.toNat followed by Int.ofNat.
why it matters
The definition supplies the saturation behavior required by foldMinusOneDecodedStep and decodeCoeff inside the Simulation2D bridge. It is invoked by the lemmas decodeCoeff_voxelStep_foldMinusOne_encodeIndex and voxelStep_foldMinusOneProgram that close the one-step correspondence between the discrete Galerkin update and the LNAL voxel semantics. It therefore supports the explicit SimulationHypothesis stated for Milestone M3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.