Exact single-rounding contracts for posit integer powers

The finite-domain contracts expose the exact rational power presented to the posit rounding kernel. Zero to a negative power is excluded; exponent zero is the constant one on all finite inputs. No posit rounding occurs inside the exponentiation or compound's addition.

theorem FloatLib.Floats.Formats.Posit.Model.roundIntPower_eq_roundRat {format : Format} (base : ℚ) (exponent : ℤ) (hdomain : base ≠ 0 ∨ 0 < exponent) : roundIntPower format base exponent = roundRat format (base ^ exponent)

In its real domain, rational integer exponentiation is followed by exactly one rounding.

theorem FloatLib.Floats.Formats.Posit.Model.roundIntPower_zero_of_neg {format : Format} (exponent : ℤ) (hexponent : exponent < 0) : roundIntPower format 0 exponent = nar format

Zero to a negative integer power has no finite limit.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.roundIntPower_exponent_zero {format : Format} (base : ℚ) : roundIntPower format base 0 = roundRat format 1

At fixed exponent zero, every finite rational base gives the constant one.

theorem FloatLib.Floats.Formats.Posit.Model.powInt_eq_roundRat {format : Format} (value : Model format) {q : ℚ} (exponent : ℤ) (hvalue : value.toRat? = some q) (hdomain : q ≠ 0 ∨ 0 < exponent) : value.powInt exponent = roundRat format (q ^ exponent)

Finite integer powers round the exact rational power once, including negative exponents.

theorem FloatLib.Floats.Formats.Posit.Model.compound_eq_roundRat {format : Format} (value : Model format) {q : ℚ} (exponent : ℤ) (hvalue : value.toRat? = some q) (hdomain : 1 + q ≠ 0 ∨ 0 < exponent) : value.compound exponent = roundRat format ((1 + q) ^ exponent)

Compound rounds the exact rational expression (1 + q) ^ exponent once.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.powInt_nar {format : Format} (exponent : ℤ) : (nar format).powInt exponent = nar format

Integer powers propagate NaR, including at exponent zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.compound_nar {format : Format} (exponent : ℤ) : (nar format).compound exponent = nar format

Compound propagates NaR, including at exponent zero.

theorem FloatLib.Floats.Formats.Posit.Model.powInt_zero_of_neg {format : Format} (exponent : ℤ) (hexponent : exponent < 0) : (zero format).powInt exponent = nar format

A zero base with negative integer exponent produces NaR.

theorem FloatLib.Floats.Formats.Posit.Model.powInt_exponent_zero {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.powInt 0 = roundRat format 1

Every finite input raised to the fixed integer zero produces rounded one.

theorem FloatLib.Floats.Formats.Posit.Model.compound_exponent_zero {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.compound 0 = roundRat format 1

Compound with fixed integer zero is constant one, including at input negative one.

theorem FloatLib.Floats.Formats.Posit.Model.powInt_zero_of_pos {format : Format} (exponent : ℤ) (hexponent : 0 < exponent) : (zero format).powInt exponent = zero format

Positive integer powers of zero are zero.

theorem FloatLib.Floats.Formats.Posit.Model.compound_eq_nar_of_neg_one {format : Format} (value : Model format) (exponent : ℤ) (hvalue : value.toRat? = some (-1)) (hexponent : exponent < 0) : value.compound exponent = nar format

Compound is undefined at base 1 + q = 0 and a negative exponent.

theorem FloatLib.Floats.Formats.Posit.Model.compound_eq_zero_of_neg_one {format : Format} (value : Model format) (exponent : ℤ) (hvalue : value.toRat? = some (-1)) (hexponent : 0 < exponent) : value.compound exponent = zero format

Positive powers of the zero compound base give zero.