Notation for TorchLean's FP32 model

TorchLean uses a proof-oriented float32 model (FP32) defined by:

• a radix $\beta=2$,
• the canonical IEEE-754 binary32 exponent function (fexp32), and
• round-to-nearest, ties-to-even (rnd32).

This file provides small, ergonomic aliases for the corresponding real-level operators:

• round₃₂ x (or ASCII round32 x): round $x\in\mathbb{R}$ to the binary32 grid.
• ulp₃₂ x and eps₃₂ x: the ULP scale (and half-ULP) associated with $x$.

We keep these under TorchLean.Floats so they are available where float semantics are in focus, without polluting unrelated namespaces.

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.round32 (x : ℝ) : ℝ

Real-level binary32 rounding operator for the canonical fexp32/rnd32 configuration.

This is definitionally the same rounding operator used in the NF/FP32 semantics, but phrased as a function $\mathbb{R}\to\mathbb{R}$ (useful for bridge theorems and error bounds).

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.ulp32 (x : ℝ) : ℝ

One ULP at x for the canonical binary32 exponent configuration.

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.eps32 (x : ℝ) : ℝ

Convenience abbreviation: half an ULP at x.

@[simp]

theorem TorchLean.Floats.ulp32_zero : ulp32 0 = neuralBpow binaryRadix (-149)

Binary32 has a smallest grid step, so its ULP at zero is $2^{-149}$.

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.round₃₂ (x : ℝ) : ℝ

Unicode alias for round32 (useful in error-bound statements).

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.ulp₃₂ (x : ℝ) : ℝ

Unicode alias for ulp32 (useful in error-bound statements).

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.eps₃₂ (x : ℝ) : ℝ

Unicode alias for eps32 (half-ULP).

@[simp]

theorem TorchLean.Floats.round₃₂_eq_round32 (x : ℝ) : round₃₂ x = round32 x

round₃₂ is definitionally equal to round32 (unicode → ASCII simp).

@[simp]

theorem TorchLean.Floats.ulp₃₂_eq_ulp32 (x : ℝ) : ulp₃₂ x = ulp32 x

ulp₃₂ is definitionally equal to ulp32 (unicode → ASCII simp).

@[simp]

theorem TorchLean.Floats.eps₃₂_eq_eps32 (x : ℝ) : eps₃₂ x = eps32 x

eps₃₂ is definitionally equal to eps32 (unicode → ASCII simp).