Flocq-style formats (FIX / FLX / FLT)

We are not defining the executable IEEE-754 layer here.

What we do here is the same separation used by Flocq:

• Core.lean gives us mantissa/exponent arithmetic on $\mathbb{R}$ plus bpow, mag, and cexp;
• this file defines format families via exponent-selection functions fexp : ℤ → ℤ.

Those fexps let us talk about “a fixed-point grid”, “an unbounded float grid”, or “a float grid with a lower exponent bound and gradual underflow” without committing to a concrete bit encoding.

In particular:

• FIX_* models a fixed exponent (useful for quantization / fixed-point reasoning),
• FLX_* models an unbounded exponent float (a convenient intermediate model),
• FLT_* has a lower exponent bound and gradual underflow, but no upper bound or overflow.

If you want NaN/Inf/signed-zero and an executable kernel, that is NN/Floats/IEEEExec/. For TorchLean-specific “which precision do we use in each phase?” configuration helpers, see NN/Floats/NeuralFloat/Metadata.lean.

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)

structure TorchLean.Floats.NeuralFormatPrecision : 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 NeuralFormatPrecision.ofInt?. This prevents a zero or negative precision from being silently reinterpreted through an absolute-value conversion.

• digits : ℕ

  Number of radix digits retained by the format.

• digits_pos : 0 < self.digits

  A floating-point precision has at least one radix digit.

@[implicit_reducible]

instance TorchLean.Floats.instDecidableEqNeuralFormatPrecision : DecidableEq NeuralFormatPrecision

def TorchLean.Floats.instDecidableEqNeuralFormatPrecision.decEq (x✝ x✝¹ : NeuralFormatPrecision) : Decidable (x✝ = x✝¹)

def TorchLean.Floats.instReprNeuralFormatPrecision.repr : NeuralFormatPrecision → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.Floats.instReprNeuralFormatPrecision : Repr NeuralFormatPrecision

def TorchLean.Floats.NeuralFormatPrecision.toInt (precision : NeuralFormatPrecision) : ℤ

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

def TorchLean.Floats.NeuralFormatPrecision.ofNat? (digits : ℕ) : Option NeuralFormatPrecision

Check a natural-number precision at a configuration boundary.

def TorchLean.Floats.NeuralFormatPrecision.ofInt? (digits : ℤ) : Option NeuralFormatPrecision

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

@[simp]

theorem TorchLean.Floats.NeuralFormatPrecision.toInt_pos (precision : NeuralFormatPrecision) : 0 < precision.toInt

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

@[simp]

theorem TorchLean.Floats.NeuralFormatPrecision.ofNat?_eq_none_iff (digits : ℕ) : ofNat? digits = none ↔ digits = 0

Natural precision validation fails exactly at zero.

@[simp]

theorem TorchLean.Floats.NeuralFormatPrecision.ofInt?_eq_none_iff (digits : ℤ) : ofInt? digits = none ↔ digits ≤ 0

Integer precision validation fails exactly for nonpositive inputs.

def TorchLean.Floats.FIXExp (emin : ℤ) : ℤ → ℤ

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

This is the Flocq “FIX” family. It is useful when you want to reason about values living on a single, fixed grid $\beta^{\mathtt{emin}}\mathbb{Z}$ (think: fixed-point arithmetic or quantization).

instance TorchLean.Floats.fixValidExp (emin : ℤ) : NeuralValidExp (FIXExp emin)

FIX_exp satisfies the standard Flocq-style Valid_exp axioms (here: NeuralValidExp).

Even though the proof is trivial, having the instance is what lets later theorems reuse the same generic lemmas for FIX/FLX/FLT.

instance TorchLean.Floats.fixMonotoneExp (emin : ℤ) : NeuralMonotoneExp (FIXExp emin)

instance TorchLean.Floats.fixBoundedExpGrowth (emin : ℤ) : NeuralBoundedExpGrowth (FIXExp emin)

theorem TorchLean.Floats.neuralUlp_zero_FIX {β : NeuralRadix} (emin : ℤ) : neuralUlp β (FIXExp emin) 0 = neuralBpow β emin

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

def TorchLean.Floats.FIXFormat {β : NeuralRadix} (emin : ℤ) (x : ℝ) : Prop

FIX_format emin x says “x is exactly representable on the fixed grid”.

This is phrased via an existential NeuralFloat β so that it composes smoothly with the rest of the rounding model (neural_to_real, ULP bounds, etc.).

def TorchLean.Floats.FLXExp (prec : ℤ) : ℤ → ℤ

FLX_exp prec is the unbounded-exponent family.

This is Flocq’s “FLX” family: it models a floating-point format with no exponent bounds but with a mantissa precision parameter prec. It is a convenient intermediate model for proofs because it removes underflow/overflow corner cases while still tracking mantissa rounding.

@[reducible, inline]

abbrev TorchLean.Floats.flxValidExp (prec : ℤ) (h : 0 < prec) : NeuralValidExp (FLXExp prec)

FLX_exp satisfies NeuralValidExp.

The side-condition 0 < prec matches the standard assumption that “precision is positive”.

theorem TorchLean.Floats.neuralValidExp_FLX_iff (prec : ℤ) : NeuralValidExp (FLXExp prec) ↔ 0 < prec

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

def TorchLean.Floats.NeuralFormatPrecision.flxExp (precision : NeuralFormatPrecision) : ℤ → ℤ

The unbounded exponent selector associated with a checked precision.

instance TorchLean.Floats.NeuralFormatPrecision.flxExpValid (precision : NeuralFormatPrecision) : NeuralValidExp precision.flxExp

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

@[reducible, inline]

abbrev TorchLean.Floats.flxMonotoneExp (prec : ℤ) : NeuralMonotoneExp (FLXExp prec)

@[reducible, inline]

abbrev TorchLean.Floats.flxBoundedExpGrowth (prec : ℤ) : NeuralBoundedExpGrowth (FLXExp prec)

def TorchLean.Floats.FLXFormat {β : NeuralRadix} (prec : ℤ) (x : ℝ) : Prop

Exact representability predicate for FLX.

Heuristically, there exists a mantissa/exponent pair with mantissa bounded by the precision, and $x=m\beta^e$.

theorem TorchLean.Floats.not_FLXFormat_of_nonpos {β : NeuralRadix} (prec : ℤ) (hprec : prec ≤ 0) (x : ℝ) : ¬FLXFormat prec x

Nonpositive precision is rejected by the explicit FLX format predicate.

theorem TorchLean.Floats.neuralNegligibleExp_FLX (prec : ℤ) (hprec : 0 < prec) : neuralNegligibleExp (FLXExp prec) = none

The unbounded FLX exponent function has no negligible exponent.

theorem TorchLean.Floats.neuralUlp_zero_FLX {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) : neuralUlp β (FLXExp prec) 0 = 0

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

def TorchLean.Floats.FLTExp (emin prec : ℤ) : ℤ → ℤ

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

This is Flocq’s “FLT” family. The exponent is bounded below by emin, but it has no upper bound, so this rounded-real format models gradual underflow but not overflow, infinities, or NaNs. Gradual underflow is captured by taking max (e - prec) emin.

@[reducible, inline]

abbrev TorchLean.Floats.fltValidExp (emin prec : ℤ) (h : 0 < prec) : NeuralValidExp (FLTExp emin prec)

FLT_exp satisfies NeuralValidExp.

This is where most format-bridge lemmas live when connecting proofs to float32-style bounds (e.g. via NN/Floats/FP32).

theorem TorchLean.Floats.neuralValidExp_FLT_iff (emin prec : ℤ) : NeuralValidExp (FLTExp emin prec) ↔ 0 < prec

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

def TorchLean.Floats.NeuralFormatPrecision.fltExp (precision : NeuralFormatPrecision) (emin : ℤ) : ℤ → ℤ

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

instance TorchLean.Floats.NeuralFormatPrecision.fltExpValid (precision : NeuralFormatPrecision) (emin : ℤ) : NeuralValidExp (precision.fltExp emin)

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

@[reducible, inline]

abbrev TorchLean.Floats.fltBoundedExpGrowth (emin prec : ℤ) : NeuralBoundedExpGrowth (FLTExp emin prec)

@[reducible, inline]

abbrev TorchLean.Floats.fltMonotoneExp (emin prec : ℤ) : NeuralMonotoneExp (FLTExp emin prec)

def TorchLean.Floats.FLTFormat {β : NeuralRadix} (emin prec : ℤ) (x : ℝ) : Prop

Exact representability predicate for FLT.

This version includes:

• a mantissa size bound (precision),
• and the lower exponent bound $\mathtt{emin}\le\mathtt{exponent}$ (no values smaller than the minimum normal/subnormal scale, depending on the choice of emin and rounding).

theorem TorchLean.Floats.not_FLTFormat_of_nonpos {β : NeuralRadix} (emin prec : ℤ) (hprec : prec ≤ 0) (x : ℝ) : ¬FLTFormat emin prec x

Nonpositive precision is rejected by the explicit FLT format predicate.

theorem TorchLean.Floats.exists_neuralNegligibleExp_FLT (emin prec : ℤ) : ∃ (n : ℤ), IsNeuralNegligibleExp (FLTExp emin prec) n

FLT has a negligible-exponent witness at emin.

theorem TorchLean.Floats.neuralUlp_zero_FLT {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) : neuralUlp β (FLTExp emin prec) 0 = neuralBpow β emin

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