Discovery Mode: Finder Functions

This module provides high-level "finder" functions that:

1. Run the appropriate algorithm (optimization, root finding, etc.)
2. Generate certificate parameters automatically
3. Assemble the proof term using the "Golden Theorems" from Certificate.lean

These functions produce proof-carrying results (Verified* types) that bundle computed data with semantic proofs.

Main Definitions

• findGlobalMin - Find and verify a global minimum
• findGlobalMax - Find and verify a global maximum
• searchRoots - Find root candidates (not formally verified)
• quickBounds - Quick interval evaluation

Design

The finders work in two stages:

1. Computation: Run the raw algorithm (e.g., globalMinimizeCore)
2. Certification: Apply the corresponding Golden Theorem to get the proof

The proof is assembled by native_decide evaluating the boolean certificate checker.

Global Minimum Finding

def LeanCert.Discovery.findGlobalMin (expr : Core.Expr) (hsupp : Core.ExprSupported expr) (domain : Engine.Optimization.Box) (cfg : DiscoveryConfig := { }) : VerifiedGlobalMin expr domain

Find a verified global minimum of an expression over a box.

This function:

1. Runs globalMinimizeCore to compute the bound
2. Uses globalMinimizeCore_lo_correct to produce a proof

The returned VerifiedGlobalMin bundles:

• The computed lower bound
• The best box containing a near-minimizer
• A proof that the bound is valid for all points in the domain

Usage:

def result := findGlobalMin expr support domain cfg
-- result.bound is the minimum bound
-- result.is_lower_bound is the proof

Equations

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

def LeanCert.Discovery.findGlobalMax (expr : Core.Expr) (hsupp : Core.ExprSupported expr) (domain : Engine.Optimization.Box) (cfg : DiscoveryConfig := { }) : VerifiedGlobalMax expr domain

Find a verified global maximum of an expression over a box.

Symmetric to findGlobalMin, using maximization instead.

Equations

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

Bound Verification

def LeanCert.Discovery.verifyUpperBound (expr : Core.Expr) (hsupp : Core.ExprSupported expr) (domain : Core.IntervalRat) (bound : ℚ) (cfg : DiscoveryConfig := { }) : Option (VerifiedUpperBound expr domain)

Verify an upper bound using interval arithmetic.

Returns some proof if the bound is verified, none otherwise.

Equations

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

def LeanCert.Discovery.verifyLowerBound (expr : Core.Expr) (hsupp : Core.ExprSupported expr) (domain : Core.IntervalRat) (bound : ℚ) (cfg : DiscoveryConfig := { }) : Option (VerifiedLowerBound expr domain)

Verify a lower bound using interval arithmetic.

Returns some proof if the bound is verified, none otherwise.

Equations

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

Root Finding

structure LeanCert.Discovery.RootSearchResult (expr : Core.Expr) : Type

Result of root search before certification

• intervals : List Core.IntervalRat

  Intervals that may contain roots

• statuses : List Engine.RootStatus

  Status for each interval

• iterations : ℕ

  Iteration count

def LeanCert.Discovery.instReprRootSearchResult.repr {expr✝ : Core.Expr} : RootSearchResult expr✝ → ℕ → Std.Format

Equations

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

instance LeanCert.Discovery.instReprRootSearchResult {expr✝ : Core.Expr} : Repr (RootSearchResult expr✝)

Equations

• LeanCert.Discovery.instReprRootSearchResult = { reprPrec := LeanCert.Discovery.instReprRootSearchResult.repr }

noncomputable def LeanCert.Discovery.searchRoots (expr : Core.Expr) (domain : Core.IntervalRat) (cfg : DiscoveryConfig := { }) : RootSearchResult expr

Find roots of an expression on an interval using bisection.

This searches for roots but doesn't provide formal proofs of existence. The results indicate where roots may exist based on sign changes.

Note: For formal verification, use the sign change theorems from Certificate.lean with the returned intervals that have hasRoot status.

Equations

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

Convenience Functions

def LeanCert.Discovery.quickBounds (expr : Core.Expr) (domain : Core.IntervalRat) (cfg : DiscoveryConfig := { }) : ℚ × ℚ

Quick bounds check: returns (lo, hi) interval containing all values of expr on domain

Equations

• LeanCert.Discovery.quickBounds expr domain cfg = ((LeanCert.Engine.evalIntervalCore1 expr domain cfg.toEvalConfig).lo, (LeanCert.Engine.evalIntervalCore1 expr domain cfg.toEvalConfig).hi)

def LeanCert.Discovery.quickGlobalBounds (expr : Core.Expr) (hsupp : Core.ExprSupported expr) (domain : Engine.Optimization.Box) (cfg : DiscoveryConfig := { }) : ℚ × ℚ

Quick global bounds: returns (min, max) bounds using optimization

Equations

• LeanCert.Discovery.quickGlobalBounds expr hsupp domain cfg = ((LeanCert.Discovery.findGlobalMin expr hsupp domain cfg).bound, (LeanCert.Discovery.findGlobalMax expr hsupp domain cfg).bound)

Adaptive Verification

These functions automatically increase precision until verification succeeds.

def LeanCert.Discovery.tryVerifyUpperBound (expr : Core.Expr) (hsupp : Core.ExprSupported expr) (domain : Core.IntervalRat) (bound : ℚ) (maxDepth : ℕ := 40) : Option (VerifiedUpperBound expr domain)

Try to verify an upper bound with increasing Taylor depths. Returns some with the verified bound if successful, none otherwise.

Equations

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

def LeanCert.Discovery.tryVerifyLowerBound (expr : Core.Expr) (hsupp : Core.ExprSupported expr) (domain : Core.IntervalRat) (bound : ℚ) (maxDepth : ℕ := 40) : Option (VerifiedLowerBound expr domain)

Try to verify a lower bound with increasing Taylor depths. Returns some with the verified bound if successful, none otherwise.

Equations

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