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.

decode_projectSqrt composes this equality with the report's saturation and encoding theorem. Reciprocal square root and hypotenuse reuse the same rounder after forming their exact rational radicands.

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.

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.

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, and the closed operation rejects negative inputs before calling this helper.

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 real root.

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.

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.

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.

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.

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.

theorem FloatLib.Floats.ExecFloat.P3109.decode_projectSqrt {format : Formats.P3109.Format} (value : Numerics.NumericalValue ℚ) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) : Formats.P3109.Format.SameDatum (projectSqrt value mode saturation).decode (Formats.P3109.Arithmetic.sqrtRealValue format { rounding := mode, saturation := saturation } value)

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

theorem FloatLib.Floats.ExecFloat.P3109.decode_sqrt {format : Formats.P3109.Format} (value : P3109 format) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) : Formats.P3109.Format.SameDatum (value.sqrt target mode saturation).decode (Formats.P3109.Arithmetic.sqrtRealValue target { rounding := mode, saturation := saturation } value.toClosedRat)

Square root evaluates the source value and rounds once into the target.

theorem FloatLib.Floats.ExecFloat.P3109.decode_rsqrt {format : Formats.P3109.Format} (value : P3109 format) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) : Formats.P3109.Format.SameDatum (value.rsqrt target mode saturation).decode (Formats.P3109.Arithmetic.sqrtRealValue target { rounding := mode, saturation := saturation } (Formats.P3109.Arithmetic.rsqrtRadicand value.toClosedRat))

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

theorem FloatLib.Floats.ExecFloat.P3109.decode_hypot {format : Formats.P3109.Format} (left right : P3109 format) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) : Formats.P3109.Format.SameDatum (left.hypot right target mode saturation).decode (Formats.P3109.Arithmetic.sqrtRealValue target { rounding := mode, saturation := saturation } (Formats.P3109.Arithmetic.hypotRadicand left.toClosedRat right.toClosedRat))

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