Adaptive Bound Verification via Branch-and-Bound

This file provides adaptive bound verification functions that use the branch-and-bound global optimization algorithm to verify bounds on expressions. Unlike single-shot interval evaluation, these functions automatically subdivide the domain until the bound can be verified or the iteration limit is reached.

Main definitions

• verifyUpperBound - Verify f(x) ≤ bound for all x in box using adaptive subdivision
• verifyLowerBound - Verify f(x) ≥ bound for all x in box using adaptive subdivision
• verifyUpperBound1 - Single-variable version
• verifyLowerBound1 - Single-variable version

Main theorems

• verifyUpperBound_correct - If verifyUpperBound returns true, the bound holds
• verifyLowerBound_correct - If verifyLowerBound returns true, the bound holds

Usage

These functions are intended to be used as fallbacks when single-shot interval evaluation fails due to over-approximation. They provide better precision at the cost of increased computation.

-- Single-shot fails on tight bounds, but adaptive succeeds
example : verifyUpperBound1 (Expr.sin (Expr.var 0)) ⟨0, 11/10, by norm_num⟩ (85/100) = true := by
  native_decide

Configuration for bound verification

structure LeanCert.Engine.Optimization.BoundVerifyConfig : Type

Configuration for adaptive bound verification

• maxIterations : ℕ

  Maximum number of subdivisions

• tolerance : ℚ

  Stop when box width is below this threshold

• taylorDepth : ℕ

  Taylor depth for interval evaluation

• useMonotonicity : Bool

  Use monotonicity-based pruning (symbolic pre-pass for gradient signs)

def LeanCert.Engine.Optimization.instReprBoundVerifyConfig.repr : BoundVerifyConfig → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.Optimization.instReprBoundVerifyConfig : Repr BoundVerifyConfig

Equations

• LeanCert.Engine.Optimization.instReprBoundVerifyConfig = { reprPrec := LeanCert.Engine.Optimization.instReprBoundVerifyConfig.repr }

def LeanCert.Engine.Optimization.instDecidableEqBoundVerifyConfig.decEq (x✝ x✝¹ : BoundVerifyConfig) : Decidable (x✝ = x✝¹)

Equations

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

instance LeanCert.Engine.Optimization.instDecidableEqBoundVerifyConfig : DecidableEq BoundVerifyConfig

Equations

• LeanCert.Engine.Optimization.instDecidableEqBoundVerifyConfig = LeanCert.Engine.Optimization.instDecidableEqBoundVerifyConfig.decEq

instance LeanCert.Engine.Optimization.instInhabitedBoundVerifyConfig : Inhabited BoundVerifyConfig

Equations

• LeanCert.Engine.Optimization.instInhabitedBoundVerifyConfig = { default := { } }

def LeanCert.Engine.Optimization.BoundVerifyConfig.toGlobalOptConfig (cfg : BoundVerifyConfig) : GlobalOptConfig

Convert BoundVerifyConfig to GlobalOptConfig

Equations

• cfg.toGlobalOptConfig = { maxIterations := cfg.maxIterations, tolerance := cfg.tolerance, useMonotonicity := cfg.useMonotonicity, taylorDepth := cfg.taylorDepth }

Witness/Epsilon-argmax structures

structure LeanCert.Engine.Optimization.WitnessPoint : Type

A witness point for an optimization result

• coords : List ℚ

  The coordinates of the witness point

• value : Core.IntervalRat

  The function value at this point (interval containing true value)

def LeanCert.Engine.Optimization.instReprWitnessPoint.repr : WitnessPoint → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.Optimization.instReprWitnessPoint : Repr WitnessPoint

Equations

• LeanCert.Engine.Optimization.instReprWitnessPoint = { reprPrec := LeanCert.Engine.Optimization.instReprWitnessPoint.repr }

structure LeanCert.Engine.Optimization.BoundVerifyResult : Type

Result of bound verification with witness information

• verified : Bool

  Whether the bound was verified

• computedBound : ℚ

  The computed bound (lo for min, hi for max)

• witness : WitnessPoint

  Approximate argmin/argmax (midpoint of best box)

• epsilon : ℚ

  Width of the best box (epsilon for ε-approximate argmin/argmax)

• iterations : ℕ

  Number of iterations used

def LeanCert.Engine.Optimization.instReprBoundVerifyResult.repr : BoundVerifyResult → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.Optimization.instReprBoundVerifyResult : Repr BoundVerifyResult

Equations

• LeanCert.Engine.Optimization.instReprBoundVerifyResult = { reprPrec := LeanCert.Engine.Optimization.instReprBoundVerifyResult.repr }

def LeanCert.Engine.Optimization.Box.midpoint (B : Box) : List ℚ

Extract witness point from a box (midpoint of each interval)

Equations

• B.midpoint = List.map (fun (I : LeanCert.Core.IntervalRat) => I.midpoint) B

def LeanCert.Engine.Optimization.Box.maxWidthQ (B : Box) : ℚ

Compute maximum width of a box (the ε in ε-approximate)

Equations

• B.maxWidthQ = List.foldl (fun (acc : ℚ) (I : LeanCert.Core.IntervalRat) => max acc (I.hi - I.lo)) 0 B

def LeanCert.Engine.Optimization.evalAtPoint (e : Core.Expr) (point : List ℚ) (cfg : EvalConfig := { }) : Core.IntervalRat

Evaluate expression at a rational point (using singleton intervals)

Equations

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

Computable bound verification functions

def LeanCert.Engine.Optimization.verifyUpperBound (e : Core.Expr) (B : Box) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : Bool

Verify f(x) ≤ bound for all x in box using adaptive subdivision. Returns true if the maximum of f over the box is ≤ bound.

Equations

• LeanCert.Engine.Optimization.verifyUpperBound e B bound cfg = decide ((LeanCert.Engine.Optimization.globalMaximizeCore e B cfg.toGlobalOptConfig).bound.hi ≤ bound)

def LeanCert.Engine.Optimization.verifyLowerBound (e : Core.Expr) (B : Box) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : Bool

Verify f(x) ≥ bound for all x in box using adaptive subdivision. Returns true if the minimum of f over the box is ≥ bound.

Equations

• LeanCert.Engine.Optimization.verifyLowerBound e B bound cfg = decide ((LeanCert.Engine.Optimization.globalMinimizeCore e B cfg.toGlobalOptConfig).bound.lo ≥ bound)

def LeanCert.Engine.Optimization.verifyUpperBoundStrict (e : Core.Expr) (B : Box) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : Bool

Verify f(x) < bound for all x in box using adaptive subdivision. Returns true if the maximum of f over the box is < bound.

Equations

• LeanCert.Engine.Optimization.verifyUpperBoundStrict e B bound cfg = decide ((LeanCert.Engine.Optimization.globalMaximizeCore e B cfg.toGlobalOptConfig).bound.hi < bound)

def LeanCert.Engine.Optimization.verifyLowerBoundStrict (e : Core.Expr) (B : Box) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : Bool

Verify f(x) > bound for all x in box using adaptive subdivision. Returns true if the minimum of f over the box is > bound.

Equations

• LeanCert.Engine.Optimization.verifyLowerBoundStrict e B bound cfg = decide ((LeanCert.Engine.Optimization.globalMinimizeCore e B cfg.toGlobalOptConfig).bound.lo > bound)

Epsilon-argmax/argmin functions with witness information

def LeanCert.Engine.Optimization.findMaxWithWitness (e : Core.Expr) (B : Box) (cfg : BoundVerifyConfig := { }) : BoundVerifyResult

Find the maximum of f over a box, returning result with witness information. The witness is an ε-approximate argmax: a point where f(witness) is within ε of the true maximum, where ε = bestBox.maxWidth.

Equations

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

def LeanCert.Engine.Optimization.findMinWithWitness (e : Core.Expr) (B : Box) (cfg : BoundVerifyConfig := { }) : BoundVerifyResult

Find the minimum of f over a box, returning result with witness information. The witness is an ε-approximate argmin: a point where f(witness) is within ε of the true minimum, where ε = bestBox.maxWidth.

Equations

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

def LeanCert.Engine.Optimization.verifyUpperBoundWithWitness (e : Core.Expr) (B : Box) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : BoundVerifyResult

Verify f(x) ≤ bound with witness information. Returns the verification result along with an ε-approximate argmax.

Equations

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

def LeanCert.Engine.Optimization.verifyLowerBoundWithWitness (e : Core.Expr) (B : Box) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : BoundVerifyResult

Verify f(x) ≥ bound with witness information. Returns the verification result along with an ε-approximate argmin.

Equations

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

Single-variable convenience functions

def LeanCert.Engine.Optimization.intervalToBox (I : Core.IntervalRat) : Box

Convert a single interval to a 1D box

Equations

• LeanCert.Engine.Optimization.intervalToBox I = [I]

def LeanCert.Engine.Optimization.verifyUpperBound1 (e : Core.Expr) (I : Core.IntervalRat) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : Bool

Single-variable version of verifyUpperBound

Equations

• LeanCert.Engine.Optimization.verifyUpperBound1 e I bound cfg = LeanCert.Engine.Optimization.verifyUpperBound e (LeanCert.Engine.Optimization.intervalToBox I) bound cfg

def LeanCert.Engine.Optimization.verifyLowerBound1 (e : Core.Expr) (I : Core.IntervalRat) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : Bool

Single-variable version of verifyLowerBound

Equations

• LeanCert.Engine.Optimization.verifyLowerBound1 e I bound cfg = LeanCert.Engine.Optimization.verifyLowerBound e (LeanCert.Engine.Optimization.intervalToBox I) bound cfg

def LeanCert.Engine.Optimization.verifyUpperBound1Strict (e : Core.Expr) (I : Core.IntervalRat) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : Bool

Single-variable version of verifyUpperBoundStrict

Equations

• LeanCert.Engine.Optimization.verifyUpperBound1Strict e I bound cfg = LeanCert.Engine.Optimization.verifyUpperBoundStrict e (LeanCert.Engine.Optimization.intervalToBox I) bound cfg

def LeanCert.Engine.Optimization.verifyLowerBound1Strict (e : Core.Expr) (I : Core.IntervalRat) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : Bool

Single-variable version of verifyLowerBoundStrict

Equations

• LeanCert.Engine.Optimization.verifyLowerBound1Strict e I bound cfg = LeanCert.Engine.Optimization.verifyLowerBoundStrict e (LeanCert.Engine.Optimization.intervalToBox I) bound cfg

def LeanCert.Engine.Optimization.findMax1WithWitness (e : Core.Expr) (I : Core.IntervalRat) (cfg : BoundVerifyConfig := { }) : BoundVerifyResult

Single-variable version of findMaxWithWitness

Equations

• LeanCert.Engine.Optimization.findMax1WithWitness e I cfg = LeanCert.Engine.Optimization.findMaxWithWitness e (LeanCert.Engine.Optimization.intervalToBox I) cfg

def LeanCert.Engine.Optimization.findMin1WithWitness (e : Core.Expr) (I : Core.IntervalRat) (cfg : BoundVerifyConfig := { }) : BoundVerifyResult

Single-variable version of findMinWithWitness

Equations

• LeanCert.Engine.Optimization.findMin1WithWitness e I cfg = LeanCert.Engine.Optimization.findMinWithWitness e (LeanCert.Engine.Optimization.intervalToBox I) cfg

def LeanCert.Engine.Optimization.verifyUpperBound1WithWitness (e : Core.Expr) (I : Core.IntervalRat) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : BoundVerifyResult

Single-variable version of verifyUpperBoundWithWitness

Equations

• LeanCert.Engine.Optimization.verifyUpperBound1WithWitness e I bound cfg = LeanCert.Engine.Optimization.verifyUpperBoundWithWitness e (LeanCert.Engine.Optimization.intervalToBox I) bound cfg

def LeanCert.Engine.Optimization.verifyLowerBound1WithWitness (e : Core.Expr) (I : Core.IntervalRat) (bound : ℚ) (cfg : BoundVerifyConfig := { }) : BoundVerifyResult

Single-variable version of verifyLowerBoundWithWitness

Equations

• LeanCert.Engine.Optimization.verifyLowerBound1WithWitness e I bound cfg = LeanCert.Engine.Optimization.verifyLowerBoundWithWitness e (LeanCert.Engine.Optimization.intervalToBox I) bound cfg

Correctness theorems (noncomputable proofs)

theorem LeanCert.Engine.Optimization.intervalToBox_envMem (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) : Box.envMem (fun (x_1 : ℕ) => x) (intervalToBox I)

Helper: convert single-variable environment to box membership

theorem LeanCert.Engine.Optimization.intervalToBox_zero (I : Core.IntervalRat) (x : ℝ) (i : ℕ) : i ≥ List.length (intervalToBox I) → (fun (x_1 : ℕ) => x) i = x

Helper: if i ≥ 1, then (fun _ => x) i = 0 is vacuously satisfiable for our purposes

theorem LeanCert.Engine.Optimization.verifyUpperBound_correct (e : Core.Expr) (hsupp : ExprSupported e) (B : Box) (bound : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e B cfg.toGlobalOptConfig).bound.hi ≤ bound) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → Core.Expr.eval ρ e ≤ ↑bound

If verifyUpperBound succeeds, the upper bound holds for all points in the box. Note: This uses the noncomputable globalMaximize for the proof, but the computable globalMaximizeCore is used for execution.

theorem LeanCert.Engine.Optimization.verifyLowerBound_correct (e : Core.Expr) (hsupp : ExprSupported e) (B : Box) (bound : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e B cfg.toGlobalOptConfig).bound.lo ≥ bound) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ↑bound ≤ Core.Expr.eval ρ e

If verifyLowerBound succeeds, the lower bound holds for all points in the box.

theorem LeanCert.Engine.Optimization.verifyUpperBound1_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (bound : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e (intervalToBox I) cfg.toGlobalOptConfig).bound.hi ≤ bound) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑bound

Single-variable upper bound correctness

theorem LeanCert.Engine.Optimization.verifyLowerBound1_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (bound : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e (intervalToBox I) cfg.toGlobalOptConfig).bound.lo ≥ bound) (x : ℝ) : x ∈ I → ↑bound ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Single-variable lower bound correctness

Expression uses only var 0

def LeanCert.Engine.Optimization.Expr.usesOnlyVar0 : Core.Expr → Bool

Predicate: expression only uses variable index 0

Equations

• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 (LeanCert.Core.Expr.const q) = true
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 (LeanCert.Core.Expr.var i) = (i == 0)
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 (e1.add e2) = (e1.usesOnlyVar0 && e2.usesOnlyVar0)
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 (e1.mul e2) = (e1.usesOnlyVar0 && e2.usesOnlyVar0)
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.neg = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.inv = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.exp = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.sin = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.cos = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.log = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.atan = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.arsinh = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.atanh = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.sinc = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.erf = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.sinh = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.cosh = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.tanh = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 e.sqrt = e.usesOnlyVar0
• LeanCert.Engine.Optimization.Expr.usesOnlyVar0 LeanCert.Core.Expr.pi = true

theorem LeanCert.Engine.Optimization.Expr.eval_usesOnlyVar0 (e : Core.Expr) (he : e.usesOnlyVar0 = true) (ρ ρ' : ℕ → ℝ) (h0 : ρ 0 = ρ' 0) : Core.Expr.eval ρ e = Core.Expr.eval ρ' e

If an expression uses only var 0, evaluation depends only on ρ 0

Tactic-facing lemmas for adaptive bound verification

theorem LeanCert.Engine.Optimization.adaptive_upper_bound (e : Core.Expr) (hsupp : ExprSupported e) (he : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e [I] cfg.toGlobalOptConfig).bound.hi ≤ c) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Tactic-facing lemma: if adaptive verification succeeds, upper bound holds. This is the key lemma that tactics use to close goals. Requires that the expression uses only var 0.

theorem LeanCert.Engine.Optimization.adaptive_lower_bound (e : Core.Expr) (hsupp : ExprSupported e) (he : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e [I] cfg.toGlobalOptConfig).bound.lo ≥ c) (x : ℝ) : x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Tactic-facing lemma: if adaptive verification succeeds, lower bound holds. Requires that the expression uses only var 0.

theorem LeanCert.Engine.Optimization.adaptive_upper_bound_strict (e : Core.Expr) (hsupp : ExprSupported e) (he : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e [I] cfg.toGlobalOptConfig).bound.hi < c) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Strict upper bound version

theorem LeanCert.Engine.Optimization.adaptive_lower_bound_strict (e : Core.Expr) (hsupp : ExprSupported e) (he : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e [I] cfg.toGlobalOptConfig).bound.lo > c) (x : ℝ) : x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Strict lower bound version

Theorem versions for Set.Icc (for tactic compatibility)

theorem LeanCert.Engine.Optimization.adaptive_upper_bound_Icc (e : Core.Expr) (hsupp : ExprSupported e) (he : e.usesOnlyVar0 = true) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e [{ lo := lo, hi := hi, le := hle }] cfg.toGlobalOptConfig).bound.hi ≤ c) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Adaptive upper bound for Set.Icc membership

theorem LeanCert.Engine.Optimization.adaptive_lower_bound_Icc (e : Core.Expr) (hsupp : ExprSupported e) (he : e.usesOnlyVar0 = true) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e [{ lo := lo, hi := hi, le := hle }] cfg.toGlobalOptConfig).bound.lo ≥ c) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Adaptive lower bound for Set.Icc membership

theorem LeanCert.Engine.Optimization.adaptive_upper_bound_Icc_strict (e : Core.Expr) (hsupp : ExprSupported e) (he : e.usesOnlyVar0 = true) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e [{ lo := lo, hi := hi, le := hle }] cfg.toGlobalOptConfig).bound.hi < c) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Strict upper bound for Set.Icc

theorem LeanCert.Engine.Optimization.adaptive_lower_bound_Icc_strict (e : Core.Expr) (hsupp : ExprSupported e) (he : e.usesOnlyVar0 = true) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e [{ lo := lo, hi := hi, le := hle }] cfg.toGlobalOptConfig).bound.lo > c) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Strict lower bound for Set.Icc