Computable domain-aware automatic differentiation

This module extends LeanCert's computable forward-mode AD path with checked reciprocal and logarithm nodes. The existing ADSupported fragment remains the domain-free fast path. Here, successful evaluation itself certifies both syntactic support and every partial-domain side condition.

def LeanCert.Engine.checkADDomain (e : Core.Expr) (ρ : DualEnv) (cfg : EvalConfig := { }) : Bool

The computable domain-aware AD fragment. Unlike ADSupported, this is a box-dependent check because reciprocal and logarithm have partial domains.

Equations

• LeanCert.Engine.checkADDomain (LeanCert.Core.Expr.const q) ρ cfg = true
• LeanCert.Engine.checkADDomain (LeanCert.Core.Expr.var idx) ρ cfg = true
• LeanCert.Engine.checkADDomain (a.add b) ρ cfg = (LeanCert.Engine.checkADDomain a ρ cfg && LeanCert.Engine.checkADDomain b ρ cfg)
• LeanCert.Engine.checkADDomain (a.mul b) ρ cfg = (LeanCert.Engine.checkADDomain a ρ cfg && LeanCert.Engine.checkADDomain b ρ cfg)
• LeanCert.Engine.checkADDomain a.neg ρ cfg = LeanCert.Engine.checkADDomain a ρ cfg
• LeanCert.Engine.checkADDomain a.exp ρ cfg = LeanCert.Engine.checkADDomain a ρ cfg
• LeanCert.Engine.checkADDomain a.sin ρ cfg = LeanCert.Engine.checkADDomain a ρ cfg
• LeanCert.Engine.checkADDomain a.cos ρ cfg = LeanCert.Engine.checkADDomain a ρ cfg
• LeanCert.Engine.checkADDomain a.inv ρ cfg = (LeanCert.Engine.checkADDomain a ρ cfg && decide ¬(LeanCert.Internal.AD.evalTotalCore a ρ cfg).val.containsZero)
• LeanCert.Engine.checkADDomain a.log ρ cfg = (LeanCert.Engine.checkADDomain a ρ cfg && decide (LeanCert.Internal.AD.evalTotalCore a ρ cfg).val.isPositive)
• LeanCert.Engine.checkADDomain e ρ cfg = false

def LeanCert.Engine.diagnoseADDomainFailure (e : Core.Expr) (ρ : DualEnv) (cfg : EvalConfig := { }) : EvalError

Best-effort structured explanation for a failed domain-aware AD check.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.diagnoseADDomainFailure a.neg ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseADDomainFailure a ρ cfg)
• LeanCert.Engine.diagnoseADDomainFailure a.exp ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseADDomainFailure a ρ cfg)
• LeanCert.Engine.diagnoseADDomainFailure a.sin ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseADDomainFailure a ρ cfg)
• LeanCert.Engine.diagnoseADDomainFailure a.cos ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseADDomainFailure a ρ cfg)
• LeanCert.Engine.diagnoseADDomainFailure (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Engine.EvalError.invalidConfiguration "successful AD expression diagnosed as failure"
• LeanCert.Engine.diagnoseADDomainFailure (LeanCert.Core.Expr.var idx) ρ cfg = LeanCert.Engine.EvalError.invalidConfiguration "successful AD expression diagnosed as failure"
• LeanCert.Engine.diagnoseADDomainFailure e ρ cfg = LeanCert.Engine.EvalError.unsupportedFeature "domain-aware automatic differentiation"

def LeanCert.Engine.evalDualChecked (e : Core.Expr) (ρ : DualEnv) (cfg : EvalConfig := { }) : EvalResult DualInterval

Computable checked dual evaluation. No finite derivative enclosure is returned unless every reciprocal denominator excludes zero and every logarithm argument is strictly positive on the input box.

Equations

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

def LeanCert.Engine.evalWithDerivChecked (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) (cfg : EvalConfig := { }) : EvalResult DualInterval

Checked value-and-derivative evaluation along coordinate idx.

Equations

• LeanCert.Engine.evalWithDerivChecked e ρ idx cfg = LeanCert.Engine.evalDualChecked e (LeanCert.Engine.mkDualEnv ρ idx) cfg

def LeanCert.Engine.derivIntervalChecked (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) (cfg : EvalConfig := { }) : EvalResult Core.IntervalRat

Checked derivative enclosure along coordinate idx.

Equations

• LeanCert.Engine.derivIntervalChecked e ρ idx cfg = do let __do_lift ← LeanCert.Engine.evalWithDerivChecked e ρ idx cfg pure __do_lift.der

def LeanCert.Engine.derivIntervalChecked1 (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig := { }) : EvalResult Core.IntervalRat

Checked derivative enclosure for a single-variable expression.

Equations

• LeanCert.Engine.derivIntervalChecked1 e I cfg = LeanCert.Engine.derivIntervalChecked e (fun (x : ℕ) => I) 0 cfg

theorem LeanCert.Engine.evalDualChecked_val_correct (e : Core.Expr) (ρReal : ℕ → ℝ) (ρDual : DualEnv) (cfg : EvalConfig) (D : DualInterval) (hρ : ∀ (i : ℕ), ρReal i ∈ (ρDual i).val) (hok : evalDualChecked e ρDual cfg = Except.ok D) : Core.Expr.eval ρReal e ∈ D.val

Successful checked dual evaluation encloses the expression value for every real environment represented by the dual environment.

theorem LeanCert.Engine.evalWithDerivChecked_differentiableAt (e : Core.Expr) (ρReal : ℕ → ℝ) (ρInt : IntervalEnv) (idx : ℕ) (cfg : EvalConfig) (D : DualInterval) (x : ℝ) (hx : x ∈ ρInt idx) (hρ : ∀ (i : ℕ), ρReal i ∈ ρInt i) (hok : evalWithDerivChecked e ρInt idx cfg = Except.ok D) : DifferentiableAt ℝ (e.evalAlong ρReal idx) x

A successful checked evaluation proves differentiability at every point in the input box along the selected coordinate.

theorem LeanCert.Engine.evalWithDerivChecked_der_correct (e : Core.Expr) (ρReal : ℕ → ℝ) (ρInt : IntervalEnv) (idx : ℕ) (cfg : EvalConfig) (D : DualInterval) (x : ℝ) (hx : x ∈ ρInt idx) (hρ : ∀ (i : ℕ), ρReal i ∈ ρInt i) (hok : evalWithDerivChecked e ρInt idx cfg = Except.ok D) : deriv (e.evalAlong ρReal idx) x ∈ D.der

Successful checked indexed AD encloses the true partial derivative.

theorem LeanCert.Engine.derivIntervalChecked_correct (e : Core.Expr) (ρReal : ℕ → ℝ) (ρInt : IntervalEnv) (idx : ℕ) (cfg : EvalConfig) (dI : Core.IntervalRat) (x : ℝ) (hx : x ∈ ρInt idx) (hρ : ∀ (i : ℕ), ρReal i ∈ ρInt i) (hok : derivIntervalChecked e ρInt idx cfg = Except.ok dI) : deriv (e.evalAlong ρReal idx) x ∈ dI

Golden soundness theorem for the checked derivative-only API.