Certificate-Driven Verification (umbrella) #
The bound checkers and Golden Theorems formerly defined in this file live in
the LeanCert.Validity.Bounds.* modules:
Bounds.Core- Boolean checkers + golden theorems for interval boundsBounds.Checked- Checkers/theorems for arbitrary expressions with domain checksBounds.Smart- Monotonicity-aware bounds using derivative informationBounds.Bridge-Set.Iccbridge theorems and subdivision combinatorsValidity.Integration- Certified integral bounds (uniform + adaptive)
This file re-exports all of them (via the imports above) and additionally defines the global-optimization and root-finding certificate layers.
Certificate-driven verification: an external agent (e.g. Python) proposes a
Certificate (expression, domain, claim, proof parameters such as Taylor
depth); Lean re-checks the boolean certificate — typically via native_decide
— and a Golden Theorem lifts the boolean result to a semantic proof. The
golden theorems themselves are axiom-free (see Tests/AxiomAudit.lean).
Usage #
example : ∀ x ∈ I01, Expr.eval (fun _ => x) exprExp ≤ 3 :=
verify_upper_bound exprExp exprExp_core I01 3 { taylorDepth := 15 } (by native_decide)
Global Optimization Certificates #
These checkers and theorems extend the certificate pattern to multivariate global optimization over n-dimensional boxes.
Boolean Checkers for Global Optimization #
Check if c is a lower bound for e over box B.
Returns true iff globalMinimizeCore(e, B, cfg).bound.lo ≥ c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Check if c is an upper bound for e over box B.
Returns true iff globalMaximizeCore(e, B, cfg).bound.hi ≤ c.
(i.e., the upper bound on max(e) is ≤ c, which proves ∀ρ, e(ρ) ≤ c)
Note: bound.hi = -globalMinimizeCore(-e).bound.lo, and by correctness globalMinimizeCore(-e).bound.lo ≤ -e(ρ) for all ρ, so e(ρ) ≤ bound.hi.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Check both lower and upper bounds for global optimization
Equations
- LeanCert.Validity.GlobalOpt.checkGlobalBounds e B lo hi cfg = (LeanCert.Validity.GlobalOpt.checkGlobalLowerBound e B lo cfg && LeanCert.Validity.GlobalOpt.checkGlobalUpperBound e B hi cfg)
Instances For
Golden Theorems for Global Optimization #
Golden Theorem for Global Lower Bounds
If checkGlobalLowerBound e B c cfg = true, then ∀ ρ ∈ B, c ≤ Expr.eval ρ e.
This converts the boolean certificate into a semantic proof about all points in the box.
Note: This uses ADSupported (no log) which guarantees domain validity automatically. For expressions with log, use the Core version with explicit domain validity proofs.
Golden Theorem for Global Upper Bounds
If checkGlobalUpperBound e B c cfg = true, then ∀ ρ ∈ B, Expr.eval ρ e ≤ c.
The maximization problem is reduced to minimization of -e.
Note: This uses ADSupported (no log) which guarantees domain validity automatically. For expressions with log, use the Core version with explicit domain validity proofs.
Two-sided global bound verification
Root Finding Certificates #
These checkers and theorems provide certificate-driven verification for root existence and uniqueness.
Configuration for root finding certificates #
Configuration for root-finding checks
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Configuration for Newton uniqueness checks
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Boolean Checkers for Root Finding #
Check if expression has a sign change on interval (indicating a root). Uses interval arithmetic to check if f(lo) and f(hi) have opposite signs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Check if interval definitely has no root (function has constant sign).
Returns true if the function's interval evaluation doesn't contain 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computable Newton Step for Unique Root Verification #
Computable Newton step using LeanCert.Internal.Rational.evalTotalCore1 and derivIntervalCore.
This is the computable equivalent of newtonStepSimple. It performs one
interval Newton iteration: N(I) = c - f(c)/f'(I) where c = midpoint(I).
Returns none if the derivative interval contains 0 (can't safely divide).
Returns some (I ∩ N) otherwise.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extract structure from newtonStepCore.
Computable check if Newton iteration contracts.
Returns true if newtonStepCore produces N with I.lo < N.lo and N.hi < I.hi.
This can be used with native_decide for unique root verification.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Check if Newton iteration contracts, indicating unique root existence.
Returns true if the Newton step from I gives N ⊂ interior(I).
Note: This is noncomputable because newtonStepSimple uses derivInterval which uses evalInterval (noncomputable). For native_decide, we would need a fully computable version using LeanCert.Internal.Rational.evalTotalCore.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Golden Theorems for Root Finding #
Golden Theorem for No Root
If checkNoRoot e I cfg = true, then ∀ x ∈ I, Expr.eval (fun _ => x) e ≠ 0.
Golden Theorem for Newton Contraction (Unique Root Existence)
If checkNewtonContracts e I cfg = true, then there exists a unique root in I.
This theorem requires additional hypotheses that the external checker must verify:
- The expression is supported
- The expression uses only variable 0
- The function is continuous on I
Core MVT Lemmas for Newton Contraction Contradiction #
These lemmas prove that if Newton contraction holds but f has constant sign at both endpoints, we get a contradiction via MVT bounds.
Key insight: If f doesn't change sign on I (both endpoints positive or both negative), then by monotonicity (from nonzero derivative), f has constant sign throughout I. But Newton contraction requires specific quotient bounds that MVT proves are violated.
MVT lower bound using derivIntervalCore: if f'(ξ) ∈ [dI.lo, dI.hi] for all ξ ∈ I, then f(y) - f(x) ≥ dI.lo * (y - x) for x ≤ y in I.
MVT upper bound using derivIntervalCore: if f'(ξ) ∈ [dI.lo, dI.hi] for all ξ ∈ I, then f(y) - f(x) ≤ dI.hi * (y - x) for x ≤ y in I.
Golden Theorem for Computable Newton Contraction (Unique Root Existence)
This version assumes both:
- Core contraction check (computable, used by search/external tools)
- Non-core contraction check (used for the formal proof, via
verify_unique_root_newton).
The formal proof only relies on the non-core checker; the core checker can be used by the external agent for optimization but is not needed logically. This avoids the need to prove complex MVT-based contradiction lemmas for the Core interval functions.
Note: The h_cert_core hypothesis is not used in the proof but is kept
in the signature so the certificate format can include it for external
tooling purposes.
Fully Computable Unique Root Verification #
The following theorems provide a fully computable path to proving unique root existence
using only checkNewtonContractsCore. This allows native_decide to work without requiring
noncomputable functions like Real.exp or Real.log.
Newton step preserves roots when using Core evaluation functions. If x is a root in I and newtonStepCore produces N, then x ∈ N.
If Newton step succeeds, there's at most one root in I (via Rolle's theorem). This uses the fact that if dI doesn't contain zero, the derivative is nonzero everywhere on I, so f is strictly monotonic.
MVT bound using Core functions: If f' ≥ dI.lo > 0 (increasing) and f(I.lo) > 0, then f(c) > dI.lo * hw where c = midpoint and hw = half-width.
MVT bound using Core functions: If f' ≥ dI.lo > 0 (increasing) and f(I.hi) < 0, then f(c) < -dI.lo * hw where c = midpoint and hw = half-width.
MVT bound using Core functions: If f' ≤ dI.hi < 0 (decreasing) and f(I.lo) < 0, then f(c) < 0 and more specifically, fc.lo / dI.hi ≥ hw.
MVT bound using Core functions: If f' ≤ dI.hi < 0 (decreasing) and f(I.hi) > 0, then f(c) > 0 and more specifically, fc.hi / dI.hi ≤ -hw.
Golden Theorem for Computable Unique Root (Fully Computable)
If checkNewtonContractsCore e I cfg = true, then there exists a unique root in I.
This theorem uses ONLY computable functions (no Real.exp, Real.log, etc.),
making it suitable for native_decide verification.
Sign Change Root Existence #
Golden Theorem for Sign Change Root Existence
If checkSignChange e I cfg = true, then there exists a root in I.
This uses the Intermediate Value Theorem: if f(lo) and f(hi) have opposite signs, and f is continuous on I, then f has a root in I.
Bisection-Based Root Existence #
Check if bisection finds a root (returns hasRoot for some sub-interval). This runs the bisection algorithm and checks if any interval has hasRoot status.
Note: This is noncomputable because bisectRoot uses LeanCert.Internal.Rational.evalUnchecked1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Golden Theorem for Bisection Root Existence
If checkHasRoot e I cfg = true, then there exists a root in I.
This uses bisectRoot_hasRoot_correct which proves that if bisection returns hasRoot for a sub-interval J ⊆ I, then there exists a root in J (hence in I).