NeuralFloat core (Flocq-style rounded arithmetic)

TorchLean frequently reasons about floating-point behavior using a classical "rounded arithmetic on $\mathbb{R}$" approach rather than a bit-level IEEE-754 model:

• 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 IEEE-754 semantics (NaN/Inf/signed zero), see NN/Floats/IEEEExec/. Training annotations and named precision policies are deliberately kept out of this mathematical core; see NN/Floats/NeuralFloat/Metadata.lean.

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 TorchLean.Floats.NeuralRadix : Type

Radix (base) for "floating-point-like" representations.

In practice we almost always use base $2$ (binaryRadix) because that's what hardware implements, but keeping the base explicit helps make the model match the literature (and it keeps some proofs parametric in the radix).

• base : ℕ

  Radix base (e.g. 2 for binary).

• base_valid : 2 ≤ self.base

  Validity condition: the base is at least 2.

def TorchLean.Floats.binaryRadix : NeuralRadix

Standard binary radix ($\beta=2$).

def TorchLean.Floats.decimalRadix : NeuralRadix

Decimal radix ($\beta=10$, useful for compact examples and exact decimal inputs).

def TorchLean.Floats.NeuralRadix.toReal (r : NeuralRadix) : ℝ

Coerce the radix base to $\mathbb{R}$ (used by bpow and logarithms).

theorem TorchLean.Floats.NeuralRadix.pos (r : NeuralRadix) : 0 < r.toReal

The radix base is positive when viewed as a real number.

theorem TorchLean.Floats.NeuralRadix.ne_zero (r : NeuralRadix) : r.toReal ≠ 0

The radix base is nonzero when viewed as a real number.

theorem TorchLean.Floats.NeuralRadix.gt_one (r : NeuralRadix) : 1 < r.toReal

The radix base is strictly greater than $1$ (for a valid radix, $2\le\mathtt{base}$).

structure TorchLean.Floats.NeuralFloat (β : NeuralRadix) : Type

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

• mantissa : ℤ

  Integer mantissa m.

• exponent : ℤ

  Integer exponent e.

def TorchLean.Floats.NeuralFloat.isZero {β : NeuralRadix} (f : NeuralFloat β) : Prop

Structural zero test (mantissa is exactly 0).

def TorchLean.Floats.NeuralFloat.sign {β : NeuralRadix} (f : NeuralFloat β) : ℤ

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

noncomputable def TorchLean.Floats.neuralBpow (β : NeuralRadix) (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 TorchLean.Floats.neuralBpow.pos (β : NeuralRadix) (e : ℤ) : 0 < neuralBpow β e

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

theorem TorchLean.Floats.neuralBpow.nonneg (β : NeuralRadix) (e : ℤ) : 0 ≤ neuralBpow β e

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

theorem TorchLean.Floats.neuralBpow.ne_zero (β : NeuralRadix) (e : ℤ) : neuralBpow β e ≠ 0

Base powers are never zero.

theorem TorchLean.Floats.neuralBpow.add_exp (β : NeuralRadix) (e1 e2 : ℤ) : neuralBpow β (e1 + e2) = neuralBpow β e1 * neuralBpow β e2

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

theorem TorchLean.Floats.neuralBpow.neg_exp (β : NeuralRadix) (e : ℤ) : neuralBpow β (-e) = (neuralBpow β e)⁻¹

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

theorem TorchLean.Floats.neuralBpow.sub_exp (β : NeuralRadix) (e₁ e₂ : ℤ) : neuralBpow β (e₁ - e₂) = neuralBpow β e₁ / neuralBpow β e₂

Exponent subtraction corresponds to division of radix powers.

noncomputable def TorchLean.Floats.neuralToReal {β : NeuralRadix} (f : NeuralFloat β) : ℝ

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

@[simp]

theorem TorchLean.Floats.neuralToReal.zero_iff {β : NeuralRadix} (f : NeuralFloat β) : neuralToReal f = 0 ↔ f.mantissa = 0

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

noncomputable def TorchLean.Floats.neuralMagnitude (β : NeuralRadix) (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 TorchLean.Floats.NeuralValidExp (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)

class TorchLean.Floats.NeuralMonotoneExp (fexp : ℤ → ℤ) : Prop

Exponent-selection functions that preserve order.

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

class TorchLean.Floats.NeuralBoundedExpGrowth (fexp : ℤ → ℤ) : Prop

Optional local growth bound used by selected numerical estimates.

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

def TorchLean.Floats.IsNeuralNegligibleExp (fexp : ℤ → ℤ) (n : ℤ) : Prop

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

noncomputable def TorchLean.Floats.neuralNegligibleExp (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 TorchLean.Floats.neuralNegligibleExp_spec {fexp : ℤ → ℤ} {n : ℤ} (h : neuralNegligibleExp fexp = some n) : IsNeuralNegligibleExp fexp n

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

theorem TorchLean.Floats.neuralNegligibleExp_eq_none_iff (fexp : ℤ → ℤ) : neuralNegligibleExp fexp = none ↔ ¬∃ (n : ℤ), IsNeuralNegligibleExp fexp n

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

noncomputable def TorchLean.Floats.neuralCexp (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp fexp] (x : ℝ) : ℤ

Canonical exponent (cexp in Flocq terminology).

Given a nonzero x, we first compute its magnitude mag(x) and then apply fexp to pick the exponent used for scaling/rounding.

def TorchLean.Floats.NeuralCanonical (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp fexp] (f : NeuralFloat β) : Prop

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

noncomputable def TorchLean.Floats.neuralScaledMantissa (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp 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 TorchLean.Floats.neuralGenericFormat (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp 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 TorchLean.Floats.neuralUlp (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp 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$.

An ULP is a property of the format and does not depend on runtime provenance annotations.

theorem TorchLean.Floats.neuralUlp.nonneg (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp fexp] (x : ℝ) : 0 ≤ neuralUlp β fexp x

neural_ulp is always nonnegative.

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

theorem TorchLean.Floats.neuralUlp.pos_of_ne_zero (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp fexp] (x : ℝ) (hx : x ≠ 0) : 0 < neuralUlp β fexp x

neural_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 TorchLean.Floats.neuralUlp.zero (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp fexp] : neuralUlp β fexp 0 = match neuralNegligibleExp fexp with | some n => neuralBpow β (fexp n) | none => 0

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

@[simp]

theorem TorchLean.Floats.neuralUlp.of_ne_zero (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp fexp] (x : ℝ) (hx : x ≠ 0) : neuralUlp β fexp x = neuralBpow β (neuralCexp β fexp x)

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