IEEE32Exec and FP32: Rational Magnitude Bounds

Real semantics of exponent tests for rationals

Some executable rounding code works by inspecting the magnitude of a rational (represented as num / den with Nats) and branching on exponent ranges. These lemmas justify those branches in terms of real inequalities, so later refinement proofs can stay “math-first”.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.ratLtPow2_eq_true_iff (num den : ℕ) (k : ℤ) (hden : den ≠ 0) : ratLtPow2 num den k = true ↔ ↑num / ↑den < neuralBpow binaryRadix k

theorem TorchLean.Floats.IEEE754.IEEE32Exec.ratGePow2_eq_true_iff (num den : ℕ) (k : ℤ) (hden : den ≠ 0) : ratGePow2 num den k = true ↔ neuralBpow binaryRadix k ≤ ↑num / ↑den

Coarse log₂ bounds for rationals

The rounding code needs cheap bounds on log₂ (or “bit-length”) to decide normal vs subnormal cases. We prove coarse but robust bounds that are easy to compute from Nat.log2.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_k0_sub_one_eq (ln ld : ℕ) : neuralBpow binaryRadix (Int.ofNat ln - Int.ofNat ld - 1) = 2 ^ ln / 2 ^ ld.succ

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_k0_add_one_eq (ln ld : ℕ) : neuralBpow binaryRadix (Int.ofNat ln - Int.ofNat ld + 1) = 2 ^ ln.succ / 2 ^ ld

theorem TorchLean.Floats.IEEE754.IEEE32Exec.rat_bounds_k0 (num den : ℕ) (hnum : num ≠ 0) (hden : den ≠ 0) : have ln := num.log2; have ld := den.log2; have k0 := Int.ofNat ln - Int.ofNat ld; neuralBpow binaryRadix (k0 - 1) ≤ ↑num / ↑den ∧ ↑num / ↑den < neuralBpow binaryRadix (k0 + 1)

theorem TorchLean.Floats.IEEE754.IEEE32Exec.floorLog2Rat_bounds (num den : ℕ) (hnum : num ≠ 0) (hden : den ≠ 0) : have k := floorLog2Rat num den; neuralBpow binaryRadix k ≤ ↑num / ↑den ∧ ↑num / ↑den < neuralBpow binaryRadix (k + 1)

FP32 refinement for executable rounding

This is the core bridge step: we prove that the executable rounding kernel (which produces an IEEE32Exec value) agrees with FP32 rounding on reals (fp32Round), provided we stay on the finite/no-overflow path.

Once we have this, most op-level bridge theorems reduce to: “compute an exact dyadic/rational intermediate, then apply this rounding refinement theorem”.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_nearest_even_eq_zero_of_abs_lt_half (x : ℝ) (hx : |x| < 1 / 2) : neuralNearestEven x = 0

theorem TorchLean.Floats.IEEE754.IEEE32Exec.abs_dyadicToReal_lt_bpow_succ_log2 (d : Dyadic) : |dyadicToReal d| < neuralBpow binaryRadix (Int.ofNat d.mant.log2 + d.exp + 1)

A coarse magnitude bound for a decoded dyadic.

Informal: |mant * 2^exp| < 2^(log2 mant + exp + 1). This is convenient when reasoning about normalization by log2 and when relating dyadic magnitudes to exponent ranges.