TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.P3109.Arithmetic.Sqrt.Proof

Real semantics and executable refinement of P3109 square root #

The reference rounder takes the floor of a real square root and compares that root with the report's exact rounding thresholds. The executable rounder computes the same result using natural-number square roots and products. Neither implementation first projects a rational approximation of the root.

The final decoding theorem composes this equality with the existing report saturation and encoding theorem. Reciprocal square root and hypotenuse reuse the same rounder after forming their exact rational radicands.

source
noncomputable def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtRoundAwayReal (format : Format) (mode : RoundingMode) (quantum : ℤ) (numerator denominator lower : ℕ) :
Bool

The report's upper-candidate decision expressed using the real square root.

Instances For
    source
    theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrtRoundAway_eq_real (format : Format) (mode : RoundingMode) (quantum : ℤ) (numerator denominator lower : ℕ) (hd : 0 < denominator) :
    sqrtRoundAway format mode quantum numerator denominator lower = sqrtRoundAwayReal format mode quantum numerator denominator lower

    Exact integer threshold tests implement real square-root rounding in every supplied mode.

    source
    noncomputable def FloatLib.Floats.Formats.P3109.Arithmetic.roundSqrtRealToPrecision (format : Format) (mode : RoundingMode) (radicand : ℚ) :
    Numerics.Dyadic

    Reference precision rounding takes the floor and threshold comparisons of a real root. As in the executable precision helper, the radicand magnitude is used; the closed operation rejects negative inputs before calling this helper.

    Instances For
      source
      theorem FloatLib.Floats.Formats.P3109.Arithmetic.roundSqrtRatToPrecision_eq_real (format : Format) (mode : RoundingMode) (radicand : ℚ) :
      roundSqrtRatToPrecision format mode radicand = roundSqrtRealToPrecision format mode radicand

      The executable precision rounder equals the rounder defined with the actual real root.

      source
      noncomputable def FloatLib.Floats.Formats.P3109.Arithmetic.sqrtRealValue (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue ℚ) :
      Numerics.NumericalValue Numerics.Dyadic

      Closed square-root reference, followed by the supplied report saturation policy.

      Instances For
        source
        theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrtValue_eq_real (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue ℚ) :
        sqrtValue format policy value = sqrtRealValue format policy value

        Closed executable square root refines the real-root reference for every input and policy.

        source
        theorem FloatLib.Floats.Formats.P3109.Arithmetic.sameDatum_decode_sqrtCode (format : Format) (policy : ProjectionPolicy) (value : Numerics.NumericalValue ℚ) :
        Format.SameDatum (format.decode (sqrtCode format policy value)) (sqrtValue format policy value)

        Encoding and decoding preserves the single rounded and saturated square-root datum.

        source
        theorem FloatLib.Floats.Formats.P3109.Arithmetic.sqrt_recip_real (value : ℚ) :
        √↑(1 / value) = 1 / √↑value

        Reciprocal square root uses the same real value as reciprocal of the positive square root.

        source
        theorem FloatLib.Floats.Formats.P3109.Arithmetic.hypotRadicand_finite_real (left right : ℚ) :
        ↑(left * left + right * right) = ↑left ^ 2 + ↑right ^ 2 ∧ 0 ≤ left * left + right * right

        The finite hypotenuse radicand is the real sum of squares and is nonnegative.

        source
        theorem FloatLib.Floats.ExecFloat.P3109.decode_projectSqrt (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (value : Numerics.NumericalValue ℚ) :
        Formats.P3109.Format.SameDatum (projectSqrt destination policy value).decode (Formats.P3109.Arithmetic.sqrtRealValue destination policy value)

        Decoding the square-root projector returns the real-root report reference.

        source
        theorem FloatLib.Floats.ExecFloat.P3109.decode_sqrtTo {source : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (value : P3109 source) :
        Formats.P3109.Format.SameDatum (sqrtTo destination policy value).decode (Formats.P3109.Arithmetic.sqrtRealValue destination policy value.toClosedRat)

        Mixed-format square root evaluates the source value and rounds once into the destination.

        source
        theorem FloatLib.Floats.ExecFloat.P3109.decode_rsqrtTo {source : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (value : P3109 source) :
        Formats.P3109.Format.SameDatum (rsqrtTo destination policy value).decode (Formats.P3109.Arithmetic.sqrtRealValue destination policy (Formats.P3109.Arithmetic.rsqrtRadicand value.toClosedRat))

        Reciprocal square root projects the root of the exact reciprocal, with its report domain.

        source
        theorem FloatLib.Floats.ExecFloat.P3109.decode_hypotTo {leftFormat rightFormat : Formats.P3109.Format} (destination : Formats.P3109.Format) (policy : Formats.P3109.ProjectionPolicy) (left : P3109 leftFormat) (right : P3109 rightFormat) :
        Formats.P3109.Format.SameDatum (hypotTo destination policy left right).decode (Formats.P3109.Arithmetic.sqrtRealValue destination policy (Formats.P3109.Arithmetic.hypotRadicand left.toClosedRat right.toClosedRat))

        Hypotenuse projects the root of the exact sum of squares without intermediate overflow.