TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.P3109.Arithmetic.External.Bounds

Precision and range of external P3109 results #

The quotient floor is strictly below 2^P; every report mode chooses it or its successor. Consequently precision rounding produces an exact binary grid value, even at a carry. Saturation then places each finite result in the external format's finite range. These two facts justify using an ordinary binary encoder without introducing a second rounding error.

source
theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.minSubnormalExponent_nonpos (format : BinaryInterchange.FloatFormat) :
format.minSubnormalExponent ≤ 0

The external subnormal quantum is nonpositive.

source
def FloatLib.Floats.Formats.P3109.Arithmetic.External.FitsGrid (format : BinaryInterchange.FloatFormat) (value : Numerics.Dyadic) :
Prop

Grid sufficient for exact external encoding, allowing a carry to the next binade.

Instances For
    source
    theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.roundFinite_fitsGrid (format : BinaryInterchange.FloatFormat) (mode : RoundingMode) (exact : ℚ) :
    FitsGrid format (roundFinite format mode exact)

    Every rounding mode, for every explicit stochastic word, lands on the external grid.

    source
    theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.endpoint_fitsGrid (format : BinaryInterchange.FloatFormat) (negative : Bool) :
    FitsGrid format (endpoint format negative)

    Each finite external endpoint lies on the precision grid.

    source
    theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.endpoint_eq_maxFiniteDyadic (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) :
    endpoint format false = BinaryInterchange.Model.maxFiniteDyadic format

    The positive endpoint is exactly the existing binary model's largest finite dyadic.

    source
    theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.abs_endpoint_toReal (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (negative : Bool) :
    |(endpoint format negative).toReal| = (BinaryInterchange.Model.posMaxFinite format).toReal

    The absolute endpoint value is the positive maximum, for either sign.

    source
    theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.magnitude_bound_of_not_overflow (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (value : Numerics.Dyadic) (h : (Numerics.Dyadic.Internal.compareScalable (endpoint format false) { negative := false, significand := value.significand, exponent := value.exponent } == Ordering.lt) = false) :
    |value.toReal| ≤ (BinaryInterchange.Model.posMaxFinite format).toReal

    Scalable comparison tests exactly the real-valued magnitude bound used by encoding.

    source
    theorem FloatLib.Floats.Formats.P3109.Arithmetic.External.saturate_finite (format : BinaryInterchange.FloatFormat) (hformat : format.isIEEE = true) (policy : ProjectionPolicy) (input : Numerics.NumericalValue Numerics.Dyadic) (hgrid : ∀ (value : Numerics.Dyadic), input = Numerics.NumericalValue.finite value → FitsGrid format value) (result : Numerics.Dyadic) (hresult : saturate format policy input = Numerics.NumericalValue.finite result) :
    FitsGrid format result ∧ |result.toReal| ≤ (BinaryInterchange.Model.posMaxFinite format).toReal

    For an IEEE descriptor with grid-aligned finite inputs, every finite saturation result stays on the grid and within the external endpoints.