Correct rounding of powers

Model.pow sends a finite nonzero base with a finite integral exponent to Power.integerPower?. This file proves that the result is the nearest-even rounding of the exact real power. A finite positive base with a non-integral exponent goes to the certified enclosure search Transcendentals.Certified.pow. Whenever that search succeeds, pow returns its result, which is the nearest-even rounding of the real power (pow_spec_of_certified).

The executable kernel has three routes. Small exact problems call powInt, which rounds the exact rational power once. A base of magnitude one gives a signed one. Every other case brackets the exact power between two dyadic endpoints (powBounds, squareScreen) and accepts the rounding only when both endpoints round to the same finite value (roundEnclosure?). If no working precision decides, powInt is the fallback. The endpoint lemmas show that the brackets are sound, toReal_of_attempt turns an accepted bracket into correct rounding, and toReal_integerPowerWith combines the three routes.

The main result is toReal_pow_of_eq_intCast: for an IEEE format, a finite nonzero base and a finite exponent with integer value n, every finite result of pow equals roundAt fmt (toReal base ^ n).

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.toRat_nonneg (x : Endpoint) : 0 ≤ x.toRat

Every endpoint is nonnegative.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.toRat_mul (x y : Endpoint) : (x.mul y).toRat = x.toRat * y.toRat

The exact product of endpoints denotes the product of their values.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.toRat_one : one.toRat = 1

The unit endpoint denotes one.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.toRat_truncDown_le (precision : ℕ) (x : Endpoint) : (truncDown precision x).toRat ≤ x.toRat

Truncation toward zero never increases an endpoint.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.le_toRat_truncUp (precision : ℕ) (x : Endpoint) : x.toRat ≤ (truncUp precision x).toRat

Truncation away from zero never decreases an endpoint.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.two_zpow_le_of_geTwoPow {x : Endpoint} {bound : ℤ} (h : x.geTwoPow bound = true) : 2 ^ bound ≤ x.toRat

The leading-bit test is a sound lower bound.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Endpoint.le_two_zpow_of_leTwoPow {x : Endpoint} {bound : ℤ} (h : x.leTwoPow bound = true) : x.toRat ≤ 2 ^ bound

The leading-bit test is a sound upper bound.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.powBounds_spec (precision : ℕ) (base : Endpoint) (exponent : ℕ) : (powBounds precision base exponent).1.toRat ≤ base.toRat ^ exponent ∧ base.toRat ^ exponent ≤ (powBounds precision base exponent).2.toRat

Binary exponentiation with directed truncation encloses the exact power.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.Screen.Holds (above below : ℤ) (remaining : ℕ) (v : ℚ) : Screen → Prop

What a screening outcome certifies about v ^ (2 ^ t) for every t ≥ remaining.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.squareScreen_holds (precision : ℕ) (above below : ℤ) (remaining : ℕ) (lower upper : Endpoint) (v : ℚ) (hv : 0 ≤ v) (hlower : lower.toRat ≤ v) (hupper : v ≤ upper.toRat) : Screen.Holds above below remaining v (squareScreen precision above below remaining lower upper)

Repeated squaring with early screening is sound for every value in the enclosure.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.toReal_of_roundEnclosure? {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) {lower upper : ℚ} {result : Model fmt} (h : roundEnclosure? fmt lower upper = some result) {target : ℝ} (hlower : ↑lower ≤ target) (hupper : target ≤ ↑upper) : result.toReal = roundAt fmt target

An accepted signed enclosure is the nearest-even rounding of every real target inside it.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.attemptTarget (negative reciprocal : Bool) (base : Endpoint) (magnitude shift : ℕ) : ℝ

The exact target of attempt: (-1)^negative * ((base ^ magnitude) ^ (2 ^ shift)) ^ (±1), with the reciprocal selected by reciprocal.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.toReal_of_attempt {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) {precision : ℕ} {negative reciprocal : Bool} {base : Endpoint} {magnitude shift : ℕ} {result : Model fmt} (h : attempt fmt precision negative reciprocal base magnitude shift = some result) (hfinite : result.isFinite = true) : result.toReal = roundAt fmt (attemptTarget negative reciprocal base magnitude shift)

Every finite result of one enclosure attempt is the correctly rounded exact power.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.zpow_integralValue_eq_attemptTarget (b : Numerics.Dyadic) (negativeExponent : Bool) (magnitude shift : ℕ) : b.toReal ^ integralValue negativeExponent magnitude shift = attemptTarget (b.negative && (shift == 0 && magnitude % 2 == 1)) negativeExponent { mantissa := b.significand, exponent := b.exponent } magnitude shift

The exact target of attempt for the decoded base is the real power toReal base ^ integralValue negativeExponent magnitude shift.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.toReal_integerPowerWith {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (exactBudget : ℕ) {base : Model fmt} {b : Numerics.Dyadic} (hb : base.toDyadic? = some b) (hzero : base.isZero = false) (negativeExponent : Bool) (magnitude shift : ℕ) (hfinite : (integerPowerWith exactBudget base b negativeExponent magnitude shift).isFinite = true) : (integerPowerWith exactBudget base b negativeExponent magnitude shift).toReal = roundAt fmt (base.toReal ^ integralValue negativeExponent magnitude shift)

integerPowerWith is correctly rounded for every exact budget: a finite result is the nearest-even rounding of the real power of a finite nonzero base.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.integralParts?_of_eq_natCast (y : Numerics.Dyadic) (value : ℕ) (h : ↑y.significand * 2 ^ y.exponent = ↑value) : ∃ (magnitude : ℕ) (shift : ℕ), integralParts? y = some (magnitude, shift) ∧ magnitude <<< shift = value

integralParts? finds the decomposition of every dyadic whose unsigned value is a natural number value, and the parts recombine to that number.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.toReal_pow_of_eq_intCast {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) {base exponent : Model fmt} {n : ℤ} (hbase : base.isFinite = true) (hbzero : base.isZero = false) (hexp : exponent.isFinite = true) (hn : exponent.toReal = ↑n) (hfinite : (base.pow exponent).isFinite = true) : (base.pow exponent).toReal = roundAt fmt (base.toReal ^ n)

Main correctness theorem for integral exponents: when the base is finite and nonzero and the exponent is a finite float with integer value n, every finite result of pow is the nearest-even rounding of the real power toReal base ^ n.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.integerPower?_eq_none_of_ne_intCast {fmt : FloatFormat} {base exponent : Model fmt} (hnonintegral : ∀ (n : ℤ), exponent.toReal ≠ ↑n) : integerPower? base exponent = none

An exponent whose real value is not an integer leaves the integral-power route.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Power.pow_spec_of_certified {fmt : FloatFormat} {base exponent : Model fmt} (hbase : base.isFinite = true) (hpositive : 0 < base.toReal) (hexp : exponent.isFinite = true) (hnonintegral : ∀ (n : ℤ), exponent.toReal ≠ ↑n) (hsettled : (Transcendentals.Certified.pow base exponent certifiedOptions).isOk = true) : (base.pow exponent).isFinite = true ∧ (base.pow exponent).toReal = roundAt fmt (base.toReal ^ exponent.toReal)

Main correctness theorem for non-integral exponents: for a finite positive base and a finite exponent whose value is not an integer, whenever the certified enclosure search Transcendentals.Certified.pow succeeds (which happens only for IEEE descriptors), pow returns a finite nearest-even rounding of the real power toReal base ^ toReal exponent.