Dyadic helpers for executable IEEE32 arithmetic.

This file contains the integer/rational scaffolding used to describe binary significands, exponents, and exact dyadic values before rounding to IEEE32.

structure TorchLean.Floats.IEEE754.IEEE32Exec.Dyadic : Type

Exact dyadic value (-1)^sign * mant * 2^exp used as an intermediate for finite ops.

• sign : Bool

  sign.

• mant : ℕ

  mant.

• exp : ℤ

  exp.

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instReprDyadic : Repr Dyadic

def TorchLean.Floats.IEEE754.IEEE32Exec.instReprDyadic.repr : Dyadic → ℕ → Std.Format

def TorchLean.Floats.IEEE754.IEEE32Exec.instDecidableEqDyadic.decEq (x✝ x✝¹ : Dyadic) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance TorchLean.Floats.IEEE754.IEEE32Exec.instDecidableEqDyadic : DecidableEq Dyadic

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.pow2 (k : ℕ) : ℕ

2^k as a natural number.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.roundShiftRightEven (n shift : ℕ) : ℕ

Round n / 2^shift to nearest, ties-to-even.

This is the primitive "shift + rounding" operation we use when shrinking a mantissa back down to a fixed bit width. It is the same tie-breaking policy as IEEE round-to-nearest-even.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.mkBits (sign : Bool) (exp frac : ℕ) : UInt32

Construct a raw binary32 bit-pattern from fields.

mkBits sign exp frac places the low bits of each supplied field:

• sign in bit 31,
• the low 8 bits of exp in bits 30..23,
• frac in bits 22..0 (masked to 23 bits).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic? (x : IEEE32Exec) : Option Dyadic

Decode a finite binary32 into an exact dyadic value.

Returns none for NaN/Inf.

def TorchLean.Floats.IEEE754.IEEE32Exec.Dyadic.toRat (d : Dyadic) : ℚ

Convert an exact dyadic value to its exact rational value.

def TorchLean.Floats.IEEE754.IEEE32Exec.toRat? (x : IEEE32Exec) : Option ℚ

Exact rational value of a finite binary32 value; returns none for NaN or infinity.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isNaN_eq_false_of_toDyadic?_some {x : IEEE32Exec} {d : Dyadic} (hx : x.toDyadic? = some d) : x.isNaN = false

If toDyadic? x = some d then x is not a NaN.

Informal: toDyadic? only returns some _ for finite floats; NaNs map to none.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isInf_eq_false_of_toDyadic?_some {x : IEEE32Exec} {d : Dyadic} (hx : x.toDyadic? = some d) : x.isInf = false

If toDyadic? x = some d then x is not an infinity.

Informal: toDyadic? only returns some _ for finite floats; infinities map to none.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_eq_true_of_toDyadic?_some {x : IEEE32Exec} {d : Dyadic} (hx : x.toDyadic? = some d) : x.isFinite = true

A successful dyadic decoding certifies that the source bit pattern is finite.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fracField_toNat_lt_pow2_23 (x : IEEE32Exec) : x.fracField.toNat < 2 ^ 23

The extracted binary32 fraction field fits in its 23-bit storage width.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.expField_toNat_le_254_of_isFinite (x : IEEE32Exec) (hfin : x.isFinite = true) : x.expField.toNat ≤ 254

A finite binary32 value has a biased exponent field at most 254.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.sign_eq_signBit_of_toDyadic?_some {x : IEEE32Exec} {d : Dyadic} (hx : x.toDyadic? = some d) : d.sign = x.signBit

Dyadic decoding preserves the sign bit of every finite executable value.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic?_eq_none_of_isNaN {x : IEEE32Exec} (hx : x.isNaN = true) : x.toDyadic? = none

NaNs have no finite dyadic decoding.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic?_eq_none_of_isInf {x : IEEE32Exec} (hx : x.isInf = true) : x.toDyadic? = none

Infinities have no finite dyadic decoding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.exists_toDyadic?_of_not_isNaN_not_isInf {x : IEEE32Exec} (hnan : x.isNaN = false) (hinf : x.isInf = false) : ∃ (d : Dyadic), x.toDyadic? = some d

A value that is neither NaN nor infinity has an exact dyadic decoding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.exists_toDyadic?_of_isFinite {x : IEEE32Exec} (hx : x.isFinite = true) : ∃ (d : Dyadic), x.toDyadic? = some d

Every finite binary32 value has an exact dyadic decoding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic?_isSome_eq_isFinite (x : IEEE32Exec) : x.toDyadic?.isSome = x.isFinite

Dyadic decoding succeeds exactly on finite executable binary32 values.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic?_eq_zero_of_isZero {x : IEEE32Exec} (hx : x.isZero = true) : x.toDyadic? = some { sign := x.signBit, mant := 0, exp := 0 }

Both signed zeros decode to the zero dyadic while retaining their sign bit.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isZero_eq_true_of_toDyadic?_some_of_mant_eq_zero {x : IEEE32Exec} {d : Dyadic} (hx : x.toDyadic? = some d) (hm : d.mant = 0) : x.isZero = true

A decoded dyadic has zero mantissa only when the source bit pattern is a signed zero.

Rounding back to binary32

The general pattern for the finite ops in this file is:

1. decode float32(s) to an exact intermediate representation (Dyadic for + - * fma sqrt, rationals for /),
2. compute the exact result in that intermediate representation,
3. round once to float32 using round-to-nearest, ties-to-even.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.roundDyadicToIEEE32 (d : Dyadic) : IEEE32Exec

Round an exact dyadic value to binary32 (ties-to-even).

This function implements:

• overflow to ±Inf,
• gradual underflow into subnormals (down to exponent -149),
• underflow-to-zero below 2^-150 (half the minimum subnormal, where ties-to-even chooses 0),
• mantissa rounding to the 24-bit precision of binary32 normal numbers.

Exact dyadic arithmetic (finite core)

Dyadic is closed under + and * (at the exact level). We use these helpers before rounding back to float32.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.addDyadic (a b : Dyadic) : Dyadic

Exact dyadic addition.

We align exponents by shifting the mantissa of the operand with the larger exponent, add signed integers, and then return an exact dyadic (no rounding yet).

Exact rationals for division

For division we compute an exact rational num/den (with den > 0) and then round it to binary32 using round-to-nearest, ties-to-even.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.roundQuotEven (num den : ℕ) : ℕ

Round num/den to nearest, ties-to-even (assumes den > 0).

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.ratLtPow2 (num den : ℕ) (k : ℤ) : Bool

Test whether num/den < 2^k without converting to reals.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.ratGePow2 (num den : ℕ) (k : ℤ) : Bool

Test whether num/den ≥ 2^k without converting to reals.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.floorLog2Rat (num den : ℕ) : ℤ

Compute ⌊log₂(num/den)⌋ as an Int (assumes num > 0 and den > 0).

We start from the initial estimate log2(num) - log2(den) and then adjust by checking against powers of two.

@[inline]

def TorchLean.Floats.IEEE754.IEEE32Exec.roundRatToIEEE32 (sign : Bool) (num den : ℕ) : IEEE32Exec

Round an exact rational num/den to binary32 (ties-to-even).

This is the division analogue of roundDyadicToIEEE32: it uses the same exponent thresholds and the same final mantissa rounding policy.