Certificate-Driven Verification with Dyadic Arithmetic

This file provides Golden Theorems for the Dyadic arithmetic backend, mirroring the structure of Validity/Bounds.lean but using the high-performance IntervalDyadic type.

Overview

The Dyadic backend offers significant performance advantages over rational arithmetic for many verification tasks, while maintaining full soundness. This module exposes the Dyadic evaluator as a first-class citizen for certificate-driven verification.

Main definitions

Boolean Checkers

• checkUpperBoundDyadic - Check if the computed upper bound is ≤ c
• checkLowerBoundDyadic - Check if the computed lower bound is ≥ c

Golden Theorems

• verify_upper_bound_dyadic - Converts boolean check to semantic proof for upper bounds
• verify_lower_bound_dyadic - Converts boolean check to semantic proof for lower bounds

For ExprSupported expressions (no log), convenience versions are provided that don't require explicit domain validity proofs.

Design

The Dyadic backend uses IntervalDyadic which represents intervals with dyadic endpoints (numbers of the form m · 2^e). This allows for faster arithmetic than arbitrary rationals while still providing rigorous bounds.

Key parameters:

• prec : Int - Precision (negative = more precision). Must satisfy prec ≤ 0.
• depth : Nat - Taylor series depth for transcendental functions.

Trust Hierarchy

This provides an alternative verification path to the rational-based Validity/Bounds.lean:

• Same Expr AST and ExprSupportedCore predicate
• Different computational backend (IntervalDyadic vs IntervalRat)
• Same semantic guarantees (bounds on real-valued evaluation)

The Dyadic path is faster but the rational path may be preferred for reproducibility across different platforms.

Boolean Checkers

These check the computed interval bounds. Domain validity is handled separately.

def LeanCert.Validity.checkUpperBoundDyadic (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) : Bool

Check if an expression's computed upper bound is ≤ c using Dyadic arithmetic. This is the computable check that native_decide will execute.

Note: Domain validity must be established separately.

Equations

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

def LeanCert.Validity.checkLowerBoundDyadic (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) : Bool

Check if an expression's computed lower bound is ≥ c using Dyadic arithmetic.

Equations

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

def LeanCert.Validity.checkStrictUpperBoundDyadic (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) : Bool

Check if an expression's computed upper bound is strictly < c using Dyadic arithmetic.

Equations

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

def LeanCert.Validity.checkStrictLowerBoundDyadic (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) : Bool

Check if an expression's computed lower bound is strictly > c using Dyadic arithmetic.

Equations

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

Golden Theorems

These theorems convert the boolean true from the checkers into semantic proofs about Real numbers.

theorem LeanCert.Validity.verify_upper_bound_dyadic (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (hdom : Engine.evalDomainValidDyadic e (fun (x : ℕ) => Core.IntervalDyadic.ofIntervalRat { lo := lo, hi := hi, le := hle } prec) { precision := prec, taylorDepth := depth }) (h_check : checkUpperBoundDyadic e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Golden Theorem for Dyadic Upper Bounds

If the bound check passes and domain validity holds, then ∀ x ∈ [lo, hi], Expr.eval (fun _ => x) e ≤ c.

This is the key theorem for certificate-driven verification using the Dyadic backend.

Parameters:

• e: The expression to evaluate
• hsupp: Proof that the expression is supported (ExprSupportedCore)
• lo, hi, hle: The interval [lo, hi] with proof lo ≤ hi
• c: The upper bound to verify
• prec: Precision (must be ≤ 0)
• depth: Taylor series depth
• h_prec: Proof that prec ≤ 0
• hdom: Proof of domain validity (automatic for ExprSupported)
• h_check: The boolean check result

theorem LeanCert.Validity.verify_lower_bound_dyadic (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (hdom : Engine.evalDomainValidDyadic e (fun (x : ℕ) => Core.IntervalDyadic.ofIntervalRat { lo := lo, hi := hi, le := hle } prec) { precision := prec, taylorDepth := depth }) (h_check : checkLowerBoundDyadic e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Golden Theorem for Dyadic Lower Bounds

If the bound check passes and domain validity holds, then ∀ x ∈ [lo, hi], c ≤ Expr.eval (fun _ => x) e.

Convenience Theorems for ExprSupported

For expressions that don't use log, domain validity is automatic. These versions don't require the hdom hypothesis.

theorem LeanCert.Validity.verify_upper_bound_dyadic' (e : Core.Expr) (hsupp : Core.ExprSupported e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (h_check : checkUpperBoundDyadic e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Convenience theorem for ExprSupported expressions (no log). Domain validity is automatic, so only the bound check is needed.

theorem LeanCert.Validity.verify_lower_bound_dyadic' (e : Core.Expr) (hsupp : Core.ExprSupported e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (h_check : checkLowerBoundDyadic e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Convenience theorem for ExprSupported expressions (no log). Domain validity is automatic, so only the bound check is needed.

Strict Inequality Theorems

theorem LeanCert.Validity.verify_strict_upper_bound_dyadic (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (hdom : Engine.evalDomainValidDyadic e (fun (x : ℕ) => Core.IntervalDyadic.ofIntervalRat { lo := lo, hi := hi, le := hle } prec) { precision := prec, taylorDepth := depth }) (h_check : checkStrictUpperBoundDyadic e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Golden Theorem for Strict Dyadic Upper Bounds

If the strict bound check passes and domain validity holds, then ∀ x ∈ [lo, hi], Expr.eval (fun _ => x) e < c.

theorem LeanCert.Validity.verify_strict_lower_bound_dyadic (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (hdom : Engine.evalDomainValidDyadic e (fun (x : ℕ) => Core.IntervalDyadic.ofIntervalRat { lo := lo, hi := hi, le := hle } prec) { precision := prec, taylorDepth := depth }) (h_check : checkStrictLowerBoundDyadic e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Golden Theorem for Strict Dyadic Lower Bounds

If the strict bound check passes and domain validity holds, then ∀ x ∈ [lo, hi], c < Expr.eval (fun _ => x) e.

Convenience Theorems for Strict Inequalities (ExprSupported)

theorem LeanCert.Validity.verify_strict_upper_bound_dyadic' (e : Core.Expr) (hsupp : Core.ExprSupported e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (h_check : checkStrictUpperBoundDyadic e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Convenience theorem for strict upper bounds with ExprSupported expressions.

theorem LeanCert.Validity.verify_strict_lower_bound_dyadic' (e : Core.Expr) (hsupp : Core.ExprSupported e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (h_check : checkStrictLowerBoundDyadic e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Convenience theorem for strict lower bounds with ExprSupported expressions.

WithInv Check Functions

These bundle domain validity + bound check for expressions containing inv/log. A single native_decide call proves both domain validity and the bound.

def LeanCert.Validity.checkUpperBoundDyadicWithInv (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) : Bool

Check upper bound for WithInv expressions (inv/log). Includes domain validity check.

Equations

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

def LeanCert.Validity.checkLowerBoundDyadicWithInv (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) : Bool

Check lower bound for WithInv expressions (inv/log). Includes domain validity check.

Equations

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

def LeanCert.Validity.checkStrictUpperBoundDyadicWithInv (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) : Bool

Check strict upper bound for WithInv expressions. Includes domain validity check.

Equations

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

def LeanCert.Validity.checkStrictLowerBoundDyadicWithInv (e : Core.Expr) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) : Bool

Check strict lower bound for WithInv expressions. Includes domain validity check.

Equations

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

WithInv Golden Theorems

For ExprSupportedWithInv expressions (with inv/log). Domain validity is extracted from the combined check function, so no separate hdom argument is needed.

theorem LeanCert.Validity.verify_upper_bound_dyadic_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (h_check : checkUpperBoundDyadicWithInv e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Golden Theorem for Dyadic upper bounds with inv/log expressions.

theorem LeanCert.Validity.verify_lower_bound_dyadic_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (h_check : checkLowerBoundDyadicWithInv e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Golden Theorem for Dyadic lower bounds with inv/log expressions.

theorem LeanCert.Validity.verify_strict_upper_bound_dyadic_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (h_check : checkStrictUpperBoundDyadicWithInv e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Golden Theorem for strict Dyadic upper bounds with inv/log expressions.

theorem LeanCert.Validity.verify_strict_lower_bound_dyadic_withInv (e : Core.Expr) (hsupp : Core.ExprSupportedWithInv e) (lo hi : ℚ) (hle : lo ≤ hi) (c : ℚ) (prec : ℤ) (depth : ℕ) (h_prec : prec ≤ 0) (h_check : checkStrictLowerBoundDyadicWithInv e lo hi hle c prec depth = true) (x : ℝ) : x ∈ Set.Icc ↑lo ↑hi → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Golden Theorem for strict Dyadic lower bounds with inv/log expressions.