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.

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

2^k as a natural number.

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.

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

Construct a raw binary32 bit-pattern from fields.

mkBits sign exp frac places:

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

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

Decode a finite binary32 into an exact dyadic value.

Returns none for NaN/Inf.

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.

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.

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.

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.

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

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

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

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

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

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

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.

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.