decodeCoeff
plain-language theorem explainer
decodeCoeff recovers a real coefficient from an LNAL voxel by multiplying its sigma sign register by the nonnegative magnitude obtained from decodeMag on the nuPhi register. Researchers verifying round-trip consistency in the 2D Galerkin-to-LNAL simulation bridge would cite this extraction step. The definition is a direct one-line composition of the sign and magnitude helpers.
Claim. For an LNAL voxel $v$ with sign register $sigma$ and register $nuPhi$, define $decodeCoeff(v) := sigma(v) · decodeMag(nuPhi(v))$, where $decodeMag$ returns the nonnegative integer value of its argument.
background
LNALVoxel is the pair (Reg6, Aux5) that stores the sigma sign register and nuPhi magnitude register. coeffMag quantizes a real coefficient to an integer magnitude via floor of its absolute value. decodeMag recovers a nonnegative integer from a possibly negative register by saturating at zero via Int.toNat, allowing decrement steps to bottom out at zero. The module establishes the one-step simulation bridge between the discrete 2D Galerkin model and LNAL execution semantics at Milestone M3, packaging the required claim as an explicit SimulationHypothesis rather than an axiom.
proof idea
One-line definition that multiplies the sigma component of the voxel by the result of decodeMag applied to the nuPhi component, then casts the integer product to real.
why it matters
decodeCoeff supplies the coefficient extraction required by decodeGalerkin2D and by the consistency lemma decodeCoeff_voxelStep_foldMinusOne_encodeIndex. It completes the decoding half of the encodeGalerkin2D bridge stated in the Simulation2D module doc. The construction inherits the coarse quantization of coeffMag, leaving open the refinement to finer magnitude recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.