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 theorem boundary

The correctness theorems in this file are stated over the noncomputable globalMaximize / globalMinimize specifications. The executable verifyUpperBound / verifyLowerBound checkers use globalMaximizeCore / globalMinimizeCore; they are useful adaptive checkers, but should not be read as having a Boolean soundness theorem until a matching core-algorithm theorem is added.

• verifyUpperBound_correct - Noncomputable upper-bound theorem
• verifyLowerBound_correct - Noncomputable lower-bound theorem

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_reducible]

instance LeanCert.Engine.Optimization.instReprBoundVerifyConfig : Repr BoundVerifyConfig

Equations

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

@[instance_reducible]

instance LeanCert.Engine.Optimization.instDecidableEqBoundVerifyConfig : DecidableEq BoundVerifyConfig

Equations

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

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_reducible]

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)

@[instance_reducible]

instance LeanCert.Engine.Optimization.instReprWitnessPoint : Repr WitnessPoint

Equations

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

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

Equations

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

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_reducible]

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.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.Box.ofInterval 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.Box.ofInterval 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.Box.ofInterval 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.Box.ofInterval 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.Box.ofInterval 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.Box.ofInterval 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.Box.ofInterval 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.Box.ofInterval I) bound cfg

Correctness theorems (noncomputable proofs)

These theorems intentionally take premises involving globalMaximize and globalMinimize, not the executable Boolean checkers above. This keeps the current trust boundary explicit: the adaptive core is available for search and candidate checking, while proof-producing users should rely on the theorem premises below or on a future globalMaximizeCore/globalMinimizeCore soundness theorem.

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

Helper: convert single-variable environment to box membership

theorem LeanCert.Engine.Optimization.Box.ofInterval_zero (I : Core.IntervalRat) (x : ℝ) (i : ℕ) : i ≥ List.length (ofInterval 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 : ADSupported e) (B : Box) (bound : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e hsupp B cfg.toGlobalOptConfig).bound.hi ≤ bound) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → Core.Expr.eval ρ e ≤ ↑bound

Noncomputable upper-bound theorem.

Despite the historical name, this is not a Boolean soundness theorem for verifyUpperBound; its premise is the semantic bound produced by globalMaximize.

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

Noncomputable lower-bound theorem.

Despite the historical name, this is not a Boolean soundness theorem for verifyLowerBound; its premise is the semantic bound produced by globalMinimize.

Tactic-facing lemmas for adaptive bound verification

theorem LeanCert.Engine.Optimization.adaptive_upper_bound (e : Core.Expr) (hsupp : ADSupported e) (he : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e hsupp [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 : ADSupported e) (he : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e hsupp [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 : ADSupported e) (he : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e hsupp [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 : ADSupported e) (he : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e hsupp [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 : ADSupported e) (he : e.usesOnlyVar0 = true) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e hsupp [{ 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 : ADSupported e) (he : e.usesOnlyVar0 = true) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e hsupp [{ 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 : ADSupported e) (he : e.usesOnlyVar0 = true) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMaximize e hsupp [{ 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 : ADSupported e) (he : e.usesOnlyVar0 = true) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : BoundVerifyConfig) (hverify : (globalMinimize e hsupp [{ 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