Real semantics of rational powers and fused minus-one exponentials

For nonnegative bases in the stated domain, the executable result equals Section 4.1 rounding of the exact real power. Negative bases with integral exponents round the exact rational integer power. NaR, zero to a nonpositive power, and negative bases with nonintegral exponents have their own exceptional-value theorems.

The proofs establish correctness, including ties and saturation. Exact boundary equality makes the logarithm search terminate at every boundary, but no theorem bounds its running time near a tie.

theorem FloatLib.Floats.Formats.Posit.Model.roundPositiveRatPower_eq_roundPositive {format : Format} (base exponent : ℚ) (hbase : 0 < base) : roundPositiveRatPower format base exponent = RealRounding.roundPositive format (↑base ^ ↑exponent)

Exact boundary comparisons round a positive-base real power exactly once.

theorem FloatLib.Floats.Formats.Posit.Model.roundRatPower_eq_roundPositive {format : Format} (base exponent : ℚ) (hbase : 0 ≤ base) (hdomain : base ≠ 0 ∨ 0 < exponent) : roundRatPower format base exponent = RealRounding.roundPositive format (↑base ^ ↑exponent)

In its nonnegative real domain, the executable power rounds the exact real power once. A zero base requires a positive exponent, and a positive base allows every exponent.

theorem FloatLib.Floats.Formats.Posit.Model.roundRatPower_eq_roundRat_of_neg {format : Format} (base exponent : ℚ) (hbase : base < 0) (hinteger : exponent.den = 1) : roundRatPower format base exponent = roundRat format (base ^ exponent.num)

A negative base with an integral exponent rounds the exact rational integer power once.

theorem FloatLib.Floats.Formats.Posit.Model.roundRatPower_eq_nar_of_neg_nonintegral {format : Format} (base exponent : ℚ) (hbase : base < 0) (hinteger : exponent.den ≠ 1) : roundRatPower format base exponent = nar format

A negative base with a nonintegral exponent produces NaR.

theorem FloatLib.Floats.Formats.Posit.Model.roundRatPower_zero_of_nonpositive {format : Format} (exponent : ℚ) (hexponent : exponent ≤ 0) : roundRatPower format 0 exponent = nar format

Zero to zero or a negative exponent produces NaR, excluding total-field conventions.

theorem FloatLib.Floats.Formats.Posit.Model.roundRatPower_zero_of_pos {format : Format} (exponent : ℚ) (hexponent : 0 < exponent) : roundRatPower format 0 exponent = zero format

Zero to a positive exponent is represented exactly.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.roundRatPower_one {format : Format} (exponent : ℚ) : roundRatPower format 1 exponent = roundRat format 1

A base of one returns rounded one without expanding denominator-sized boundary powers.

theorem FloatLib.Floats.Formats.Posit.Model.pow_eq_roundPositive {format : Format} (base exponent : Model format) {b e : ℚ} (hbase : base.toRat? = some b) (hexponent : exponent.toRat? = some e) (hb : 0 ≤ b) (hdomain : b ≠ 0 ∨ 0 < e) : base.pow exponent = RealRounding.roundPositive format (↑b ^ ↑e)

Finite nonnegative posit powers round the exact real power once in its real domain.

theorem FloatLib.Floats.Formats.Posit.Model.pow_eq_roundRat_of_neg {format : Format} (base exponent : Model format) {b e : ℚ} (hbase : base.toRat? = some b) (hexponent : exponent.toRat? = some e) (hb : b < 0) (hinteger : e.den = 1) : base.pow exponent = roundRat format (b ^ e.num)

A finite negative posit base with an integral exponent rounds its exact rational power.

theorem FloatLib.Floats.Formats.Posit.Model.pow_eq_nar_of_neg_nonintegral {format : Format} (base exponent : Model format) {b e : ℚ} (hbase : base.toRat? = some b) (hexponent : exponent.toRat? = some e) (hb : b < 0) (hinteger : e.den ≠ 1) : base.pow exponent = nar format

Negative bases with finite nonintegral posit exponents produce NaR.

theorem FloatLib.Floats.Formats.Posit.Model.pow_zero_of_nonpositive {format : Format} (exponent : Model format) {e : ℚ} (hexponent : exponent.toRat? = some e) (he : e ≤ 0) : (zero format).pow exponent = nar format

Zero to a finite nonpositive posit exponent produces NaR, including zero to zero.

theorem FloatLib.Floats.Formats.Posit.Model.pow_zero_of_pos {format : Format} (exponent : Model format) {e : ℚ} (hexponent : exponent.toRat? = some e) (he : 0 < e) : (zero format).pow exponent = zero format

Zero to a finite positive posit exponent is zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.pow_nar_left {format : Format} (exponent : Model format) : (nar format).pow exponent = nar format

An exceptional base propagates even when its exponent is zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.pow_nar_right {format : Format} (base : Model format) : base.pow (nar format) = nar format

An exceptional exponent propagates even when its base is one.

theorem FloatLib.Floats.Formats.Posit.Model.exp2_eq_roundPositive {format : Format} (value : Model format) {e : ℚ} (hvalue : value.toRat? = some e) : value.exp2 = RealRounding.roundPositive format (2 ^ ↑e)

Base-two exponential rounds the exact real power for every finite input.

theorem FloatLib.Floats.Formats.Posit.Model.exp10_eq_roundPositive {format : Format} (value : Model format) {e : ℚ} (hvalue : value.toRat? = some e) : value.exp10 = RealRounding.roundPositive format (10 ^ ↑e)

Base-ten exponential rounds the exact real power for every finite input.

@[simp]

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

Base-two exponential propagates NaR.

@[simp]

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

Base-ten exponential propagates NaR.

theorem FloatLib.Floats.Formats.Posit.Model.roundRatPowerMinusOne_eq_round {format : Format} (base exponent : ℚ) (hbase : 0 < base) : roundRatPowerMinusOne format base exponent = RealRounding.round format (↑base ^ ↑exponent - 1)

Shifting the rational candidates fuses subtraction with the final signed real rounding.

theorem FloatLib.Floats.Formats.Posit.Model.exp2Minus1_eq_round {format : Format} (value : Model format) {e : ℚ} (hvalue : value.toRat? = some e) : value.exp2Minus1 = RealRounding.round format (2 ^ ↑e - 1)

Every finite input gives a single rounding of the exact base-two power minus one.

theorem FloatLib.Floats.Formats.Posit.Model.exp10Minus1_eq_round {format : Format} (value : Model format) {e : ℚ} (hvalue : value.toRat? = some e) : value.exp10Minus1 = RealRounding.round format (10 ^ ↑e - 1)

Every finite input gives a single rounding of the exact base-ten power minus one.

@[simp]

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

Base-two exponential minus one propagates NaR.

@[simp]

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

Base-ten exponential minus one propagates NaR.