NF: a rounded scalar type

FloatRep (the record with a mantissa/exponent) is useful for talking about the grid and for stating format predicates like FLTFormat. Higher-level specifications are easier to state with a scalar carrier that already performs the rounding step.

NF β fexp rnd is that scalar carrier:

• it stores a semantic value val : ℝ,
• and every primitive arithmetic operation rounds back to the format using 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.

Addition, for example, satisfies:

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 and FloatRep model real values and rounding in Lean.
• 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 ExecFloat.Binary (exponentBits := 8) (fractionBits := 23) and its binary-interchange model.
• 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 FloatLib.Floats.Formats.Flocq.NF (β : Numerics.Radix) (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 : ℝ

  Exact real value represented by this rounded-real model value.

@[inline]

noncomputable def FloatLib.Floats.Formats.Flocq.NF.roundR {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (x : ℝ) : ℝ

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

@[inline]

noncomputable def FloatLib.Floats.Formats.Flocq.NF.ofReal {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (x : ℝ) : NF β fexp rnd

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

@[inline]

noncomputable def FloatLib.Floats.Formats.Flocq.NF.toReal {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} (x : NF β fexp rnd) : ℝ

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

def FloatLib.Floats.Formats.Flocq.NF.IsRepresentable {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (x : NF β fexp rnd) : Prop

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

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.toReal_ofReal {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (x : ℝ) : (ofReal x).toReal = roundR x

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

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.val_ofReal {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (x : ℝ) : (ofReal x).val = roundR x

The underlying val field of ofReal x is roundR x.

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instInhabited {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Inhabited (NF β fexp rnd)

A default inhabitant (rounded zero).

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instNatCast {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : NatCast (NF β fexp rnd)

Cast a natural number into NF by rounding (n : ℝ) onto the grid.

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instZero {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Zero (NF β fexp rnd)

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

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instOne {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : One (NF β fexp rnd)

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

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instNeg {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Neg (NF β fexp rnd)

Negate the real value and round onto the grid. For a representable input, negation is exact.

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instAdd {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Add (NF β fexp rnd)

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

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instSub {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Sub (NF β fexp rnd)

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

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instMul {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Mul (NF β fexp rnd)

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

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instDiv {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Div (NF β fexp rnd)

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

noncomputable def FloatLib.Floats.Formats.Flocq.NF.checkedDiv {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp 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 FloatLib.Floats.Formats.Flocq.NF.checkedDiv_eq_none_iff {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (a b : NF β fexp rnd) : a.checkedDiv b = none ↔ b.val = 0

Checked division rejects exactly the zero-divisor case.

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instLinearOrder {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} : LinearOrder (NF β fexp rnd)

Linear order on NF induced by val, with semantic minimum and maximum.

noncomputable def FloatLib.Floats.Formats.Flocq.NF.powNat {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (a : NF β fexp rnd) (n : ℕ) : NF β fexp rnd

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

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instPowNat {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Pow (NF β fexp rnd) ℕ

Natural powers have unambiguous real semantics for every base.

noncomputable def FloatLib.Floats.Formats.Flocq.NF.positiveRealPow {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp 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 FloatLib.Floats.Formats.Flocq.NF.checkedRealPow {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp 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 FloatLib.Floats.Formats.Flocq.NF.checkedRealPow_of_pos {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp 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 FloatLib.Floats.Formats.Flocq.NF.checkedRealPow_zero_of_pos_not_int {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp 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.

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instMathFunctions {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Numerics.MathFunctions (NF β fexp rnd)

Evaluate each mathematical function in ℝ and round once. These noncomputable specifications use Mathlib's totalized real functions; checkedSqrt and checkedLog enforce their usual real domains.

noncomputable def FloatLib.Floats.Formats.Flocq.NF.checkedSqrt {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (x : NF β fexp rnd) : Option (NF β fexp rnd)

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

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.checkedSqrt_eq_none_iff {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (x : NF β fexp rnd) : x.checkedSqrt = none ↔ ¬0 ≤ x.val

Checked square root rejects exactly the negative inputs.

noncomputable def FloatLib.Floats.Formats.Flocq.NF.checkedLog {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (x : NF β fexp rnd) : Option (NF β fexp rnd)

Checked rounded logarithm; zero and negative inputs are rejected.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.checkedLog_eq_none_iff {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (x : NF β fexp rnd) : x.checkedLog = none ↔ ¬0 < x.val

Checked logarithm rejects exactly the nonpositive inputs.