Flocq-style formats (FIX / FLX / FLT)

Exponent-selection functions fexp : ℤ → ℤ describe three real-valued format families:

• FIX is a fixed-exponent grid;
• FLX has fixed precision and unbounded exponents;
• FLT has fixed precision, a lower exponent bound, and gradual underflow.

FLT has no upper exponent bound or overflow. Executable binary formats with infinities, NaNs, and signed zeros are defined in FloatLib/Floats/Formats/BinaryInterchange/.

References:

• Flocq project: 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)

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.FormatPrecision : Type

A positive number of radix digits for FLX, FLT, and FTZ formats.

Raw exponent functions remain available for algebraic proofs, but callers accepting an integer configuration should first use FormatPrecision.ofInt?. This prevents a zero or negative precision from being silently reinterpreted through an absolute-value conversion.

This is Mathlib's proof-erased positive-natural carrier rather than another project-local structure.

def FloatLib.Floats.Formats.Flocq.FormatPrecision.toInt (precision : FormatPrecision) : ℤ

Convert a proof-carrying format precision to the integer parameter used by exponent formulas.

def FloatLib.Floats.Formats.Flocq.FormatPrecision.ofNat? (digits : ℕ) : Option FormatPrecision

Check a natural-number precision at a configuration boundary.

def FloatLib.Floats.Formats.Flocq.FormatPrecision.ofInt? (digits : ℤ) : Option FormatPrecision

Check an integer precision, rejecting zero and every negative value.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.FormatPrecision.toInt_pos (precision : FormatPrecision) : 0 < precision.toInt

A checked precision remains positive after conversion to the integer exponent parameter.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.FormatPrecision.ofNat?_eq_none_iff (digits : ℕ) : ofNat? digits = none ↔ digits = 0

Natural precision validation fails exactly at zero.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.FormatPrecision.ofInt?_eq_none_iff (digits : ℤ) : ofInt? digits = none ↔ digits ≤ 0

Integer precision validation fails exactly for nonpositive inputs.

def FloatLib.Floats.Formats.Flocq.fixExp (emin : ℤ) : ℤ → ℤ

fixExp emin is the simplest exponent-selection function: it always returns the same exponent.

This is Flocq's FIX_exp. It describes values living on a single fixed grid $\beta^{\mathtt{emin}}\mathbb{Z}$, as in fixed-point arithmetic or quantization.

instance FloatLib.Floats.Formats.Flocq.fixValidExp (emin : ℤ) : ValidExp (fixExp emin)

fixExp emin satisfies the exponent-validity axioms ValidExp. Registering the result as an instance lets the FIX theorems reuse the generic format lemmas shared with FLX and FLT.

instance FloatLib.Floats.Formats.Flocq.fixMonotoneExp (emin : ℤ) : MonotoneExp (fixExp emin)

instance FloatLib.Floats.Formats.Flocq.fixBoundedExpGrowth (emin : ℤ) : BoundedExpGrowth (fixExp emin)

theorem FloatLib.Floats.Formats.Flocq.ulp_zero_FIX {β : Numerics.Radix} (emin : ℤ) : ulp β (fixExp emin) 0 = bpow β emin

The ULP at zero for a fixed-point grid is its fixed grid step.

def FloatLib.Floats.Formats.Flocq.FIXFormat {β : Numerics.Radix} (emin : ℤ) (x : ℝ) : Prop

FIXFormat emin x says that x is exactly representable on the fixed grid with exponent emin.

The predicate is phrased through an existential FloatRep β so that it composes with the rest of the rounding model (toReal, ULP bounds and so on).

def FloatLib.Floats.Formats.Flocq.flxExp (prec : ℤ) : ℤ → ℤ

flxExp prec is the unbounded-exponent family.

This is Flocq's FLX_exp: a floating-point format with no exponent bounds and mantissa precision prec. It is a convenient intermediate model for proofs because it removes the underflow and overflow corner cases while still tracking mantissa rounding.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.flxValidExp (prec : ℤ) (h : 0 < prec) : ValidExp (flxExp prec)

flxExp prec satisfies ValidExp for positive precision.

theorem FloatLib.Floats.Formats.Flocq.validExp_FLX_iff (prec : ℤ) : ValidExp (flxExp prec) ↔ 0 < prec

flxExp prec satisfies the generic exponent axioms exactly when prec is positive.

def FloatLib.Floats.Formats.Flocq.FormatPrecision.flxExp (precision : FormatPrecision) : ℤ → ℤ

The unbounded exponent selector associated with a checked precision.

instance FloatLib.Floats.Formats.Flocq.FormatPrecision.flxExpValid (precision : FormatPrecision) : ValidExp precision.flxExp

A checked precision automatically discharges the FLX exponent-validity obligation.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.flxMonotoneExp (prec : ℤ) : MonotoneExp (flxExp prec)

The FLX exponent selector is monotone for every precision parameter.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.flxBoundedExpGrowth (prec : ℤ) : BoundedExpGrowth (flxExp prec)

The FLX exponent selector has bounded one-step growth.

def FloatLib.Floats.Formats.Flocq.FLXFormat {β : Numerics.Radix} (prec : ℤ) (x : ℝ) : Prop

Exact representability predicate for FLX.

The precision is positive, and $x=m\beta^e$ for an integer mantissa satisfying $|m|<\beta^{\mathtt{prec}}$.

theorem FloatLib.Floats.Formats.Flocq.not_flxFormat_of_nonpos {β : Numerics.Radix} (prec : ℤ) (hprec : prec ≤ 0) (x : ℝ) : ¬FLXFormat prec x

Nonpositive precision is rejected by the explicit FLX format predicate.

theorem FloatLib.Floats.Formats.Flocq.negligibleExp_FLX (prec : ℤ) (hprec : 0 < prec) : negligibleExp (flxExp prec) = none

The unbounded FLX exponent function has no negligible exponent.

theorem FloatLib.Floats.Formats.Flocq.ulp_zero_FLX {β : Numerics.Radix} (prec : ℤ) (hprec : 0 < prec) : ulp β (flxExp prec) 0 = 0

Consequently, the generic ULP of zero is zero for FLX.

def FloatLib.Floats.Formats.Flocq.fltExp (emin prec : ℤ) : ℤ → ℤ

fltExp emin prec is the lower-exponent-bounded family with gradual underflow.

This is Flocq's FLT_exp. The exponent is bounded below by emin but has no upper bound, so the format models gradual underflow but not overflow, infinities, or NaNs. Gradual underflow is captured by taking max (e - prec) emin.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.fltValidExp (emin prec : ℤ) (h : 0 < prec) : ValidExp (fltExp emin prec)

fltExp emin prec satisfies ValidExp for positive precision.

This validity witness connects proofs to an executable binary descriptor through BinaryInterchange.Model.fexpOf and BinaryInterchange.Model.roundAt.

theorem FloatLib.Floats.Formats.Flocq.validExp_FLT_iff (emin prec : ℤ) : ValidExp (fltExp emin prec) ↔ 0 < prec

fltExp emin prec satisfies the exponent axioms exactly for positive precision.

def FloatLib.Floats.Formats.Flocq.FormatPrecision.fltExp (precision : FormatPrecision) (emin : ℤ) : ℤ → ℤ

The gradual-underflow exponent selector associated with a checked precision.

instance FloatLib.Floats.Formats.Flocq.FormatPrecision.fltExpValid (precision : FormatPrecision) (emin : ℤ) : ValidExp (precision.fltExp emin)

A checked precision automatically discharges the gradual-underflow validity obligation.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.fltBoundedExpGrowth (emin prec : ℤ) : BoundedExpGrowth (fltExp emin prec)

The gradual-underflow FLT exponent selector has bounded one-step growth.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.fltMonotoneExp (emin prec : ℤ) : MonotoneExp (fltExp emin prec)

The gradual-underflow FLT exponent selector is monotone.

def FloatLib.Floats.Formats.Flocq.FLTFormat {β : Numerics.Radix} (emin prec : ℤ) (x : ℝ) : Prop

Exact representability predicate for FLT.

The precision is positive, and $x=m\beta^e$ with $|m|<\beta^{\mathtt{prec}}$ and $\mathtt{emin}\le e$. In particular, every nonzero value has magnitude at least $\beta^{\mathtt{emin}}$.

theorem FloatLib.Floats.Formats.Flocq.not_fltFormat_of_nonpos {β : Numerics.Radix} (emin prec : ℤ) (hprec : prec ≤ 0) (x : ℝ) : ¬FLTFormat emin prec x

Nonpositive precision is rejected by the explicit FLT format predicate.

theorem FloatLib.Floats.Formats.Flocq.exists_negligibleExp_FLT (emin prec : ℤ) : ∃ (n : ℤ), IsNegligibleExp (fltExp emin prec) n

FLT has a negligible-exponent witness at emin.

theorem FloatLib.Floats.Formats.Flocq.ulp_zero_FLT {β : Numerics.Radix} (emin prec : ℤ) (hprec : 0 < prec) : ulp β (fltExp emin prec) 0 = bpow β emin

The ULP at zero for FLT is the smallest grid step $\beta^{\mathtt{emin}}$.