Numerics Interval Basic

Rigorous interval arithmetic

Interval arithmetic is a way of doing calculations with ranges of values instead of single numbers. Instead of asking what sin(1) equals, you ask what interval is guaranteed to contain sin(1). Each operation on intervals produces a new interval that is guaranteed to contain the result of applying that operation to any point inside the original intervals. The cost is that the answer is a range, not a point, but the benefit is that the range is a certificate: if the interval is narrow, you know the true value is close to the midpoint.

The idea dates to the late 1950s, when Ramon E. Moore began developing it as a tool for error analysis in numerical computation. Its modern use is in verified numerical methods, where a computer program must prove, not just suggest, that its output is correct. In such methods, a floating-point approximation is not enough, because rounding errors can accumulate invisibly. Interval arithmetic makes the rounding error explicit: every operation widens the interval by at least the amount of the uncertainty, and the final interval is a rigorous enclosure of the true value.

The basic operations follow simple rules. For addition, the lower endpoint of the sum is the sum of the lower endpoints, and the upper endpoint is the sum of the upper endpoints. For subtraction, the lower endpoint of the difference is the lower endpoint of the first minus the upper endpoint of the second, and the upper endpoint is the upper endpoint of the first minus the lower endpoint of the second. Negation swaps the endpoints and flips their signs. Multiplication is more delicate: for positive intervals, the product's lower endpoint is the product of the lower endpoints and its upper endpoint is the product of the upper endpoints, but in general you must consider all four pairwise products.

In Recognition Science, the framework's machine-checked library of formal theorems contains a module, numerics interval basic, that implements this arithmetic with rational endpoints. A rational number is a fraction of two integers, so the computer can represent it exactly, with no rounding. The module defines an interval as a pair of rational numbers, a lower bound and an upper bound, together with a proof that the lower bound is no greater than the upper bound. It then proves, for each operation, that the resulting interval contains the true result.

The key theorems are the containment lemmas. For addition, the theorem states that if x is in interval I and y is in interval J, then x plus y is in I plus J. The analogous statements hold for subtraction, negation, multiplication by a positive rational, and powers. Each is a formal proof, checked by the machine, that the interval operation is sound: it never loses a possible value. The module also provides a way to construct a point interval, where the lower and upper bounds are equal, and to compare an interval's bounds against a rational number to extract inequalities about any real number the interval contains.

What this establishes in plain language is that the framework has a trustworthy foundation for computing bounds on transcendental functions. Because the endpoints are rational, every bound is exact in the sense that it is a fraction of integers, not a rounded decimal. The theorems guarantee that if you start with intervals that contain your inputs, every interval you compute contains the true output. This is the first step toward verified numerical results in the framework: a way to compute that carries its own proof of correctness.

/-- A closed interval with rational endpoints. -/
structure Interval where
  lo : ℚ
  hi : ℚ
  valid : lo ≤ hi
  deriving DecidableEq

theorem add_contains_add {x y : ℝ} {I J : Interval}
    (hx : I.contains x) (hy : J.contains y) : (I + J).contains (x + y) := by
  constructor
  · simp only [add_lo, Rat.cast_add]
    exact add_le_add hx.1 hy.1
  · simp only [add_hi, Rat.cast_add]
    exact add_le_add hx.2 hy.2

theorem sub_contains_sub {x y : ℝ} {I J : Interval}
    (hx : I.contains x) (hy : J.contains y) : (I - J).contains (x - y) := by
  constructor
  · simp only [sub_lo, Rat.cast_sub]
    exact sub_le_sub hx.1 hy.2
  · simp only [sub_hi, Rat.cast_sub]
    exact sub_le_sub hx.2 hy.1

theorem neg_contains_neg {x : ℝ} {I : Interval} (hx : I.contains x) : (-I).contains (-x) := by
  constructor
  · simp only [neg_lo, Rat.cast_neg]
    exact neg_le_neg hx.2
  · simp only [neg_hi, Rat.cast_neg]
    exact neg_le_neg hx.1

theorem smulPos_contains_smul {q : ℚ} {x : ℝ} {I : Interval}
    (hq : 0 < q) (hx : I.contains x) : (smulPos q I hq).contains ((q : ℝ) * x) := by
  have hq_pos : (0 : ℝ) < q := by exact_mod_cast hq
  constructor
  · simp only [smulPos, Rat.cast_mul]
    exact mul_le_mul_of_nonneg_left hx.1 (le_of_lt hq_pos)
  · simp only [smulPos, Rat.cast_mul]
    exact mul_le_mul_of_nonneg_left hx.2 (le_of_lt hq_pos)

theorem npow_contains_pow {x : ℝ} {I : Interval} {n : ℕ}
    (hIpos : 0 < I.lo) (hx : I.contains x) : (npow I n hIpos).contains (x ^ n) := by
  have hIlo_pos : (0 : ℝ) < I.lo := by exact_mod_cast hIpos
  have hx_pos : 0 < x := lt_of_lt_of_le hIlo_pos hx.1
  constructor
  · simp only [npow, Rat.cast_pow]
    exact pow_le_pow_left₀ (le_of_lt hIlo_pos) hx.1 n
  · simp only [npow, Rat.cast_pow]
    exact pow_le_pow_left₀ (le_of_lt hx_pos) hx.2 n

/-- Point interval containing a single rational -/
def point (q : ℚ) : Interval where
  lo := q
  hi := q
  valid := le_refl q

What this page does not claim

This module does not provide a complete implementation of transcendental functions. The containment theorems do not guarantee that the computed interval is the narrowest possible interval containing the true result. The framework does not claim that interval arithmetic eliminates all numerical error, only that it makes the error explicit and bounded.

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