Generic format properties

The Flocq-style generic format describes representability through a radix and a canonical exponent function, before choosing a concrete FIX, FLX, or FLT family. This module develops the closure and representation facts needed by later rounding theory.

The layer is mathematical rather than executable: it gives binary-interchange and other format implementations a common real-valued specification against which their exact integer algorithms can be proved.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.magnitude_neg {β : Numerics.Radix} (x : ℝ) : magnitude β (-x) = magnitude β x

Magnitude is invariant under negation.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.cexp_neg {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : cexp β fexp (-x) = cexp β fexp x

The canonical exponent is invariant under negation.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.scaledMantissa_neg {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : scaledMantissa β fexp (-x) = -scaledMantissa β fexp x

Negation negates the canonical scaled mantissa.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.generic_format_zero {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] : genericFormat β fexp 0

Zero belongs to every valid generic format.

theorem FloatLib.Floats.Formats.Flocq.generic_format_neg {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) (hx : genericFormat β fexp x) : genericFormat β fexp (-x)

Generic formats are closed under negation.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.generic_format_neg_iff {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : genericFormat β fexp (-x) ↔ genericFormat β fexp x

A value is representable exactly when its negation is representable.

theorem FloatLib.Floats.Formats.Flocq.generic_format_abs_iff {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : genericFormat β fexp |x| ↔ genericFormat β fexp x

A value is representable exactly when its absolute value is representable.

theorem FloatLib.Floats.Formats.Flocq.generic_format_bpow {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (e : ℤ) (h : fexp (e + 1) ≤ e) : genericFormat β fexp (bpow β e)

A radix power is representable whenever its canonical exponent is no larger than its exponent.

theorem FloatLib.Floats.Formats.Flocq.generic_format_of_toReal_of_cexp_le {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (f : FloatRep β) (x : ℝ) (hxf : x = toReal f) (he : cexp β fexp x ≤ f.exponent) : genericFormat β fexp x

A mantissa/exponent representation is generic when its stored exponent is at least the canonical exponent selected for its value.

theorem FloatLib.Floats.Formats.Flocq.cexp_lt_magnitude_of_pos_generic {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : 0 < x) (hfmt : genericFormat β fexp x) : cexp β fexp x < magnitude β x

A positive representable value uses a canonical exponent strictly below its magnitude.

theorem FloatLib.Floats.Formats.Flocq.fexp_succ_le_of_generic_bpow {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (e : ℤ) (hfmt : genericFormat β fexp (bpow β e)) : fexp (e + 1) ≤ e

Representability of β^e forces its canonical exponent to be at most e.

theorem FloatLib.Floats.Formats.Flocq.fexp_le_of_generic_bpow {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (e : ℤ) (hfmt : genericFormat β fexp (bpow β e)) : fexp e ≤ e

If β^e is representable, the exponent selected for the bin below it is at most e.

theorem FloatLib.Floats.Formats.Flocq.generic_inclusion_mag {β : Numerics.Radix} {fexp₁ fexp₂ : ℤ → ℤ} [ValidExp fexp₁] [ValidExp fexp₂] {x : ℝ} (hexp : x ≠ 0 → fexp₂ (magnitude β x) ≤ fexp₁ (magnitude β x)) (hx : genericFormat β fexp₁ x) : genericFormat β fexp₂ x

A value representable with fexp₁ remains representable with fexp₂ when the second canonical exponent is no larger at that value's magnitude. The condition is local because representability of x only depends on the exponent selected at magnitude x.

theorem FloatLib.Floats.Formats.Flocq.generic_inclusion {β : Numerics.Radix} {fexp₁ fexp₂ : ℤ → ℤ} [ValidExp fexp₁] [ValidExp fexp₂] (hexp : ∀ (e : ℤ), fexp₂ e ≤ fexp₁ e) {x : ℝ} (hx : genericFormat β fexp₁ x) : genericFormat β fexp₂ x

Pointwise-smaller exponent selection defines a containing generic format.

theorem FloatLib.Floats.Formats.Flocq.generic_format_discrete {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) (m : ℤ) (hlower : ↑m * bpow β (cexp β fexp x) < x) (hupper : x < ↑(m + 1) * bpow β (cexp β fexp x)) : ¬genericFormat β fexp x

No generic-format value lies strictly between consecutive points on its canonical grid.

theorem FloatLib.Floats.Formats.Flocq.canonical_exists_of_generic {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : genericFormat β fexp x) : ∃ (f : FloatRep β), x = toReal f ∧ Canonical β fexp f

Every generic-format value has a canonical mantissa/exponent representation.

theorem FloatLib.Floats.Formats.Flocq.generic_format_of_canonical {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (f : FloatRep β) (hf : Canonical β fexp f) : genericFormat β fexp (toReal f)

The real value of a canonical representation belongs to its generic format.

theorem FloatLib.Floats.Formats.Flocq.canonical_unique {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {f g : FloatRep β} (hf : Canonical β fexp f) (hg : Canonical β fexp g) (hval : toReal f = toReal g) : f = g

Canonical representations of the same real value are equal.