QInterval — Rational Interval Arithmetic with ℝ Containment

Closed intervals [lo, hi] over ℚ, with proofs that arithmetic operations preserve ℝ containment. This is the foundation for the rsa_decide tactic:

1. Reify an ℝ expression into a tree of QInterval operations
2. Evaluate the tree to get a concrete [lo, hi] (computable ℚ)
3. Check separation b.hi < a.lo (decidable on ℚ)
4. Conclude a > b on ℝ via gt_of_separated

structure Linglib.Interval.QInterval : Type

A closed rational interval [lo, hi].

• lo : ℚ
• hi : ℚ
• valid : self.lo ≤ self.hi

def Linglib.Interval.instReprQInterval.repr : QInterval → ℕ → Std.Format

Equations

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

instance Linglib.Interval.instReprQInterval : Repr QInterval

Equations

• Linglib.Interval.instReprQInterval = { reprPrec := Linglib.Interval.instReprQInterval.repr }

def Linglib.Interval.QInterval.containsReal (I : QInterval) (x : ℝ) : Prop

The interval contains a real number x: lo ≤ x ≤ hi (via ℚ → ℝ cast).

Equations

• I.containsReal x = (↑I.lo ≤ x ∧ x ≤ ↑I.hi)

def Linglib.Interval.QInterval.exact (q : ℚ) : QInterval

Zero-width interval [q, q].

Equations

• Linglib.Interval.QInterval.exact q = { lo := q, hi := q, valid := ⋯ }

theorem Linglib.Interval.QInterval.exact_containsReal (q : ℚ) : (exact q).containsReal ↑q

theorem Linglib.Interval.QInterval.exact_zero_containsReal : (exact 0).containsReal 0

Containment for (0 : ℝ). Uses the literal 0 so the proof type mentions @OfNat.ofNat ℝ 0 _ (= @Zero.zero ℝ _), matching expressions directly.

theorem Linglib.Interval.QInterval.exact_one_containsReal : (exact 1).containsReal 1

Containment for (1 : ℝ). Uses the literal 1 so the proof type mentions @OfNat.ofNat ℝ 1 _ (= @One.one ℝ _), avoiding the Nat.cast 1 = 0 + 1 mismatch that breaks nested proof terms.

theorem Linglib.Interval.QInterval.exact_natCast_containsReal (n : ℕ) : (exact ↑n).containsReal ↑n

Containment for natural number literals ≥ 2 cast via Nat.cast. For n ≥ 2, @OfNat.ofNat ℝ n _ is definitionally equal to @Nat.cast ℝ _ n (via Mathlib's instOfNat). For n = 0, 1, use exact_zero_containsReal / exact_one_containsReal instead (since Nat.cast 1 ≢ OfNat.ofNat 1).

def Linglib.Interval.QInterval.add (a b : QInterval) : QInterval

Interval addition: [a.lo + b.lo, a.hi + b.hi].

Equations

• a.add b = { lo := a.lo + b.lo, hi := a.hi + b.hi, valid := ⋯ }

theorem Linglib.Interval.QInterval.add_containsReal {a b : QInterval} {x y : ℝ} (hx : a.containsReal x) (hy : b.containsReal y) : (a.add b).containsReal (x + y)

def Linglib.Interval.QInterval.neg (a : QInterval) : QInterval

Interval negation: [-hi, -lo].

Equations

• a.neg = { lo := -a.hi, hi := -a.lo, valid := ⋯ }

theorem Linglib.Interval.QInterval.neg_containsReal {a : QInterval} {x : ℝ} (hx : a.containsReal x) : a.neg.containsReal (-x)

def Linglib.Interval.QInterval.sub (a b : QInterval) : QInterval

Interval subtraction: a - b = a + (-b).

Equations

• a.sub b = a.add b.neg

theorem Linglib.Interval.QInterval.sub_containsReal {a b : QInterval} {x y : ℝ} (hx : a.containsReal x) (hy : b.containsReal y) : (a.sub b).containsReal (x - y)

def Linglib.Interval.QInterval.mulNonneg (a b : QInterval) (ha : 0 ≤ a.lo) (hb : 0 ≤ b.lo) : QInterval

Multiplication for nonneg intervals: [a.lob.lo, a.hib.hi].

Equations

• a.mulNonneg b ha hb = { lo := a.lo * b.lo, hi := a.hi * b.hi, valid := ⋯ }

theorem Linglib.Interval.QInterval.mulNonneg_containsReal {a b : QInterval} {x y : ℝ} (ha : 0 ≤ a.lo) (hb : 0 ≤ b.lo) (hx : a.containsReal x) (hy : b.containsReal y) : (a.mulNonneg b ha hb).containsReal (x * y)

def Linglib.Interval.QInterval.divPos (a b : QInterval) (ha : 0 ≤ a.lo) (hb_pos : 0 < b.lo) : QInterval

Division of nonneg by positive: [a.lo/b.hi, a.hi/b.lo]. Requires 0 ≤ a.lo for monotonicity.

Equations

• a.divPos b ha hb_pos = { lo := a.lo / b.hi, hi := a.hi / b.lo, valid := ⋯ }

theorem Linglib.Interval.QInterval.divPos_containsReal {a b : QInterval} {x y : ℝ} (ha : 0 ≤ a.lo) (hb_pos : 0 < b.lo) (hx : a.containsReal x) (hy : b.containsReal y) : (a.divPos b ha hb_pos).containsReal (x / y)

def Linglib.Interval.QInterval.mul (a b : QInterval) : QInterval

General interval multiplication via 4-corner method. For intervals [a, b] and [c, d], the product interval is [min(ac, ad, bc, bd), max(ac, ad, bc, bd)]. Handles arbitrary signs (unlike mulNonneg which requires both nonneg).

Equations

• a.mul b = { lo := min (min (a.lo * b.lo) (a.lo * b.hi)) (min (a.hi * b.lo) (a.hi * b.hi)), hi := max (max (a.lo * b.lo) (a.lo * b.hi)) (max (a.hi * b.lo) (a.hi * b.hi)), valid := ⋯ }

theorem Linglib.Interval.QInterval.mul_containsReal {a b : QInterval} {x y : ℝ} (hx : a.containsReal x) (hy : b.containsReal y) : (a.mul b).containsReal (x * y)

Containment for general interval multiplication. For a.lo ≤ x ≤ a.hi and b.lo ≤ y ≤ b.hi, x·y lies between min(corners) and max(corners) since extrema of a bilinear function on a rectangle occur at corners.

def Linglib.Interval.QInterval.scaleNonneg (q : ℚ) (a : QInterval) (hq : 0 ≤ q) : QInterval

Scale interval by a nonneg rational: [qa.lo, qa.hi].

Equations

• Linglib.Interval.QInterval.scaleNonneg q a hq = { lo := q * a.lo, hi := q * a.hi, valid := ⋯ }

theorem Linglib.Interval.QInterval.scaleNonneg_containsReal {q : ℚ} {a : QInterval} {x : ℝ} (hq : 0 ≤ q) (hx : a.containsReal x) : (scaleNonneg q a hq).containsReal (↑q * x)

def Linglib.Interval.QInterval.separated (a b : QInterval) : Bool

Check that a.lo > b.hi (decidable on ℚ).

Equations

• a.separated b = decide (b.hi < a.lo)

theorem Linglib.Interval.QInterval.gt_of_separated {a b : QInterval} {x y : ℝ} (hx : a.containsReal x) (hy : b.containsReal y) (hsep : b.hi < a.lo) : x > y

Key theorem: interval separation implies ℝ strict ordering.

theorem Linglib.Interval.QInterval.le_of_separated {a b : QInterval} {x y : ℝ} (hx : a.containsReal x) (hy : b.containsReal y) (hsep : a.hi ≤ b.lo) : x ≤ y

If a.hi ≤ b.lo, then x ≤ y. Dual of gt_of_separated.

theorem Linglib.Interval.QInterval.ge_of_le_lo {a b : QInterval} {x y : ℝ} (hx : a.containsReal x) (hy : b.containsReal y) (hge : b.hi ≤ a.lo) : x ≥ y

Interval separation implies ≥.

theorem Linglib.Interval.QInterval.eq_of_exact {q : ℚ} {x y : ℝ} (hx : (exact q).containsReal x) (hy : (exact q).containsReal y) : x = y

Two exact intervals at the same point imply equality.

theorem Linglib.Interval.QInterval.ite_neg_containsReal {c : Prop} [Decidable c] {I : QInterval} {x y : ℝ} (hc : ¬c) (hy : I.containsReal y) : I.containsReal (if c then x else y)

If the condition is known false, take the else branch.

theorem Linglib.Interval.QInterval.ite_pos_containsReal {c : Prop} [Decidable c] {I : QInterval} {x y : ℝ} (hc : c) (hx : I.containsReal x) : I.containsReal (if c then x else y)

If the condition is known true, take the then branch.

theorem Linglib.Interval.QInterval.decidable_rec_pos_containsReal {p : Prop} {inst : Decidable p} {I : QInterval} (f : ¬p → ℝ) (g : p → ℝ) (hc : p) (hx : I.containsReal (g hc)) : I.containsReal (Decidable.rec f g inst)

Decidable.rec with condition known true → take the isTrue branch. Handles the case where ite has been unfolded to Decidable.rec by whnf.

theorem Linglib.Interval.QInterval.decidable_rec_neg_containsReal {p : Prop} {inst : Decidable p} {I : QInterval} (f : ¬p → ℝ) (g : p → ℝ) (hnc : ¬p) (hy : I.containsReal (f hnc)) : I.containsReal (Decidable.rec f g inst)

Decidable.rec with condition known false → take the isFalse branch.

theorem Linglib.Interval.QInterval.pos_of_lo_pos {a : QInterval} {x : ℝ} (hx : a.containsReal x) (hlo : 0 < a.lo) : 0 < x

If an interval has positive lower bound, the contained value is positive.

theorem Linglib.Interval.QInterval.ne_zero_of_lo_pos {a : QInterval} {x : ℝ} (hx : a.containsReal x) (hlo : 0 < a.lo) : x ≠ 0

If an interval has positive lower bound, the contained value is nonzero.

theorem Linglib.Interval.QInterval.eq_zero_of_contained_nonneg {I : QInterval} {x : ℝ} (hx : I.containsReal x) (hlo : 0 ≤ I.lo) (hhi : I.hi ≤ 0) : x = 0

If an interval has nonneg lower bound and nonpos upper bound, the value is zero. Used by the tactic to prove x = 0 when the interval is [0, 0].

def Linglib.Interval.QInterval.invPos (a : QInterval) (ha : 0 < a.lo) : QInterval

Inverse of a positive interval: [1/hi, 1/lo].

Equations

• a.invPos ha = { lo := 1 / a.hi, hi := 1 / a.lo, valid := ⋯ }

theorem Linglib.Interval.QInterval.invPos_containsReal {a : QInterval} {x : ℝ} (ha : 0 < a.lo) (hx : a.containsReal x) : (a.invPos ha).containsReal x⁻¹

theorem Linglib.Interval.QInterval.eq_zero_of_bounds {a : QInterval} {x : ℝ} (hx : a.containsReal x) (hlo : a.lo = 0) (hhi : a.hi = 0) : x = 0

If an interval has lo = 0 and hi = 0, the contained value equals zero.

theorem Linglib.Interval.QInterval.zero_mul_containsReal {a : QInterval} {x y : ℝ} (hx : a.containsReal x) (hlo : a.lo = 0) (hhi : a.hi = 0) : (exact 0).containsReal (x * y)

If x is in a zero interval, x * y is in the zero interval.

theorem Linglib.Interval.QInterval.mul_zero_containsReal {b : QInterval} {x y : ℝ} (hy : b.containsReal y) (hlo : b.lo = 0) (hhi : b.hi = 0) : (exact 0).containsReal (x * y)

If y is in a zero interval, x * y is in the zero interval.

theorem Linglib.Interval.QInterval.zero_div_containsReal {a : QInterval} {x y : ℝ} (hx : a.containsReal x) (hlo : a.lo = 0) (hhi : a.hi = 0) : (exact 0).containsReal (x / y)

If x is in a zero interval, x / y is in the zero interval.

theorem Linglib.Interval.QInterval.containsReal_of_eq {I : QInterval} {x y : ℝ} (h : y = x) (hx : I.containsReal x) : I.containsReal y

Transport containment along a real-valued equality. If y = x and the interval contains x, it contains y.

def Linglib.Interval.QInterval.rpowNat (a : QInterval) (n : ℕ) (ha : 0 ≤ a.lo) : QInterval

Interval for nonneg base raised to a natural power: [lo^n, hi^n].

Equations

• a.rpowNat n ha = { lo := a.lo ^ n, hi := a.hi ^ n, valid := ⋯ }

theorem Linglib.Interval.QInterval.powNat_containsReal {a : QInterval} {x : ℝ} (n : ℕ) (ha : 0 ≤ a.lo) (hx : a.containsReal x) : (a.rpowNat n ha).containsReal (x ^ n)

Containment for x ^ n (nat power) with nonneg base.

def Linglib.Interval.QInterval.powNat (iv : QInterval) (n : ℕ) : QInterval

Raise an interval to a natural power. No proof obligation — checks nonneg at runtime and uses rpowNat for sound computation, fallback otherwise.

Equations

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

theorem Linglib.Interval.QInterval.eq_zero_of_containsReal {I : QInterval} {x : ℝ} (h : I.containsReal x) (hlo : I.lo = 0) (hhi : I.hi = 0) : x = 0

If a real value is contained in an interval with lo = 0 and hi = 0, the value equals zero.

def Linglib.Interval.QInterval.maxBits : ℕ

Maximum bit length for rational numerator/denominator. 64 bits ≈ 19 decimal digits, enough precision for RSA comparisons.

Equations

• Linglib.Interval.QInterval.maxBits = 64

def Linglib.Interval.QInterval.coarsen (I : QInterval) (bits : ℕ := maxBits) : QInterval

Widen an interval to bounded-precision rationals. Sound: only makes the interval wider, so containment is preserved.

Equations

• I.coarsen bits = { lo := Linglib.Interval.QInterval.truncDown✝ I.lo bits, hi := Linglib.Interval.QInterval.truncUp✝ I.hi bits, valid := ⋯ }

theorem Linglib.Interval.QInterval.coarsen_containsReal {I : QInterval} {x : ℝ} (bits : ℕ) (hx : I.containsReal x) : (I.coarsen bits).containsReal x