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

instance LeanCert.Engine.Optimization.instReprGlobalOptConfig : Repr GlobalOptConfig

Equations

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

@[instance_reducible]

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

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

Equations

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

@[instance_reducible]

instance LeanCert.Engine.Optimization.instReprGlobalBound : Repr GlobalBound

Equations

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

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)

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

Equations

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

@[instance_reducible]

instance LeanCert.Engine.Optimization.instReprGlobalResult : Repr GlobalResult

Equations

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

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

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

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) (hsupp : ADSupported e) (B : Box) (_cfg : GlobalOptConfig) : Core.IntervalRat

Evaluate expression on a box and get interval bounds

Equations

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

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

One step of branch-and-bound for minimization with explicit global-safe lower bound 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) (hsupp : ADSupported e) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (iters : ℕ) : GlobalResult

Run branch-and-bound for a fixed number of iterations with explicit global-safe lower bound tracking.

Equations

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

noncomputable def LeanCert.Engine.Optimization.globalMinimize (e : Core.Expr) (hsupp : ADSupported e) (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) (hsupp : ADSupported e) (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.Internal.Rational.evalTotalCore 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.

Correctness theorems

theorem LeanCert.Engine.Optimization.evalOnBox_lo_correct (e : Core.Expr) (hsupp : ADSupported e) (B : Box) (cfg : GlobalOptConfig) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) : ↑(evalOnBox e hsupp 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 : ADSupported e) (B : Box) (cfg : GlobalOptConfig) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) : Core.Expr.eval ρ e ≤ ↑(evalOnBox e hsupp 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.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

Simplified correctness architecture with explicit global-safe lower bound tracking

The key idea: track both bestLB (a global-safe lower bound, not necessarily the tightest active-queue lower bound) and bestUB (a global upper-bound witness) 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) (hsupp : ADSupported e) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) : ∃ (result : List (ℚ × Box) × ℚ × ℚ × Box), minimizeStep e hsupp 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) (hsupp : ADSupported e) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e hsupp 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) (hsupp : ADSupported e) (cfg : GlobalOptConfig) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e hsupp 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) (hsupp : ADSupported e) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e hsupp 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) (hsupp : ADSupported e) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e hsupp 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) (hsupp : ADSupported e) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e hsupp 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 : ADSupported e) (cfg : GlobalOptConfig) (hd : ℚ × Box) (tl : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e hsupp 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_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 : ADSupported e) (cfg : GlobalOptConfig) (origB : Box) (queue : List (ℚ × Box)) (bestLB bestUB : ℚ) (bestBox : Box) (queue' : List (ℚ × Box)) (bestLB' bestUB' : ℚ) (bestBox' : Box) (hStep : minimizeStep e hsupp 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 : ADSupported 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 hsupp 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 : ADSupported e) (B : Box) (cfg : GlobalOptConfig) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ↑(globalMinimize e hsupp 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 : ADSupported e) (B : Box) (cfg : GlobalOptConfig) : ∃ (ρ : ℕ → ℝ), Box.envMem ρ B ∧ (∀ i ≥ List.length B, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑(globalMinimize e hsupp 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 ADSupported 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_reducible]

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

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

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

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.

Checked branch-and-bound

These entry points never consume a finite fallback from a legacy evaluator. Domain failures are propagated to the caller. Optional monotonicity pruning is implemented through a checked computable-AD pre-pass; unsupported derivative expressions use the identity pruner.

theorem LeanCert.Engine.Optimization.Box.envMem_splitWidest_cases (B : Box) (rho : ℕ → ℝ) (hrho : envMem rho B) : envMem rho B.splitWidest.1 ∨ envMem rho B.splitWidest.2

theorem LeanCert.Engine.Optimization.Box.splitWidest_fst_length (B : Box) : List.length B.splitWidest.1 = List.length B

theorem LeanCert.Engine.Optimization.Box.splitWidest_snd_length (B : Box) : List.length B.splitWidest.2 = List.length B

def LeanCert.Engine.Optimization.minimumStoredBound (fallback : ℚ) : List (ℚ × Box) → ℚ

Minimum lower endpoint stored in a collection of bounded boxes. The fallback is used only for an empty internal state.

Equations

• LeanCert.Engine.Optimization.minimumStoredBound fallback [] = fallback
• LeanCert.Engine.Optimization.minimumStoredBound fallback [entry] = entry.1
• LeanCert.Engine.Optimization.minimumStoredBound fallback (entry :: next :: rest) = min entry.1 (LeanCert.Engine.Optimization.minimumStoredBound fallback (next :: rest))

theorem LeanCert.Engine.Optimization.minimumStoredBound_le_of_mem (fallback : ℚ) (boxes : List (ℚ × Box)) (entry : ℚ × Box) (hentry : entry ∈ boxes) : minimumStoredBound fallback boxes ≤ entry.1

def LeanCert.Engine.Optimization.minimizeStepCheckedWith (evalBox : Box → EvalResult Core.IntervalRat) (pruneBox : Box → Box) (tolerance : ℚ) (queue finished : List (ℚ × Box)) (bestUB : ℚ) (bestBox : Box) : EvalResult (Option (List (ℚ × Box) × List (ℚ × Box) × ℚ × Box))

One backend-independent checked branch-and-bound step.

finished stores terminal boxes. Keeping their local lower bounds separate from the active queue lets the global lower bound rise as the active partition is refined; the former implementation retained the root lower bound forever.

Equations

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

def LeanCert.Engine.Optimization.CheckedLowerInvariant (value : (ℕ → ℝ) → ℝ) (original : Box) (queue finished : List (ℚ × Box)) : Prop

Every point of the original box is represented by a current partition cell whose stored lower endpoint is valid for that point.

Equations

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

theorem LeanCert.Engine.Optimization.minimizeStepCheckedWith_preserves_lower (evalBox : Box → EvalResult Core.IntervalRat) (pruneBox : Box → Box) (tolerance : ℚ) (value : (ℕ → ℝ) → ℝ) (original : Box) (queue finished : List (ℚ × Box)) (bestUB : ℚ) (bestBox : Box) (queue' finished' : List (ℚ × Box)) (bestUB' : ℚ) (bestBox' : Box) (hevalSound : ∀ (B : Box) (I : Core.IntervalRat), evalBox B = Except.ok I → List.length B = List.length original → ∀ (rho : ℕ → ℝ), Box.envMem rho B → (∀ i ≥ List.length original, rho i = 0) → ↑I.lo ≤ value rho) (hpruneSound : ∀ (B : Box), List.length B = List.length original → ∀ (rho : ℕ → ℝ), Box.envMem rho B → (∀ i ≥ List.length original, rho i = 0) → ∃ (rho' : ℕ → ℝ), Box.envMem rho' (pruneBox B) ∧ (∀ i ≥ List.length original, rho' i = 0) ∧ List.length (pruneBox B) = List.length original ∧ value rho' ≤ value rho) (hinv : CheckedLowerInvariant value original queue finished) (hstep : minimizeStepCheckedWith evalBox pruneBox tolerance queue finished bestUB bestBox = Except.ok (some (queue', finished', bestUB', bestBox'))) : CheckedLowerInvariant value original queue' finished'

def LeanCert.Engine.Optimization.minimizeLoopCheckedWith (evalBox : Box → EvalResult Core.IntervalRat) (pruneBox : Box → Box) (maxIterations : ℕ) (tolerance fallbackLB : ℚ) (queue finished : List (ℚ × Box)) (bestUB : ℚ) (bestBox : Box) : ℕ → EvalResult GlobalResult

Checked branch-and-bound loop.

Equations

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

theorem LeanCert.Engine.Optimization.minimizeStepCheckedWith_eq_ok_none_iff (evalBox : Box → EvalResult Core.IntervalRat) (pruneBox : Box → Box) (tolerance : ℚ) (queue finished : List (ℚ × Box)) (bestUB : ℚ) (bestBox : Box) : minimizeStepCheckedWith evalBox pruneBox tolerance queue finished bestUB bestBox = Except.ok none ↔ queue = []

theorem LeanCert.Engine.Optimization.CheckedLowerInvariant.minimumStoredBound_correct (value : (ℕ → ℝ) → ℝ) (original : Box) (queue finished : List (ℚ × Box)) (fallback : ℚ) (hinv : CheckedLowerInvariant value original queue finished) (rho : ℕ → ℝ) (hrho : Box.envMem rho original) (hzero : ∀ i ≥ List.length original, rho i = 0) : ↑(minimumStoredBound fallback (finished ++ queue)) ≤ value rho

theorem LeanCert.Engine.Optimization.minimizeLoopCheckedWith_lower_correct (evalBox : Box → EvalResult Core.IntervalRat) (pruneBox : Box → Box) (maxIterations : ℕ) (tolerance fallbackLB : ℚ) (value : (ℕ → ℝ) → ℝ) (original : Box) (hevalSound : ∀ (B : Box) (I : Core.IntervalRat), evalBox B = Except.ok I → List.length B = List.length original → ∀ (rho : ℕ → ℝ), Box.envMem rho B → (∀ i ≥ List.length original, rho i = 0) → ↑I.lo ≤ value rho) : (∀ (B : Box), List.length B = List.length original → ∀ (rho : ℕ → ℝ), Box.envMem rho B → (∀ i ≥ List.length original, rho i = 0) → ∃ (rho' : ℕ → ℝ), Box.envMem rho' (pruneBox B) ∧ (∀ i ≥ List.length original, rho' i = 0) ∧ List.length (pruneBox B) = List.length original ∧ value rho' ≤ value rho) → ∀ (iters : ℕ) (queue finished : List (ℚ × Box)) (bestUB : ℚ) (bestBox : Box) (result : GlobalResult), CheckedLowerInvariant value original queue finished → minimizeLoopCheckedWith evalBox pruneBox maxIterations tolerance fallbackLB queue finished bestUB bestBox iters = Except.ok result → ∀ (rho : ℕ → ℝ), Box.envMem rho original → (∀ i ≥ List.length original, rho i = 0) → ↑result.bound.lo ≤ value rho

def LeanCert.Engine.Optimization.checkedMonotonicityPruner (e : Core.Expr) (enabled : Bool) (cfg : EvalConfig) : Box → Box

Checked minimization parameterized by a sound finite-enclosure backend.

Equations

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

theorem LeanCert.Engine.Optimization.checkedMonotonicityPruner_correct (e : Core.Expr) (enabled : Bool) (cfg : EvalConfig) (B : Box) (rho : ℕ → ℝ) : Box.envMem rho B → (∀ i ≥ List.length B, rho i = 0) → ∃ (rho' : ℕ → ℝ), Box.envMem rho' (checkedMonotonicityPruner e enabled cfg B) ∧ (∀ i ≥ List.length B, rho' i = 0) ∧ List.length (checkedMonotonicityPruner e enabled cfg B) = List.length B ∧ Core.Expr.eval rho' e ≤ Core.Expr.eval rho e

theorem LeanCert.Engine.Optimization.checkedMonotonicityPruner_correct_of_length (e : Core.Expr) (enabled : Bool) (cfg : EvalConfig) (original B : Box) (hlen : List.length B = List.length original) (rho : ℕ → ℝ) (hrho : Box.envMem rho B) (hzero : ∀ i ≥ List.length original, rho i = 0) : ∃ (rho' : ℕ → ℝ), Box.envMem rho' (checkedMonotonicityPruner e enabled cfg B) ∧ (∀ i ≥ List.length original, rho' i = 0) ∧ List.length (checkedMonotonicityPruner e enabled cfg B) = List.length original ∧ Core.Expr.eval rho' e ≤ Core.Expr.eval rho e

def LeanCert.Engine.Optimization.globalMinimizeCheckedWith (evalBox : Box → EvalResult Core.IntervalRat) (pruneBox : Box → Box) (B : Box) (maxIterations : ℕ) (tolerance : ℚ) : EvalResult GlobalResult

Equations

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

theorem LeanCert.Engine.Optimization.globalMinimizeCheckedWith_lower_correct (evalBox : Box → EvalResult Core.IntervalRat) (pruneBox : Box → Box) (B : Box) (maxIterations : ℕ) (tolerance : ℚ) (value : (ℕ → ℝ) → ℝ) (hevalSound : ∀ (box : Box) (I : Core.IntervalRat), evalBox box = Except.ok I → List.length box = List.length B → ∀ (rho : ℕ → ℝ), Box.envMem rho box → (∀ i ≥ List.length B, rho i = 0) → ↑I.lo ≤ value rho) (hpruneSound : ∀ (box : Box), List.length box = List.length B → ∀ (rho : ℕ → ℝ), Box.envMem rho box → (∀ i ≥ List.length B, rho i = 0) → ∃ (rho' : ℕ → ℝ), Box.envMem rho' (pruneBox box) ∧ (∀ i ≥ List.length B, rho' i = 0) ∧ List.length (pruneBox box) = List.length B ∧ value rho' ≤ value rho) (result : GlobalResult) (hsuccess : globalMinimizeCheckedWith evalBox pruneBox B maxIterations tolerance = Except.ok result) (rho : ℕ → ℝ) : Box.envMem rho B → (∀ i ≥ List.length B, rho i = 0) → ↑result.bound.lo ≤ value rho

def LeanCert.Engine.Optimization.globalMaximizeCheckedWith (evalBox : Core.Expr → Box → EvalResult Core.IntervalRat) (pruneBox : Core.Expr → Box → Box) (e : Core.Expr) (B : Box) (maxIterations : ℕ) (tolerance : ℚ) : EvalResult GlobalResult

Checked maximization parameterized by a sound finite-enclosure backend.

Equations

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

theorem LeanCert.Engine.Optimization.globalMaximizeCheckedWith_upper_correct (evalBox : Core.Expr → Box → EvalResult Core.IntervalRat) (pruneBox : Core.Expr → Box → Box) (e : Core.Expr) (B : Box) (maxIterations : ℕ) (tolerance : ℚ) (hevalSound : ∀ (box : Box) (I : Core.IntervalRat), evalBox e.neg box = Except.ok I → List.length box = List.length B → ∀ (rho : ℕ → ℝ), Box.envMem rho box → (∀ i ≥ List.length B, rho i = 0) → ↑I.lo ≤ Core.Expr.eval rho e.neg) (hpruneSound : ∀ (box : Box), List.length box = List.length B → ∀ (rho : ℕ → ℝ), Box.envMem rho box → (∀ i ≥ List.length B, rho i = 0) → ∃ (rho' : ℕ → ℝ), Box.envMem rho' (pruneBox e.neg box) ∧ (∀ i ≥ List.length B, rho' i = 0) ∧ List.length (pruneBox e.neg box) = List.length B ∧ Core.Expr.eval rho' e.neg ≤ Core.Expr.eval rho e.neg) (result : GlobalResult) (hsuccess : globalMaximizeCheckedWith evalBox pruneBox e B maxIterations tolerance = Except.ok result) (rho : ℕ → ℝ) : Box.envMem rho B → (∀ i ≥ List.length B, rho i = 0) → Core.Expr.eval rho e ≤ ↑result.bound.hi

def LeanCert.Engine.Optimization.evalOnBoxRationalChecked (e : Core.Expr) (B : Box) : EvalResult Core.IntervalRat

Checked rational evaluation on a box.

Equations

• LeanCert.Engine.Optimization.evalOnBoxRationalChecked e B = LeanCert.Engine.evalIntervalChecked e B.toEnv

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

Equations

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

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

Equations

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

theorem LeanCert.Engine.Optimization.evalOnBoxRationalChecked_lo_correct (e : Core.Expr) (B : Box) (I : Core.IntervalRat) (hsuccess : evalOnBoxRationalChecked e B = Except.ok I) (rho : ℕ → ℝ) (hrho : Box.envMem rho B) (hzero : ∀ i ≥ List.length B, rho i = 0) : ↑I.lo ≤ Core.Expr.eval rho e

theorem LeanCert.Engine.Optimization.globalMinimizeRationalChecked_lo_correct (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig) (result : GlobalResult) (hsuccess : globalMinimizeRationalChecked e B cfg = Except.ok result) (rho : ℕ → ℝ) : Box.envMem rho B → (∀ i ≥ List.length B, rho i = 0) → ↑result.bound.lo ≤ Core.Expr.eval rho e

theorem LeanCert.Engine.Optimization.globalMaximizeRationalChecked_hi_correct (e : Core.Expr) (B : Box) (cfg : GlobalOptConfig) (result : GlobalResult) (hsuccess : globalMaximizeRationalChecked e B cfg = Except.ok result) (rho : ℕ → ℝ) : Box.envMem rho B → (∀ i ≥ List.length B, rho i = 0) → Core.Expr.eval rho e ≤ ↑result.bound.hi

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

Checked Dyadic evaluation on a box.

Equations

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

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

Equations

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

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

Equations

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

theorem LeanCert.Engine.Optimization.evalOnBoxDyadicChecked_lo_correct (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigDyadic) (hprec : cfg.precision ≤ 0) (I : Core.IntervalRat) (hsuccess : evalOnBoxDyadicChecked e B cfg = Except.ok I) (rho : ℕ → ℝ) (hrho : Box.envMem rho B) (hzero : ∀ i ≥ List.length B, rho i = 0) : ↑I.lo ≤ Core.Expr.eval rho e

theorem LeanCert.Engine.Optimization.globalMinimizeDyadicChecked_lo_correct (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigDyadic) (hprec : cfg.precision ≤ 0) (result : GlobalResult) (hsuccess : globalMinimizeDyadicChecked e B cfg = Except.ok result) (rho : ℕ → ℝ) : Box.envMem rho B → (∀ i ≥ List.length B, rho i = 0) → ↑result.bound.lo ≤ Core.Expr.eval rho e

theorem LeanCert.Engine.Optimization.globalMaximizeDyadicChecked_hi_correct (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigDyadic) (hprec : cfg.precision ≤ 0) (result : GlobalResult) (hsuccess : globalMaximizeDyadicChecked e B cfg = Except.ok result) (rho : ℕ → ℝ) : Box.envMem rho B → (∀ i ≥ List.length B, rho i = 0) → Core.Expr.eval rho e ≤ ↑result.bound.hi

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

Checked affine evaluation on a box.

Equations

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

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

Equations

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

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

Equations

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

theorem LeanCert.Engine.Optimization.evalOnBoxAffineChecked_lo_correct (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigAffine) (I : Core.IntervalRat) (hsuccess : evalOnBoxAffineChecked e B cfg = Except.ok I) (rho : ℕ → ℝ) (hrho : Box.envMem rho B) (hzero : ∀ i ≥ List.length B, rho i = 0) : ↑I.lo ≤ Core.Expr.eval rho e

theorem LeanCert.Engine.Optimization.globalMinimizeAffineChecked_lo_correct (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigAffine) (result : GlobalResult) (hsuccess : globalMinimizeAffineChecked e B cfg = Except.ok result) (rho : ℕ → ℝ) : Box.envMem rho B → (∀ i ≥ List.length B, rho i = 0) → ↑result.bound.lo ≤ Core.Expr.eval rho e

theorem LeanCert.Engine.Optimization.globalMaximizeAffineChecked_hi_correct (e : Core.Expr) (B : Box) (cfg : GlobalOptConfigAffine) (result : GlobalResult) (hsuccess : globalMaximizeAffineChecked e B cfg = Except.ok result) (rho : ℕ → ℝ) : Box.envMem rho B → (∀ i ≥ List.length B, rho i = 0) → Core.Expr.eval rho e ≤ ↑result.bound.hi