Certificate-Driven Verification Examples

This file demonstrates the certificate-driven verification system. All proofs use native_decide to execute the boolean checkers.

Design

The golden theorems (verify_upper_bound, etc.) take:

1. The expression e
2. A proof hsupp that e is in ExprSupportedCore
3. The interval I
4. The bound c
5. An EvalConfig specifying Taylor depth
6. A proof h_cert that the checker returns true

The last argument is discharged by native_decide.

Examples

Basic algebraic bounds

• x² ≤ 1 on [0, 1] with depth 10

Transcendental bounds with varying depth

• exp(x) ≤ 3 on [0, 1] with depth 10
• sin(x) ≤ 1 on [0, 1] with depth 10
• Tighter bounds with higher depth

Demonstrating depth sensitivity

• Same bound may require different depths for different interval widths

Setup: Expressions and intervals

def LeanCert.Examples.Certificate.I01 : Core.IntervalRat

The unit interval [0, 1]

Equations

• LeanCert.Examples.Certificate.I01 = { lo := 0, hi := 1, le := LeanCert.Examples.Certificate.I01._proof_1 }

def LeanCert.Examples.Certificate.I012 : Core.IntervalRat

The interval [0, 1.2]

Equations

• LeanCert.Examples.Certificate.I012 = { lo := 0, hi := 6 / 5, le := LeanCert.Examples.Certificate.I012._proof_1 }

def LeanCert.Examples.Certificate.exprXSq : Core.Expr

The expression x²

Equations

• LeanCert.Examples.Certificate.exprXSq = (LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0)

def LeanCert.Examples.Certificate.exprXSq_core : Core.ExprSupportedCore exprXSq

Support proof for x²

Equations

• LeanCert.Examples.Certificate.exprXSq_core = ⋯

def LeanCert.Examples.Certificate.exprExp : Core.Expr

The expression exp(x)

Equations

• LeanCert.Examples.Certificate.exprExp = (LeanCert.Core.Expr.var 0).exp

def LeanCert.Examples.Certificate.exprExp_core : Core.ExprSupportedCore exprExp

Support proof for exp(x)

Equations

• LeanCert.Examples.Certificate.exprExp_core = ⋯

def LeanCert.Examples.Certificate.exprSin : Core.Expr

The expression sin(x)

Equations

• LeanCert.Examples.Certificate.exprSin = (LeanCert.Core.Expr.var 0).sin

def LeanCert.Examples.Certificate.exprSin_core : Core.ExprSupportedCore exprSin

Support proof for sin(x)

Equations

• LeanCert.Examples.Certificate.exprSin_core = ⋯

def LeanCert.Examples.Certificate.exprCos : Core.Expr

The expression cos(x)

Equations

• LeanCert.Examples.Certificate.exprCos = (LeanCert.Core.Expr.var 0).cos

def LeanCert.Examples.Certificate.exprCos_core : Core.ExprSupportedCore exprCos

Support proof for cos(x)

Equations

• LeanCert.Examples.Certificate.exprCos_core = ⋯

def LeanCert.Examples.Certificate.exprXExp : Core.Expr

The expression x * exp(x)

Equations

• LeanCert.Examples.Certificate.exprXExp = (LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0).exp

def LeanCert.Examples.Certificate.exprXExp_core : Core.ExprSupportedCore exprXExp

Support proof for x * exp(x)

Equations

• LeanCert.Examples.Certificate.exprXExp_core = ⋯

Basic algebraic bounds

theorem LeanCert.Examples.Certificate.xsq_le_one_cert (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq ≤ ↑1

x² ≤ 1 on [0, 1] with default depth 10

theorem LeanCert.Examples.Certificate.zero_le_xsq_cert (x : ℝ) : x ∈ I01 → ↑0 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq

0 ≤ x² on [0, 1] with default depth 10

Transcendental bounds

theorem LeanCert.Examples.Certificate.exp_le_three_cert (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprExp ≤ ↑3

exp(x) ≤ 3 on [0, 1] with depth 10

theorem LeanCert.Examples.Certificate.nine_tenths_le_exp_cert (x : ℝ) : x ∈ I01 → ↑(9 / 10) ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprExp

9/10 ≤ exp(x) on [0, 1] with depth 10 Note: The Taylor model gives a conservative lower bound slightly below 1, so we use 9/10 as a safe lower bound that the interval arithmetic can verify.

theorem LeanCert.Examples.Certificate.sin_le_one_cert (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprSin ≤ ↑1

sin(x) ≤ 1 on [0, 1]

theorem LeanCert.Examples.Certificate.cos_le_one_cert (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprCos ≤ ↑1

cos(x) ≤ 1 on [0, 1]

Tighter bounds with higher depth

Higher Taylor depth allows tighter bounds to be verified.

theorem LeanCert.Examples.Certificate.exp_le_275_cert (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprExp ≤ ↑(11 / 4)

exp(x) ≤ 2.75 on [0, 1] requires higher depth for tighter bound

Combined expression: x * exp(x)

This demonstrates the certificate system on a more complex expression. On [0, 1], we have:

• x ∈ [0, 1]
• exp(x) ∈ [1, e]
• x * exp(x) ∈ [0, e] ≈ [0, 2.718]

theorem LeanCert.Examples.Certificate.xexp_le_three_cert (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXExp ≤ ↑3

x * exp(x) ≤ 3 on [0, 1]

theorem LeanCert.Examples.Certificate.zero_le_xexp_cert (x : ℝ) : x ∈ I01 → ↑0 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprXExp

0 ≤ x * exp(x) on [0, 1]

Strict bounds

theorem LeanCert.Examples.Certificate.xsq_lt_two_cert (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq < ↑2

x² < 2 on [0, 1] (strict upper bound)

theorem LeanCert.Examples.Certificate.neg_one_lt_xsq_cert (x : ℝ) : x ∈ I01 → ↑(-1) < Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq

-1 < x² on [0, 1] (strict lower bound)

Two-sided bounds

theorem LeanCert.Examples.Certificate.xsq_bounds_cert (x : ℝ) : x ∈ I01 → ↑0 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq ∧ Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSq ≤ ↑1

0 ≤ x² ≤ 1 on [0, 1]

theorem LeanCert.Examples.Certificate.exp_bounds_cert (x : ℝ) : x ∈ I01 → ↑(9 / 10) ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprExp ∧ Core.Expr.eval (fun (x_1 : ℕ) => x) exprExp ≤ ↑3

9/10 ≤ exp(x) ≤ 3 on [0, 1]

Example: RPC workflow simulation

This section demonstrates what Python-generated code would look like. Python determines the required depth, then generates a one-liner proof.

theorem LeanCert.Examples.Certificate.rpc_exp_bound (x : ℝ) : x ∈ I01 → Core.Expr.eval (fun (x_1 : ℕ) => x) exprExp ≤ ↑(14 / 5)

Simulated RPC call: Python found depth 12 sufficient for exp(x) ≤ 2.8 on [0,1]