Single-rounding semantics of posit algebraic functions

The finite-input theorems identify the exact expression before rounding, including irrational square roots. Exceptional-input theorems give the NaR rules from the Posit Standard (2022), §5.1.

theorem FloatLib.Floats.Formats.Posit.Model.rSqrt_eq_roundPositive {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : 0 < q) : value.rSqrt = RealRounding.roundPositive format (1 / √↑q)

A positive finite reciprocal square root is the once-rounded reciprocal of the real root.

theorem FloatLib.Floats.Formats.Posit.Model.rSqrt_eq_nar_of_nonpositive {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : q ≤ 0) : value.rSqrt = nar format

Nonpositive finite inputs lie outside the real domain of reciprocal square root.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.rSqrt_nar {format : Format} : (nar format).rSqrt = nar format

Reciprocal square root propagates NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.rSqrt_zero {format : Format} : (zero format).rSqrt = nar format

Reciprocal square root of zero is NaR.

theorem FloatLib.Floats.Formats.Posit.Model.hypot_eq_roundPositive {format : Format} (left right : Model format) {a b : ℚ} (hleft : left.toRat? = some a) (hright : right.toRat? = some b) : left.hypot right = RealRounding.roundPositive format √(↑a ^ 2 + ↑b ^ 2)

Finite hypotenuse inputs give the standard rounding of the exact Euclidean norm.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.hypot_nar_left {format : Format} (right : Model format) : (nar format).hypot right = nar format

A NaR first argument makes the hypotenuse NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.hypot_nar_right {format : Format} (left : Model format) : left.hypot (nar format) = nar format

A NaR second argument makes the hypotenuse NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.hypot_zero_zero {format : Format} : (zero format).hypot (zero format) = zero format

The norm of the zero pair is zero.

theorem FloatLib.Floats.Formats.Posit.Model.hypot_comm {format : Format} (left right : Model format) : left.hypot right = right.hypot left

Hypotenuse does not depend on the order of its inputs.

theorem FloatLib.Floats.Formats.Posit.Model.fMM_eq_roundRat {format : Format} (left right third : Model format) {a b c : ℚ} (hleft : left.toRat? = some a) (hright : right.toRat? = some b) (hthird : third.toRat? = some c) : left.fMM right third = roundRat format (a * b * c)

Finite fused triple multiplication rounds the exact three-factor rational product once.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.fMM_nar_left {format : Format} (right third : Model format) : (nar format).fMM right third = nar format

A NaR first factor propagates through fused triple multiplication, even beside zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.fMM_nar_right {format : Format} (left third : Model format) : left.fMM (nar format) third = nar format

A NaR second factor propagates through fused triple multiplication.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.fMM_nar_third {format : Format} (left right : Model format) : left.fMM right (nar format) = nar format

A NaR third factor propagates through fused triple multiplication.

theorem FloatLib.Floats.Formats.Posit.Model.fMM_swap_left {format : Format} (left right third : Model format) : left.fMM right third = right.fMM left third

Swapping the first two factors preserves the once-rounded triple product.

theorem FloatLib.Floats.Formats.Posit.Model.fMM_swap_right {format : Format} (left right third : Model format) : left.fMM right third = left.fMM third right

Swapping the last two factors preserves the once-rounded triple product.