decodeMag
plain-language theorem explainer
decodeMag extracts the nonnegative magnitude from an integer register value by sending negatives to zero. Researchers building the 2D Galerkin-to-LNAL simulation bridge cite it when reconstructing coefficients after voxel updates. The definition is a direct one-line application of Int.toNat followed by Int.ofNat.
Claim. $zmapsto max(z,0)$ for $z in mathbb{Z}$, interpreting negative nuPhi register values as zero to permit saturation under decrement steps.
background
The Simulation2D module states the one-step simulation bridge between the discrete 2D Galerkin model and LNAL execution semantics applied to an encoded field. At milestone M3 the module packages the required claim as an explicit SimulationHypothesis without proving analytic correctness. decodeMag supplies the nonnegative magnitude extraction from the nuPhi component of an LNALVoxel so that a decrement can saturate at zero.
proof idea
One-line definition that applies Int.toNat (yielding zero on negatives) then Int.ofNat to return the clamped nonnegative integer.
why it matters
decodeMag is used by decodeCoeff and by foldMinusOneDecodedStep, which in turn support the lemma decodeCoeff_voxelStep_foldMinusOne_encodeIndex verifying that post-step decoding matches the discrete update. It supplies the encoding layer needed for the SimulationHypothesis at M3. The declaration sits inside the classical bridge domain and does not yet invoke the forcing chain, RCL, or phi-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.