eInterval
eInterval defines the closed rational interval [2.718, 2.719] that is guaranteed to contain e = exp(1). Numerics code in Recognition Science would cite it when constructing rigorous bounds for the exponential in interval arithmetic. The definition populates the Interval structure directly and discharges the endpoint ordering with a single norm_num call.
claimDefine the closed interval $I = [2718/1000, 2719/1000] = [2.718, 2.719]$ whose rational endpoints satisfy $2718/1000 ≤ 2719/1000$.
background
Interval is the structure with fields lo : ℚ, hi : ℚ and valid : lo ≤ hi, introduced in Numerics.Interval.Basic; a parallel version with real endpoints appears in Recognition.Certification. The module Numerics.Interval.Exp supplies rigorous interval bounds for the exponential using Mathlib's exp_one_gt_d9 and exp_one_lt_d9. For arguments in a subinterval of [0,1) the exponential is monotonic, so the image lies between the images of the endpoints; the module also records the general inequalities exp(x) ≤ 1/(1-x) and x + 1 ≤ exp(x).
proof idea
Direct definition that constructs the Interval record with the two rational literals and invokes norm_num to prove the ordering lo ≤ hi. No external lemmas are applied beyond the structure constructor and the numeric tactic.
why it matters in Recognition Science
The definition supplies the concrete interval used by the downstream theorem e_in_eInterval to certify e ∈ I. It forms part of the numerics layer that supports interval arithmetic for constants and mass formulas on the phi-ladder. It closes a small explicit-bound gap without introducing floating-point approximations.
scope and limits
- Does not tighten the interval beyond [2.718, 2.719].
- Does not bound exp at any argument other than 1.
- Does not reference the J-cost function or the phi-ladder.
- Does not claim optimality among possible rational intervals.
formal statement (Lean)
73def eInterval : Interval where
74 lo := 2718 / 1000
proof body
Definition body.
75 hi := 2719 / 1000
76 valid := by norm_num
77
78/-- e is contained in eInterval - PROVEN using Mathlib's exp_one_gt_d9/lt_d9 -/