Core Bound Verification

This module provides the fundamental infrastructure for certificate-driven verification of numerical bounds using interval arithmetic.

Main definitions

Boolean Checkers

• checkUpperBound - Check if ∀ x ∈ I, f(x) ≤ c via interval arithmetic
• checkLowerBound - Check if ∀ x ∈ I, c ≤ f(x) via interval arithmetic
• checkStrictUpperBound - Check if ∀ x ∈ I, f(x) < c
• checkStrictLowerBound - Check if ∀ x ∈ I, c < f(x)

Golden Theorems

• verify_upper_bound - Converts checkUpperBound = true to semantic proof
• verify_lower_bound - Converts checkLowerBound = true to semantic proof
• verify_strict_upper_bound - Converts checkStrictUpperBound = true to semantic proof
• verify_strict_lower_bound - Converts checkStrictLowerBound = true to semantic proof

Boolean Checkers

These are the functions native_decide will execute. They return Bool, not Prop.

def LeanCert.Validity.checkUpperBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) : Bool

Check if an expression is bounded above by c on interval I. Returns true iff domain validity holds AND the computed upper bound is ≤ c.

Equations

• LeanCert.Validity.checkUpperBound e I c cfg = (LeanCert.Engine.checkDomainValid1 e I cfg && decide ((LeanCert.Internal.Rational.evalTotalCore1 e I cfg).hi ≤ c))

def LeanCert.Validity.checkLowerBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) : Bool

Check if an expression is bounded below by c on interval I. Returns true iff domain validity holds AND the computed lower bound is ≥ c.

Equations

• LeanCert.Validity.checkLowerBound e I c cfg = (LeanCert.Engine.checkDomainValid1 e I cfg && decide (c ≤ (LeanCert.Internal.Rational.evalTotalCore1 e I cfg).lo))

def LeanCert.Validity.checkStrictUpperBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) : Bool

Check if an expression is strictly bounded above by c on interval I. Returns true iff domain validity holds AND the computed upper bound is < c.

Equations

• LeanCert.Validity.checkStrictUpperBound e I c cfg = (LeanCert.Engine.checkDomainValid1 e I cfg && decide ((LeanCert.Internal.Rational.evalTotalCore1 e I cfg).hi < c))

def LeanCert.Validity.checkStrictLowerBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) : Bool

Check if an expression is strictly bounded below by c on interval I. Returns true iff domain validity holds AND the computed lower bound is > c.

Equations

• LeanCert.Validity.checkStrictLowerBound e I c cfg = (LeanCert.Engine.checkDomainValid1 e I cfg && decide (c < (LeanCert.Internal.Rational.evalTotalCore1 e I cfg).lo))

Golden Theorems

These theorems convert the boolean true from the checkers into semantic proofs about Real numbers. They are the theorems a tactic will apply.

theorem LeanCert.Validity.verify_upper_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkUpperBound e I c cfg = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Golden Theorem for Upper Bounds

If checkUpperBound e I c cfg = true, then ∀ x ∈ I, Expr.eval (fun _ => x) e ≤ c.

theorem LeanCert.Validity.verify_lower_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkLowerBound e I c cfg = true) (x : ℝ) : x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Golden Theorem for Lower Bounds

If checkLowerBound e I c cfg = true, then ∀ x ∈ I, c ≤ Expr.eval (fun _ => x) e.

theorem LeanCert.Validity.verify_strict_upper_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkStrictUpperBound e I c cfg = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Golden Theorem for Strict Upper Bounds

If checkStrictUpperBound e I c cfg = true, then ∀ x ∈ I, Expr.eval (fun _ => x) e < c.

theorem LeanCert.Validity.verify_strict_lower_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkStrictLowerBound e I c cfg = true) (x : ℝ) : x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Golden Theorem for Strict Lower Bounds

If checkStrictLowerBound e I c cfg = true, then ∀ x ∈ I, c < Expr.eval (fun _ => x) e.

Convenience lemmas for pointwise bounds

theorem LeanCert.Validity.verify_upper_bound_pt (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (x : ℝ) (hx : x ∈ I) (h_cert : checkUpperBound e I c cfg = true) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Pointwise upper bound: if check passes and x ∈ I, then f(x) ≤ c

theorem LeanCert.Validity.verify_lower_bound_pt (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig) (x : ℝ) (hx : x ∈ I) (h_cert : checkLowerBound e I c cfg = true) : ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Pointwise lower bound: if check passes and x ∈ I, then c ≤ f(x)

Two-sided bounds

def LeanCert.Validity.checkBounds (e : Core.Expr) (I : Core.IntervalRat) (lo hi : ℚ) (cfg : Engine.EvalConfig) : Bool

Check both lower and upper bounds simultaneously

Equations

• LeanCert.Validity.checkBounds e I lo hi cfg = (LeanCert.Validity.checkLowerBound e I lo cfg && LeanCert.Validity.checkUpperBound e I hi cfg)

theorem LeanCert.Validity.verify_bounds (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (lo hi : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkBounds e I lo hi cfg = true) (x : ℝ) : x ∈ I → ↑lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e ∧ Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑hi

Two-sided bound verification: if both checks pass, then lo ≤ f(x) ≤ hi for all x ∈ I

Argmax/Argmin Verification

def LeanCert.Validity.checkPointLowerBound (e : Core.Expr) (x c : ℚ) (cfg : Engine.EvalConfig) : Bool

Check that evaluating f at a point x gives a value ≥ c.

Equations

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

def LeanCert.Validity.checkPointUpperBound (e : Core.Expr) (x c : ℚ) (cfg : Engine.EvalConfig) : Bool

Check that evaluating f at a point x gives a value ≤ c.

Equations

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

theorem LeanCert.Validity.verify_point_lower_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (x c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkPointLowerBound e x c cfg = true) : ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => ↑x) e

Verify that c ≤ f(x) at a specific point x.

theorem LeanCert.Validity.verify_point_upper_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (x c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkPointUpperBound e x c cfg = true) : Core.Expr.eval (fun (x_1 : ℕ) => ↑x) e ≤ ↑c

Verify that f(x) ≤ c at a specific point x.

theorem LeanCert.Validity.verify_argmax (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (x c : ℚ) (cfg : Engine.EvalConfig) (_hx : ↑x ∈ I) (h_upper : checkUpperBound e I c cfg = true) (h_point : checkPointLowerBound e x c cfg = true) (y : ℝ) : y ∈ I → Core.Expr.eval (fun (x : ℕ) => y) e ≤ Core.Expr.eval (fun (x_1 : ℕ) => ↑x) e

Argmax Verification Theorem

Proves ∀ y ∈ I, f(y) ≤ f(x) (x is a maximizer) by:

1. Checking that ∀ y ∈ I, f(y) ≤ c (the max over I is at most c)
2. Checking that c ≤ f(x) (the value at x is at least c)

theorem LeanCert.Validity.verify_argmin (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (x c : ℚ) (cfg : Engine.EvalConfig) (_hx : ↑x ∈ I) (h_lower : checkLowerBound e I c cfg = true) (h_point : checkPointUpperBound e x c cfg = true) (y : ℝ) : y ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => ↑x) e ≤ Core.Expr.eval (fun (x : ℕ) => y) e

Argmin Verification Theorem

Proves ∀ y ∈ I, f(x) ≤ f(y) (x is a minimizer).