NF: a rounded scalar type (rounding-on-ℝ)

NeuralFloat (the record with a mantissa/exponent) is useful for talking about the grid and for stating format predicates like FLT_format. In many places, though, we want something closer to a “numeric scalar type” that we can plug into higher-level specs and examples.

NF β fexp rnd is that scalar carrier:

• it stores a semantic value val : ℝ,
• and every primitive arithmetic operation rounds back to the format using neural_round.

The public constructor remains available because proof developments sometimes embed an arbitrary real as a comparison value. Such a value need not be representable. NF.IsRepresentable records the grid invariant when a theorem needs it; NF.ofReal and arithmetic results establish that invariant.

So when you write a + b in NF, what you get is:

val(a + b) = round( val(a) + val(b) )

This is the standard textbook model used for floating-point error analysis: compute in reals, then incur a rounding error at each step (Higham/Goldberg style).

Trust boundary:

• NF/NeuralFloat are proof-relevant Lean models of rounded arithmetic (built on ℝ).
• Instantiating NF with IEEE single parameters + round-to-nearest-even models domain-valid, finite, no-overflow arithmetic with binary32's precision and gradual-underflow grid. The format has no upper exponent bound, and Mathlib's real division, square root, and logarithm are totalized; exceptional IEEE behavior belongs to IEEE32Exec.
• Correspondence to hardware float32 / Lean's builtin Float is not proved in this file; that connection is an external assumption/interface boundary (or requires a separate verified kernel).

structure TorchLean.Floats.NF (β : NeuralRadix) (fexp : ℤ → ℤ) (rnd : ℝ → ℤ) : Type

Rounded scalar value at a given radix/format/rounding mode.

β is the radix (typically 2), fexp selects the exponent grid, and rnd rounds the scaled mantissa to an integer.

• val : ℝ

  val.

@[inline]

noncomputable def TorchLean.Floats.NF.roundR {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : ℝ) : ℝ

The rounding operator associated with the format: roundR x = neural_round … x.

@[inline]

noncomputable def TorchLean.Floats.NF.ofReal {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : ℝ) : NF β fexp rnd

Inject a real into NF by rounding it onto the target grid.

@[inline]

noncomputable def TorchLean.Floats.NF.toReal {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} (x : NF β fexp rnd) : ℝ

Forgetful projection (semantic view): treat an NF as a real number.

def TorchLean.Floats.NF.IsRepresentable {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : NF β fexp rnd) : Prop

The semantic value of an NF lies on its declared radix/exponent grid.

@[simp]

theorem TorchLean.Floats.NF.toReal_ofReal {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : ℝ) : (ofReal x).toReal = roundR x

toReal (ofReal x) is definitionally the rounded real roundR x.

@[simp]

theorem TorchLean.Floats.NF.val_ofReal {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : ℝ) : (ofReal x).val = roundR x

The underlying val field of ofReal x is roundR x.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instInhabited {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Inhabited (NF β fexp rnd)

A default inhabitant (rounded zero).

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instCoeNat {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Coe ℕ (NF β fexp rnd)

Coerce natural literals into NF by rounding (n : ℝ) onto the grid.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instZero {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Zero (NF β fexp rnd)

0 and 1 for NF are defined via ofReal, so they live on the target grid.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instOne {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : One (NF β fexp rnd)

1 : NF is ofReal 1, i.e. the rounded real 1 on the target grid.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instNeg {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Neg (NF β fexp rnd)

Arithmetic on NF is “compute in ℝ, then round”.

This is the key choice that makes many error bounds compositional: each primitive incurs at most ulp/2 of rounding error (under round-to-nearest assumptions), so long compositions can be bounded by accumulating per-op bounds.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instAdd {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Add (NF β fexp rnd)

Rounded addition: val(a + b) = roundR (val a + val b).

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instSub {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Sub (NF β fexp rnd)

Rounded subtraction: val(a - b) = roundR (val a - val b).

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instMul {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Mul (NF β fexp rnd)

Rounded multiplication: val(a * b) = roundR (val a * val b).

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instDiv {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Div (NF β fexp rnd)

Rounded division: val(a / b) = roundR (val a / val b).

noncomputable def TorchLean.Floats.NF.checkedDiv {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (a b : NF β fexp rnd) : Option (NF β fexp rnd)

Checked rounded division. Unlike the totalized Div instance, this rejects a zero divisor.

@[simp]

theorem TorchLean.Floats.NF.checkedDiv_eq_none_iff {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (a b : NF β fexp rnd) : a.checkedDiv b = none ↔ b.val = 0

Checked division rejects exactly the zero-divisor case.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instBEq {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} : BEq (NF β fexp rnd)

Boolean equality on NF values (semantic equality of reals).

This is not intended as a fast runtime check (it relies on classical decidability for ℝ), but it is convenient for specs that want a BEq instance for logging or compact examples.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instLT {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} : LT (NF β fexp rnd)

Strict order on NF induced by the strict order on ℝ via the val field.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instLE {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} : LE (NF β fexp rnd)

Non-strict order on NF induced by ≤ on ℝ via the val field.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instMin {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} : Min (NF β fexp rnd)

Min/max in the semantic order on ℝ, lifted to NF.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instMax {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} : Max (NF β fexp rnd)

max on NF, defined by comparing the underlying real values.

noncomputable def TorchLean.Floats.NF.powNat {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (a : NF β fexp rnd) (n : ℕ) : NF β fexp rnd

Natural exponentiation evaluated in ℝ and rounded once onto the target grid.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instPowNat {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Pow (NF β fexp rnd) ℕ

Natural powers have unambiguous real semantics for every base.

noncomputable def TorchLean.Floats.NF.positiveRealPow {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (a b : NF β fexp rnd) (_ha : 0 < a.val) : NF β fexp rnd

Positive-base real exponentiation, evaluated as exp (b * log a) and rounded once.

The positivity proof is part of the API so negative bases and 0^0 cannot silently acquire an arbitrary totalized value.

noncomputable def TorchLean.Floats.NF.checkedRealPow {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (a b : NF β fexp rnd) : Option (NF β fexp rnd)

Checked real exponentiation.

Positive bases accept every real exponent. Negative bases accept integer exponents, including negative integer exponents. Zero uses the usual natural-power convention for nonnegative integer exponents, maps positive noninteger exponents to zero, and rejects negative exponents. Thus the remaining rejected case is a negative base with a noninteger exponent. Natural powers can also use powNat directly.

theorem TorchLean.Floats.NF.checkedRealPow_of_pos {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (a b : NF β fexp rnd) (ha : 0 < a.val) : a.checkedRealPow b = some (a.positiveRealPow b ha)

On a positive base, checked exponentiation is the ordinary positive real-power formula.

theorem TorchLean.Floats.NF.checkedRealPow_zero_of_pos_not_int {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (a b : NF β fexp rnd) (ha : a.val = 0) (hb : 0 < b.val) (hni : ¬∃ (z : ℤ), b.val = ↑z) : a.checkedRealPow b = some (ofReal 0)

A positive noninteger exponent of zero uses the unambiguous real value zero.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instMathFunctions {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : MathFunctions (NF β fexp rnd)

Common math functions lifted to NF by “evaluate in ℝ, then round”.

This matches the same modeling decision as Add/Mul: the spec says what real function we intend, and the rounding model accounts for discretization.

noncomputable def TorchLean.Floats.NF.checkedSqrt {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : NF β fexp rnd) : Option (NF β fexp rnd)

Checked rounded square root; negative inputs are rejected instead of using real totalization.

@[simp]

theorem TorchLean.Floats.NF.checkedSqrt_eq_none_iff {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : NF β fexp rnd) : x.checkedSqrt = none ↔ ¬0 ≤ x.val

Checked square root rejects exactly the negative inputs.

noncomputable def TorchLean.Floats.NF.checkedLog {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : NF β fexp rnd) : Option (NF β fexp rnd)

Checked rounded logarithm; zero and negative inputs are rejected.

@[simp]

theorem TorchLean.Floats.NF.checkedLog_eq_none_iff {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : NF β fexp rnd) : x.checkedLog = none ↔ ¬0 < x.val

Checked logarithm rejects exactly the nonpositive inputs.

@[implicit_reducible]

noncomputable instance TorchLean.Floats.NF.instNumbers {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] : Numbers (NF β fexp rnd)

Numeric constants for NF via rounded reals.

noncomputable def TorchLean.Floats.NF.mantExp {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : NF β fexp rnd) : ℤ × ℤ

Extract an approximate radix-β mantissa/exponent pair for debugging.

We compute:

• e := cexp(x) from the format (fexp),
• m := rnd( scaled_mantissa(x) ),

so that x ≈ m · β^e (with the approximation coming from rounding).

This is meant for logs / human inspection; it is not used by the core proofs.

@[inline]

def TorchLean.Floats.NF.fmtInt (n : ℤ) : String

Format an integer in base 10.

noncomputable def TorchLean.Floats.NF.formatRadix {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (x : NF β fexp rnd) : String

Format an NF value as a radix-β scientific string "m * β^e".

Example (β = 2): "-123 * 2^7".

noncomputable def TorchLean.Floats.NF.formatIntervalRadix {β : NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [NeuralValidExp fexp] (lo hi : NF β fexp rnd) : String

Format an interval [lo, hi] for NF values using formatRadix.