Bounds — Rational Interval Arithmetic for the rsa_predict Backend

Closed intervals [lo, hi] over ℚ, with proofs that arithmetic and transcendental operations preserve ℝ containment. This is the numeric foundation for the rsa_predict 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

Layered structure

The file is organized in dependency order:

• QInterval — the core type and exact arithmetic (add, sub, mul, divPos, invPos, powNat, rpowNat), separation predicate, and rational coarsening (truncDown/truncUp/coarsen) that bounds bit growth across long products.
• PadeExp — [4/4] Padé approximant for Real.exp on [-1, 1] with argument reduction by repeated squaring, giving expPoint/expInterval with relative error < 1/4000000.
• LogInterval — Real.log for positive rationals via 50-step bisection against expPoint, with bracket bits proportional to log q. Includes a log 0 fall-through.
• SqrtInterval — √x = exp(log x / 2) for positive intervals, used by Hellinger-distance RSA models (@cite{herbstritt-franke-2019}).
• rpow specials — rpowNat_containsReal (real-exponent bridge for QInterval.rpowNat), rpowZero, rpowOne_containsReal for the dominant RSA case (α : ℕ).

All transcendental routines deliberately stop at containsReal rather than proving exact bounds: the rsa_predict tactic only needs lo ≤ ⟦e⟧ ≤ hi.

structure Interval.QInterval : Type

A closed rational interval [lo, hi].

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

@[implicit_reducible]

instance Interval.instReprQInterval : Repr QInterval

Equations

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

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

Equations

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

def 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 Interval.QInterval.exact (q : ℚ) : QInterval

Zero-width interval [q, q].

Equations

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

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

theorem 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 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 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 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 Interval.QInterval.add_containsReal {a b : QInterval} {x y : ℝ} (hx : a.containsReal x) (hy : b.containsReal y) : (a.add b).containsReal (x + y)

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

Interval negation: [-hi, -lo].

Equations

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

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

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

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

Equations

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

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

def 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 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 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 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 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 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 Interval.QInterval.scaleNonneg (q : ℚ) (a : QInterval) (hq : 0 ≤ q) : QInterval

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

Equations

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

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

def 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 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 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 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 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 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 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 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 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 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 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 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 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 Interval.QInterval.invPos_containsReal {a : QInterval} {x : ℝ} (ha : 0 < a.lo) (hx : a.containsReal x) : (a.invPos ha).containsReal x⁻¹

theorem 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 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 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 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 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 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 Interval.QInterval.maxBits : ℕ

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

Equations

• Interval.QInterval.maxBits = 64

def 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 := Interval.QInterval.truncDown✝ I.lo bits, hi := Interval.QInterval.truncUp✝ I.hi bits, valid := ⋯ }

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

def Interval.padeNum (x : ℚ) : ℚ

Padé [4/4] numerator: 1 + x/2 + 3x²/28 + x³/84 + x⁴/1680 (Horner form).

Equations

• Interval.padeNum x = 1 + x * (1 / 2 + x * (3 / 28 + x * (1 / 84 + x * (1 / 1680))))

def Interval.padeDen (x : ℚ) : ℚ

Padé [4/4] denominator: padeNum(-x).

Equations

• Interval.padeDen x = Interval.padeNum (-x)

def Interval.padeExp (x : ℚ) : ℚ

Padé [4/4] approximant: padeNum(x) / padeDen(x).

Equations

• Interval.padeExp x = Interval.padeNum x / Interval.padeDen x

def Interval.padeErrorBound : ℚ

Conservative error bound for Padé [4/4] on [-1, 1]. True error is ~4.3×10⁻⁸; this bound gives 2.3× safety margin.

Equations

• Interval.padeErrorBound = 1 / 4000000

theorem Interval.pade_error_bound (q : ℚ) (hq_lo : -1 ≤ q) (hq_hi : q ≤ 1) (hden_pos : 0 < padeDen q) : |Real.exp ↑q - ↑(padeExp q)| ≤ ↑padeErrorBound

The Padé [4/4] approximant is within padeErrorBound of exp on [-1, 1].

Proof via triangle inequality: |exp(q) - P(q)/Q(q)| ≤ |exp(q) - T₁₀(q)| + |T₁₀(q) - P(q)/Q(q)| where T₁₀ is the degree-10 Taylor polynomial. The first term is bounded by Real.exp_bound with n = 11 (≤ 1/36590400 ≈ 2.73×10⁻⁸). The second term equals |T₁₀·Q - P|/Q; the numerator is a polynomial with terms only at degrees 9-14 (Padé matching property), bounded by 187/2032128000 ≈ 9.2×10⁻⁸ via coefficient sum, and Q ≥ 143/240.

def Interval.reductionSteps (q : ℚ) : ℕ

Number of halvings needed so q / 2^k ∈ [-1, 1].

Equations

• Interval.reductionSteps q = if q.num.natAbs ≤ q.den then 0 else Nat.log 2 q.num.natAbs - Nat.log 2 q.den + 1

def Interval.repeatedSq (I : QInterval) (n : ℕ) (h : 0 ≤ I.lo) : QInterval

Repeated squaring of a nonneg interval. Squares I a total of n times: repeatedSq I 0 = I, repeatedSq I (n+1) = (repeatedSq I n)².

Equations

• Interval.repeatedSq I n h = ↑(Interval.repeatedSqCore✝ I n h)

theorem Interval.repeatedSq_nonneg (I : QInterval) (n : ℕ) (h : 0 ≤ I.lo) : 0 ≤ (repeatedSq I n h).lo

def Interval.expPoint (q : ℚ) : QInterval

Point interval containing exp(q) for arbitrary rational q.

Strategy: reduce q → q' = q/2^k with |q'| ≤ 1 via reductionSteps, compute exp(q') via Padé [4/4], then square k times since exp(q) = exp(q')^(2^k).

The nonneg guard on small.lo is always true by construction: padeExp(q') ≈ exp(q') ≥ exp(-1) ≈ 0.368 >> padeErrorBound = 2.5×10⁻⁷.

Equations

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

theorem Interval.expPoint_containsReal (q : ℚ) : (expPoint q).containsReal (Real.exp ↑q)

Containment theorem for expPoint.

def Interval.expInterval (I : QInterval) : QInterval

Interval containing exp(x) for x in rational interval I.

Uses monotonicity of exp: for x ∈ [lo, hi], exp(lo) ≤ exp(x) ≤ exp(hi) so exp(x) ∈ [expPoint(lo).lo, expPoint(hi).hi].

Equations

• Interval.expInterval I = { lo := (Interval.expPoint I.lo).lo, hi := (Interval.expPoint I.hi).hi, valid := ⋯ }

theorem Interval.expInterval_containsReal {I : QInterval} {x : ℝ} (hx : I.containsReal x) : (expInterval I).containsReal (Real.exp x)

Containment theorem for expInterval: monotonicity of exp + expPoint containment.

def Interval.logIterations : ℕ

Number of bisection iterations.

Equations

• Interval.logIterations = 50

def Interval.logPoint (q : ℚ) (_hq : 0 < q) : QInterval

Point interval containing log(q) for rational q > 0.

Initial bracket: [-(Nat.log 2 q.den + 1), Nat.log 2 q.num.natAbs + 1]. This uses bit lengths instead of raw values, giving a bracket width proportional to log₂(q) rather than q itself — critical for large-denominator rationals from interval arithmetic chains.

Lower: exp(-(log₂ d + 1)) < 1/d ≤ q since d < 2^(log₂ d + 1) ≤ exp(log₂ d + 1). Upper: q ≤ p ≤ exp(log₂ p + 1) by the same argument.

50 bisection iterations narrow this to precision bracket_width / 2^50.

Equations

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

theorem Interval.logPoint_containsReal (q : ℚ) (hq : 0 < q) : (logPoint q hq).containsReal (Real.log ↑q)

Containment theorem for logPoint: the bisection invariant exp(lo) ≤ q ≤ exp(hi) implies lo ≤ log(q) ≤ hi by monotonicity of log.

def Interval.logInterval (I : QInterval) (hI : 0 < I.lo) : QInterval

Interval containing log(x) for x in a positive rational interval I.

Uses monotonicity of log: for x ∈ [lo, hi] with lo > 0, log(lo) ≤ log(x) ≤ log(hi) so log(x) ∈ [logPoint(lo).lo, logPoint(hi).hi].

Equations

• Interval.logInterval I hI = { lo := (Interval.logPoint I.lo hI).lo, hi := (Interval.logPoint I.hi ⋯).hi, valid := ⋯ }

theorem Interval.logInterval_containsReal {I : QInterval} {x : ℝ} (hI : 0 < I.lo) (hx : I.containsReal x) : (logInterval I hI).containsReal (Real.log x)

Containment theorem for logInterval: monotonicity of log + logPoint containment.

theorem Interval.log_zero_containsReal {I : QInterval} {x : ℝ} (hx : I.containsReal x) (hlo : 0 ≤ I.lo) (hhi : I.hi ≤ 0) : (QInterval.exact 0).containsReal (Real.log x)

When the argument is known to be zero (from interval [0,0]), Real.log x = Real.log 0 = 0, contained in exact 0.

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

Interval square root for positive intervals. Uses the identity √x = exp(log(x) / 2) for x > 0. Chains logInterval, rational halving, and expInterval.

Equations

• Interval.sqrtInterval a ha = Interval.expInterval { lo := (Interval.logInterval a ha).lo / 2, hi := (Interval.logInterval a ha).hi / 2, valid := ⋯ }

theorem Interval.sqrtInterval_containsReal {a : QInterval} {x : ℝ} (ha : 0 < a.lo) (hx : a.containsReal x) : (sqrtInterval a ha).containsReal √x

Soundness: if x ∈ [a.lo, a.hi] and a.lo > 0, then √x ∈ sqrtInterval a.

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

Real-exponent bridge for QInterval.rpowNat: same proof as QInterval.powNat_containsReal, but with the goal stated using Real.rpow (real-valued exponent) rather than HPow.hPow (nat).

def Interval.rpowZero : QInterval

Interval for rpow(x, 0) = [1, 1].

Equations

• Interval.rpowZero = Interval.QInterval.exact 1

theorem Interval.rpowZero_containsReal (x : ℝ) : rpowZero.containsReal (x ^ 0)

theorem Interval.rpowOne_containsReal {a : QInterval} {x : ℝ} (_ha : 0 ≤ a.lo) (hx : a.containsReal x) : a.containsReal (x ^ 1)

For rpow(x, 1) with x ∈ interval a, the result is just a.