Numerics Interval Exp E In E Interval

A proven interval for e

Euler's number e, approximately 2.718281828, is one of the most important constants in mathematics. It is the base of natural logarithms and appears throughout calculus, probability, and physics. A standard way to pin down an irrational number like e is to give a rational interval that contains it: for example, we know e lies between 2.718 and 2.719. This is a simple statement, but proving it rigorously requires care, because e is defined as an infinite sum or limit, not as a finite decimal.

In the Recognition Science framework's machine-checked library of formal theorems, a declaration named e_in_eInterval establishes exactly this containment. The framework defines an interval object with lower bound 2718/1000 and upper bound 2719/1000, and then proves that the actual value of e, written as exp(1), lies inside that interval. The proof uses two known facts about the exponential function: a lower bound that exp(x) is at least x + 1, and an upper bound that for x between 0 and 1, exp(x) is at most 1/(1 - x). For x = 1, these give the crude bounds 2 and infinity, but the framework instead relies on Mathlib's existing theorems that exp(1) is greater than 2.7182818283 and less than 2.7182818286. The declaration then combines these with simple arithmetic to show 2.718 ≤ e ≤ 2.719.

What this declaration does not claim is just as important. It does not prove that e is irrational or transcendental; those are classical results outside this declaration's scope. It does not give the tightest possible interval for e; the true value 2.718281828... is much closer to the lower bound than to the upper bound, but the interval is chosen for simplicity, not precision. It also does not compute e to any new digits; the interval merely confirms a well-known approximation. The declaration is a small, rigorous building block: it shows that a specific rational interval provably contains e, which is useful for any later work that needs a certified bound on this constant.

In practice, this kind of interval arithmetic is a tool for verified numerical computation. When a larger proof needs to know that e falls in a certain range, it can cite e_in_eInterval as a trusted fact rather than trusting a decimal approximation from a calculator. The declaration is a model of how the framework handles numerical constants: it does not assert a value from thin air, but proves containment using established theorems and exact rational arithmetic.

/-- e is contained in eInterval - PROVEN using Mathlib's exp_one_gt_d9/lt_d9 -/
theorem e_in_eInterval : eInterval.contains (exp 1) := by
  simp only [Interval.contains, eInterval]
  constructor
  · -- 2.718 ≤ exp(1)
    have h := Real.exp_one_gt_d9  -- 2.7182818283 < exp 1
    have h1 : ((2718 / 1000 : ℚ) : ℝ) = (2.718 : ℝ) := by norm_num
    linarith
  · -- exp(1) ≤ 2.719
    have h := Real.exp_one_lt_d9  -- exp 1 < 2.7182818286
    have h1 : ((2719 / 1000 : ℚ) : ℝ) = (2.719 : ℝ) := by norm_num
    linarith

/-- e is contained in eInterval - PROVEN using Mathlib's exp_one_gt_d9/lt_d9 -/
theorem e_in_eInterval : eInterval.contains (exp 1) := by
  simp only [Interval.contains, eInterval]
  constructor
  · -- 2.718 ≤ exp(1)
    have h := Real.exp_one_gt_d9  -- 2.7182818283 < exp 1
    have h1 : ((2718 / 1000 : ℚ) : ℝ) = (2.718 : ℝ) := by norm_num
    linarith
  · -- exp(1) ≤ 2.719
    have h := Real.exp_one_lt_d9  -- exp 1 < 2.7182818286
    have h1 : ((2719 / 1000 : ℚ) : ℝ) = (2.719 : ℝ) := by norm_num
    linarith

What this page does not claim

This declaration does not prove that e is irrational or transcendental. This declaration does not give the tightest possible interval for e. This declaration does not compute any new digits of e.

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/Exp.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: