Correct rounding of accepted binary exponential, logarithm, and power results

Taylor enclosure bounds and exact decoding prove that each returned encoding is finite and equals nearest-even rounding of the real function. The domain certificates instantiate the finite-real contract on the executable success predicate.

For powers, rpow_eq_exp_reduced writes (s * 2 ^ e) ^ b as exp (b * log s + (b * e - k) * log 2) * 2 ^ k for every integer k. The grid enclosures of log s and log 2, the exponential enclosure, and the scaled endpoint check Enclosure.roundScaled? then give toReal_of_powRat_eq_ok and toReal_of_pow_eq_ok.

These are partial-correctness theorems: they describe a result whenever the kernel returns .ok, and no theorem says which inputs succeed. The one proved success is the signed-zero passthrough of expMinus1 and logPlus1. exp, log, and pow have no proved success case.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.accept_eq_ok {fmt : FloatFormat} {result : Option (Model fmt)} {failure : Failure} {value : Model fmt} : accept result failure = Except.ok value ↔ result = some value

accept succeeds exactly with the certified encoding it was given.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.expRat_eq_guarded (fmt : FloatFormat) (argument : ℚ) (options : Options) : expRat fmt argument options = if (!fmt.isIEEE) = true then Except.error Failure.unsupportedFormat else if argument = 0 then accept (Enclosure.round? fmt (Numerics.RationalInterval.point 1)) Failure.inconclusive else if Numerics.ElementaryComparison.compareExp argument (expUnderflowInterval fmt).hi ≠ Ordering.gt then accept (Enclosure.round? fmt (expUnderflowInterval fmt)) Failure.inconclusive else if Numerics.ElementaryComparison.compareExp argument (expUpperBound fmt) ≠ Ordering.lt then Except.error Failure.range else have search := refine fmt (Numerics.Enclosure.BinaryGrid.exp argument) (max 1 options.initialDegree) (Numerics.Enclosure.BinaryGrid.expPrecision (fmt.fracWidth + 1) argument (max 1 options.initialDegree)) options.maxSteps; accept search (if search.isSome = true then Failure.inconclusive else expSearchFailure fmt argument 0)

The rational argument checks preserve the original guarded exponential for every attempt budget, including zero attempts and formats outside the supported domain.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.expMinus1Rat_eq_guarded (fmt : FloatFormat) (argument : ℚ) (options : Options) : expMinus1Rat fmt argument options = if (!fmt.isIEEE) = true then Except.error Failure.unsupportedFormat else if argument = 0 then accept (Enclosure.round? fmt (Numerics.RationalInterval.point 0)) Failure.inconclusive else if Numerics.ElementaryComparison.compareExp argument (expUnderflowInterval fmt).hi ≠ Ordering.gt then accept (Enclosure.round? fmt ((expUnderflowInterval fmt).sub (Numerics.RationalInterval.point 1))) Failure.inconclusive else if Numerics.ElementaryComparison.compareExp argument (expUpperBound fmt + 1) ≠ Ordering.lt then Except.error Failure.range else have search := refine fmt (fun (degree precision : ℕ) => (Numerics.Enclosure.BinaryGrid.exp argument degree precision).sub (Numerics.RationalInterval.point 1)) (max 1 options.initialDegree) (Numerics.Enclosure.BinaryGrid.expPrecision (fmt.fracWidth + 1) argument (max 1 options.initialDegree) true) options.maxSteps; accept search (if search.isSome = true then Failure.inconclusive else expSearchFailure fmt argument 1)

Skipping impossible guards preserves both accepted encodings and failures of expMinus1Rat.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_expRat_eq_ok {fmt : FloatFormat} {argument : ℚ} {options : Options} {result : Model fmt} (hresult : expRat fmt argument options = Except.ok result) : result.isFinite = true

Successful rational-input exponentials are finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_expRat_eq_ok {fmt : FloatFormat} {argument : ℚ} {options : Options} {result : Model fmt} (hresult : expRat fmt argument options = Except.ok result) : result.toReal = roundAt fmt (Real.exp ↑argument)

An accepted rational exponential equals rounding of the exact real exponential.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_logRat_eq_ok {fmt : FloatFormat} {argument : ℚ} {options : Options} {result : Model fmt} (hresult : logRat fmt argument options = Except.ok result) : result.isFinite = true

Successful rational-input logarithms are finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_logRat_eq_ok {fmt : FloatFormat} {argument : ℚ} {options : Options} {result : Model fmt} (hresult : logRat fmt argument options = Except.ok result) : result.toReal = roundAt fmt (Real.log ↑argument)

An accepted rational logarithm equals rounding of the exact real logarithm.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_expMinus1Rat_eq_ok {fmt : FloatFormat} {argument : ℚ} {options : Options} {result : Model fmt} (hresult : expMinus1Rat fmt argument options = Except.ok result) : result.isFinite = true

Successful rational-input expMinus1 results are finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_expMinus1Rat_eq_ok {fmt : FloatFormat} {argument : ℚ} {options : Options} {result : Model fmt} (hresult : expMinus1Rat fmt argument options = Except.ok result) : result.toReal = roundAt fmt (Real.exp ↑argument - 1)

The subtraction takes place in the exact real expression, before its only rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_logPlus1Rat_eq_ok {fmt : FloatFormat} {argument : ℚ} {options : Options} {result : Model fmt} (hresult : logPlus1Rat fmt argument options = Except.ok result) : result.isFinite = true

Successful rational-input logPlus1 results are finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_logPlus1Rat_eq_ok {fmt : FloatFormat} {argument : ℚ} {options : Options} {result : Model fmt} (hresult : logPlus1Rat fmt argument options = Except.ok result) : result.toReal = roundAt fmt (Real.log (1 + ↑argument))

Forming 1 + argument exactly avoids an intermediate floating-point rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_exp_eq_ok {fmt : FloatFormat} {input result : Model fmt} {options : Options} (hresult : exp input options = Except.ok result) : result.isFinite = true

Every exponential result returned by the concrete refinement algorithm is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_exp_eq_ok {fmt : FloatFormat} {input result : Model fmt} {options : Options} (hresult : exp input options = Except.ok result) : result.toReal = roundAt fmt (Real.exp input.toReal)

The concrete exponential kernel certifies nearest-even rounding of the exact input's exp.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_log_eq_ok {fmt : FloatFormat} {input result : Model fmt} {options : Options} (hresult : log input options = Except.ok result) : result.isFinite = true

Every logarithm result returned by the concrete refinement algorithm is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_log_eq_ok {fmt : FloatFormat} {input result : Model fmt} {options : Options} (hresult : log input options = Except.ok result) : result.toReal = roundAt fmt (Real.log input.toReal)

The concrete logarithm kernel certifies nearest-even rounding of the exact input's log.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_expMinus1_eq_ok {fmt : FloatFormat} {input result : Model fmt} {options : Options} (hresult : expMinus1 input options = Except.ok result) : result.isFinite = true

Each accepted expMinus1 result is finite, including the signed-zero branch.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_expMinus1_eq_ok {fmt : FloatFormat} {input result : Model fmt} {options : Options} (hresult : expMinus1 input options = Except.ok result) : result.toReal = roundAt fmt (Real.exp input.toReal - 1)

An accepted expMinus1 equals nearest-even rounding of Real.exp x - 1.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_logPlus1_eq_ok {fmt : FloatFormat} {input result : Model fmt} {options : Options} (hresult : logPlus1 input options = Except.ok result) : result.isFinite = true

Each accepted logPlus1 result is finite, including the signed-zero branch.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_logPlus1_eq_ok {fmt : FloatFormat} {input result : Model fmt} {options : Options} (hresult : logPlus1 input options = Except.ok result) : result.toReal = roundAt fmt (Real.log (1 + input.toReal))

An accepted logPlus1 equals nearest-even rounding of Real.log (1 + x).

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.expMinus1_of_isZero {fmt : FloatFormat} {input : Model fmt} (hfmt : fmt.isIEEE = true) (hzero : input.isZero = true) (options : Options) : expMinus1 input options = Except.ok input

The IEEE input's zero encoding passes through expMinus1 unchanged.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.logPlus1_of_isZero {fmt : FloatFormat} {input : Model fmt} (hfmt : fmt.isIEEE = true) (hzero : input.isZero = true) (options : Options) : logPlus1 input options = Except.ok input

The IEEE input's zero encoding passes through logPlus1 unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.exp_correctlyRoundedCertificateOn (fmt : FloatFormat) (options : Options) : Contract.CorrectlyRoundedCertificateOn fmt Real.exp (fun (input : Model fmt) => (exp input options).toOption.getD (zero fmt false)) fun (input : Model fmt) => (exp input options).isOk = true

The finite-real contract holds on the exponential kernel's executable success domain. The zero fallback adapts the certified result to the contract's total-function argument.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.log_correctlyRoundedCertificateOn (fmt : FloatFormat) (options : Options) : Contract.CorrectlyRoundedCertificateOn fmt Real.log (fun (input : Model fmt) => (log input options).toOption.getD (zero fmt false)) fun (input : Model fmt) => (log input options).isOk = true

The finite-real contract holds on the inputs accepted by the logarithm kernel.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.expMinus1_correctlyRoundedCertificateOn (fmt : FloatFormat) (options : Options) : Contract.CorrectlyRoundedCertificateOn fmt (fun (x : ℝ) => Real.exp x - 1) (fun (input : Model fmt) => (expMinus1 input options).toOption.getD (zero fmt false)) fun (input : Model fmt) => (expMinus1 input options).isOk = true

Correct rounding of exp x - 1 on the executable acceptance domain.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.logPlus1_correctlyRoundedCertificateOn (fmt : FloatFormat) (options : Options) : Contract.CorrectlyRoundedCertificateOn fmt (fun (x : ℝ) => Real.log (1 + x)) (fun (input : Model fmt) => (logPlus1 input options).toOption.getD (zero fmt false)) fun (input : Model fmt) => (logPlus1 input options).isOk = true

Correct rounding of log (1 + x) on the executable acceptance domain.

Real powers

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.containsReal_logReduced {value : ℚ} (hvalue : 0 < value) (precision : ℕ) : Numerics.Interval.ContainsReal (Numerics.Interval.BinaryGrid.decode precision) (logReduced value precision) (Real.log ↑value)

Table reduction preserves logarithm containment for every positive rational.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.containsReal_powArgument {logScaled logTwo : Numerics.Interval ℤ} {precision : ℕ} {logValue : ℝ} (hlog : Numerics.Interval.ContainsReal (Numerics.Interval.BinaryGrid.decode precision) logScaled logValue) (hlogTwo : Numerics.Interval.ContainsReal (Numerics.Interval.BinaryGrid.decode precision) logTwo (Real.log 2)) (exponent multiple : ℚ) : Numerics.Interval.ContainsReal (Numerics.Interval.BinaryGrid.decode precision) (powArgument logScaled logTwo exponent multiple) (↑exponent * logValue + ↑multiple * Real.log 2)

The grid combination encloses exponent * log s + multiple * log 2.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.contains_expInterval {argument : Numerics.RationalInterval} {x : ℝ} (hx : argument.Contains x) (degree precision : ℕ) : (expInterval argument degree precision).Contains (Real.exp x)

One exponential at the lower end encloses exp over the whole argument interval.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.contains_expReduced {reduced : ℕ → Numerics.Interval ℤ} {r : ℝ} (hreduced : ∀ (grid : ℕ), Numerics.Interval.ContainsReal (Numerics.Interval.BinaryGrid.decode grid) (reduced grid) r) (extraBits degree precision : ℕ) : (expReduced reduced extraBits degree precision).Contains (Real.exp r)

An argument enclosed on every grid gives an enclosure of its exponential.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.rpow_eq_exp_reduced {scaled : ℚ} (hscaled : 0 < scaled) (binaryExponent scale : ℤ) (exponent : ℚ) : (↑scaled * 2 ^ binaryExponent) ^ ↑exponent = Real.exp (↑exponent * Real.log ↑scaled + ↑(exponent * ↑binaryExponent - ↑scale) * Real.log 2) * 2 ^ scale

The real power of a positive scaled rational is the exponential of the reduced argument times the removed power of two, for every integer scale.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.contains_exp_underflow {fmt : FloatFormat} {t : ℝ} {bound : ℚ} (ht : t ≤ ↑bound) (hbound : bound ≤ ↑(fmt.minSubnormalExponent - 1) * logTwoUpper) : { lo := 0, hi := 1 }.Contains (Real.exp t * 2 ^ (-(fmt.minSubnormalExponent - 1)))

An argument at most the screened bound has an exponential of at most half the least subnormal: [0, 1] contains it times 2 ^ -(minSubnormalExponent - 1), so the screen never forms that power.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_powRatScaled_eq_ok {fmt : FloatFormat} {scaled : ℚ} {binaryExponent : ℤ} {exponent : ℚ} {options : Options} {result : Model fmt} (hresult : powRatScaled fmt scaled binaryExponent exponent options = Except.ok result) : result.isFinite = true

Successful scaled powers are finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_powRatScaled_eq_ok {fmt : FloatFormat} {scaled : ℚ} {binaryExponent : ℤ} {exponent : ℚ} {options : Options} {result : Model fmt} (hresult : powRatScaled fmt scaled binaryExponent exponent options = Except.ok result) : result.toReal = roundAt fmt ((↑scaled * 2 ^ binaryExponent) ^ ↑exponent)

An accepted scaled power equals rounding of the real power of scaled * 2 ^ binaryExponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.splitTwoPow_spec {value : ℚ} (hvalue : 0 < value) : 0 < (splitTwoPow value).1 ∧ ↑(splitTwoPow value).1 * 2 ^ (splitTwoPow value).2 = ↑value

The binary split of a positive rational is positive and recombines to its value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_powRat_eq_ok {fmt : FloatFormat} {base exponent : ℚ} {options : Options} {result : Model fmt} (hresult : powRat fmt base exponent options = Except.ok result) : result.isFinite = true

Successful rational-input powers are finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_powRat_eq_ok {fmt : FloatFormat} {base exponent : ℚ} {options : Options} {result : Model fmt} (hresult : powRat fmt base exponent options = Except.ok result) : result.toReal = roundAt fmt (↑base ^ ↑exponent)

An accepted rational power equals nearest-even rounding of the real power base ^ exponent (Real.rpow, with base > 0 whenever the result is accepted).

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.base_pos_of_powRat_eq_ok {fmt : FloatFormat} {base exponent : ℚ} {options : Options} {result : Model fmt} (hresult : powRat fmt base exponent options = Except.ok result) : 0 < base

An accepted rational power has a positive base.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.abs_mul_log_lt_two_pow_powArgumentExponent {base exponent : Numerics.Dyadic} (hnegative : base.negative = false) (hsignificand : base.significand ≠ 0) : |exponent.toReal * Real.log base.toReal| < 2 ^ powArgumentExponent base exponent

The stored-field bound powArgumentExponent bounds |exponent * log base|.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.contains_exp_powNearOne (fmt : FloatFormat) {t : ℝ} (ht : |t| < 2 ^ (-(↑fmt.fracWidth + 4))) : (powNearOne fmt).Contains (Real.exp t)

Every exponential of an argument below 2 ^ -(fracWidth + 4) lies in powNearOne.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.isFinite_of_pow_eq_ok {fmt : FloatFormat} {base exponent : Model fmt} {options : Options} {result : Model fmt} (hresult : pow base exponent options = Except.ok result) : result.isFinite = true

Every power returned by the certified search is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Certified.toReal_of_pow_eq_ok {fmt : FloatFormat} {base exponent : Model fmt} {options : Options} {result : Model fmt} (hresult : pow base exponent options = Except.ok result) : result.toReal = roundAt fmt (base.toReal ^ exponent.toReal)

An accepted certified power equals nearest-even rounding of the real power toReal base ^ toReal exponent (Real.rpow, since the base of an accepted result is positive).