RatScaling

Small algebraic helper lemmas about powers of two and Nat.shiftLeft used by the IEEE32Exec kernel.

Several proofs (notably the bridge theorems and division soundness) need to normalize expressions of the form dyadicToReal dx / dyadicToReal dy into the same signed rational shape that the executable implementation uses:

• align dyadic exponents by shifting either the numerator or denominator,
• extract a sign bit via Bool.xor,
• and express the quotient as ±(num/den).

This module provides the shared normalization lemmas used by the bridge theorems without creating import cycles.

noncomputable def TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (d : Dyadic) : ℝ

Interpret an exact dyadic (-1)^sign * mant * 2^exp as a real.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.scaleRat_ofNat (num den sh : ℕ) : ↑num / ↑den * neuralBpow binaryRadix (Int.ofNat sh) = ↑(num.shiftLeft sh) / ↑den

Scale a rational by a nonnegative exponent difference by shifting the numerator.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.scaleRat_negSucc (num den sh : ℕ) : ↑num / ↑den * neuralBpow binaryRadix (Int.negSucc sh) = ↑num / ↑(den.shiftLeft (sh + 1))

Scale a rational by a negative exponent difference by shifting the denominator.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neural_bpow_div (e1 e2 : ℤ) : neuralBpow binaryRadix e1 / neuralBpow binaryRadix e2 = neuralBpow binaryRadix (e1 - e2)

Exponent subtraction law for neuralBpow, packaged as a division identity.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_div_eq_signedRat_mul (dx dy : Dyadic) (hy0 : dy.mant ≠ 0) : have sign := dx.sign ^^ dy.sign; have eDiff := dx.exp - dy.exp; match match eDiff with | Int.ofNat sh => (dx.mant.shiftLeft sh, dy.mant) | Int.negSucc sh => (dx.mant, dy.mant.shiftLeft (sh + 1)) with | (num, den) => dyadicToReal dx / dyadicToReal dy = (if sign = true then -1 else 1) * (↑num / ↑den)

Rewrite dyadic division into the same signed rational shape used by div/divDown/divUp.

This is the "multiplicative" form: (-1)^sign * (num/den).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal_div_eq_signedRat (dx dy : Dyadic) (hy0 : dy.mant ≠ 0) : have sign := dx.sign ^^ dy.sign; have eDiff := dx.exp - dy.exp; match match eDiff with | Int.ofNat sh => (dx.mant.shiftLeft sh, dy.mant) | Int.negSucc sh => (dx.mant, dy.mant.shiftLeft (sh + 1)) with | (num, den) => dyadicToReal dx / dyadicToReal dy = if sign = true then -(↑num / ↑den) else ↑num / ↑den

Rewrite dyadic division into a signed rational ±(num/den).

This is the "conditional negation" form used by the directed rounding soundness proofs.