FloatRep core (Flocq-style rounded arithmetic)

The rounded-real model separates representation, value, and format:

• represent a value with integer mantissa $m$ and exponent $e$,
• interpret it as the real number $m\beta^e$,
• describe the format via an exponent-selection function fexp : ℤ → ℤ and a rounding operator.

This decomposition is the same one used by the Coq library Flocq. It makes many theorems reusable across formats (fixed-point, unbounded floats, and lower-exponent-bounded floats) and aligns well with ULP-style error bounds from numerical analysis.

For executable, bit-level binary semantics (NaN/Inf/signed zero), see FloatLib/Floats/Formats/BinaryInterchange/.

References

• Flocq project (documentation + sources): https://flocq.gitlabpages.inria.fr/flocq/
• S. Boldo, G. Melquiond, “Flocq: a unified Coq library for proving floating-point algorithms correct” (ARITH 2011), DOI: 10.1109/ARITH.2011.40
• IEEE Standard for Floating-Point Arithmetic (IEEE 754-2019)
• N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM, 2002

structure FloatLib.Floats.Formats.Flocq.FloatRep (β : Numerics.Radix) : Type

A radix-$\beta$ floating-point representation with integer mantissa and exponent.

• mantissa : ℤ

  Integer mantissa m.

• exponent : ℤ

  Integer exponent e.

def FloatLib.Floats.Formats.Flocq.FloatRep.isZero {β : Numerics.Radix} (f : FloatRep β) : Prop

Structural zero test (mantissa is exactly 0).

def FloatLib.Floats.Formats.Flocq.FloatRep.sign {β : Numerics.Radix} (f : FloatRep β) : ℤ

Sign of the mantissa (matches the sign of toReal since $\beta^e>0$).

noncomputable def FloatLib.Floats.Formats.Flocq.bpow (β : Numerics.Radix) (e : ℤ) : ℝ

Base power: $\beta^e$ as a real number.

This is Flocq's bpow concept: the scaling factor used to interpret mantissa/exponent pairs.

theorem FloatLib.Floats.Formats.Flocq.bpow.pos (β : Numerics.Radix) (e : ℤ) : 0 < bpow β e

Base powers are positive: $\beta^e>0$ for any exponent $e$.

theorem FloatLib.Floats.Formats.Flocq.bpow.nonneg (β : Numerics.Radix) (e : ℤ) : 0 ≤ bpow β e

Base powers are nonnegative: $\beta^e\ge0$ for any exponent $e$.

theorem FloatLib.Floats.Formats.Flocq.bpow.ne_zero (β : Numerics.Radix) (e : ℤ) : bpow β e ≠ 0

Base powers are never zero.

theorem FloatLib.Floats.Formats.Flocq.bpow.add_exp (β : Numerics.Radix) (e1 e2 : ℤ) : bpow β (e1 + e2) = bpow β e1 * bpow β e2

Exponent addition law: $\beta^{e_1+e_2}=\beta^{e_1}\beta^{e_2}$.

theorem FloatLib.Floats.Formats.Flocq.bpow.neg_exp (β : Numerics.Radix) (e : ℤ) : bpow β (-e) = (bpow β e)⁻¹

Negating the exponent inverts the base power: $\beta^{-e}=(\beta^e)^{-1}$.

theorem FloatLib.Floats.Formats.Flocq.bpow.sub_exp (β : Numerics.Radix) (e₁ e₂ : ℤ) : bpow β (e₁ - e₂) = bpow β e₁ / bpow β e₂

Exponent subtraction corresponds to division of radix powers.

noncomputable def FloatLib.Floats.Formats.Flocq.toReal {β : Numerics.Radix} (f : FloatRep β) : ℝ

Interpret a FloatRep as the real number $m\beta^e$.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.toReal.zero_iff {β : Numerics.Radix} (f : FloatRep β) : toReal f = 0 ↔ f.mantissa = 0

toReal is zero iff the mantissa is zero (since $\beta^e\ne0$).

noncomputable def FloatLib.Floats.Formats.Flocq.magnitude (β : Numerics.Radix) (x : ℝ) : ℤ

Magnitude in base $\beta$ of a real number.

This matches the usual definition $\operatorname{mag}(x)=\lfloor\log_\beta|x|\rfloor+1$ for $x\ne0$, and $0$ for $x=0$. It is the bridge between a real input $x$ and the exponent-selection function fexp.

class FloatLib.Floats.Formats.Flocq.ValidExp (fexp : ℤ → ℤ) : Prop

Validity predicate for exponent-selection functions.

This is the exponent-validity condition used by Flocq. Properties that are not consequences of validity, such as monotonicity, are separate classes so generic results do not acquire unnecessary hypotheses.

• flocq_valid (k : ℤ) : (fexp k < k → fexp (k + 1) ≤ k) ∧ (k ≤ fexp k → fexp (fexp k + 1) ≤ fexp k ∧ ∀ l ≤ fexp k, fexp l = fexp k)

  Exponent compatibility at successive magnitudes and below a negligible exponent.

class FloatLib.Floats.Formats.Flocq.MonotoneExp (fexp : ℤ → ℤ) : Prop

Exponent-selection functions that preserve order.

• monotone (k1 k2 : ℤ) : k1 ≤ k2 → fexp k1 ≤ fexp k2

  Increasing the magnitude cannot decrease the selected exponent.

class FloatLib.Floats.Formats.Flocq.BoundedExpGrowth (fexp : ℤ → ℤ) : Prop

Optional local growth bound used by selected numerical estimates.

• boundedGrowth (k : ℤ) : |fexp (k + 1) - fexp k| ≤ 1

  Successive magnitudes select exponents differing by at most one.

def FloatLib.Floats.Formats.Flocq.IsNegligibleExp (fexp : ℤ → ℤ) (n : ℤ) : Prop

A witness that the format has a lower exponent region, in Flocq's sense.

noncomputable def FloatLib.Floats.Formats.Flocq.negligibleExp (fexp : ℤ → ℤ) : Option ℤ

Select a witness $n\le\mathtt{fexp}(n)$ when the format has one. Unbounded formats such as FLX return none; lower-bounded formats such as FLT return some n.

theorem FloatLib.Floats.Formats.Flocq.negligibleExp_spec {fexp : ℤ → ℤ} {n : ℤ} (h : negligibleExp fexp = some n) : IsNegligibleExp fexp n

A selected negligible exponent satisfies $n\le\mathtt{fexp}(n)$.

theorem FloatLib.Floats.Formats.Flocq.negligibleExp_eq_none_iff (fexp : ℤ → ℤ) : negligibleExp fexp = none ↔ ¬∃ (n : ℤ), IsNegligibleExp fexp n

A format has no selected negligible exponent exactly when no negligible exponent exists.

noncomputable def FloatLib.Floats.Formats.Flocq.cexp (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) : ℤ

Canonical exponent (cexp in Flocq terminology).

Apply fexp to the input's magnitude; at zero this gives fexp 0. The ValidExp instance restricts the API to valid exponent functions, although evaluating this expression needs only fexp.

def FloatLib.Floats.Formats.Flocq.Canonical (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (f : FloatRep β) : Prop

A float representation is canonical when its stored exponent is the exponent selected for its value.

noncomputable def FloatLib.Floats.Formats.Flocq.scaledMantissa (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) : ℝ

Scaled mantissa $x\beta^{-\operatorname{cexp}(x)}$.

Intuitively: rescale x so that rounding “happens around exponent 0”, which is where rnd acts.

def FloatLib.Floats.Formats.Flocq.genericFormat (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) : Prop

Generic format predicate (Flocq-style).

This says that $x$ is exactly representable in the format picked out by $\beta$ and fexp. One way to read it is: the scaled mantissa is an integer (so there is no rounding error).

noncomputable def FloatLib.Floats.Formats.Flocq.ulp (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) : ℝ

Unit in the last place (ULP) associated with $x$ and the format selected by fexp.

This is the scale of the “one ulp” step at the exponent selected by cexp. For round-to-nearest, many standard bounds have the shape $|\operatorname{round}(x)-x|\le\operatorname{ulp}(x)/2$.

At zero, a negligible exponent determines the spacing when one exists; otherwise the ULP is zero.

theorem FloatLib.Floats.Formats.Flocq.ulp.nonneg (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) : 0 ≤ ulp β fexp x

ulp is always nonnegative.

Informally: an ulp is a step size on a real grid, so it cannot be negative.

theorem FloatLib.Floats.Formats.Flocq.ulp.pos_of_ne_zero (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) (hx : x ≠ 0) : 0 < ulp β fexp x

ulp is strictly positive away from zero.

If $x\ne0$, the exponent selection $\operatorname{cexp}(x)$ picks a power of $\beta$, which is strictly positive.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.ulp.zero (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] : ulp β fexp 0 = match negligibleExp fexp with | some n => bpow β (fexp n) | none => 0

The ULP at zero is determined by the format's negligible exponent, when one exists.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.ulp.of_ne_zero (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) (hx : x ≠ 0) : ulp β fexp x = bpow β (cexp β fexp x)

Away from zero, ulp is the base grid step $\beta^{\operatorname{cexp}(x)}$.