Dyadic Intervals

Intervals with Dyadic endpoints. These support "Outward Rounding", ensuring mathematical soundness even when we limit numerical precision.

Main definitions

• IntervalDyadic - Interval with Dyadic endpoints
• IntervalDyadic.add, mul, neg - Interval arithmetic operations
• IntervalDyadic.roundOut - Outward rounding to control precision
• IntervalDyadic.toIntervalRat - Convert to rational interval for verification

Design notes

The key feature is roundOut: after each operation, we can enforce a minimum exponent to prevent precision explosion. When rounding:

• Lower bounds are shifted down (toward -∞)
• Upper bounds are shifted up (toward +∞)

This maintains the containment invariant: the rounded interval always contains the original interval, which contains the true mathematical value.

Performance

In v1.0, Rat multiplication of 1/3 * 1/3 * ... * 1/3 (10 times) creates a denominator of 3^10 = 59049. Each operation requires GCD computation.

In v1.1, with precision = -10, the denominator stays fixed at 2^10 = 1024. The result is slightly less tight but computed significantly faster.

structure LeanCert.Core.IntervalDyadic : Type

An interval with Dyadic endpoints.

Maintains invariant: lo.toRat ≤ hi.toRat

• lo : Dyadic

  Lower bound

• hi : Dyadic

  Upper bound

• le : self.lo.toRat ≤ self.hi.toRat

  Invariant: lower bound ≤ upper bound

def LeanCert.Core.instReprIntervalDyadic.repr : IntervalDyadic → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance LeanCert.Core.instReprIntervalDyadic : Repr IntervalDyadic

Equations

• LeanCert.Core.instReprIntervalDyadic = { reprPrec := LeanCert.Core.instReprIntervalDyadic.repr }

Membership and Sets

def LeanCert.Core.IntervalDyadic.toSet (I : IntervalDyadic) : Set ℝ

The set of reals contained in this interval

Equations

• I.toSet = Set.Icc I.lo.toReal I.hi.toReal

@[instance_reducible]

instance LeanCert.Core.IntervalDyadic.instMembershipReal : Membership ℝ IntervalDyadic

Membership in a Dyadic interval

Equations

• LeanCert.Core.IntervalDyadic.instMembershipReal = { mem := fun (I : LeanCert.Core.IntervalDyadic) (x : ℝ) => ↑I.lo.toRat ≤ x ∧ x ≤ ↑I.hi.toRat }

@[simp]

theorem LeanCert.Core.IntervalDyadic.mem_def (x : ℝ) (I : IntervalDyadic) : x ∈ I ↔ ↑I.lo.toRat ≤ x ∧ x ≤ ↑I.hi.toRat

Conversion to IntervalRat

def LeanCert.Core.IntervalDyadic.toIntervalRat (I : IntervalDyadic) : IntervalRat

Convert to IntervalRat for verification with existing theorems

Equations

• I.toIntervalRat = { lo := I.lo.toRat, hi := I.hi.toRat, le := ⋯ }

theorem LeanCert.Core.IntervalDyadic.mem_toIntervalRat {x : ℝ} {I : IntervalDyadic} : x ∈ I ↔ x ∈ I.toIntervalRat

Membership is preserved by conversion to IntervalRat

Construction

def LeanCert.Core.IntervalDyadic.singleton (d : Dyadic) : IntervalDyadic

Create a singleton interval from a Dyadic

Equations

• LeanCert.Core.IntervalDyadic.singleton d = { lo := d, hi := d, le := ⋯ }

theorem LeanCert.Core.IntervalDyadic.mem_singleton (d : Dyadic) : ↑d.toRat ∈ singleton d

A Dyadic value is in its singleton interval

@[instance_reducible]

instance LeanCert.Core.IntervalDyadic.instInhabited : Inhabited IntervalDyadic

Default interval [0, 0]

Equations

• LeanCert.Core.IntervalDyadic.instInhabited = { default := LeanCert.Core.IntervalDyadic.singleton LeanCert.Core.Dyadic.zero }

def LeanCert.Core.IntervalDyadic.mk? (lo hi : Dyadic) : Option IntervalDyadic

Create an interval, checking the invariant

Equations

• LeanCert.Core.IntervalDyadic.mk? lo hi = if h : lo.toRat ≤ hi.toRat then some { lo := lo, hi := hi, le := h } else none

def LeanCert.Core.IntervalDyadic.width (I : IntervalDyadic) : Dyadic

The width of an interval

Equations

• I.width = I.hi.sub I.lo

@[simp]

theorem LeanCert.Core.IntervalDyadic.width_toRat (I : IntervalDyadic) : I.width.toRat = I.hi.toRat - I.lo.toRat

The dyadic width denotes endpoint subtraction exactly.

def LeanCert.Core.IntervalDyadic.midpoint (I : IntervalDyadic) : Dyadic

Exact midpoint of a dyadic interval.

Dyadics are closed under division by two, so midpoint construction must lower the exponent rather than shift (and potentially round) the mantissa.

Equations

• I.midpoint = (I.lo.add I.hi).scale2 (-1)

@[simp]

theorem LeanCert.Core.IntervalDyadic.midpoint_toRat (I : IntervalDyadic) : I.midpoint.toRat = (I.lo.toRat + I.hi.toRat) / 2

The dyadic midpoint denotes the ordinary rational midpoint exactly.

theorem LeanCert.Core.IntervalDyadic.lo_le_midpoint (I : IntervalDyadic) : I.lo.toRat ≤ I.midpoint.toRat

The lower endpoint is at most the exact midpoint.

theorem LeanCert.Core.IntervalDyadic.midpoint_le_hi (I : IntervalDyadic) : I.midpoint.toRat ≤ I.hi.toRat

The exact midpoint is at most the upper endpoint.

def LeanCert.Core.IntervalDyadic.bisect (I : IntervalDyadic) : IntervalDyadic × IntervalDyadic

Split a dyadic interval into two exact closed halves.

Equations

• I.bisect = ({ lo := I.lo, hi := I.midpoint, le := ⋯ }, { lo := I.midpoint, hi := I.hi, le := ⋯ })

theorem LeanCert.Core.IntervalDyadic.mem_bisect_left {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (hm : x ≤ ↑I.midpoint.toRat) : x ∈ I.bisect.1

A point in the original interval and left of the midpoint is in the left half.

theorem LeanCert.Core.IntervalDyadic.mem_bisect_right {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (hm : ↑I.midpoint.toRat ≤ x) : x ∈ I.bisect.2

A point in the original interval and right of the midpoint is in the right half.

theorem LeanCert.Core.IntervalDyadic.mem_of_mem_bisect_left {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I.bisect.1) : x ∈ I

Membership in the left half implies membership in the original interval.

theorem LeanCert.Core.IntervalDyadic.mem_of_mem_bisect_right {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I.bisect.2) : x ∈ I

Membership in the right half implies membership in the original interval.

theorem LeanCert.Core.IntervalDyadic.mem_bisect_or {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) : x ∈ I.bisect.1 ∨ x ∈ I.bisect.2

The two closed halves cover the original interval, including their shared seam.

theorem LeanCert.Core.IntervalDyadic.midpoint_mem_bisect_both (I : IntervalDyadic) : ↑I.midpoint.toRat ∈ I.bisect.1 ∧ ↑I.midpoint.toRat ∈ I.bisect.2

Both closed halves contain the midpoint seam.

theorem LeanCert.Core.IntervalDyadic.bisect_intersection (I : IntervalDyadic) : I.bisect.1.toSet ∩ I.bisect.2.toSet = {I.midpoint.toReal}

The overlap of the two closed children is exactly their midpoint seam.

theorem LeanCert.Core.IntervalDyadic.bisect_left_width_toRat (I : IntervalDyadic) : I.bisect.1.width.toRat = I.width.toRat / 2

The left child has exactly half the semantic width of its parent.

theorem LeanCert.Core.IntervalDyadic.bisect_right_width_toRat (I : IntervalDyadic) : I.bisect.2.width.toRat = I.width.toRat / 2

The right child has exactly half the semantic width of its parent.

Outward Rounding

def LeanCert.Core.IntervalDyadic.roundOut (I : IntervalDyadic) (minExp : ℤ) : IntervalDyadic

Outward rounding: enforces a maximum precision (minimum exponent).

This is the key operation for preventing precision explosion. minExp is the minimum allowed exponent (higher = coarser precision).

For example, minExp = -10 ensures all values are multiples of 2^(-10) ≈ 0.001.

Equations

• I.roundOut minExp = { lo := I.lo.shiftDown minExp, hi := I.hi.shiftUp minExp, le := ⋯ }

theorem LeanCert.Core.IntervalDyadic.roundOut_contains {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (minExp : ℤ) : x ∈ I.roundOut minExp

roundOut produces an interval containing the original

Interval Negation

def LeanCert.Core.IntervalDyadic.neg (I : IntervalDyadic) : IntervalDyadic

Negate an interval

Equations

• I.neg = { lo := I.hi.neg, hi := I.lo.neg, le := ⋯ }

theorem LeanCert.Core.IntervalDyadic.mem_neg {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) : -x ∈ I.neg

FTIA for negation

Interval Addition

def LeanCert.Core.IntervalDyadic.add (I J : IntervalDyadic) : IntervalDyadic

Add two intervals

Equations

• I.add J = { lo := I.lo.add J.lo, hi := I.hi.add J.hi, le := ⋯ }

theorem LeanCert.Core.IntervalDyadic.mem_add {x y : ℝ} {I J : IntervalDyadic} (hx : x ∈ I) (hy : y ∈ J) : x + y ∈ I.add J

FTIA for addition

def LeanCert.Core.IntervalDyadic.addRounded (I J : IntervalDyadic) (prec : ℤ := -53) : IntervalDyadic

Add with precision control

Equations

• I.addRounded J prec = (I.add J).roundOut prec

Interval Subtraction

def LeanCert.Core.IntervalDyadic.sub (I J : IntervalDyadic) : IntervalDyadic

Subtract two intervals

Equations

• I.sub J = I.add J.neg

theorem LeanCert.Core.IntervalDyadic.mem_sub {x y : ℝ} {I J : IntervalDyadic} (hx : x ∈ I) (hy : y ∈ J) : x - y ∈ I.sub J

FTIA for subtraction

Interval Multiplication

def LeanCert.Core.IntervalDyadic.mul (I J : IntervalDyadic) : IntervalDyadic

Multiply two intervals.

Uses min/max of all four endpoint products to handle signs correctly. This is the exact multiplication - mantissas may grow. Use mulRounded or mulNormalized for controlled precision.

Correctness: For x ∈ [a,b] and y ∈ [c,d], the product x*y lies in the interval [min(ac,ad,bc,bd), max(ac,ad,bc,bd)].

Equations

• I.mul J = { lo := (I.lo.mul J.lo).min4 (I.lo.mul J.hi) (I.hi.mul J.lo) (I.hi.mul J.hi), hi := (I.lo.mul J.lo).max4 (I.lo.mul J.hi) (I.hi.mul J.lo) (I.hi.mul J.hi), le := ⋯ }

theorem LeanCert.Core.IntervalDyadic.mem_mul {x y : ℝ} {I J : IntervalDyadic} (hx : x ∈ I) (hy : y ∈ J) : x * y ∈ I.mul J

FTIA for multiplication

theorem LeanCert.Core.IntervalDyadic.mem_mulFast {x y : ℝ} {I J : IntervalDyadic} (hx : x ∈ I) (hy : y ∈ J) : x * y ∈ LeanCert.Core.IntervalDyadic.mulFast✝ I J

mulFast preserves the containment property of mul. This is retained as documentation and a future audited optimization hook; production certificate checking currently uses mul directly.

def LeanCert.Core.IntervalDyadic.mulRounded (I J : IntervalDyadic) (prec : ℤ := -53) : IntervalDyadic

Multiply with precision control (outward rounding)

Equations

• I.mulRounded J prec = (I.mul J).roundOut prec

def LeanCert.Core.IntervalDyadic.mulNormalized (I J : IntervalDyadic) (maxBits : ℕ := 256) : IntervalDyadic

Multiply with mantissa normalization (prevents bit explosion)

Equations

• I.mulNormalized J maxBits = { lo := (I.mul J).lo.normalizeDown maxBits, hi := (I.mul J).hi.normalizeUp maxBits, le := ⋯ }

Interval Scaling

def LeanCert.Core.IntervalDyadic.scale (I : IntervalDyadic) (c : Dyadic) : IntervalDyadic

Scale an interval by a constant Dyadic

Equations

• I.scale c = if hc : LeanCert.Core.Dyadic.zero.le c = true then { lo := I.lo.mul c, hi := I.hi.mul c, le := ⋯ } else { lo := I.hi.mul c, hi := I.lo.mul c, le := ⋯ }

def LeanCert.Core.IntervalDyadic.scale2 (I : IntervalDyadic) (n : ℤ) : IntervalDyadic

Scale by a power of 2 (very efficient: just adjusts exponents)

Equations

• I.scale2 n = { lo := I.lo.scale2 n, hi := I.hi.scale2 n, le := ⋯ }

Square Root

def LeanCert.Core.IntervalDyadic.sqrt (I : IntervalDyadic) (_prec : ℤ := -53) : IntervalDyadic

Square root of an interval. Returns a conservative bound [0, max(hi, 1)]. This is sound because:

• sqrt(x) = 0 for x < 0 (by definition in Mathlib)
• sqrt(x) ≥ 0 for all x
• sqrt(x) ≤ max(x, 1) for x ≥ 0 Therefore for any x ∈ [lo, hi], sqrt(x) ∈ [0, max(hi, 1)].

Equations

• I.sqrt _prec = { lo := LeanCert.Core.Dyadic.zero, hi := I.hi.max (LeanCert.Core.Dyadic.ofInt 1), le := ⋯ }

theorem LeanCert.Core.IntervalDyadic.mem_sqrt {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (hx_nn : 0 ≤ x) (prec : ℤ) : √x ∈ I.sqrt prec

Soundness of interval sqrt: if x ∈ I, x ≥ 0, then Real.sqrt x ∈ sqrt I

theorem LeanCert.Core.IntervalDyadic.mem_sqrt' {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) (prec : ℤ) : √x ∈ I.sqrt prec

General soundness of interval sqrt for any real input. Handles both non-negative inputs and negative inputs (where Real.sqrt returns 0).

Comparison and Containment

def LeanCert.Core.IntervalDyadic.containsZero (I : IntervalDyadic) : Bool

Check if interval contains zero

Equations

• I.containsZero = (I.lo.le LeanCert.Core.Dyadic.zero && LeanCert.Core.Dyadic.zero.le I.hi)

def LeanCert.Core.IntervalDyadic.isPositive (I : IntervalDyadic) : Bool

Check if entire interval is positive

Equations

• I.isPositive = LeanCert.Core.Dyadic.zero.lt I.lo

def LeanCert.Core.IntervalDyadic.isNegative (I : IntervalDyadic) : Bool

Check if entire interval is negative

Equations

• I.isNegative = I.hi.lt LeanCert.Core.Dyadic.zero

def LeanCert.Core.IntervalDyadic.subset (I J : IntervalDyadic) : Bool

Check if I ⊆ J

Equations

• I.subset J = (J.lo.le I.lo && I.hi.le J.hi)

def LeanCert.Core.IntervalDyadic.upperBoundedBy (I : IntervalDyadic) (q : ℚ) : Bool

Check if the upper bound is ≤ a rational

Equations

• I.upperBoundedBy q = decide (I.hi.toRat ≤ q)

def LeanCert.Core.IntervalDyadic.lowerBoundedBy (I : IntervalDyadic) (q : ℚ) : Bool

Check if a rational is ≤ the lower bound

Equations

• I.lowerBoundedBy q = decide (q ≤ I.lo.toRat)

theorem LeanCert.Core.IntervalDyadic.le_hi_of_mem {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) : x ≤ ↑I.hi.toRat

Upper bound extraction from membership

theorem LeanCert.Core.IntervalDyadic.lo_le_of_mem {x : ℝ} {I : IntervalDyadic} (hx : x ∈ I) : ↑I.lo.toRat ≤ x

Lower bound extraction from membership

theorem LeanCert.Core.IntervalDyadic.upperBoundedBy_spec {I : IntervalDyadic} {q : ℚ} (h : I.upperBoundedBy q = true) : ↑I.hi.toRat ≤ ↑q

What upperBoundedBy means: the interval's hi endpoint is ≤ q

theorem LeanCert.Core.IntervalDyadic.lowerBoundedBy_spec {I : IntervalDyadic} {q : ℚ} (h : I.lowerBoundedBy q = true) : ↑q ≤ ↑I.lo.toRat

What lowerBoundedBy means: q is ≤ the interval's lo endpoint

Helper for Transcendentals

def LeanCert.Core.IntervalDyadic.ofIntervalRat (I : IntervalRat) (prec : ℤ := -53) : IntervalDyadic

Convert from IntervalRat (for transcendental results)

Equations

• One or more equations did not get rendered due to their size.

theorem LeanCert.Core.IntervalDyadic.mem_ofIntervalRat {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (prec : ℤ) (hprec : prec ≤ 0 := by norm_num) : x ∈ ofIntervalRat I prec

If x ∈ IntervalRat I, then x ∈ ofIntervalRat I prec (outward rounding preserves membership). Requires precision ≤ 0 (e.g. -53).