Numerics Interval Exp Exp Interval Simple Contains Exp

Guaranteed bounds

The exponential function, written exp(x) or eˣ, grows so quickly that even a computer with finite precision can struggle to track it. Interval arithmetic tames this by replacing a single number with a guaranteed range: instead of saying "exp(0.5) is about 1.6487", it says "exp(0.5) lies somewhere between 1.5 and 2". The challenge is to make such ranges both narrow enough to be useful and wide enough to be always correct, never missing the true value.

The declaration expIntervalSimple_contains_exp is a machine-checked theorem in the framework's library of formal mathematics. It states a precise guarantee: if you take any interval [lo, hi] that lies entirely within [0, 1), and x is any real number inside that interval, then the simple interval method produces a new interval that always contains exp(x). The method itself is deliberately simple. For the lower bound it uses the fact that exp(x) ≥ x + 1, a classic inequality that holds for every real x. For the upper bound it uses exp(x) ≤ 1/(1 − x), which is valid when x is between 0 and 1. Both bounds are elementary, and the theorem proves that their combination is rigorous.

What makes this worth stating as a formal theorem rather than a casual observation is the word "always". The claim covers every possible input interval in the allowed range, not just the nice cases. The proof, checked by the machine, verifies that the lower bound never exceeds the upper bound and that both inequalities hold for all real x in the interval. It is a small but complete piece of numerical rigor: no floating-point rounding, no hidden assumptions, no unexamined edge cases.

In Recognition Science, this kind of guaranteed interval is a building block. The framework's approach to physics relies on exact arithmetic over rational numbers, and interval methods like this one let it compute with real numbers while preserving every result as provably correct. The theorem does not, however, claim that the simple bounds are the tightest possible. For x near 1, the upper bound 1/(1 − x) becomes very large, and a more sophisticated method would produce a narrower range. The theorem only promises correctness, not optimality.

The practical consequence is that any computation using expIntervalSimple can trust its output as a true enclosure of the exponential function, within the stated domain. That trust is not a matter of convention or good practice; it is a proved fact, audited by the machine. For a reader, the takeaway is simple: when the framework reports a range for exp(x), that range is guaranteed to contain the real value, and the guarantee has been checked line by line.

theorem expIntervalSimple_contains_exp {I : Interval}
    (hI_lo : 0 ≤ I.lo) (hI_hi : I.hi < 1)
    {x : ℝ} (hx : I.contains x) :
    (expIntervalSimple I hI_lo hI_hi).contains (exp x) := by
  simp only [contains, expIntervalSimple, expLowerSimple, expUpperSimple]
  have hx_lo : (I.lo : ℝ) ≤ x := hx.1
  have hx_hi : x ≤ (I.hi : ℝ) := hx.2
  have hx_nonneg : 0 ≤ x := le_trans (by exact_mod_cast hI_lo) hx_lo
  have hx_lt_one : x < 1 := lt_of_le_of_lt hx_hi (by exact_mod_cast hI_hi)
  have h_hi_lt_one : (I.hi : ℝ) < 1 := by exact_mod_cast hI_hi
  constructor
  · -- Lower bound: I.lo + 1 ≤ exp(x)
    have h1 : (I.lo : ℝ) + 1 ≤ x + 1 := by linarith
    have h2 : x + 1 ≤ exp x := Real.add_one_le_exp x
    simp only [Rat.cast_add, Rat.cast_one]
    linarith
  · -- Upper bound: exp(x) ≤ 1/(1 - I.hi)
    have h1 : exp x ≤ 1 / (1 - x) := Real.exp_bound_div_one_sub_of_interval hx_nonneg hx_lt_one
    have h2 : 1 / (1 - x) ≤ 1 / (1 - I.hi) := by
      apply div_le_div_of_nonneg_left
      · linarith
      · linarith
      · linarith
    simp only [Rat.cast_div, Rat.cast_one, Rat.cast_sub]
    linarith

/-- Simple lower bound: exp(x) ≥ x + 1 for all x -/
def expLowerSimple (x : ℚ) : ℚ := x + 1

/-- Simple upper bound: exp(x) ≤ 1/(1-x) for 0 ≤ x < 1 -/
def expUpperSimple (x : ℚ) : ℚ := 1 / (1 - x)

What this page does not claim

The simple bounds are the tightest possible for exp(x). The interval method works for inputs outside [0, 1). The theorem says anything about the framework's physical derivations.

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: