Notation for TorchLean's FP32 model

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

• a radix (β = 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 : ℝ 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 ℝ → ℝ (useful for bridge theorems and error bounds).

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.ulp32 (x : ℝ) (phase : TrainingPhase := TrainingPhase.forward) : ℝ

One ULP at x for the canonical binary32 exponent configuration.

The optional phase parameter matches TorchLean's mixed-precision hook: TrainingPhase.requires_high_precision tightens the bound by one extra bit.

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.eps32 (x : ℝ) (phase : TrainingPhase := TrainingPhase.forward) : ℝ

Convenience abbreviation: half-ULP at x (with the same optional phase hook as ulp32).

@[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 : ℝ) (phase : TrainingPhase := TrainingPhase.forward) : ℝ

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

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.eps₃₂ (x : ℝ) (phase : TrainingPhase := TrainingPhase.forward) : ℝ

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 : ℝ) (phase : TrainingPhase := TrainingPhase.forward) : ulp₃₂ x phase = ulp32 x phase

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

@[simp]

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

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