Global Optimization via Branch-and-Bound

This file implements a branch-and-bound algorithm for rigorous global optimization of expressions over n-dimensional boxes.

Main definitions

• GlobalBound - Result of global optimization (lower bound and optional upper bound)
• globalMinimize - Branch-and-bound minimization over a box
• globalMaximize - Branch-and-bound maximization over a box

Algorithm

The branch-and-bound algorithm works by:

1. Evaluating the expression over the current box using interval arithmetic
2. Using the interval lower bound to prune boxes that can't contain the minimum
3. Splitting the widest dimension when bounds aren't tight enough
4. Optionally pruning using monotonicity (gradient sign information)

Correctness

The algorithm maintains the invariant that the returned lower bound is ≤ f(x) for all x in the original box. When the interval upper bound equals the lower bound (or is close enough), we have found the global minimum.

Configuration

structure LeanCert.Engine.Optimization.GlobalOptConfig : Type

Configuration for global optimization

• maxIterations : ℕ

  Maximum number of subdivisions

• tolerance : ℚ

  Stop when box width is below this threshold

• useMonotonicity : Bool

  Use monotonicity pruning (requires gradient computation)

• taylorDepth : ℕ

  Taylor depth for interval evaluation

def LeanCert.Engine.Optimization.instReprGlobalOptConfig.repr : GlobalOptConfig → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.Optimization.instReprGlobalOptConfig : Repr GlobalOptConfig

Equations

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

instance LeanCert.Engine.Optimization.instInhabitedGlobalOptConfig : Inhabited GlobalOptConfig

Equations

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

Result types

structure LeanCert.Engine.Optimization.GlobalBound : Type

Result of global optimization

• lo : ℚ

  Lower bound: f(x) ≥ lo for all x in the box

• hi : ℚ

  Upper bound: there exists x in box with f(x) ≤ hi

• bestBox : Box

  Best box found (smallest interval containing minimum)

• iterations : ℕ

  Number of iterations used

instance LeanCert.Engine.Optimization.instReprGlobalBound : Repr GlobalBound

Equations

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

def LeanCert.Engine.Optimization.instReprGlobalBound.repr : GlobalBound → ℕ → Std.Format

Equations

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

structure LeanCert.Engine.Optimization.GlobalResult : Type

Result of optimization with certificate data

• bound : GlobalBound

  The computed bound

• remainingBoxes : List (ℚ × Box)

  Priority queue of remaining boxes (for resumption)

instance LeanCert.Engine.Optimization.instReprGlobalResult : Repr GlobalResult

Equations

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

def LeanCert.Engine.Optimization.instReprGlobalResult.repr : GlobalResult → ℕ → Std.Format

Equations

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

Priority queue operations

def LeanCert.Engine.Optimization.insertByBound (queue : List (ℚ × Box)) (lb : ℚ) (B : Box) : List (ℚ × Box)

Insert a box with its lower bound into a sorted list (ascending by bound)

Equations

• LeanCert.Engine.Optimization.insertByBound [] lb B = [(lb, B)]
• LeanCert.Engine.Optimization.insertByBound ((lb', B') :: rest) lb B = if lb ≤ lb' then (lb, B) :: (lb', B') :: rest else (lb', B') :: LeanCert.Engine.Optimization.insertByBound rest lb B

def LeanCert.Engine.Optimization.popBest (queue : List (ℚ × Box)) : Option ((ℚ × Box) × List (ℚ × Box))

Pop the box with smallest lower bound

Equations

• LeanCert.Engine.Optimization.popBest [] = none
• LeanCert.Engine.Optimization.popBest (best :: rest) = some (best, rest)

Core algorithm

noncomputable def LeanCert.Engine.Optimization.evalOnBox (e : Core.Expr) (B : Box) (_cfg : GlobalOptConfig) : Core.IntervalRat

Evaluate expression on a box and get interval bounds

Equations

• LeanCert.Engine.Optimization.evalOnBox e B _cfg = LeanCert.Engine.evalIntervalRefined e B.toEnv

noncomputable def LeanCert.Engine.Optimization.minimizeStep (e : Core.Expr) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) : Option (List (ℚ × Box) × ℚ × ℚ × Box)

One step of branch-and-bound for minimization with explicit bestLB tracking. When cfg.useMonotonicity is true, applies gradient-based pruning before evaluation.

Equations

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

noncomputable def LeanCert.Engine.Optimization.minimizeLoop (e : Core.Expr) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) : GlobalResult

Run branch-and-bound for a fixed number of iterations with explicit bestLB tracking

Equations

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

noncomputable def LeanCert.Engine.Optimization.globalMinimize (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig := { }) : GlobalResult

Global minimization over a box

Equations

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

noncomputable def LeanCert.Engine.Optimization.globalMaximize (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig := { }) : GlobalResult

Global maximization over a box (minimize -e)

Equations

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

Computable versions for execution

def LeanCert.Engine.Optimization.evalOnBoxCore (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig) : Core.IntervalRat

Evaluate expression on a box (computable version for ExprSupportedCore)

Equations

• LeanCert.Engine.Optimization.evalOnBoxCore e B cfg = LeanCert.Engine.evalIntervalCore e B.toEnv { taylorDepth := cfg.taylorDepth }

def LeanCert.Engine.Optimization.evalOnBoxCoreDiv (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig) : Core.IntervalRat

Evaluate expression on a box (computable version with division support). This is used by the Python bridge for applications where division is common. Note: No formal correctness proof yet; returns sound but possibly wide bounds.

Equations

• LeanCert.Engine.Optimization.evalOnBoxCoreDiv e B cfg = LeanCert.Engine.evalIntervalCoreWithDiv e B.toEnv { taylorDepth := cfg.taylorDepth }

def LeanCert.Engine.Optimization.minimizeStepCore (e : Core.Expr) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) : Option (List (ℚ × Box) × ℚ × ℚ × Box)

One step of branch-and-bound (computable version) with explicit bestLB tracking. When cfg.useMonotonicity is true, applies gradient-based pruning before evaluation.

Equations

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

def LeanCert.Engine.Optimization.minimizeLoopCore (e : Core.Expr) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) : GlobalResult

Run branch-and-bound (computable version) with explicit bestLB tracking

Equations

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

def LeanCert.Engine.Optimization.globalMinimizeCore (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig := { }) : GlobalResult

Global minimization (computable version)

Equations

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

def LeanCert.Engine.Optimization.globalMaximizeCore (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig := { }) : GlobalResult

Global maximization (computable version)

Equations

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

Division-supporting versions for Python bridge

These variants use evalIntervalCoreWithDiv which handles division (inv) properly. They have the same structure as the standard versions but support expressions with division.

def LeanCert.Engine.Optimization.minimizeStepCoreDiv (e : Core.Expr) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) : Option (List (ℚ × Box) × ℚ × ℚ × Box)

One step of branch-and-bound with division support

Equations

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

def LeanCert.Engine.Optimization.minimizeLoopCoreDiv (e : Core.Expr) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) : GlobalResult

Run branch-and-bound loop with division support

Equations

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

def LeanCert.Engine.Optimization.globalMinimizeCoreDiv (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig := { }) : GlobalResult

Global minimization with division support

Equations

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

def LeanCert.Engine.Optimization.globalMaximizeCoreDiv (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig := { }) : GlobalResult

Global maximization with division support

Equations

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

Correctness theorems

theorem LeanCert.Engine.Optimization.evalOnBox_lo_correct (e : Core.Expr) (hsupp : ExprSupported e) (B : Box) (cfg : GlobalOptConfig) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) : ↑(evalOnBox e B cfg).lo ≤ Core.Expr.eval ρ e

The lower bound from interval evaluation is correct.

theorem LeanCert.Engine.Optimization.evalOnBox_hi_correct (e : Core.Expr) (hsupp : ExprSupported e) (B : Box) (cfg : GlobalOptConfig) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) : Core.Expr.eval ρ e ≤ ↑(evalOnBox e B cfg).hi

The upper bound from interval evaluation is correct (∃ point achieving it).

noncomputable def LeanCert.Engine.Optimization.Box.midpointEnv (B : Box) : ℕ → ℝ

Helper: construct a midpoint environment for a box

Equations

• B.midpointEnv i = if h : i < List.length B then ↑B[i].midpoint else 0

theorem LeanCert.Engine.Optimization.Box.midpointEnv_mem (B : Box) : envMem B.midpointEnv B

The midpoint environment is in the box

theorem LeanCert.Engine.Optimization.Box.midpointEnv_zero (B : Box) (i : ℕ) : i ≥ List.length B → B.midpointEnv i = 0

The midpoint environment is zero outside the box

theorem LeanCert.Engine.Optimization.Box.split_length_eq (B : Box) (d : ℕ) : List.length (B.split d).1 = List.length B ∧ List.length (B.split d).2 = List.length B

Helper lemma: split preserves box length

theorem LeanCert.Engine.Optimization.Box.splitWidest_length_eq (B : Box) : List.length B.splitWidest.1 = List.length B ∧ List.length B.splitWidest.2 = List.length B

Helper lemma: splitWidest preserves box length

New simplified correctness architecture with explicit bestLB tracking

The key idea: track both bestLB (global lower bound) and bestUB (global upper bound) explicitly. This makes the invariants much simpler:

• (Global LB) For all ρ in the original box, bestLB ≤ f(ρ)
• (Global UB witness) There exists ρ* in bestBox such that f(ρ*) ≤ bestUB
• (Queue boxes are sub-boxes) Every B' in queue is a sub-box of the original box

theorem LeanCert.Engine.Optimization.mem_insertByBound (queue : List (ℚ × Box)) (lb : ℚ) (B : Box) (lb' : ℚ) (B' : Box) : (lb', B') ∈ insertByBound queue lb B ↔ (lb', B') = (lb, B) ∨ (lb', B') ∈ queue

Membership in insertByBound: element is either the inserted one or was in original

theorem LeanCert.Engine.Optimization.minimizeStep_nonempty (e : Core.Expr) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) : ∃ (result : List (ℚ × Box) × ℚ × ℚ × Box), minimizeStep e cfg (hd :: tl) bestLB bestUB bestBox = some result

minimizeStep always returns some for non-empty queue

theorem LeanCert.Engine.Optimization.minimizeStep_bestUB_le (e : Core.Expr) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e cfg queue bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) : bestUB' ≤ bestUB

Helper: bestUB only decreases during minimizeStep

theorem LeanCert.Engine.Optimization.minimizeStep_bestLB_le (e : Core.Expr) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e cfg queue bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) : bestLB' ≤ bestLB

Helper: bestLB only decreases during minimizeStep

theorem LeanCert.Engine.Optimization.minimizeStep_queue_entries (e : Core.Expr) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e cfg (hd :: tl) bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) (lb : ℚ) (B' : Box) (hmem : (lb, B') ∈ queue') : (lb, B') ∈ tl ∨ lb ≤ bestUB'

Helper: new queue entries either come from original tail or have lb ≤ newBestUB

theorem LeanCert.Engine.Optimization.minimizeStep_bestBox_cases (e : Core.Expr) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e cfg (hd :: tl) bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) : bestBox' = bestBox ∨ bestBox' = if cfg.useMonotonicity = true then (pruneBoxForMin hd.2 (gradientIntervalN e hd.2 (List.length hd.2))).1 else hd.2

Helper: bestBox' is either bestBox or a subset of hd.2 (the pruned box B_curr). When monotonicity pruning is enabled, bestBox' may be the pruned version of hd.2.

theorem LeanCert.Engine.Optimization.minimizeStep_queue_boxes (e : Core.Expr) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e cfg (hd :: tl) bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) (lb : ℚ) (B' : Box) (hmem : (lb, B') ∈ queue') : have B_curr := if cfg.useMonotonicity = true then (pruneBoxForMin hd.2 (gradientIntervalN e hd.2 (List.length hd.2))).1 else hd.2; (lb, B') ∈ tl ∨ B' = B_curr.splitWidest.1 ∨ B' = B_curr.splitWidest.2

Helper: queue entries in result are either from tl or splits of B_curr (the possibly pruned hd.2)

theorem LeanCert.Engine.Optimization.minimizeStep_bestUB_achievable (e : Core.Expr) (hsupp : ExprSupported e) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e cfg (hd :: tl) bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) (hBestUB : ∃ (ρ : ℕ → ℝ), Box.envMem ρ bestBox ∧ (∀ i ≥ List.length bestBox, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑bestUB) : ∃ (ρ : ℕ → ℝ), Box.envMem ρ bestBox' ∧ (∀ i ≥ List.length bestBox', ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑bestUB'

Helper: bestUB' is achievable if bestUB is achievable

theorem LeanCert.Engine.Optimization.Box.envMem_of_envMem_split (B : Box) (d : ℕ) (ρ : ℕ → ℝ) : envMem ρ (B.split d).1 → envMem ρ B

Helper: if ρ is in a split of B, then ρ is in B

theorem LeanCert.Engine.Optimization.Box.envMem_of_envMem_split_right (B : Box) (d : ℕ) (ρ : ℕ → ℝ) : envMem ρ (B.split d).2 → envMem ρ B

theorem LeanCert.Engine.Optimization.Box.envMem_of_envMem_splitWidest (B : Box) (ρ : ℕ → ℝ) : envMem ρ B.splitWidest.1 ∨ envMem ρ B.splitWidest.2 → envMem ρ B

Helper: if ρ is in a split of B, then ρ is in B

theorem LeanCert.Engine.Optimization.Box.splitWidest_length (B : Box) : List.length B.splitWidest.1 = List.length B ∧ List.length B.splitWidest.2 = List.length B

Helper: splits preserve length

Key correctness theorem: minimizeStep preserves lower bound invariant

theorem LeanCert.Engine.Optimization.pruneBoxForMin_sub_aux (B : Box) (grad : List Core.IntervalRat) (ρ : ℕ → ℝ) (h : Box.envMem ρ (pruneBoxForMin B grad).1) : Box.envMem ρ B

Pruning returns a sub-box: any point in the pruned box is also in the original. This is a direct consequence of pruneBoxForMin_subset from Gradient.lean.

theorem LeanCert.Engine.Optimization.minimizeStep_preserves_LB (e : Core.Expr) (hsupp : ExprSupported e) (cfg : GlobalOptConfig) (origB : Box) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e cfg queue bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) (hLB : ∀ (ρ : ℕ → ℝ), Box.envMem ρ origB → (∀ i ≥ List.length origB, ρ i = 0) → ↑bestLB ≤ Core.Expr.eval ρ e) (hUB : ∃ (ρ : ℕ → ℝ), Box.envMem ρ origB ∧ (∀ i ≥ List.length origB, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑bestUB) (hQueueSub : ∀ (lb : ℚ) (B' : Box), (lb, B') ∈ queue → ∀ (ρ : ℕ → ℝ), Box.envMem ρ B' → Box.envMem ρ origB ∧ List.length B' = List.length origB) : (∀ (ρ : ℕ → ℝ), Box.envMem ρ origB → (∀ i ≥ List.length origB, ρ i = 0) → ↑bestLB' ≤ Core.Expr.eval ρ e) ∧ (∃ (ρ : ℕ → ℝ), Box.envMem ρ origB ∧ (∀ i ≥ List.length origB, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑bestUB') ∧ ∀ (lb : ℚ) (B' : Box), (lb, B') ∈ queue' → ∀ (ρ : ℕ → ℝ), Box.envMem ρ B' → Box.envMem ρ origB ∧ List.length B' = List.length origB

minimizeStep preserves the lower bound invariant. If bestLB ≤ f(ρ) for all ρ in origB before the step, then bestLB' ≤ f(ρ) for all ρ after.

theorem LeanCert.Engine.Optimization.minimizeLoop_correct (e : Core.Expr) (hsupp : ExprSupported e) (cfg : GlobalOptConfig) (origB : Box) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) (hLB : ∀ (ρ : ℕ → ℝ), Box.envMem ρ origB → (∀ i ≥ List.length origB, ρ i = 0) → ↑bestLB ≤ Core.Expr.eval ρ e) (hUB : ∃ (ρ : ℕ → ℝ), Box.envMem ρ origB ∧ (∀ i ≥ List.length origB, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑bestUB) (hQueueSub : ∀ (lb : ℚ) (B' : Box), (lb, B') ∈ queue → ∀ (ρ : ℕ → ℝ), Box.envMem ρ B' → Box.envMem ρ origB ∧ List.length B' = List.length origB) : have result := minimizeLoop e cfg queue bestLB bestUB bestBox iters; (∀ (ρ : ℕ → ℝ), Box.envMem ρ origB → (∀ i ≥ List.length origB, ρ i = 0) → ↑result.bound.lo ≤ Core.Expr.eval ρ e) ∧ ∃ (ρ : ℕ → ℝ), Box.envMem ρ origB ∧ (∀ i ≥ List.length origB, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑result.bound.hi

The main loop correctness theorem with explicit bestLB tracking

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

The key correctness theorem: globalMinimize returns a lower bound that is ≤ the minimum of f over any point in the original box.

theorem LeanCert.Engine.Optimization.globalMinimize_hi_achievable (e : Core.Expr) (hsupp : ExprSupported e) (B : Box) (cfg : GlobalOptConfig) : ∃ (ρ : ℕ → ℝ), Box.envMem ρ B ∧ (∀ i ≥ List.length B, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑(globalMinimize e B cfg).bound.hi

There exists a point achieving (approximately) the upper bound.

Correctness theorems for Core (computable) versions

theorem LeanCert.Engine.Optimization.evalOnBoxCore_lo_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfig) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) (hdom : evalDomainValid e B.toEnv { taylorDepth := cfg.taylorDepth }) : ↑(evalOnBoxCore e B cfg).lo ≤ Core.Expr.eval ρ e

The lower bound from core interval evaluation is correct.

theorem LeanCert.Engine.Optimization.evalOnBoxCore_hi_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfig) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) (hdom : evalDomainValid e B.toEnv { taylorDepth := cfg.taylorDepth }) : Core.Expr.eval ρ e ≤ ↑(evalOnBoxCore e B cfg).hi

The upper bound from core interval evaluation is correct.

theorem LeanCert.Engine.Optimization.minimizeStepCore_preserves_LB (e : Core.Expr) (hsupp : ExprSupportedCore e) (cfg : GlobalOptConfig) (origB : Box) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStepCore e cfg queue bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) (hLB : ∀ (ρ : ℕ → ℝ), Box.envMem ρ origB → (∀ i ≥ List.length origB, ρ i = 0) → ↑bestLB ≤ Core.Expr.eval ρ e) (hUB : ∃ (ρ : ℕ → ℝ), Box.envMem ρ origB ∧ (∀ i ≥ List.length origB, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑bestUB) (hQueueSub : ∀ (lb : ℚ) (B' : Box), (lb, B') ∈ queue → ∀ (ρ : ℕ → ℝ), Box.envMem ρ B' → Box.envMem ρ origB ∧ List.length B' = List.length origB) (hdom : ∀ (B' : Box), List.length B' = List.length origB → evalDomainValid e B'.toEnv { taylorDepth := cfg.taylorDepth }) : (∀ (ρ : ℕ → ℝ), Box.envMem ρ origB → (∀ i ≥ List.length origB, ρ i = 0) → ↑bestLB' ≤ Core.Expr.eval ρ e) ∧ (∃ (ρ : ℕ → ℝ), Box.envMem ρ origB ∧ (∀ i ≥ List.length origB, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑bestUB') ∧ ∀ (lb : ℚ) (B' : Box), (lb, B') ∈ queue' → ∀ (ρ : ℕ → ℝ), Box.envMem ρ B' → Box.envMem ρ origB ∧ List.length B' = List.length origB

minimizeStepCore preserves the lower bound invariant.

This version uses ExprSupportedCore with an explicit domain validity hypothesis for all boxes of the same length as origB. This is necessary because the branch-and-bound algorithm operates on sub-boxes that maintain the same length.

theorem LeanCert.Engine.Optimization.minimizeLoopCore_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (cfg : GlobalOptConfig) (origB : Box) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) (hLB : ∀ (ρ : ℕ → ℝ), Box.envMem ρ origB → (∀ i ≥ List.length origB, ρ i = 0) → ↑bestLB ≤ Core.Expr.eval ρ e) (hUB : ∃ (ρ : ℕ → ℝ), Box.envMem ρ origB ∧ (∀ i ≥ List.length origB, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑bestUB) (hQueueSub : ∀ (lb : ℚ) (B' : Box), (lb, B') ∈ queue → ∀ (ρ : ℕ → ℝ), Box.envMem ρ B' → Box.envMem ρ origB ∧ List.length B' = List.length origB) (hdom : ∀ (B' : Box), List.length B' = List.length origB → evalDomainValid e B'.toEnv { taylorDepth := cfg.taylorDepth }) : have result := minimizeLoopCore e cfg queue bestLB bestUB bestBox iters; (∀ (ρ : ℕ → ℝ), Box.envMem ρ origB → (∀ i ≥ List.length origB, ρ i = 0) → ↑result.bound.lo ≤ Core.Expr.eval ρ e) ∧ ∃ (ρ : ℕ → ℝ), Box.envMem ρ origB ∧ (∀ i ≥ List.length origB, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑result.bound.hi

The main loop correctness theorem for Core version

theorem LeanCert.Engine.Optimization.globalMinimizeCore_lo_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfig) (hdom : ∀ (B' : Box), List.length B' = List.length B → evalDomainValid e B'.toEnv { taylorDepth := cfg.taylorDepth }) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ↑(globalMinimizeCore e B cfg).bound.lo ≤ Core.Expr.eval ρ e

The key correctness theorem for Core version: globalMinimizeCore returns a lower bound that is ≤ the minimum of f over any point in the original box.

This theorem requires a domain validity hypothesis for ExprSupportedCore expressions. For ExprSupported expressions, use globalMinimizeCore_lo_correct_supported which derives domain validity automatically.

theorem LeanCert.Engine.Optimization.globalMinimizeCore_hi_achievable (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfig) (hdom : ∀ (B' : Box), List.length B' = List.length B → evalDomainValid e B'.toEnv { taylorDepth := cfg.taylorDepth }) : ∃ (ρ : ℕ → ℝ), Box.envMem ρ B ∧ (∀ i ≥ List.length B, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑(globalMinimizeCore e B cfg).bound.hi

There exists a point achieving (approximately) the upper bound for Core version.

theorem LeanCert.Engine.Optimization.globalMinimizeCore_lo_le_hi (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfig) (hdom : ∀ (B' : Box), List.length B' = List.length B → evalDomainValid e B'.toEnv { taylorDepth := cfg.taylorDepth }) : (globalMinimizeCore e B cfg).bound.lo ≤ (globalMinimizeCore e B cfg).bound.hi

The lower bound is ≤ the upper bound. This follows from the existence of a witness: there's some ρ with f(ρ) ≤ hi, and lo ≤ f(ρ) for all ρ in B, so lo ≤ f(witness) ≤ hi.

Maximization correctness theorems

theorem LeanCert.Engine.Optimization.globalMaximizeCore_hi_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfig) (hdom : ∀ (B' : Box), List.length B' = List.length B → evalDomainValid e B'.toEnv { taylorDepth := cfg.taylorDepth }) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → Core.Expr.eval ρ e ≤ ↑(globalMaximizeCore e B cfg).bound.hi

The upper bound from globalMaximizeCore is correct: f(ρ) ≤ hi for all ρ in B.

theorem LeanCert.Engine.Optimization.globalMaximizeCore_lo_achievable (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfig) (hdom : ∀ (B' : Box), List.length B' = List.length B → evalDomainValid e B'.toEnv { taylorDepth := cfg.taylorDepth }) : ∃ (ρ : ℕ → ℝ), Box.envMem ρ B ∧ (∀ i ≥ List.length B, ρ i = 0) ∧ ↑(globalMaximizeCore e B cfg).bound.lo ≤ Core.Expr.eval ρ e

There exists a point achieving approximately the lower bound for maximization.

theorem LeanCert.Engine.Optimization.globalMaximizeCore_lo_le_hi (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfig) (hdom : ∀ (B' : Box), List.length B' = List.length B → evalDomainValid e B'.toEnv { taylorDepth := cfg.taylorDepth }) : (globalMaximizeCore e B cfg).bound.lo ≤ (globalMaximizeCore e B cfg).bound.hi

The lower bound is ≤ the upper bound for maximization.

Dyadic backend versions for high-performance optimization

These variants use Dyadic arithmetic (n * 2^e) instead of rationals, preventing denominator explosion for deep expressions. 10-100x faster for complex expressions like neural networks.

structure LeanCert.Engine.Optimization.GlobalOptConfigDyadic : Type

Configuration for Dyadic global optimization

• maxIterations : ℕ

  Maximum number of subdivisions

• tolerance : ℚ

  Stop when box width is below this threshold

• useMonotonicity : Bool

  Use monotonicity pruning (requires gradient computation)

• taylorDepth : ℕ

  Taylor depth for interval evaluation

• precision : ℤ

  Dyadic precision (minimum exponent for outward rounding)

instance LeanCert.Engine.Optimization.instReprGlobalOptConfigDyadic : Repr GlobalOptConfigDyadic

Equations

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

def LeanCert.Engine.Optimization.instReprGlobalOptConfigDyadic.repr : GlobalOptConfigDyadic → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.Optimization.instInhabitedGlobalOptConfigDyadic : Inhabited GlobalOptConfigDyadic

Equations

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

def LeanCert.Engine.Optimization.evalOnBoxDyadic (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigDyadic) : Core.IntervalRat

Evaluate expression on a box using Dyadic arithmetic

Equations

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

def LeanCert.Engine.Optimization.minimizeStepDyadic (e : Core.Expr) (cfg : GlobalOptConfigDyadic) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) : Option (List (ℚ × Box) × ℚ × ℚ × Box)

One step of branch-and-bound using Dyadic arithmetic

Equations

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

def LeanCert.Engine.Optimization.minimizeLoopDyadic (e : Core.Expr) (cfg : GlobalOptConfigDyadic) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) : GlobalResult

Run branch-and-bound loop using Dyadic arithmetic

Equations

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

theorem LeanCert.Engine.Optimization.minimizeStepDyadic_bestLB_le (e : Core.Expr) (cfg : GlobalOptConfigDyadic) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStepDyadic e cfg queue bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) : bestLB' ≤ bestLB

Helper: bestLB only decreases during minimizeStepDyadic.

theorem LeanCert.Engine.Optimization.minimizeLoopDyadic_bestLB_le (e : Core.Expr) (cfg : GlobalOptConfigDyadic) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) : (minimizeLoopDyadic e cfg queue bestLB bestUB bestBox iters).bound.lo ≤ bestLB

Helper: minimizeLoopDyadic preserves the initial lower bound.

def LeanCert.Engine.Optimization.globalMinimizeDyadic (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigDyadic := { }) : GlobalResult

Global minimization using Dyadic arithmetic

Equations

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

def LeanCert.Engine.Optimization.globalMaximizeDyadic (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigDyadic := { }) : GlobalResult

Global maximization using Dyadic arithmetic

Equations

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

Affine backend versions for tight bounds

These variants use Affine Arithmetic to track correlations between variables, solving the "dependency problem" in interval arithmetic. For example:

• Interval: x - x on [-1, 1] gives [-2, 2]
• Affine: x - x on [-1, 1] gives [0, 0] (exact!)

structure LeanCert.Engine.Optimization.GlobalOptConfigAffine : Type

Configuration for Affine global optimization

• maxIterations : ℕ

  Maximum number of subdivisions

• tolerance : ℚ

  Stop when box width is below this threshold

• useMonotonicity : Bool

  Use monotonicity pruning (requires gradient computation)

• taylorDepth : ℕ

  Taylor depth for interval evaluation

• maxNoiseSymbols : ℕ

  Max noise symbols before consolidation (0 = no limit)

instance LeanCert.Engine.Optimization.instReprGlobalOptConfigAffine : Repr GlobalOptConfigAffine

Equations

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

def LeanCert.Engine.Optimization.instReprGlobalOptConfigAffine.repr : GlobalOptConfigAffine → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.Optimization.instInhabitedGlobalOptConfigAffine : Inhabited GlobalOptConfigAffine

Equations

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

def LeanCert.Engine.Optimization.evalOnBoxAffine (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigAffine) : Core.IntervalRat

Evaluate expression on a box using Affine arithmetic

Equations

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

def LeanCert.Engine.Optimization.minimizeStepAffine (e : Core.Expr) (cfg : GlobalOptConfigAffine) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) : Option (List (ℚ × Box) × ℚ × ℚ × Box)

One step of branch-and-bound using Affine arithmetic

Equations

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

def LeanCert.Engine.Optimization.minimizeLoopAffine (e : Core.Expr) (cfg : GlobalOptConfigAffine) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) : GlobalResult

Run branch-and-bound loop using Affine arithmetic

Equations

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

theorem LeanCert.Engine.Optimization.minimizeStepAffine_bestLB_le (e : Core.Expr) (cfg : GlobalOptConfigAffine) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStepAffine e cfg queue bestLB bestUB bestBox = some (queue', bestLB', bestUB', bestBox')) : bestLB' ≤ bestLB

Helper: bestLB only decreases during minimizeStepAffine.

theorem LeanCert.Engine.Optimization.minimizeLoopAffine_bestLB_le (e : Core.Expr) (cfg : GlobalOptConfigAffine) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) : (minimizeLoopAffine e cfg queue bestLB bestUB bestBox iters).bound.lo ≤ bestLB

Helper: minimizeLoopAffine preserves the initial lower bound.

def LeanCert.Engine.Optimization.globalMinimizeAffine (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigAffine := { }) : GlobalResult

Global minimization using Affine arithmetic

Equations

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

def LeanCert.Engine.Optimization.globalMaximizeAffine (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigAffine := { }) : GlobalResult

Global maximization using Affine arithmetic

Equations

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

Correctness theorems for Dyadic optimization

theorem LeanCert.Engine.Optimization.evalOnBoxDyadic_lo_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfigDyadic) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) (hprec : cfg.precision ≤ 0 := by norm_num) (hdom : evalDomainValidDyadic e (fun (i : ℕ) => Core.IntervalDyadic.ofIntervalRat (List.getD B i (Core.IntervalRat.singleton 0)) cfg.precision) { precision := cfg.precision, taylorDepth := cfg.taylorDepth }) : ↑(evalOnBoxDyadic e B cfg).lo ≤ Core.Expr.eval ρ e

The lower bound from Dyadic interval evaluation is correct.

The proof uses evalIntervalDyadic_correct and IntervalDyadic.toIntervalRat_correct to show that the true value is contained in the resulting rational interval.

Note: Requires domain validity for expressions with log.

theorem LeanCert.Engine.Optimization.globalMinimizeDyadic_lo_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfigDyadic) (hprec : cfg.precision ≤ 0 := by norm_num) (hdom : evalDomainValidDyadic e (fun (i : ℕ) => Core.IntervalDyadic.ofIntervalRat (List.getD B i (Core.IntervalRat.singleton 0)) cfg.precision) { precision := cfg.precision, taylorDepth := cfg.taylorDepth }) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ↑(globalMinimizeDyadic e B cfg).bound.lo ≤ Core.Expr.eval ρ e

The key correctness theorem for Dyadic minimization: globalMinimizeDyadic returns a lower bound that is ≤ the minimum of f over any point in the original box.

Note: Requires domain validity for expressions with log.

theorem LeanCert.Engine.Optimization.globalMaximizeDyadic_hi_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfigDyadic) (hprec : cfg.precision ≤ 0 := by norm_num) (hdom : evalDomainValidDyadic e (fun (i : ℕ) => Core.IntervalDyadic.ofIntervalRat (List.getD B i (Core.IntervalRat.singleton 0)) cfg.precision) { precision := cfg.precision, taylorDepth := cfg.taylorDepth }) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → Core.Expr.eval ρ e ≤ ↑(globalMaximizeDyadic e B cfg).bound.hi

The upper bound from globalMaximizeDyadic is correct: f(ρ) ≤ hi for all ρ in B.

Note: Requires domain validity for expressions with log.

Correctness theorems for Affine optimization

theorem LeanCert.Engine.Optimization.evalOnBoxAffine_lo_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfigAffine) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) (hdom : evalDomainValidAffine e (toAffineEnv B) { taylorDepth := cfg.taylorDepth, maxNoiseSymbols := cfg.maxNoiseSymbols }) : ↑(evalOnBoxAffine e B cfg).lo ≤ Core.Expr.eval ρ e

The lower bound from Affine interval evaluation is correct. Note: Requires ExprSupportedCore, valid noise assignment, and domain validity for log.

theorem LeanCert.Engine.Optimization.globalMinimizeAffine_lo_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfigAffine) (hdom : evalDomainValidAffine e (toAffineEnv B) { taylorDepth := cfg.taylorDepth, maxNoiseSymbols := cfg.maxNoiseSymbols }) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ↑(globalMinimizeAffine e B cfg).bound.lo ≤ Core.Expr.eval ρ e

The key correctness theorem for Affine minimization.

Note: Requires domain validity for expressions with log.

theorem LeanCert.Engine.Optimization.globalMaximizeAffine_hi_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (B : Box) (cfg : GlobalOptConfigAffine) (hdom : evalDomainValidAffine e (toAffineEnv B) { taylorDepth := cfg.taylorDepth, maxNoiseSymbols := cfg.maxNoiseSymbols }) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → Core.Expr.eval ρ e ≤ ↑(globalMaximizeAffine e B cfg).bound.hi

The upper bound from globalMaximizeAffine is correct.

Note: Requires domain validity for expressions with log.