Refinement and exact semantics of configured posit algebraic functions

Every configured operation decodes to its model operation, for any lawful storage codec. The finite-domain corollaries expose the exact once-rounded rational or real expression.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_rSqrt {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (rSqrt value) = (toModel value).rSqrt

Configured reciprocal square root refines the exact model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_hypot {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (hypot left right) = (toModel left).hypot (toModel right)

Configured hypotenuse refines the exact model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_fMM {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right third : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (fMM left right third) = (toModel left).fMM (toModel right) (toModel third)

Configured triple multiplication refines the exact model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_rootN {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (degree : ℤ) : toModel (rootN value degree) = (toModel value).rootN degree

Configured integer roots refine the exact model operation for every integer degree.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_powInt {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (exponent : ℤ) : toModel (powInt value exponent) = (toModel value).powInt exponent

Configured integer powers refine the exact model operation for every integer exponent.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_compound {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (exponent : ℤ) : toModel (compound value exponent) = (toModel value).compound exponent

Configured compound refines the exact model operation for every integer exponent.

theorem FloatLib.Floats.ExecFloat.Posit.rSqrt_eq_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (hq : 0 < q) : toModel (rSqrt value) = Formats.Posit.Model.RealRounding.roundPositive format (1 / √↑q)

A positive finite configured reciprocal square root rounds the exact real reciprocal root.

theorem FloatLib.Floats.ExecFloat.Posit.hypot_eq_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) {a b : ℚ} (hleft : toRat? left = some a) (hright : toRat? right = some b) : toModel (hypot left right) = Formats.Posit.Model.RealRounding.roundPositive format √(↑a ^ 2 + ↑b ^ 2)

Finite configured hypotenuse inputs round the exact real Euclidean norm once.

theorem FloatLib.Floats.ExecFloat.Posit.fMM_eq_roundRat {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right third : ExecFloat (Formats.Posit.Configured.Family format code plan)) {a b c : ℚ} (hleft : toRat? left = some a) (hright : toRat? right = some b) (hthird : toRat? third = some c) : toModel (fMM left right third) = Formats.Posit.Model.roundRat format (a * b * c)

Finite configured triple multiplication rounds the exact rational product once.

theorem FloatLib.Floats.ExecFloat.Posit.rootN_eq_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (degree : ℤ) (hvalue : toRat? value = some q) (hq : 0 ≤ q) (hdegree : degree ≠ 0) (hdomain : q ≠ 0 ∨ 0 < degree) : toModel (rootN value degree) = Formats.Posit.Model.RealRounding.roundPositive format (↑q ^ (↑degree)⁻¹)

A defined nonnegative configured integer root rounds the exact real power.

theorem FloatLib.Floats.ExecFloat.Posit.rootN_eq_neg_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (degree : ℤ) (hvalue : toRat? value = some q) (hq : q < 0) (hodd : degree % 2 ≠ 0) : toModel (rootN value degree) = (Formats.Posit.Model.RealRounding.roundPositive format ((-↑q) ^ (↑degree)⁻¹)).neg

An odd-degree configured root of a negative finite input rounds the signed real root.

theorem FloatLib.Floats.ExecFloat.Posit.powInt_eq_roundRat {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (exponent : ℤ) (hvalue : toRat? value = some q) (hdomain : q ≠ 0 ∨ 0 < exponent) : toModel (powInt value exponent) = Formats.Posit.Model.roundRat format (q ^ exponent)

Defined configured integer powers round the exact rational power once.

theorem FloatLib.Floats.ExecFloat.Posit.compound_eq_roundRat {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (exponent : ℤ) (hvalue : toRat? value = some q) (hdomain : 1 + q ≠ 0 ∨ 0 < exponent) : toModel (compound value exponent) = Formats.Posit.Model.roundRat format ((1 + q) ^ exponent)

Defined configured compound rounds the exact addition and integer power once.

theorem FloatLib.Floats.ExecFloat.Posit.powInt_exponent_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) : toModel (powInt value 0) = Formats.Posit.Model.roundRat format 1

Fixed exponent zero gives rounded one for every finite configured input.

theorem FloatLib.Floats.ExecFloat.Posit.compound_exponent_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) : toModel (compound value 0) = Formats.Posit.Model.roundRat format 1

Fixed exponent zero makes compound constant one, including at input negative one.