Discovery Mode: Proof-Carrying Result Types

This module defines structures that bundle computed results with their semantic proofs. These are the foundation of "Discovery Mode" - finding and certifying answers automatically.

Main Definitions

• VerifiedGlobalMin - A global minimum bound with proof
• VerifiedGlobalMax - A global maximum bound with proof
• VerifiedRoot - An isolating interval with existence proof
• UniqueVerifiedRoot - An isolating interval with uniqueness proof
• VerifiedIntegral - Integral bounds with containment proof

Design Philosophy

Each structure contains:

1. Data: The computed numerical result (bounds, intervals, etc.)
2. Witness: Location information (which box/interval contains the extremum)
3. Proof: A Lean proof term establishing the semantic correctness

The proofs use the "Golden Theorems" from Certificate.lean applied to computationally verified certificates.

Configuration

structure LeanCert.Validity.DiscoveryConfig : Type

Configuration for discovery operations

• maxIterations : ℕ

  Maximum iterations for optimization

• tolerance : ℚ

  Tolerance for convergence

• taylorDepth : ℕ

  Taylor expansion depth

• useMonotonicity : Bool

  Use monotonicity pruning

• maxBisectionDepth : ℕ

  Maximum depth for root finding bisection

def LeanCert.Validity.instReprDiscoveryConfig.repr : DiscoveryConfig → ℕ → Std.Format

Equations

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

instance LeanCert.Validity.instReprDiscoveryConfig : Repr DiscoveryConfig

Equations

• LeanCert.Validity.instReprDiscoveryConfig = { reprPrec := LeanCert.Validity.instReprDiscoveryConfig.repr }

def LeanCert.Validity.instInhabitedDiscoveryConfig.default : DiscoveryConfig

Equations

• LeanCert.Validity.instInhabitedDiscoveryConfig.default = { maxIterations := default, tolerance := default, taylorDepth := default, useMonotonicity := default, maxBisectionDepth := default }

instance LeanCert.Validity.instInhabitedDiscoveryConfig : Inhabited DiscoveryConfig

Equations

• LeanCert.Validity.instInhabitedDiscoveryConfig = { default := LeanCert.Validity.instInhabitedDiscoveryConfig.default }

def LeanCert.Validity.DiscoveryConfig.toGlobalOptConfig (cfg : DiscoveryConfig) : Engine.Optimization.GlobalOptConfig

Convert to GlobalOptConfig

Equations

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

def LeanCert.Validity.DiscoveryConfig.toEvalConfig (cfg : DiscoveryConfig) : Engine.EvalConfig

Convert to EvalConfig

Equations

• cfg.toEvalConfig = { taylorDepth := cfg.taylorDepth }

Global Minimum

structure LeanCert.Validity.VerifiedGlobalMin (expr : Core.Expr) (domain : Engine.Optimization.Box) : Type

A verified global minimum bound.

This structure bundles:

• The computed lower bound bound
• The best box minimizerBox containing a near-minimizer
• A proof that bound ≤ f(x) for all x in the domain

The proof establishes: ∀ ρ, Box.envMem ρ domain → (∀ i ≥ domain.length, ρ i = 0) → bound ≤ Expr.eval ρ expr

• bound : ℚ

  The verified lower bound

• upperBound : ℚ

  Upper bound on the minimum (for convergence info)

• minimizerBox : Engine.Optimization.Box

  Box containing a near-minimizer

• iterations : ℕ

  Number of iterations used

• is_lower_bound (ρ : ℕ → ℝ) : Engine.Optimization.Box.envMem ρ domain → (∀ i ≥ List.length domain, ρ i = 0) → ↑self.bound ≤ Core.Expr.eval ρ expr

  Proof that bound is a valid lower bound

def LeanCert.Validity.VerifiedGlobalMin.width {expr : Core.Expr} {domain : Engine.Optimization.Box} (v : VerifiedGlobalMin expr domain) : ℚ

Width of the bound interval

Equations

• v.width = v.upperBound - v.bound

def LeanCert.Validity.VerifiedGlobalMin.isTight {expr : Core.Expr} {domain : Engine.Optimization.Box} (v : VerifiedGlobalMin expr domain) (tol : ℚ) : Bool

Check if the bound is tight within tolerance

Equations

• v.isTight tol = decide (v.width ≤ tol)

Global Maximum

structure LeanCert.Validity.VerifiedGlobalMax (expr : Core.Expr) (domain : Engine.Optimization.Box) : Type

A verified global maximum bound.

This structure bundles:

• The computed upper bound bound
• The best box maximizerBox containing a near-maximizer
• A proof that f(x) ≤ bound for all x in the domain

• bound : ℚ

  The verified upper bound

• lowerBound : ℚ

  Lower bound on the maximum (for convergence info)

• maximizerBox : Engine.Optimization.Box

  Box containing a near-maximizer

• iterations : ℕ

  Number of iterations used

• is_upper_bound (ρ : ℕ → ℝ) : Engine.Optimization.Box.envMem ρ domain → (∀ i ≥ List.length domain, ρ i = 0) → Core.Expr.eval ρ expr ≤ ↑self.bound

  Proof that bound is a valid upper bound

def LeanCert.Validity.VerifiedGlobalMax.width {expr : Core.Expr} {domain : Engine.Optimization.Box} (v : VerifiedGlobalMax expr domain) : ℚ

Width of the bound interval

Equations

• v.width = v.bound - v.lowerBound

Root Finding

inductive LeanCert.Validity.VerifiedRootStatus : Type

Status of a verified root

• exists_root : VerifiedRootStatus

  Root exists (sign change detected)

• unique_root : VerifiedRootStatus

  Unique root (Newton contraction verified)

instance LeanCert.Validity.instReprVerifiedRootStatus : Repr VerifiedRootStatus

Equations

• LeanCert.Validity.instReprVerifiedRootStatus = { reprPrec := LeanCert.Validity.instReprVerifiedRootStatus.repr }

def LeanCert.Validity.instReprVerifiedRootStatus.repr : VerifiedRootStatus → ℕ → Std.Format

Equations

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

instance LeanCert.Validity.instDecidableEqVerifiedRootStatus : DecidableEq VerifiedRootStatus

Equations

• LeanCert.Validity.instDecidableEqVerifiedRootStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance LeanCert.Validity.instInhabitedVerifiedRootStatus : Inhabited VerifiedRootStatus

Equations

• LeanCert.Validity.instInhabitedVerifiedRootStatus = { default := LeanCert.Validity.instInhabitedVerifiedRootStatus.default }

def LeanCert.Validity.instInhabitedVerifiedRootStatus.default : VerifiedRootStatus

Equations

• LeanCert.Validity.instInhabitedVerifiedRootStatus.default = LeanCert.Validity.VerifiedRootStatus.exists_root

structure LeanCert.Validity.VerifiedRoot (expr : Core.Expr) : Type

A verified root of an expression.

This structure bundles:

• An isolating interval interval containing a root
• The status (existence vs uniqueness)
• A proof that there exists x ∈ interval with f(x) = 0

• interval : Core.IntervalRat

  Isolating interval containing the root

• status : VerifiedRootStatus

  Status: existence or uniqueness

• exists_root : ∃ x ∈ self.interval, Core.Expr.eval (fun (x_1 : ℕ) => x) expr = 0

  Proof of root existence

def LeanCert.Validity.VerifiedRoot.approxLocation {expr : Core.Expr} (v : VerifiedRoot expr) : ℚ

Approximate location of the root (midpoint)

Equations

• v.approxLocation = (v.interval.lo + v.interval.hi) / 2

def LeanCert.Validity.VerifiedRoot.width {expr : Core.Expr} (v : VerifiedRoot expr) : ℚ

Width of the isolating interval

Equations

• v.width = v.interval.width

structure LeanCert.Validity.UniqueVerifiedRoot (expr : Core.Expr) extends LeanCert.Validity.VerifiedRoot expr : Type

A verified unique root with uniqueness proof

• interval : Core.IntervalRat
• status : VerifiedRootStatus
• exists_root : ∃ x ∈ self.interval, Core.Expr.eval (fun (x_1 : ℕ) => x) expr = 0
• unique (x y : ℝ) : x ∈ self.interval → y ∈ self.interval → Core.Expr.eval (fun (x_1 : ℕ) => x) expr = 0 → Core.Expr.eval (fun (x : ℕ) => y) expr = 0 → x = y

  Proof of uniqueness within the interval

Integration

structure LeanCert.Validity.VerifiedIntegral (expr : Core.Expr) (a b : ℚ) : Type

A verified integral bound.

This structure bundles:

• Lower and upper bounds on the integral
• A proof that the true integral lies within these bounds

• lowerBound : ℚ

  Lower bound on the integral

• upperBound : ℚ

  Upper bound on the integral

• partitions : ℕ

  Number of partitions used

• integral_bounds : self.lowerBound ≤ self.upperBound ∧ ∃ (I : ℝ), ↑self.lowerBound ≤ I ∧ I ≤ ↑self.upperBound

  Proof that the integral lies in [lowerBound, upperBound]

def LeanCert.Validity.VerifiedIntegral.width {expr : Core.Expr} {a b : ℚ} (v : VerifiedIntegral expr a b) : ℚ

Width of the integral bound

Equations

• v.width = v.upperBound - v.lowerBound

Bound Verification

structure LeanCert.Validity.VerifiedUpperBound (expr : Core.Expr) (domain : Core.IntervalRat) : Type

A verified upper bound certificate.

Proves: ∀ x ∈ domain, f(x) ≤ bound

• bound : ℚ

  The verified upper bound

• is_upper_bound (x : ℝ) : x ∈ domain → Core.Expr.eval (fun (x_1 : ℕ) => x) expr ≤ ↑self.bound

  Proof that bound is valid

structure LeanCert.Validity.VerifiedLowerBound (expr : Core.Expr) (domain : Core.IntervalRat) : Type

A verified lower bound certificate.

Proves: ∀ x ∈ domain, bound ≤ f(x)

• bound : ℚ

  The verified lower bound

• is_lower_bound (x : ℝ) : x ∈ domain → ↑self.bound ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) expr

  Proof that bound is valid

Multi-dimensional variants

structure LeanCert.Validity.VerifiedBoxBound (expr : Core.Expr) (domain : Engine.Optimization.Box) : Type

A verified bound over a box (multi-dimensional domain)

• lo : ℚ

  Lower bound

• hi : ℚ

  Upper bound

• bounds_valid (ρ : ℕ → ℝ) : Engine.Optimization.Box.envMem ρ domain → (∀ i ≥ List.length domain, ρ i = 0) → ↑self.lo ≤ Core.Expr.eval ρ expr ∧ Core.Expr.eval ρ expr ≤ ↑self.hi

  Proof of bounds