Numerics Interval Pow Rpow Interval Simple Contains Rpow

A simple containment theorem

Interval arithmetic is a way of computing with ranges of values instead of single numbers. When a calculation involves a quantity known only to lie between two bounds, interval arithmetic replaces each number by its enclosing interval and propagates the uncertainty through every operation. The result is a new interval that is guaranteed to contain the true answer, provided each step is sound.

The theorem rpowIntervalSimple_contains_rpow in the framework's machine-checked library of formal theorems states one such sound step for the power function x^y. It says that if you have already established, by any means, that the value of x^y lies between a lower bound and an upper bound, then the interval built from those two bounds contains x^y. The proof is immediate: the interval is defined to be exactly the set of numbers between its bounds, and the two hypotheses are precisely the two halves of the membership condition. The declaration is a packaging step, not a new numerical method.

The theorem does not compute the bounds itself. It takes the bounds as inputs, along with a proof that the lower bound does not exceed the upper bound, and returns the containment statement. It also does not require x to be positive, nor does it depend on the monotonicity of the power function. Those properties appear in other declarations in the same module, such as the lemmas stating that goldenRatio^x is strictly increasing in x, but they are not needed for this simple containment result.

In the Recognition Science framework, this theorem supports a chain of interval-based verifications. For example, the module proves that the golden ratio raised to various powers, such as the fifth power, lies in explicitly given rational intervals. Each such proof ultimately relies on the same containment principle: once the bounds are known, the interval claim follows. The simple theorem is the hinge that connects a computed bound to a formal interval statement.

What the declaration does not claim is any information about how tight the interval is, or how the bounds were obtained. It also does not assert that the power function is monotone, continuous, or defined for all real exponents. Those are separate facts, proved elsewhere. The theorem is a small, precise tool: given a containment fact, it packages it into the interval form that the rest of the library consumes.

/-- The simple power interval contains x^y if the bounds are correct -/
theorem rpowIntervalSimple_contains_rpow
    {result_lo result_hi : ℚ}
    (h_valid : result_lo ≤ result_hi)
    {x y : ℝ}
    (h_lo : (result_lo : ℝ) ≤ x.rpow y)
    (h_hi : x.rpow y ≤ (result_hi : ℝ)) :
    (rpowIntervalSimple result_lo result_hi h_valid).contains (x.rpow y) :=
  ⟨h_lo, h_hi⟩

/-- The simple power interval contains x^y if the bounds are correct -/
theorem rpowIntervalSimple_contains_rpow
    {result_lo result_hi : ℚ}
    (h_valid : result_lo ≤ result_hi)
    {x y : ℝ}
    (h_lo : (result_lo : ℝ) ≤ x.rpow y)
    (h_hi : x.rpow y ≤ (result_hi : ℝ)) :
    (rpowIntervalSimple result_lo result_hi h_valid).contains (x.rpow y) :=
  ⟨h_lo, h_hi⟩

What this page does not claim

The theorem does not establish any bound on the width or tightness of the interval. The theorem does not assert that the power function x^y is defined for all real x and y. The theorem does not depend on the monotonicity of the power function.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Numerics/Interval/Pow.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: