Standard Format Theorems

Connections between the generic format predicate and the concrete FIX, FLX, and FLT families. The fixed-point equivalence is the first instance of the generic pattern used by the floating-point families.

theorem TorchLean.Floats.FIXFormat_of_generic {β : NeuralRadix} (emin : ℤ) (x : ℝ) (hx : neuralGenericFormat β (FIXExp emin) x) : FIXFormat emin x

The generic format generated by FIXExp emin is contained in FIXFormat emin.

theorem TorchLean.Floats.generic_of_FIXFormat {β : NeuralRadix} (emin : ℤ) (x : ℝ) (hx : FIXFormat emin x) : neuralGenericFormat β (FIXExp emin) x

Every fixed-point value belongs to the generic format generated by FIXExp emin.

theorem TorchLean.Floats.generic_format_FIX_iff {β : NeuralRadix} (emin : ℤ) (x : ℝ) : neuralGenericFormat β (FIXExp emin) x ↔ FIXFormat emin x

FIXFormat and the corresponding generic format describe the same real values.

theorem TorchLean.Floats.neuralBpow_eq_natPow {β : NeuralRadix} (p : ℤ) (hp : 0 ≤ p) : neuralBpow β p = ↑(β.base ^ p.toNat)

A nonnegative radix power agrees with the corresponding natural-number power.

theorem TorchLean.Floats.FLXFormat_of_generic {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : neuralGenericFormat β (FLXExp prec) x) : FLXFormat prec x

The generic FLXExp format satisfies the explicit FLX mantissa bound.

theorem TorchLean.Floats.generic_of_FLXFormat {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : FLXFormat prec x) : neuralGenericFormat β (FLXExp prec) x

Every explicit bounded-mantissa FLX value belongs to the corresponding generic format.

theorem TorchLean.Floats.generic_format_FLX_iff {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (x : ℝ) : neuralGenericFormat β (FLXExp prec) x ↔ FLXFormat prec x

FLXFormat is exactly the generic format generated by FLXExp.

theorem TorchLean.Floats.FLTFormat_of_generic {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : neuralGenericFormat β (FLTExp emin prec) x) : FLTFormat emin prec x

The generic FLTExp format satisfies the explicit FLT mantissa and exponent bounds.

theorem TorchLean.Floats.generic_of_FLTFormat {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) (x : ℝ) (hx : FLTFormat emin prec x) : neuralGenericFormat β (FLTExp emin prec) x

Every explicit bounded-mantissa FLT value belongs to the corresponding generic format.

theorem TorchLean.Floats.generic_format_FLT_iff {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) (x : ℝ) : neuralGenericFormat β (FLTExp emin prec) x ↔ FLTFormat emin prec x

FLTFormat is exactly the generic format generated by FLTExp.