Certificate-Driven Verification

This file provides the infrastructure for certificate-driven verification of numerical bounds. Instead of Lean searching for a proof, an external agent (e.g., Python) provides a Certificate containing:

• Expr: The function f(x)
• Domain: The interval I
• Claim: E.g., f(I) ⊆ [a, b]
• ProofParams: Parameters like Taylor series depth

If the agent determines that exp(x) needs 20 Taylor terms to satisfy a bound, it passes taylorDepth := 20 to Lean. Lean runs the computation with that depth and checks the boolean result via native_decide.

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

Design

The boolean checkers are fully computable and can be evaluated by native_decide. The golden theorems bridge the gap between the boolean result and the semantic proof about real numbers.

Usage

Manual usage (before tactic implementation):

example : ∀ x ∈ I01, Expr.eval (fun _ => x) exprExp ≤ 3 :=
  verify_upper_bound exprExp exprExp_core I01 3 { taylorDepth := 15 } (by native_decide)

RPC workflow:

1. Python receives a request: "Prove x·e^x ≤ 5 on [0, 1.2]"
2. Python runs its own fast implementation to find sufficient depth (e.g., 15)
3. Python generates Lean code with the certificate:

   verify_upper_bound myExpr myExpr_core I_0_1_2 5 { taylorDepth := 15 } (by native_decide)
   

4. Lean executes, running evalIntervalCore with depth 15, checks boolean, closes goal

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.Engine.evalIntervalCore1 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.Engine.evalIntervalCore1 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.Engine.evalIntervalCore1 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.Engine.evalIntervalCore1 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.

This is the key theorem for certificate-driven verification of upper bounds. The proof uses:

1. The boolean check ensures (evalIntervalCore1 e I cfg).hi ≤ c
2. The fundamental correctness theorem ensures Expr.eval ... e ≤ hi
3. Transitivity gives Expr.eval ... 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.

This is the key theorem for certificate-driven verification of lower bounds. The proof uses:

1. The boolean check ensures c ≤ (evalIntervalCore1 e I cfg).lo
2. The fundamental correctness theorem ensures lo ≤ Expr.eval ... e
3. Transitivity gives c ≤ Expr.eval ... 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

These theorems support proving ∀ y ∈ I, f(y) ≤ f(x) (argmax) and ∀ y ∈ I, f(x) ≤ f(y) (argmin) via a concrete rational bound.

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. We evaluate on the point interval [x, x] and check the lower bound. This gives us c ≤ f(x) when x is rational.

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) This implies f(y) ≤ c ≤ f(x) by transitivity.

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) by:

1. Checking that ∀ y ∈ I, c ≤ f(y) (the min over I is at least c)
2. Checking that f(x) ≤ c (the value at x is at most c) This implies f(x) ≤ c ≤ f(y) by transitivity.

ExprSupportedWithInv bounds

Support for expressions with inv, log, atan, arsinh, atanh. These use the evalInterval? evaluator which may return none for invalid inputs.

NOTE: These are noncomputable because evalInterval? uses Real Taylor approximations. They cannot be used with native_decide. Use the verification theorems directly in term proofs or with explicit computation.

def LeanCert.Validity.checkUpperBoundWithInv (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) : Bool

Check upper bound for ExprSupportedWithInv expressions. Returns true iff evalInterval?1 succeeds and the upper bound is ≤ c. NOTE: Noncomputable - cannot be used with native_decide.

Equations

• LeanCert.Validity.checkUpperBoundWithInv e I c = match LeanCert.Engine.evalInterval?1 e I with | some J => decide (J.hi ≤ c) | none => false

def LeanCert.Validity.checkLowerBoundWithInv (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) : Bool

Check lower bound for ExprSupportedWithInv expressions. Returns true iff evalInterval?1 succeeds and the lower bound is ≥ c. NOTE: Noncomputable - cannot be used with native_decide.

Equations

• LeanCert.Validity.checkLowerBoundWithInv e I c = match LeanCert.Engine.evalInterval?1 e I with | some J => decide (c ≤ J.lo) | none => false

def LeanCert.Validity.checkStrictUpperBoundWithInv (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) : Bool

Check strict upper bound for ExprSupportedWithInv expressions. NOTE: Noncomputable - cannot be used with native_decide.

Equations

• LeanCert.Validity.checkStrictUpperBoundWithInv e I c = match LeanCert.Engine.evalInterval?1 e I with | some J => decide (J.hi < c) | none => false

def LeanCert.Validity.checkStrictLowerBoundWithInv (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) : Bool

Check strict lower bound for ExprSupportedWithInv expressions. NOTE: Noncomputable - cannot be used with native_decide.

Equations

• LeanCert.Validity.checkStrictLowerBoundWithInv e I c = match LeanCert.Engine.evalInterval?1 e I with | some J => decide (c < J.lo) | none => false

theorem LeanCert.Validity.verify_upper_bound_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (I : Core.IntervalRat) (c : ℚ) (h_cert : checkUpperBoundWithInv e I c = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Verification theorem for upper bounds with ExprSupportedWithInv.

theorem LeanCert.Validity.verify_lower_bound_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (I : Core.IntervalRat) (c : ℚ) (h_cert : checkLowerBoundWithInv e I c = true) (x : ℝ) : x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Verification theorem for lower bounds with ExprSupportedWithInv.

theorem LeanCert.Validity.verify_strict_upper_bound_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (I : Core.IntervalRat) (c : ℚ) (h_cert : checkStrictUpperBoundWithInv e I c = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Verification theorem for strict upper bounds with ExprSupportedWithInv.

theorem LeanCert.Validity.verify_strict_lower_bound_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (I : Core.IntervalRat) (c : ℚ) (h_cert : checkStrictLowerBoundWithInv e I c = true) (x : ℝ) : x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Verification theorem for strict lower bounds with ExprSupportedWithInv.

theorem LeanCert.Validity.verify_upper_bound_Icc_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (h_cert : checkUpperBoundWithInv e { lo := lo, hi := hi, le := hle } c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Bridge theorem for Set.Icc upper bounds with ExprSupportedWithInv.

theorem LeanCert.Validity.verify_lower_bound_Icc_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (h_cert : checkLowerBoundWithInv e { lo := lo, hi := hi, le := hle } c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge theorem for Set.Icc lower bounds with ExprSupportedWithInv.

theorem LeanCert.Validity.verify_strict_upper_bound_Icc_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (h_cert : checkStrictUpperBoundWithInv e { lo := lo, hi := hi, le := hle } c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Bridge theorem for Set.Icc strict upper bounds with ExprSupportedWithInv.

theorem LeanCert.Validity.verify_strict_lower_bound_Icc_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (h_cert : checkStrictLowerBoundWithInv e { lo := lo, hi := hi, le := hle } c = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge theorem for Set.Icc strict lower bounds with ExprSupportedWithInv.

Smart Bounds with Monotonicity

These checkers use derivative information to get tighter bounds at interval endpoints. If the function is monotonic on the interval, we can evaluate at the appropriate endpoint to get an exact bound, avoiding Taylor series remainder widening.

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

Smart lower bound check using monotonicity.

1. Tries standard interval check first (fastest).
2. If fails, computes derivative interval.
3. If derivative > 0 (increasing), checks if f(I.lo) ≥ c.
4. If derivative < 0 (decreasing), checks if f(I.hi) ≥ c.

Equations

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

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

Smart upper bound check using monotonicity.

1. Tries standard interval check first.
2. If fails, computes derivative interval.
3. If derivative > 0 (increasing), checks if f(I.hi) ≤ c.
4. If derivative < 0 (decreasing), checks if f(I.lo) ≤ c.

Equations

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

Smart Golden Theorems

theorem LeanCert.Validity.increasing_min_at_left_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hpos : 0 < (Engine.derivIntervalCore e I cfg).lo) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x : ℕ) => ↑I.lo) e ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Helper: For increasing functions, the minimum is at the left endpoint

theorem LeanCert.Validity.decreasing_min_at_right_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hneg : (Engine.derivIntervalCore e I cfg).hi < 0) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x : ℕ) => ↑I.hi) e ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Helper: For decreasing functions, the minimum is at the right endpoint

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

Smart lower bound verification using monotonicity

theorem LeanCert.Validity.increasing_max_at_right_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hpos : 0 < (Engine.derivIntervalCore e I cfg).lo) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ Core.Expr.eval (fun (x : ℕ) => ↑I.hi) e

Helper: For increasing functions, the maximum is at the right endpoint

theorem LeanCert.Validity.decreasing_max_at_left_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hneg : (Engine.derivIntervalCore e I cfg).hi < 0) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ Core.Expr.eval (fun (x : ℕ) => ↑I.lo) e

Helper: For decreasing functions, the maximum is at the left endpoint

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

Smart upper bound verification using monotonicity

Set.Icc Bridge Theorems

These theorems bridge between IntervalRat-based proofs and Set.Icc goals, allowing tactics to work with the more natural Set.Icc syntax.

theorem LeanCert.Validity.verify_upper_bound_Icc (e : Core.Expr) (hsupp : Core.ExprSupported e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkUpperBoundSmart e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Bridge from IntervalRat proof to Set.Icc upper bound goal

theorem LeanCert.Validity.verify_lower_bound_Icc (e : Core.Expr) (hsupp : Core.ExprSupported e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkLowerBoundSmart e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from IntervalRat proof to Set.Icc lower bound goal

theorem LeanCert.Validity.verify_upper_bound_Icc_core (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkUpperBound e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Bridge from IntervalRat proof to Set.Icc upper bound goal (Core version). This version uses ExprSupportedCore and the basic checkUpperBound (no monotonicity).

theorem LeanCert.Validity.verify_lower_bound_Icc_core (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkLowerBound e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from IntervalRat proof to Set.Icc lower bound goal (Core version). This version uses ExprSupportedCore and the basic checkLowerBound (no monotonicity).

theorem LeanCert.Validity.verify_strict_upper_bound_Icc_core (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkStrictUpperBound e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Bridge from IntervalRat proof to Set.Icc strict upper bound goal (Core version).

theorem LeanCert.Validity.verify_strict_lower_bound_Icc_core (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkStrictLowerBound e { lo := lo, hi := hi, le := hle } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from IntervalRat proof to Set.Icc strict lower bound goal (Core version).

Subdivision Theorems

These theorems allow combining bounds from interval subdivisions. When interval arithmetic gives overly wide bounds, subdividing the domain and proving bounds on each piece can help.

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

Combine upper bounds from two halves using splitMid. If f ≤ c on both halves, then f ≤ c on the whole interval.

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

Combine lower bounds from two halves using splitMid.

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

Combine strict upper bounds from two halves.

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

Combine strict lower bounds from two halves.

theorem LeanCert.Validity.verify_upper_bound_Icc_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkUpperBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).1 c cfg = true) (h_right : checkUpperBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).2 c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Bridge from subdivision to Set.Icc upper bound goal.

theorem LeanCert.Validity.verify_lower_bound_Icc_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkLowerBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).1 c cfg = true) (h_right : checkLowerBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).2 c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from subdivision to Set.Icc lower bound goal.

theorem LeanCert.Validity.verify_strict_upper_bound_Icc_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictUpperBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).1 c cfg = true) (h_right : checkStrictUpperBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).2 c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Bridge from subdivision to Set.Icc strict upper bound goal.

theorem LeanCert.Validity.verify_strict_lower_bound_Icc_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictLowerBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).1 c cfg = true) (h_right : checkStrictLowerBound e (Engine.splitMid { lo := lo, hi := hi, le := hle }).2 c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Bridge from subdivision to Set.Icc strict lower bound goal.

General Split Theorems

These theorems work with arbitrary split points, not just midpoints. Useful for adaptive subdivision algorithms.

theorem LeanCert.Validity.mem_split_general {lo mid hi : ℚ} {x : ℝ} (hx : x ∈ Set.Icc ↑lo ↑hi) (_hLeMid : lo ≤ mid) (_hMidLe : mid ≤ hi) : x ∈ Set.Icc ↑lo ↑mid ∨ x ∈ Set.Icc ↑mid ↑hi

Any x in [lo, hi] is in [lo, mid] or [mid, hi] for any mid in between

theorem LeanCert.Validity.verify_upper_bound_general_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo mid hi : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (_hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkUpperBound e { lo := lo, hi := mid, le := hLo } c cfg = true) (h_right : checkUpperBound e { lo := mid, hi := hi, le := hHi } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Combine upper bounds from two arbitrary adjacent intervals. If f ≤ c on [lo, mid] and f ≤ c on [mid, hi], then f ≤ c on [lo, hi].

theorem LeanCert.Validity.verify_lower_bound_general_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo mid hi : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (_hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkLowerBound e { lo := lo, hi := mid, le := hLo } c cfg = true) (h_right : checkLowerBound e { lo := mid, hi := hi, le := hHi } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Combine lower bounds from two arbitrary adjacent intervals.

theorem LeanCert.Validity.verify_strict_upper_bound_general_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo mid hi : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (_hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictUpperBound e { lo := lo, hi := mid, le := hLo } c cfg = true) (h_right : checkStrictUpperBound e { lo := mid, hi := hi, le := hHi } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Combine strict upper bounds from two arbitrary adjacent intervals.

theorem LeanCert.Validity.verify_strict_lower_bound_general_split (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo mid hi : ℚ) (hLo : lo ≤ mid) (hHi : mid ≤ hi) (_hle : lo ≤ hi) (c : ℚ) (cfg : Engine.EvalConfig) (h_left : checkStrictLowerBound e { lo := lo, hi := mid, le := hLo } c cfg = true) (h_right : checkStrictLowerBound e { lo := mid, hi := hi, le := hHi } c cfg = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Combine strict lower bounds from two arbitrary adjacent intervals.

Global Optimization Certificates

These checkers and theorems extend the certificate pattern to multivariate global optimization over n-dimensional boxes.

Boolean Checkers for Global Optimization

def LeanCert.Validity.GlobalOpt.checkGlobalLowerBound (e : Core.Expr) (B : Engine.Optimization.Box) (c : ℚ) (cfg : Engine.Optimization.GlobalOptConfig) : Bool

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.

def LeanCert.Validity.GlobalOpt.checkGlobalUpperBound (e : Core.Expr) (B : Engine.Optimization.Box) (c : ℚ) (cfg : Engine.Optimization.GlobalOptConfig) : Bool

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.

def LeanCert.Validity.GlobalOpt.checkGlobalBounds (e : Core.Expr) (B : Engine.Optimization.Box) (lo hi : ℚ) (cfg : Engine.Optimization.GlobalOptConfig) : Bool

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)

Golden Theorems for Global Optimization

theorem LeanCert.Validity.GlobalOpt.verify_global_lower_bound (e : Core.Expr) (hsupp : Core.ExprSupported e) (B : Engine.Optimization.Box) (c : ℚ) (cfg : Engine.Optimization.GlobalOptConfig) (h_cert : checkGlobalLowerBound e B c cfg = true) (ρ : ℕ → ℝ) : Engine.Optimization.Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ↑c ≤ Core.Expr.eval ρ e

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 ExprSupported (no log) which guarantees domain validity automatically. For expressions with log, use the Core version with explicit domain validity proofs.

theorem LeanCert.Validity.GlobalOpt.verify_global_upper_bound (e : Core.Expr) (hsupp : Core.ExprSupported e) (B : Engine.Optimization.Box) (c : ℚ) (cfg : Engine.Optimization.GlobalOptConfig) (h_cert : checkGlobalUpperBound e B c cfg = true) (ρ : ℕ → ℝ) : Engine.Optimization.Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → Core.Expr.eval ρ e ≤ ↑c

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 ExprSupported (no log) which guarantees domain validity automatically. For expressions with log, use the Core version with explicit domain validity proofs.

theorem LeanCert.Validity.GlobalOpt.verify_global_bounds (e : Core.Expr) (hsupp : Core.ExprSupported e) (B : Engine.Optimization.Box) (lo hi : ℚ) (cfg : Engine.Optimization.GlobalOptConfig) (h_cert : checkGlobalBounds e B lo hi cfg = true) (ρ : ℕ → ℝ) : Engine.Optimization.Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ↑lo ≤ Core.Expr.eval ρ e ∧ Core.Expr.eval ρ e ≤ ↑hi

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

structure LeanCert.Validity.RootFinding.RootConfig : Type

Configuration for root-finding checks

• maxDepth : ℕ

  Maximum bisection depth

• taylorDepth : ℕ

  Taylor depth for interval evaluation

instance LeanCert.Validity.RootFinding.instReprRootConfig : Repr RootConfig

Equations

• LeanCert.Validity.RootFinding.instReprRootConfig = { reprPrec := LeanCert.Validity.RootFinding.instReprRootConfig.repr }

def LeanCert.Validity.RootFinding.instReprRootConfig.repr : RootConfig → ℕ → Std.Format

Equations

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

instance LeanCert.Validity.RootFinding.instInhabitedRootConfig : Inhabited RootConfig

Equations

• LeanCert.Validity.RootFinding.instInhabitedRootConfig = { default := LeanCert.Validity.RootFinding.instInhabitedRootConfig.default }

def LeanCert.Validity.RootFinding.instInhabitedRootConfig.default : RootConfig

Equations

• LeanCert.Validity.RootFinding.instInhabitedRootConfig.default = { maxDepth := default, taylorDepth := default }

structure LeanCert.Validity.RootFinding.NewtonConfig : Type

Configuration for Newton uniqueness checks

• iterations : ℕ

  Number of Newton iterations

• tmDegree : ℕ

  Taylor model degree

instance LeanCert.Validity.RootFinding.instReprNewtonConfig : Repr NewtonConfig

Equations

• LeanCert.Validity.RootFinding.instReprNewtonConfig = { reprPrec := LeanCert.Validity.RootFinding.instReprNewtonConfig.repr }

def LeanCert.Validity.RootFinding.instReprNewtonConfig.repr : NewtonConfig → ℕ → Std.Format

Equations

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

def LeanCert.Validity.RootFinding.instInhabitedNewtonConfig.default : NewtonConfig

Equations

• LeanCert.Validity.RootFinding.instInhabitedNewtonConfig.default = { iterations := default, tmDegree := default }

instance LeanCert.Validity.RootFinding.instInhabitedNewtonConfig : Inhabited NewtonConfig

Equations

• LeanCert.Validity.RootFinding.instInhabitedNewtonConfig = { default := LeanCert.Validity.RootFinding.instInhabitedNewtonConfig.default }

Boolean Checkers for Root Finding

def LeanCert.Validity.RootFinding.checkSignChange (e : Core.Expr) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) : Bool

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.

def LeanCert.Validity.RootFinding.checkNoRoot (e : Core.Expr) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) : Bool

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.

Computable Newton Step for Unique Root Verification

def LeanCert.Validity.RootFinding.newtonStepCore (e : Core.Expr) (I : Core.IntervalRat) (cfg : Engine.EvalConfig := default) : Option Core.IntervalRat

Computable Newton step using evalIntervalCore1 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.

theorem LeanCert.Validity.RootFinding.newtonStepCore_extract (e : Core.Expr) (I N : Core.IntervalRat) (cfg : Engine.EvalConfig) (hCore : newtonStepCore e I cfg = some N) : have c := I.midpoint; have fc := Engine.evalIntervalCore1 e (Core.IntervalRat.singleton c) cfg; have dI := Engine.derivIntervalCore e I cfg; ∃ (hdI_nonzero : ¬dI.containsZero), have dNonzero := { toIntervalRat := dI, nonzero := hdI_nonzero }; have Q := fc.mul (Core.IntervalRat.invNonzero dNonzero); N.lo = max I.lo (c - Q.hi) ∧ N.hi = min I.hi (c - Q.lo)

Extract structure from newtonStepCore.

def LeanCert.Validity.RootFinding.checkNewtonContractsCore (e : Core.Expr) (I : Core.IntervalRat) (cfg : Engine.EvalConfig := default) : Bool

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.

noncomputable def LeanCert.Validity.RootFinding.checkNewtonContracts (e : Core.Expr) (I : Core.IntervalRat) (_cfg : NewtonConfig) : Bool

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 evalIntervalCore.

Equations

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

Golden Theorems for Root Finding

theorem LeanCert.Validity.RootFinding.verify_no_root (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (h_cert : checkNoRoot e I cfg = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≠ 0

Golden Theorem for No Root

If checkNoRoot e I cfg = true, then ∀ x ∈ I, Expr.eval (fun _ => x) e ≠ 0.

theorem LeanCert.Validity.RootFinding.verify_unique_root_newton (e : Core.Expr) (hsupp : Core.ExprSupported e) (hvar0 : Engine.UsesOnlyVar0 e) (I : Core.IntervalRat) (cfg : NewtonConfig) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) (h_cert : checkNewtonContracts e I cfg = true) : ∃! x : ℝ, x ∈ I ∧ Core.Expr.eval (fun (x_1 : ℕ) => 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.

theorem LeanCert.Validity.RootFinding.mvt_lower_bound_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hCont : ContinuousOn (Engine.evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)) (x y : ℝ) : x ∈ I → y ∈ I → x ≤ y → ↑(Engine.derivIntervalCore e I cfg).lo * (y - x) ≤ Engine.evalFunc1 e y - Engine.evalFunc1 e x

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.

theorem LeanCert.Validity.RootFinding.mvt_upper_bound_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hCont : ContinuousOn (Engine.evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)) (x y : ℝ) : x ∈ I → y ∈ I → x ≤ y → Engine.evalFunc1 e y - Engine.evalFunc1 e x ≤ ↑(Engine.derivIntervalCore e I cfg).hi * (y - x)

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.

theorem LeanCert.Validity.RootFinding.verify_unique_root_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (hvar0 : Engine.UsesOnlyVar0 e) (I : Core.IntervalRat) (evalCfg : Engine.EvalConfig) (newtonCfg : NewtonConfig) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) (_h_cert_core : checkNewtonContractsCore e I evalCfg = true) (h_cert_newton : checkNewtonContracts e I newtonCfg = true) : ∃! x : ℝ, x ∈ I ∧ Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

Golden Theorem for Computable Newton Contraction (Unique Root Existence)

This version assumes both:

1. Core contraction check (computable, used by search/external tools)
2. 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.

theorem LeanCert.Validity.RootFinding.newton_preserves_root_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (hvar0 : Engine.UsesOnlyVar0 e) (I N : Core.IntervalRat) (cfg : Engine.EvalConfig) (hStep : newtonStepCore e I cfg = some N) (x : ℝ) (hx : x ∈ I) (hroot : Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0) : x ∈ N

Newton step preserves roots when using Core evaluation functions. If x is a root in I and newtonStepCore produces N, then x ∈ N.

theorem LeanCert.Validity.RootFinding.newton_step_core_at_most_one_root (e : Core.Expr) (hsupp : Core.ExprSupported e) (_hvar0 : Engine.UsesOnlyVar0 e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hStep : ∃ (N : Core.IntervalRat), newtonStepCore e I cfg = some N) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) (x y : ℝ) (hx : x ∈ I) (hy : y ∈ I) (hx_root : Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0) (hy_root : Core.Expr.eval (fun (x : ℕ) => y) e = 0) : x = y

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.

theorem LeanCert.Validity.RootFinding.mvt_fc_lower_bound_pos_increasing_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (_hI_nonsingleton : I.lo < I.hi) (_hdI_lo_pos : 0 < (Engine.derivIntervalCore e I cfg).lo) (hCont : ContinuousOn (Engine.evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)) (hf_Ilo_pos : 0 < Engine.evalFunc1 e ↑I.lo) : have c := I.midpoint; have hw := (I.hi - I.lo) / 2; have dI := Engine.derivIntervalCore e I cfg; Engine.evalFunc1 e ↑c > ↑dI.lo * ↑hw

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.

theorem LeanCert.Validity.RootFinding.mvt_fc_upper_bound_pos_increasing_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (_hI_nonsingleton : I.lo < I.hi) (_hdI_lo_pos : 0 < (Engine.derivIntervalCore e I cfg).lo) (hCont : ContinuousOn (Engine.evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)) (hf_Ihi_neg : Engine.evalFunc1 e ↑I.hi < 0) : have c := I.midpoint; have hw := (I.hi - I.lo) / 2; have dI := Engine.derivIntervalCore e I cfg; Engine.evalFunc1 e ↑c < -(↑dI.lo * ↑hw)

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.

theorem LeanCert.Validity.RootFinding.mvt_fc_upper_bound_neg_decreasing_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (_hI_nonsingleton : I.lo < I.hi) (_hdI_hi_neg : (Engine.derivIntervalCore e I cfg).hi < 0) (hCont : ContinuousOn (Engine.evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)) (hf_Ilo_neg : Engine.evalFunc1 e ↑I.lo < 0) : have c := I.midpoint; have hw := (I.hi - I.lo) / 2; have dI := Engine.derivIntervalCore e I cfg; Engine.evalFunc1 e ↑c < ↑dI.hi * ↑hw

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.

theorem LeanCert.Validity.RootFinding.mvt_fc_lower_bound_neg_decreasing_core (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (_hI_nonsingleton : I.lo < I.hi) (_hdI_hi_neg : (Engine.derivIntervalCore e I cfg).hi < 0) (hCont : ContinuousOn (Engine.evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)) (hf_Ihi_pos : 0 < Engine.evalFunc1 e ↑I.hi) : have c := I.midpoint; have hw := (I.hi - I.lo) / 2; have dI := Engine.derivIntervalCore e I cfg; Engine.evalFunc1 e ↑c > -(↑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.

theorem LeanCert.Validity.RootFinding.verify_unique_root_computable (e : Core.Expr) (hsupp : Core.ExprSupported e) (hvar0 : Engine.UsesOnlyVar0 e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) (h_cert : checkNewtonContractsCore e I cfg = true) : ∃! x : ℝ, x ∈ I ∧ Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

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

theorem LeanCert.Validity.RootFinding.verify_sign_change (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) (h_cert : checkSignChange e I cfg = true) : ∃ x ∈ I, Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

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

noncomputable def LeanCert.Validity.RootFinding.checkHasRoot (e : Core.Expr) (I : Core.IntervalRat) (cfg : RootConfig) : Bool

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 evalInterval1.

Equations

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

theorem LeanCert.Validity.RootFinding.verify_has_root (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (cfg : RootConfig) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) (h_cert : checkHasRoot e I cfg = true) : ∃ x ∈ I, Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

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).

Integration Certificates

Computable Integration Infrastructure

For interval_integrate tactic, we need:

1. A computable integration function using evalIntervalCore1
2. A theorem that ExprSupportedCore implies IntervalIntegrable
3. A verification theorem linking the computation to the real integral

def LeanCert.Validity.Integration.uniformPartitionCore (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) : List Core.IntervalRat

Computable uniform partition using evalIntervalCore1

Equations

• LeanCert.Validity.Integration.uniformPartitionCore I n hn = List.ofFn fun (i : Fin n) => { lo := I.lo + (I.hi - I.lo) / ↑n * ↑↑i, hi := I.lo + (I.hi - I.lo) / ↑n * (↑↑i + 1), le := ⋯ }

def LeanCert.Validity.Integration.sumIntervalBoundsCore (e : Core.Expr) (parts : List Core.IntervalRat) (cfg : Engine.EvalConfig) : Core.IntervalRat

Sum of interval bounds over a partition using computable evalIntervalCore1

Equations

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

def LeanCert.Validity.Integration.integrateIntervalCore (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (cfg : Engine.EvalConfig := default) : Core.IntervalRat

Computable interval bounds on ∫_a^b f(x) dx using uniform partitioning

Equations

• LeanCert.Validity.Integration.integrateIntervalCore e I n hn cfg = LeanCert.Validity.Integration.sumIntervalBoundsCore e (LeanCert.Validity.Integration.uniformPartitionCore I n hn) cfg

def LeanCert.Validity.Integration.integrateInterval1Core (e : Core.Expr) (I : Core.IntervalRat) (cfg : Engine.EvalConfig := default) : Core.IntervalRat

For single-interval integration (n=1), computable version

Equations

• LeanCert.Validity.Integration.integrateInterval1Core e I cfg = (LeanCert.Core.IntervalRat.singleton I.width).mul (LeanCert.Engine.evalIntervalCore1 e I cfg)

IntervalIntegrable from ExprSupportedCore

All ExprSupportedCore expressions are continuous, hence integrable on compact intervals.

theorem LeanCert.Validity.Integration.exprSupportedCore_intervalIntegrable (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (hdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi

All ExprSupportedCore expressions are interval integrable on any compact interval.

This follows because ExprSupportedCore expressions are continuous (see exprSupportedCore_continuousOn), and continuous functions on compact intervals are integrable.

Note: Requires domain validity for expressions with log.

Correctness of Computable Integration

theorem LeanCert.Validity.Integration.integrateInterval1Core_correct (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hdom : Engine.evalDomainValid1 e I cfg) (hcontdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateInterval1Core e I cfg

Single-interval integration correctness for ExprSupportedCore.

This is proved directly using the same structure as integrateInterval1_correct but with the computable evalIntervalCore1 instead of noncomputable evalInterval1.

The hdom hypothesis ensures evaluation domain validity (e.g., log arguments have positive interval bounds). The hcontdom hypothesis ensures continuity domain validity (e.g., log arguments are positive on the set).

def LeanCert.Validity.Integration.checkIntegralBoundsCore (e : Core.Expr) (I : Core.IntervalRat) (target : ℚ) (cfg : Engine.EvalConfig := default) : Bool

Check if the integral bound contains a given rational value. Returns true if domain is valid and the computed integral bound contains the target value.

Equations

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

theorem LeanCert.Validity.Integration.verify_integral_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (_target : ℚ) (cfg : Engine.EvalConfig) (h_cert : checkIntegralBoundsCore e I _target cfg = true) (hcontdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ integrateInterval1Core e I cfg

Golden Theorem for Integration Bounds

If checkIntegralBoundsCore e I target cfg = true, then the integral is bounded by the computed interval.

Note: The target parameter and h_cert hypothesis are used for the native_decide workflow where we verify at compile time that target is in the computed interval. The actual proof of interval membership uses integrateInterval1Core_correct directly.

This theorem allows proving statements like "∫_a^b f(x) dx ∈ [lo, hi]".

Note: Requires continuity domain validity for expressions with log.

def LeanCert.Validity.Integration.getIntegralBound (e : Core.Expr) (I : Core.IntervalRat) (cfg : Engine.EvalConfig := default) : Core.IntervalRat

Extract the computed integral bound as an interval

Equations

• LeanCert.Validity.Integration.getIntegralBound e I cfg = LeanCert.Validity.Integration.integrateInterval1Core e I cfg

theorem LeanCert.Validity.Integration.integral_in_bound (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (cfg : Engine.EvalConfig) (hdom : Engine.evalDomainValid1 e I cfg) (hcontdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) : ↑(getIntegralBound e I cfg).lo ≤ ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∧ ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑(getIntegralBound e I cfg).hi

The integral lies within the computed bound (computable version)

Note: Requires continuity domain validity for expressions with log.

Single-interval integration for ExprSupportedWithInv

def LeanCert.Validity.Integration.integrateInterval1WithInv (e : Core.Expr) (I : Core.IntervalRat) : Option Core.IntervalRat

Computable single-interval integration using evalInterval?1. Returns none if interval evaluation fails (e.g., log domain invalid).

Equations

• LeanCert.Validity.Integration.integrateInterval1WithInv e I = match LeanCert.Engine.evalInterval?1 e I with | some J => some ((LeanCert.Core.IntervalRat.singleton I.width).mul J) | none => none

theorem LeanCert.Validity.Integration.integrateInterval1WithInv_correct (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (I bound : Core.IntervalRat) (hsome : integrateInterval1WithInv e I = some bound) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ bound

Single-interval integration correctness for ExprSupportedWithInv. Requires that evalInterval?1 succeeds on the interval.

def LeanCert.Validity.Integration.checkIntegralBoundsWithInv (e : Core.Expr) (I : Core.IntervalRat) (target : ℚ) : Bool

Check if the computed integration bound contains a target value. Returns false if interval evaluation fails.

Equations

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

theorem LeanCert.Validity.Integration.verify_integral_bound_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (I : Core.IntervalRat) (_target : ℚ) (h_cert : checkIntegralBoundsWithInv e I _target = true) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∃ (bound : Core.IntervalRat), integrateInterval1WithInv e I = some bound ∧ ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ bound

Golden Theorem for Integration Bounds (WithInv)

If checkIntegralBoundsWithInv e I target = true, then the integral lies in the computed bound. The target parameter is for the native_decide workflow.

Partitioned integration for ExprSupportedWithInv

def LeanCert.Validity.Integration.collectBoundsWithInv (e : Core.Expr) (parts : List Core.IntervalRat) : Option (List Core.IntervalRat)

Collect per-subinterval bounds using evalInterval?1. Returns none if any subinterval fails.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Validity.Integration.collectBoundsWithInv e [] = some []

def LeanCert.Validity.Integration.integratePartitionWithInv (e : Core.Expr) (I : Core.IntervalRat) (n : ℕ) : Option Core.IntervalRat

Sum bounds over a uniform partition using evalInterval?1.

Equations

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

theorem LeanCert.Validity.Integration.collectBoundsWithInv_length (e : Core.Expr) (parts bounds : List Core.IntervalRat) : collectBoundsWithInv e parts = some bounds → bounds.length = parts.length

theorem LeanCert.Validity.Integration.collectBoundsWithInv_getElem (e : Core.Expr) (parts bounds : List Core.IntervalRat) (h : collectBoundsWithInv e parts = some bounds) (i : ℕ) (hi : i < parts.length) : integrateInterval1WithInv e parts[i] = some bounds[i]

theorem LeanCert.Validity.Integration.integral_subinterval_bounded_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : k < n) (bound : Core.IntervalRat) (hsome : integrateInterval1WithInv e (Engine.partitionInterval I n hn k hk) = some bound) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in Engine.partitionPoints I n k..Engine.partitionPoints I n (k + 1), Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ bound

theorem LeanCert.Validity.Integration.integratePartitionWithInv_correct (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (I : Core.IntervalRat) (n : ℕ) (hn : 0 < n) (bound : Core.IntervalRat) (hsome : integratePartitionWithInv e I n = some bound) (hInt : IntervalIntegrable (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) MeasureTheory.volume ↑I.lo ↑I.hi) : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ bound