IEEE32Exec and FP32: Dyadic Rounding Helpers

Exact dyadic addition (used by op-level refinement theorems)

IEEE-754 addition is “exact add, then round”. To connect an executable add to the FP32 model, we factor the refinement into two steps:

1. perform an exact addition in an unbounded format (here: dyadics with integer exponents), and
2. apply float32 rounding.

addDyadic is our exact step (it aligns exponents, adds signed mantissas, and normalizes), and the lemmas in this section show that its real interpretation is literally real addition.

noncomputable def TorchLean.Floats.IEEE754.IEEE32Exec.signedMant (sign : Bool) (m : ℕ) : ℤ

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_eq_signedMant (d : Dyadic) : dyadicToReal d = ↑(signedMant d.sign d.mant) * neuralBpow binaryRadix d.exp

theorem TorchLean.Floats.IEEE754.IEEE32Exec.signedMant_shiftLeft (sign : Bool) (m sh : ℕ) : ↑(signedMant sign (m.shiftLeft sh)) = ↑(signedMant sign m) * neuralBpow binaryRadix (Int.ofNat sh)

theorem TorchLean.Floats.IEEE754.IEEE32Exec.signFactor_natAbs_int (s : ℤ) : (if decide (s < 0) = true then -1 else 1) * ↑s.natAbs = ↑s

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_ofNatAbs (s e : ℤ) : dyadicToReal { sign := decide (s < 0), mant := s.natAbs, exp := e } = ↑s * neuralBpow binaryRadix e

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_zero (sign : Bool) : dyadicToReal { sign := sign, mant := 0, exp := 0 } = 0

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_addDyadic_exact (a b : Dyadic) : dyadicToReal (addDyadic a b) = dyadicToReal a + dyadicToReal b

addDyadic is exact with respect to dyadicToReal.

Informal: addDyadic aligns exponents, adds signed mantissas, and normalizes; decoding the result gives the sum of the decoded inputs.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_magnitude_dyadic (d : Dyadic) (hm : d.mant ≠ 0) : neuralMagnitude binaryRadix (dyadicToReal d) = Int.ofNat (Nat.log 2 d.mant) + d.exp + 1

For a nonzero dyadic, neural_magnitude matches the expected “power-of-two interval” characterization: mag = ⌊logb 2 (mant)⌋ + exp + 1.

We use this as a key link between the FP32 rounding model (defined using neural_magnitude) and the executable kernel (which naturally computes Nat.log2 mant + exp from the decoded dyadic).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_magnitude_eq_of_bpow_bounds (x : ℝ) (k : ℤ) (hx0 : x ≠ 0) (hlo : neuralBpow binaryRadix k ≤ |x|) (hhi : |x| < neuralBpow binaryRadix (k + 1)) : neuralMagnitude binaryRadix x = k + 1

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fract_real_div_nat (n den : ℕ) (hden : den ≠ 0) : ↑n / ↑den - ↑(n / den) = ↑(n % den) / ↑den

theorem TorchLean.Floats.IEEE754.IEEE32Exec.floor_real_nat_div (n den : ℕ) : ⌊↑n / ↑den⌋ = ↑(n / den)

theorem TorchLean.Floats.IEEE754.IEEE32Exec.div_lt_half_iff (r den : ℕ) (hden : den ≠ 0) : ↑r / ↑den < 2⁻¹ ↔ 2 * r < den

theorem TorchLean.Floats.IEEE754.IEEE32Exec.half_lt_div_iff (r den : ℕ) (hden : den ≠ 0) : 2⁻¹ < ↑r / ↑den ↔ den < 2 * r

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_nearest_even_div_eq_roundQuotEven (num den : ℕ) (hden : den ≠ 0) : neuralNearestEven (↑num / ↑den) = Int.ofNat (roundQuotEven num den)