Correct rounding of natural posit elementary functions

The real-rounding theorems cover every finite input in the function's domain, including extreme magnitudes, exact zero results, and the standard nonzero saturation rule. Separate theorems record NaR propagation and invalid logarithm domains.

theorem FloatLib.Floats.Formats.Posit.Model.Elementary.expRat_eq_real (format : Format) (argument offset : ℚ) : expRat format argument offset = RealRounding.round format (Real.exp ↑argument - ↑offset)

Exact exponential evaluation and output subtraction share one final rounding.

theorem FloatLib.Floats.Formats.Posit.Model.Elementary.logRat_eq_real (format : Format) (argument : ℚ) (hpositive : 0 < argument) : logRat format argument = RealRounding.round format (Real.log ↑argument)

A positive rational logarithm argument is rounded according to its exact real value.

theorem FloatLib.Floats.Formats.Posit.Model.Elementary.logRat_eq_nar (format : Format) (argument : ℚ) (hnonpositive : argument ≤ 0) : logRat format argument = nar format

Nonpositive arguments produce NaR before logarithm evaluation.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Elementary.applyExp_nar {format : Format} (offset : ℚ) : applyExp offset (nar format) = nar format

Exponential evaluation propagates NaR for every exact output offset.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Elementary.applyLog_nar {format : Format} (offset : ℚ) : applyLog offset (nar format) = nar format

Logarithm evaluation propagates NaR for every exact input offset.

theorem FloatLib.Floats.Formats.Posit.Model.Elementary.applyExp_eq_real {format : Format} (offset : ℚ) (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : applyExp offset value = RealRounding.round format (Real.exp ↑q - ↑offset)

Finite exponential evaluation agrees with signed real rounding.

theorem FloatLib.Floats.Formats.Posit.Model.Elementary.applyLog_eq_real {format : Format} (offset : ℚ) (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hpositive : 0 < q + offset) : applyLog offset value = RealRounding.round format (Real.log (↑q + ↑offset))

Finite logarithm evaluation forms its input offset exactly.

theorem FloatLib.Floats.Formats.Posit.Model.Elementary.applyLog_eq_nar {format : Format} (offset : ℚ) (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hnonpositive : q + offset ≤ 0) : applyLog offset value = nar format

Invalid exact-offset logarithm arguments produce NaR.

theorem FloatLib.Floats.Formats.Posit.Model.exp_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.exp = RealRounding.round format (Real.exp ↑q)

Natural exponential has the exact signed real rounding required by the standard.

theorem FloatLib.Floats.Formats.Posit.Model.expMinus1_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.expMinus1 = RealRounding.round format (Real.exp ↑q - 1)

expMinus1 rounds the exact exponential minus one, including near zero.

theorem FloatLib.Floats.Formats.Posit.Model.log_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : 0 < q) : value.log = RealRounding.round format (Real.log ↑q)

Natural logarithm has the exact signed real rounding on its positive domain.

theorem FloatLib.Floats.Formats.Posit.Model.logPlus1_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : -1 < q) : value.logPlus1 = RealRounding.round format (Real.log (1 + ↑q))

logPlus1 forms 1 + x exactly before rounding the natural logarithm.

@[simp]

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

Natural exponential propagates NaR.

@[simp]

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

Exponential minus one propagates NaR.

@[simp]

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

Natural logarithm propagates NaR.

@[simp]

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

Natural logarithm of one plus the input propagates NaR.

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

Natural logarithm rejects zero and negative finite values.

theorem FloatLib.Floats.Formats.Posit.Model.logPlus1_eq_nar_of_le_neg_one {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hq : q ≤ -1) : value.logPlus1 = nar format

Natural Plus1 logarithm rejects finite values at or below -1.