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:

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

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 the finite fragment of IEEE-754 binary32 (subnormals/rounding via fexp, but no NaN/Inf).
• 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.

@[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).

@[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 small 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.

@[implicit_reducible]

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

Exponentiation, rounded back to the grid.

We define a^b via exp(b * log a) when a > 0. If a ≤ 0 we return 0 to keep the operation total in ℝ. (In practical ML code this is usually guarded or avoided; here we prefer a total spec-level function over partiality.)

@[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.

@[implicit_reducible]

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

Numeric constants for NF via rounded reals.

@[implicit_reducible]

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

Context instance used by TorchLean specs.

We provide a decidable > relation by classical reasoning on ℝ (noncomputable, but fine for the spec layer).

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.