Real correctness of configured natural posit functions

The configured operations inherit the model's real-rounding theorem at every supported width. The Minus1 and Plus1 statements include the exact subtraction or addition in the value being rounded.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_exp {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 (exp value) = (toModel value).exp

Configured exponential refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_expMinus1 {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 (expMinus1 value) = (toModel value).expMinus1

Configured exponential minus one refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_log {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 (log value) = (toModel value).log

Configured logarithm refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_logPlus1 {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 (logPlus1 value) = (toModel value).logPlus1

Configured logarithm of one plus the input refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.exp_eq_real {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 (exp value) = Formats.Posit.Model.RealRounding.round format (Real.exp ↑q)

Natural exponential rounds its exact real value at the destination width.

theorem FloatLib.Floats.ExecFloat.Posit.expMinus1_eq_real {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 (expMinus1 value) = Formats.Posit.Model.RealRounding.round format (Real.exp ↑q - 1)

Exponential minus one has no intermediate posit rounding.

theorem FloatLib.Floats.ExecFloat.Posit.log_eq_real {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 (log value) = Formats.Posit.Model.RealRounding.round format (Real.log ↑q)

Natural logarithm rounds its exact real value on the positive domain.

theorem FloatLib.Floats.ExecFloat.Posit.logPlus1_eq_real {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 : -1 < q) : toModel (logPlus1 value) = Formats.Posit.Model.RealRounding.round format (Real.log (1 + ↑q))

The input addition in logPlus1 is exact before logarithm evaluation.