expIntervalSimple_contains_exp
plain-language theorem explainer
The theorem shows that the simple interval enclosure for the exponential function, defined via lower bound x+1 and upper bound 1/(1-x) on [0,1), correctly contains exp(x) whenever x lies in the input interval I. Recognition Science numerics routines cite this result to obtain certified bounds on e and related constants without relying on floating-point approximations. The proof unfolds the interval definitions and chains the standard inequalities add_one_le_exp and exp_bound_div_one_sub_of_interval with monotonicity arguments.
Claim. Let $I$ be a closed interval with rational endpoints satisfying $0 ≤ lo(I)$ and $hi(I) < 1$. For any real $x$ contained in $I$, the interval produced by the simple exponential constructor on $I$ contains $exp(x)$.
background
The Interval structure is a closed interval with rational endpoints lo and hi together with a proof that lo ≤ hi. The contains predicate states that a real x belongs to I precisely when lo(I) ≤ x ≤ hi(I) after casting the rationals to reals. The module supplies interval arithmetic for the exponential on subintervals of [0,1) by using monotonicity of exp together with the elementary bounds x + 1 ≤ exp(x) and exp(x) ≤ 1/(1-x). The constructor expIntervalSimple builds a new interval whose lower endpoint is expLowerSimple(I.lo) = I.lo + 1 and whose upper endpoint is expUpperSimple(I.hi) = 1/(1 - I.hi).
proof idea
The tactic proof begins by simplifying the contains predicate on both the input and output intervals. It extracts the concrete inequalities lo(I) ≤ x ≤ hi(I), derives non-negativity of x and x < 1, then splits into two goals. The lower goal applies add_one_le_exp to obtain x + 1 ≤ exp(x) and closes with linarith after casting. The upper goal invokes exp_bound_div_one_sub_of_interval to obtain exp(x) ≤ 1/(1-x), shows that the right-hand side is monotone in the denominator, and again closes with linarith.
why it matters
This theorem certifies the correctness of the simple exponential interval constructor that appears in the numerics layer. It supplies the justification needed to compute rigorous enclosures for e = exp(1) and thereby supports downstream calculations of constants such as phi and the fine-structure constant inside the Recognition Science framework. No downstream uses are recorded, indicating the result functions as a foundational building block for certified transcendental arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.