Real semantics of exact integer powers

The power is evaluated in the rationals before any format rounding. Casting commutes with integer exponentiation, including negative exponents, so the established rational-rounding theorem proves a single rounding of the exact real power. IEEE overflow has no real denotation and is excluded by the finite-result premise.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Algebraic.toReal_of_toRat?_eq_some {fmt : FloatFormat} {value : Model fmt} {q : ℚ} (hvalue : value.toRat? = some q) : value.toReal = ↑q

A successful rational decode is the exact real value of the stored operand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Algebraic.isFinite_of_toRat?_eq_some {fmt : FloatFormat} {value : Model fmt} {q : ℚ} (hvalue : value.toRat? = some q) : value.isFinite = true

Successful rational decoding characterizes a finite operand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundAlgebraicRat (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (value : ℚ) (hfinite : (roundAlgebraicRat fmt value).isFinite = true) : (roundAlgebraicRat fmt value).toReal = roundAt fmt ↑value

The exact rational boundary rounds once to the independent nearest-even real grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.powInt_of_isSNaN {fmt : FloatFormat} (value : Model fmt) (exponent : ℤ) (hsignaling : value.isSNaN = true) : value.powInt exponent = value.quietNaN

A signaling NaN is quieted before every exponent case, including exponent zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.powInt_zero {fmt : FloatFormat} (value : Model fmt) (hnan : value.isSNaN = false) : value.powInt 0 = posOne fmt

The zero exponent returns one unless the base is a signaling NaN.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.powInt_eq_roundAlgebraicRat {fmt : FloatFormat} (value : Model fmt) (exponent : ℤ) {q : ℚ} (hvalue : value.toRat? = some q) (hzero : value.isZero = false) (hexponent : exponent ≠ 0) : value.powInt exponent = roundAlgebraicRat fmt (q ^ exponent)

A finite nonzero base uses exactly one rational rounding for every nonzero exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_powInt_eq_roundAt {fmt : FloatFormat} (value : Model fmt) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hvalue : value.isFinite = true) (hzero : value.isZero = false) (hfinite : (value.powInt exponent).isFinite = true) : (value.powInt exponent).toReal = roundAt fmt (value.toReal ^ exponent)

Integer powers of finite nonzero inputs round the exact real power once, for positive, negative and zero integer exponents. The output may be subnormal or zero; only overflow is excluded.