e_in_eInterval
plain-language theorem explainer
The declaration certifies that exp(1) lies inside the closed rational interval with endpoints 2.718 and 2.719. Numerics routines that certify exponential bounds cite this result to anchor the value of e. The tactic proof reduces the containment predicate to two real inequalities and discharges them with Mathlib's exp_one_gt_d9 and exp_one_lt_d9 lemmas via norm_num and linarith.
Claim. $2718/1000 ≤ exp(1) ≤ 2719/1000$
background
The module supplies interval bounds for the exponential function. An Interval is a structure with rational lower and upper bounds satisfying lo ≤ hi. The predicate contains(I, x) holds when lo ≤ x ≤ hi. The specific interval eInterval is defined with endpoints 2718/1000 and 2719/1000. Upstream, the contains definition from Basic and the Interval structure from Certification provide the containment logic. The module doc states that for x in [lo, hi] ⊆ [0,1) the exponential is bounded using monotonicity together with add_one_le_exp for lower bounds and 1/(1-x) for upper bounds.
proof idea
The proof first simplifies the goal using the definitions of contains and eInterval, yielding the conjunction of two inequalities. It then splits into cases. For the lower bound it invokes Real.exp_one_gt_d9 to obtain exp(1) > 2.7182818283, normalizes the rational 2718/1000 to 2.718, and applies linarith. The upper bound proceeds analogously with Real.exp_one_lt_d9 and 2719/1000.
why it matters
This result anchors the exponential interval in the numerics module, supporting rigorous bounds needed for Recognition Science computations of constants. It implements the module's strategy for exp bounds at the point x=1. No downstream uses are recorded yet, but it closes the certification of eInterval. It touches the framework's need for precise numerical intervals when deriving constants such as the fine-structure constant bounds inside (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.