Moving sofa: related mathematical developments

• LeanCert.Engine.AD.PartialCorrectness.
• LeanCert.Engine.IntervalEvalDyadic.
• LeanCert.Engine.AD.Dyadic.
• LeanCert.Engine.AD.
• LeanCert.Engine.Optimization.Box.
• LeanCert.Engine.Optimize.
• LeanCert.Engine.Optimization.Gradient.
• LeanCert.Engine.RootFinding.Krawczyk.

Automatic Differentiation - Partial Correctness Theorems

This file proves the correctness of the partial dual evaluator evalDualOption which handles expressions with inv, log, and other domain-restricted functions.

Main theorems

• evalDualOption_val_correct - Value component is correct when evalDualOption returns some
• evalDualOption1_val_correct - Single-variable version
• evalFunc1_differentiableAt_of_evalDualOption - Differentiability when evalDualOption succeeds
• evalDualOption_der_correct - Derivative component is correct
• evalDualOption1_correct - Combined correctness theorem

Design notes

All theorems are FULLY PROVED with no sorry or axioms. The key insight is that when evalDualOption returns some, the domain constraints (nonzero for inv, positive for log) are satisfied.

Correctness of partial dual evaluator

theorem LeanCert.Engine.evalDualOption_val_correct (e : Core.Expr) (ρ_real : ℕ → ℝ) (ρ_dual : DualEnv) (D : DualInterval) (hsome : evalDualOption e ρ_dual = some D) (hρ : ∀ (i : ℕ), ρ_real i ∈ (ρ_dual i).val) : Core.Expr.eval ρ_real e ∈ D.val

The value component of evalDualOption is correct when it returns some. This theorem extends to expressions with inv.

theorem LeanCert.Engine.evalDualOption1_val_correct (e : Core.Expr) (I : Core.IntervalRat) (D : DualInterval) (x : ℝ) (hx : x ∈ I) (hsome : evalDualOption1 e I = some D) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ D.val

Single-variable version of evalDualOption_val_correct

theorem LeanCert.Engine.evalFunc1_inv (e : Core.Expr) : evalFunc1 e.inv = fun (t : ℝ) => (evalFunc1 e t)⁻¹

Helper lemma: evalFunc1 for inv unfolds correctly

theorem LeanCert.Engine.evalFunc1_differentiableAt_of_evalDualOption (e : Core.Expr) (I : Core.IntervalRat) (D : DualInterval) (x : ℝ) (hx : x ∈ I) (hsome : evalDualOption1 e I = some D) : DifferentiableAt ℝ (evalFunc1 e) x

Expressions with inv are differentiable when the denominator is nonzero.

theorem LeanCert.Engine.evalDualOption_der_correct (e : Core.Expr) (I : Core.IntervalRat) (D : DualInterval) (x : ℝ) (hx : x ∈ I) (hsome : evalDualOption1 e I = some D) : deriv (evalFunc1 e) x ∈ D.der

theorem LeanCert.Engine.evalDualOption1_correct (e : Core.Expr) (I : Core.IntervalRat) (D : DualInterval) (x : ℝ) (hx : x ∈ I) (hsome : evalDualOption1 e I = some D) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ D.val ∧ deriv (evalFunc1 e) x ∈ D.der

Combined correctness theorem for evalDualOption1

High-Performance Dyadic Interval Evaluator

This evaluator replaces Rat with Dyadic to prevent denominator explosion. It is designed for complex expressions where the standard evaluator becomes slow.

Main definitions

• DyadicConfig - Configuration for precision and Taylor depth
• LeanCert.Internal.Dyadic.evalUnchecked - Dyadic interval evaluator for expressions
• evalIntervalDyadic_correct - Correctness theorem

Performance

In v1.0, every Rat multiplication required GCD normalization. For deep expressions (e.g., Taylor series with 20+ terms, or optimization with 100+ iterations), denominators grow exponentially, causing timeouts.

In v1.1, Dyadic arithmetic uses bit-shifts instead of GCD. With roundOut, we can enforce a maximum precision after each operation, keeping computation bounded regardless of expression depth.

Example

Consider computing sin(sin(sin(x))) with 15-term Taylor series:

• v1.0 (Rat): ~500ms per call, denominators grow to millions of digits
• v1.1 (Dyadic): ~5ms per call, precision stays at 53 bits

Design notes

For transcendental functions (sin, cos, exp), we delegate to the existing IntervalRat implementation with Taylor series, then convert the result to IntervalDyadic with outward rounding. This reuses verified code while gaining the performance benefits of Dyadic for polynomial operations.

Configuration

structure LeanCert.Engine.DyadicConfig : Type

Configuration for Dyadic interval evaluation.

• precision - Minimum exponent for outward rounding. A value of -53 gives IEEE double-like precision (~15 decimal digits). Use -100 for higher precision.
• taylorDepth - Number of Taylor terms for transcendental functions.

• precision : ℤ

  Minimum exponent (higher = coarser). -53 ≈ IEEE double precision.

• taylorDepth : ℕ

  Number of Taylor series terms for transcendental functions

@[instance_reducible]

instance LeanCert.Engine.instReprDyadicConfig : Repr DyadicConfig

Equations

• LeanCert.Engine.instReprDyadicConfig = { reprPrec := LeanCert.Engine.instReprDyadicConfig.repr }

def LeanCert.Engine.instReprDyadicConfig.repr : DyadicConfig → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Engine.instDecidableEqDyadicConfig : DecidableEq DyadicConfig

Equations

• LeanCert.Engine.instDecidableEqDyadicConfig = LeanCert.Engine.instDecidableEqDyadicConfig.decEq

def LeanCert.Engine.instDecidableEqDyadicConfig.decEq (x✝ x✝¹ : DyadicConfig) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance LeanCert.Engine.instInhabitedDyadicConfig : Inhabited DyadicConfig

Default configuration with IEEE double-like precision

Equations

• LeanCert.Engine.instInhabitedDyadicConfig = { default := { } }

def LeanCert.Engine.DyadicConfig.highPrecision : DyadicConfig

High-precision configuration for critical calculations

Equations

• LeanCert.Engine.DyadicConfig.highPrecision = { precision := -100, taylorDepth := 20 }

def LeanCert.Engine.DyadicConfig.fast : DyadicConfig

Fast configuration for rapid evaluation (lower precision)

Equations

• LeanCert.Engine.DyadicConfig.fast = { precision := -30, taylorDepth := 8 }

Variable Environment

@[reducible, inline]

abbrev LeanCert.Engine.IntervalDyadicEnv : Type

Variable assignment as Dyadic intervals

Equations

• LeanCert.Engine.IntervalDyadicEnv = (ℕ → LeanCert.Core.IntervalDyadic)

def LeanCert.Engine.toDyadicEnv (ρ : IntervalEnv) (prec : ℤ := -53) : IntervalDyadicEnv

Convert a rational interval environment to Dyadic

Equations

• LeanCert.Engine.toDyadicEnv ρ prec i = LeanCert.Core.IntervalDyadic.ofIntervalRat (ρ i) prec

Transcendental Function Wrappers

def LeanCert.Engine.sinIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

Compute sin interval using rational Taylor series, convert to Dyadic

Equations

• LeanCert.Engine.sinIntervalDyadic I cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (I.toIntervalRat.sinComputable cfg.taylorDepth) cfg.precision

def LeanCert.Engine.cosIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

Compute cos interval using rational Taylor series, convert to Dyadic

Equations

• LeanCert.Engine.cosIntervalDyadic I cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (I.toIntervalRat.cosComputable cfg.taylorDepth) cfg.precision

def LeanCert.Engine.expIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

Compute exp interval using rational Taylor series, convert to Dyadic

Equations

• LeanCert.Engine.expIntervalDyadic I cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (I.toIntervalRat.expComputable cfg.taylorDepth) cfg.precision

def LeanCert.Engine.sinhIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

Compute sinh interval using rational Taylor series, convert to Dyadic

Equations

• LeanCert.Engine.sinhIntervalDyadic I cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (I.toIntervalRat.sinhComputable cfg.taylorDepth) cfg.precision

def LeanCert.Engine.coshIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

Compute cosh interval using rational Taylor series, convert to Dyadic

Equations

• LeanCert.Engine.coshIntervalDyadic I cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (I.toIntervalRat.coshComputable cfg.taylorDepth) cfg.precision

def LeanCert.Engine.atanIntervalDyadic (_I : Core.IntervalDyadic) (_cfg : DyadicConfig) : Core.IntervalDyadic

atan interval: global bound [-2, 2]

Equations

• LeanCert.Engine.atanIntervalDyadic _I _cfg = { lo := LeanCert.Core.Dyadic.ofInt (-2), hi := LeanCert.Core.Dyadic.ofInt 2, le := LeanCert.Engine.atanIntervalDyadic._proof_1 }

def LeanCert.Engine.tanhIntervalDyadic (_I : Core.IntervalDyadic) (_cfg : DyadicConfig) : Core.IntervalDyadic

tanh interval: global bound [-1, 1]

Equations

• LeanCert.Engine.tanhIntervalDyadic _I _cfg = { lo := LeanCert.Core.Dyadic.ofInt (-1), hi := LeanCert.Core.Dyadic.ofInt 1, le := LeanCert.Engine.tanhIntervalDyadic._proof_1 }

def LeanCert.Engine.arsinhIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

arsinh interval: wide box bound via rational arsinhInterval

Equations

• LeanCert.Engine.arsinhIntervalDyadic I cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (LeanCert.Engine.arsinhInterval I.toIntervalRat) cfg.precision

def LeanCert.Engine.atanhIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

atanh interval: computable Taylor series via rational atanhComputable

Equations

• LeanCert.Engine.atanhIntervalDyadic I cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (I.toIntervalRat.atanhComputable cfg.taylorDepth) cfg.precision

def LeanCert.Engine.sincIntervalDyadic (_I : Core.IntervalDyadic) (_cfg : DyadicConfig) : Core.IntervalDyadic

sinc interval: global bound [-1, 1]

Equations

• LeanCert.Engine.sincIntervalDyadic _I _cfg = { lo := LeanCert.Core.Dyadic.ofInt (-1), hi := LeanCert.Core.Dyadic.ofInt 1, le := LeanCert.Engine.tanhIntervalDyadic._proof_1 }

def LeanCert.Engine.erfIntervalDyadic (_I : Core.IntervalDyadic) (_cfg : DyadicConfig) : Core.IntervalDyadic

erf interval: global bound [-1, 1]

Equations

• LeanCert.Engine.erfIntervalDyadic _I _cfg = { lo := LeanCert.Core.Dyadic.ofInt (-1), hi := LeanCert.Core.Dyadic.ofInt 1, le := LeanCert.Engine.tanhIntervalDyadic._proof_1 }

def LeanCert.Engine.invIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

Compute inv interval: convert to Rat, use invInterval, convert back to Dyadic

Equations

• LeanCert.Engine.invIntervalDyadic I cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (LeanCert.Engine.invInterval I.toIntervalRat) cfg.precision

def LeanCert.Engine.sqrtIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

sqrt interval: uses conservative bound [0, max(hi, 1)]

Equations

• LeanCert.Engine.sqrtIntervalDyadic I cfg = I.sqrt cfg.precision

def LeanCert.Engine.logIntervalDyadic (I : Core.IntervalDyadic) (cfg : DyadicConfig) : Core.IntervalDyadic

log interval: conservative global bound. For any x > 0, log(x) ∈ (-∞, ∞), but we use a finite interval. For x ∈ [lo, hi] with lo > 0:

• log is monotone, so log(x) ∈ [log(lo), log(hi)]
• Legacy total-evaluator fallback; strict callers reject this domain

Equations

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

def LeanCert.Engine.rpowFromCachedLogDyadic (logBase : Core.IntervalDyadic) (p : ℚ) (cfg : DyadicConfig) : Core.IntervalDyadic

Real power from a cached logarithm interval.

If Real.log x ∈ logBase, this computes an interval for x ^ (p : ℝ) as exp(p * log x) without recomputing log x. This is the hot-path primitive for cached finite sums with many terms of the form x ^ q_k.

Equations

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

def LeanCert.Engine.rpowIntervalDyadic (base : Core.IntervalDyadic) (p : ℚ) (cfg : DyadicConfig) : Core.IntervalDyadic

Real power x^p for x > 0 and rational p, computed via exp(p * log(x)).

For x ∈ [lo, hi] with lo > 0 and rational exponent p:

• x^p = exp(p * log(x))
• We compute log(x), multiply by p, then apply exp

This is the key operation for BKLNW-style sums where terms are x^(1/k - 1/3).

Equations

• LeanCert.Engine.rpowIntervalDyadic base p cfg = LeanCert.Engine.rpowFromCachedLogDyadic (LeanCert.Engine.logIntervalDyadic base cfg) p cfg

theorem LeanCert.Engine.mem_rpowFromCachedLogDyadic {x : ℝ} {logBase : Core.IntervalDyadic} (hlog : Real.log x ∈ logBase) (hx_pos : 0 < x) (p : ℚ) (cfg : DyadicConfig) (hprec : cfg.precision ≤ 0 := by norm_num) : x ^ ↑p ∈ rpowFromCachedLogDyadic logBase p cfg

Correctness of rpowFromCachedLogDyadic: a cached interval containing Real.log x is enough to enclose x ^ p.

theorem LeanCert.Engine.mem_rpowIntervalDyadic {x : ℝ} {base : Core.IntervalDyadic} (hx : x ∈ base) (hpos : base.toIntervalRat.lo > 0) (p : ℚ) (cfg : DyadicConfig) (hprec : cfg.precision ≤ 0 := by norm_num) : x ^ ↑p ∈ rpowIntervalDyadic base p cfg

Correctness of rpowIntervalDyadic: if x ∈ base and base.lo > 0, then x^p ∈ result

Main Evaluator

def LeanCert.Internal.Dyadic.evalUnchecked (e : Core.Expr) (ρ : Engine.IntervalDyadicEnv) (cfg : Engine.DyadicConfig := { }) : Core.IntervalDyadic

High-performance Dyadic interval evaluator.

This is the core function for v1.1. It evaluates expressions using Dyadic arithmetic for polynomial operations (add, mul, neg) and delegates to rational Taylor series for transcendentals.

Returns an interval guaranteed to contain all possible values of the expression when ExprSupportedCore holds. For other expressions, it computes conservative fallbacks (e.g., inv/log), but the core correctness theorem does not apply.

Equations

• LeanCert.Internal.Dyadic.evalUnchecked (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (LeanCert.Core.IntervalRat.singleton q) cfg.precision
• LeanCert.Internal.Dyadic.evalUnchecked (LeanCert.Core.Expr.var idx) ρ cfg = ρ idx
• LeanCert.Internal.Dyadic.evalUnchecked (e₁.add e₂) ρ cfg = ((LeanCert.Internal.Dyadic.evalUnchecked e₁ ρ cfg).add (LeanCert.Internal.Dyadic.evalUnchecked e₂ ρ cfg)).roundOut cfg.precision
• LeanCert.Internal.Dyadic.evalUnchecked (e₁.mul e₂) ρ cfg = ((LeanCert.Internal.Dyadic.evalUnchecked e₁ ρ cfg).mul (LeanCert.Internal.Dyadic.evalUnchecked e₂ ρ cfg)).roundOut cfg.precision
• LeanCert.Internal.Dyadic.evalUnchecked e_2.neg ρ cfg = (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg).neg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.inv ρ cfg = LeanCert.Engine.invIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.exp ρ cfg = LeanCert.Engine.expIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.sin ρ cfg = LeanCert.Engine.sinIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.cos ρ cfg = LeanCert.Engine.cosIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.log ρ cfg = LeanCert.Engine.logIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.atan ρ cfg = LeanCert.Engine.atanIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.arsinh ρ cfg = LeanCert.Engine.arsinhIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.atanh ρ cfg = LeanCert.Engine.atanhIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.sinc ρ cfg = LeanCert.Engine.sincIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.erf ρ cfg = LeanCert.Engine.erfIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.sinh ρ cfg = LeanCert.Engine.sinhIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.cosh ρ cfg = LeanCert.Engine.coshIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.tanh ρ cfg = LeanCert.Engine.tanhIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked e_2.sqrt ρ cfg = LeanCert.Engine.sqrtIntervalDyadic (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg) cfg
• LeanCert.Internal.Dyadic.evalUnchecked (LeanCert.Core.Expr.namedConst c) ρ cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat c.interval cfg.precision

Correctness

def LeanCert.Engine.envMemDyadic (ρ_real : ℕ → ℝ) (ρ_dyad : IntervalDyadicEnv) : Prop

A real environment is contained in a Dyadic interval environment

Equations

• LeanCert.Engine.envMemDyadic ρ_real ρ_dyad = ∀ (i : ℕ), ρ_real i ∈ ρ_dyad i

def LeanCert.Engine.evalDomainValidDyadic (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig := { }) : Prop

Domain validity for Dyadic evaluation. This is defined directly in terms of LeanCert.Internal.Dyadic.evalUnchecked to ensure compatibility. For log, we require the argument interval (converted to Rat) to have positive lower bound.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.evalDomainValidDyadic (LeanCert.Core.Expr.const q) ρ cfg = True
• LeanCert.Engine.evalDomainValidDyadic (LeanCert.Core.Expr.var idx) ρ cfg = True
• LeanCert.Engine.evalDomainValidDyadic (e₁.add e₂) ρ cfg = (LeanCert.Engine.evalDomainValidDyadic e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValidDyadic e₂ ρ cfg)
• LeanCert.Engine.evalDomainValidDyadic (e₁.mul e₂) ρ cfg = (LeanCert.Engine.evalDomainValidDyadic e₁ ρ cfg ∧ LeanCert.Engine.evalDomainValidDyadic e₂ ρ cfg)
• LeanCert.Engine.evalDomainValidDyadic e_2.neg ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.exp ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.sin ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.cos ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.log ρ cfg = (LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg ∧ (LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg).toIntervalRat.lo > 0)
• LeanCert.Engine.evalDomainValidDyadic e_2.atan ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.arsinh ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.sinc ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.erf ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.sinh ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.cosh ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.tanh ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic e_2.sqrt ρ cfg = LeanCert.Engine.evalDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.evalDomainValidDyadic (LeanCert.Core.Expr.namedConst c) ρ cfg = True

def LeanCert.Engine.checkDomainValidDyadic (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig := { }) : Bool

Computable (Bool) domain validity check for Dyadic evaluation.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.checkDomainValidDyadic (LeanCert.Core.Expr.const q) ρ cfg = true
• LeanCert.Engine.checkDomainValidDyadic (LeanCert.Core.Expr.var idx) ρ cfg = true
• LeanCert.Engine.checkDomainValidDyadic (e₁.add e₂) ρ cfg = (LeanCert.Engine.checkDomainValidDyadic e₁ ρ cfg && LeanCert.Engine.checkDomainValidDyadic e₂ ρ cfg)
• LeanCert.Engine.checkDomainValidDyadic (e₁.mul e₂) ρ cfg = (LeanCert.Engine.checkDomainValidDyadic e₁ ρ cfg && LeanCert.Engine.checkDomainValidDyadic e₂ ρ cfg)
• LeanCert.Engine.checkDomainValidDyadic e_2.neg ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.exp ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.sin ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.cos ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.log ρ cfg = (LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg && decide ((LeanCert.Internal.Dyadic.evalUnchecked e_2 ρ cfg).toIntervalRat.lo > 0))
• LeanCert.Engine.checkDomainValidDyadic e_2.atan ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.arsinh ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.sinc ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.erf ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.sinh ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.cosh ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.tanh ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic e_2.sqrt ρ cfg = LeanCert.Engine.checkDomainValidDyadic e_2 ρ cfg
• LeanCert.Engine.checkDomainValidDyadic (LeanCert.Core.Expr.namedConst c) ρ cfg = true

theorem LeanCert.Engine.checkDomainValidDyadic_correct (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig) : checkDomainValidDyadic e ρ cfg = true → evalDomainValidDyadic e ρ cfg

structure LeanCert.Internal.Dyadic.PreparedContext : Type

Static data prepared once for repeated Dyadic evaluation.

The context is operation-independent: logarithm, exponential, trigonometric, and inverse-hyperbolic kernels share certified constants and coefficient families without changing the public evaluator configuration.

• cfg : Engine.DyadicConfig

  Precision and rounding settings shared by prepared interval computations.

• ln2 : Core.IntervalRat

  A precomputed rational enclosure of the natural logarithm of two.

• expCoeffs : List ℚ

  Precomputed rational coefficients for the exponential Taylor polynomial.

• sinCoeffs : List ℚ

  Precomputed rational coefficients for the sine Taylor polynomial.

• cosCoeffs : List ℚ

  Precomputed rational coefficients for the cosine Taylor polynomial.

• atanhCoeffs : List ℚ

  Precomputed rational coefficients for the inverse hyperbolic tangent expansion.

def LeanCert.Internal.Dyadic.instReprPreparedContext.repr : PreparedContext → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Internal.Dyadic.instReprPreparedContext : Repr PreparedContext

Equations

• LeanCert.Internal.Dyadic.instReprPreparedContext = { reprPrec := LeanCert.Internal.Dyadic.instReprPreparedContext.repr }

def LeanCert.Internal.Dyadic.prepareContext (cfg : Engine.DyadicConfig) : PreparedContext

Deterministically prepare all configuration-dependent numerical data.

Equations

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

@[simp]

theorem LeanCert.Internal.Dyadic.prepareContext_cfg (cfg : Engine.DyadicConfig) : (prepareContext cfg).cfg = cfg

def LeanCert.Internal.Dyadic.logIntervalPrepared (I : Core.IntervalDyadic) (ctx : PreparedContext) : Core.IntervalDyadic

Logarithm kernel using the context's prepared certified constants.

Equations

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

theorem LeanCert.Internal.Dyadic.logIntervalPrepared_prepareContext (I : Core.IntervalDyadic) (cfg : Engine.DyadicConfig) : logIntervalPrepared I (prepareContext cfg) = Engine.logIntervalDyadic I cfg

def LeanCert.Internal.Dyadic.expIntervalPrepared (I : Core.IntervalDyadic) (ctx : PreparedContext) : Core.IntervalDyadic

Exponential kernel using the context's prepared Taylor coefficients.

Equations

• LeanCert.Internal.Dyadic.expIntervalPrepared I ctx = LeanCert.Core.IntervalDyadic.ofIntervalRat (I.toIntervalRat.expComputableWithCoeffs ctx.cfg.taylorDepth ctx.expCoeffs) ctx.cfg.precision

theorem LeanCert.Internal.Dyadic.expIntervalPrepared_prepareContext (I : Core.IntervalDyadic) (cfg : Engine.DyadicConfig) : expIntervalPrepared I (prepareContext cfg) = Engine.expIntervalDyadic I cfg

def LeanCert.Internal.Dyadic.sinIntervalPrepared (I : Core.IntervalDyadic) (ctx : PreparedContext) : Core.IntervalDyadic

Sine kernel using the context's prepared Taylor coefficients.

Equations

• LeanCert.Internal.Dyadic.sinIntervalPrepared I ctx = LeanCert.Core.IntervalDyadic.ofIntervalRat (I.toIntervalRat.sinComputableWithCoeffs ctx.cfg.taylorDepth ctx.sinCoeffs) ctx.cfg.precision

theorem LeanCert.Internal.Dyadic.sinIntervalPrepared_prepareContext (I : Core.IntervalDyadic) (cfg : Engine.DyadicConfig) : sinIntervalPrepared I (prepareContext cfg) = Engine.sinIntervalDyadic I cfg

def LeanCert.Internal.Dyadic.cosIntervalPrepared (I : Core.IntervalDyadic) (ctx : PreparedContext) : Core.IntervalDyadic

Cosine kernel using the context's prepared Taylor coefficients.

Equations

• LeanCert.Internal.Dyadic.cosIntervalPrepared I ctx = LeanCert.Core.IntervalDyadic.ofIntervalRat (I.toIntervalRat.cosComputableWithCoeffs ctx.cfg.taylorDepth ctx.cosCoeffs) ctx.cfg.precision

theorem LeanCert.Internal.Dyadic.cosIntervalPrepared_prepareContext (I : Core.IntervalDyadic) (cfg : Engine.DyadicConfig) : cosIntervalPrepared I (prepareContext cfg) = Engine.cosIntervalDyadic I cfg

def LeanCert.Internal.Dyadic.atanhIntervalPrepared (I : Core.IntervalDyadic) (ctx : PreparedContext) : Core.IntervalDyadic

Inverse-hyperbolic-tangent kernel using prepared Taylor coefficients.

Equations

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

theorem LeanCert.Internal.Dyadic.atanhIntervalPrepared_prepareContext (I : Core.IntervalDyadic) (cfg : Engine.DyadicConfig) : atanhIntervalPrepared I (prepareContext cfg) = Engine.atanhIntervalDyadic I cfg

def LeanCert.Internal.Dyadic.evalCached (e : Core.Expr) (ρ : Engine.IntervalDyadicEnv) (cfg : Engine.DyadicConfig := { }) : Core.IntervalDyadic × Bool

Evaluate an expression and its domain-validity bit in one traversal. The value component is exactly LeanCert.Internal.Dyadic.evalUnchecked; the validity component is exactly checkDomainValidDyadic.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Internal.Dyadic.evalCached (LeanCert.Core.Expr.const q) ρ cfg = (LeanCert.Core.IntervalDyadic.ofIntervalRat (LeanCert.Core.IntervalRat.singleton q) cfg.precision, true)
• LeanCert.Internal.Dyadic.evalCached (LeanCert.Core.Expr.var idx) ρ cfg = (ρ idx, true)
• LeanCert.Internal.Dyadic.evalCached e_2.neg ρ cfg = ((LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).1.neg, (LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).2)
• LeanCert.Internal.Dyadic.evalCached e_2.exp ρ cfg = (LeanCert.Engine.expIntervalDyadic (LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).1 cfg, (LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).2)
• LeanCert.Internal.Dyadic.evalCached e_2.sin ρ cfg = (LeanCert.Engine.sinIntervalDyadic (LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).1 cfg, (LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).2)
• LeanCert.Internal.Dyadic.evalCached e_2.cos ρ cfg = (LeanCert.Engine.cosIntervalDyadic (LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).1 cfg, (LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).2)
• LeanCert.Internal.Dyadic.evalCached e_2.erf ρ cfg = (LeanCert.Engine.erfIntervalDyadic (LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).1 cfg, (LeanCert.Internal.Dyadic.evalCached e_2 ρ cfg).2)
• LeanCert.Internal.Dyadic.evalCached (LeanCert.Core.Expr.namedConst c) ρ cfg = (LeanCert.Core.IntervalDyadic.ofIntervalRat c.interval cfg.precision, true)

def LeanCert.Internal.Dyadic.evalPreparedCached (e : Core.Expr) (ρ : Engine.IntervalDyadicEnv) (ctx : PreparedContext) : Core.IntervalDyadic × Bool

Prepared evaluator: identical certificate semantics to evalCached, but configuration-dependent data is shared across every evaluation.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Internal.Dyadic.evalPreparedCached (LeanCert.Core.Expr.const q) ρ ctx = (LeanCert.Core.IntervalDyadic.ofIntervalRat (LeanCert.Core.IntervalRat.singleton q) ctx.cfg.precision, true)
• LeanCert.Internal.Dyadic.evalPreparedCached (LeanCert.Core.Expr.var idx) ρ ctx = (ρ idx, true)
• LeanCert.Internal.Dyadic.evalPreparedCached e_2.neg ρ ctx = ((LeanCert.Internal.Dyadic.evalPreparedCached e_2 ρ ctx).1.neg, (LeanCert.Internal.Dyadic.evalPreparedCached e_2 ρ ctx).2)
• LeanCert.Internal.Dyadic.evalPreparedCached (LeanCert.Core.Expr.namedConst c) ρ ctx = (LeanCert.Core.IntervalDyadic.ofIntervalRat c.interval ctx.cfg.precision, true)

theorem LeanCert.Engine.evalIntervalDyadicCached_fst (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig := { }) : (Internal.Dyadic.evalCached e ρ cfg).1 = Internal.Dyadic.evalUnchecked e ρ cfg

theorem LeanCert.Engine.evalIntervalDyadicCached_snd (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig := { }) : (Internal.Dyadic.evalCached e ρ cfg).2 = checkDomainValidDyadic e ρ cfg

theorem LeanCert.Engine.evalIntervalDyadicPreparedCached_fst (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig := { }) : (Internal.Dyadic.evalPreparedCached e ρ (Internal.Dyadic.prepareContext cfg)).1 = Internal.Dyadic.evalUnchecked e ρ cfg

theorem LeanCert.Engine.evalIntervalDyadicPreparedCached_snd (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig := { }) : (Internal.Dyadic.evalPreparedCached e ρ (Internal.Dyadic.prepareContext cfg)).2 = checkDomainValidDyadic e ρ cfg

@[irreducible]

def LeanCert.Engine.diagnoseEvalIntervalDyadicFailure (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig := { }) : EvalError

Diagnose the first failed Dyadic domain check.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.neg ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.exp ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.sin ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.cos ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.atan ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.arsinh ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.sinc ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.erf ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.sinh ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.cosh ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.tanh ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2.sqrt ρ cfg = LeanCert.Engine.EvalError.nestedFailure "unary operand" (LeanCert.Engine.diagnoseEvalIntervalDyadicFailure e_2 ρ cfg)
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Engine.EvalError.unsupportedBackend "internal: total Dyadic expression unexpectedly failed"
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure (LeanCert.Core.Expr.var idx) ρ cfg = LeanCert.Engine.EvalError.unsupportedBackend "internal: total Dyadic expression unexpectedly failed"
• LeanCert.Engine.diagnoseEvalIntervalDyadicFailure (LeanCert.Core.Expr.namedConst c) ρ cfg = LeanCert.Engine.EvalError.unsupportedBackend "internal: total Dyadic expression unexpectedly failed"

def LeanCert.Engine.evalIntervalDyadicChecked (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig := { }) : EvalResult Core.IntervalDyadic

Checked Dyadic evaluator. The finite fallback branches of the legacy total evaluator are never exposed after a failed domain check.

Equations

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

theorem LeanCert.Engine.evalDomainValidDyadic_of_ExprSupported {e : Core.Expr} (hsupp : ADSupported e) (ρ : IntervalDyadicEnv) (cfg : DyadicConfig := { }) : evalDomainValidDyadic e ρ cfg

Domain validity is trivially true for ADSupported expressions (which exclude log).

theorem LeanCert.Engine.evalIntervalDyadic_correct (e : Core.Expr) (hsupp : ExprSupportedCore e) (ρ_real : ℕ → ℝ) (ρ_dyad : IntervalDyadicEnv) (hρ : envMemDyadic ρ_real ρ_dyad) (cfg : DyadicConfig := { }) (hprec : cfg.precision ≤ 0 := by norm_num) (hdom : evalDomainValidDyadic e ρ_dyad cfg) : Core.Expr.eval ρ_real e ∈ Internal.Dyadic.evalUnchecked e ρ_dyad cfg

Fundamental correctness theorem for Dyadic evaluation.

This theorem states that for any supported expression and any real values within the input intervals, the result of evaluating the expression is contained in the computed Dyadic interval.

The proof follows the same structure as evalIntervalCore_correct, but with additional steps for handling Dyadic ↔ Rat conversions and rounding. Requires cfg.precision ≤ 0 (the default -53 satisfies this).

Note: Requires domain validity for log (positive argument interval).

theorem LeanCert.Engine.evalIntervalDyadic_correct_of_domain (e : Core.Expr) (ρ_real : ℕ → ℝ) (ρ_dyad : IntervalDyadicEnv) (hρ : envMemDyadic ρ_real ρ_dyad) (cfg : DyadicConfig := { }) (hprec : cfg.precision ≤ 0 := by norm_num) (hdom : evalDomainValidDyadic e ρ_dyad cfg) : Core.Expr.eval ρ_real e ∈ Internal.Dyadic.evalUnchecked e ρ_dyad cfg

Correctness of Dyadic evaluation for every expression whose recursively checked domain conditions hold.

theorem LeanCert.Engine.evalIntervalDyadicChecked_correct (e : Core.Expr) (ρ_real : ℕ → ℝ) (ρ_dyad : IntervalDyadicEnv) (hρ : envMemDyadic ρ_real ρ_dyad) (cfg : DyadicConfig := { }) (hprec : cfg.precision ≤ 0 := by norm_num) (result : Core.IntervalDyadic) (hsuccess : evalIntervalDyadicChecked e ρ_dyad cfg = Except.ok result) : Core.Expr.eval ρ_real e ∈ result

Successful checked Dyadic evaluation encloses the true value for every expression, provided outward-rounding precision is nonpositive.

Verification Checkers

def LeanCert.Engine.checkUpperBoundDyadic (e : Core.Expr) (ρ : IntervalDyadicEnv) (q : ℚ) (cfg : DyadicConfig := { }) : Bool

Check if expression is bounded above by q

Equations

• LeanCert.Engine.checkUpperBoundDyadic e ρ q cfg = (LeanCert.Internal.Dyadic.evalUnchecked e ρ cfg).upperBoundedBy q

def LeanCert.Engine.checkLowerBoundDyadic (e : Core.Expr) (ρ : IntervalDyadicEnv) (q : ℚ) (cfg : DyadicConfig := { }) : Bool

Check if expression is bounded below by q

Equations

• LeanCert.Engine.checkLowerBoundDyadic e ρ q cfg = (LeanCert.Internal.Dyadic.evalUnchecked e ρ cfg).lowerBoundedBy q

def LeanCert.Engine.checkBoundsDyadic (e : Core.Expr) (ρ : IntervalDyadicEnv) (lo hi : ℚ) (cfg : DyadicConfig := { }) : Bool

Check if expression is bounded in interval [lo, hi]

Equations

• LeanCert.Engine.checkBoundsDyadic e ρ lo hi cfg = ((LeanCert.Internal.Dyadic.evalUnchecked e ρ cfg).lowerBoundedBy lo && (LeanCert.Internal.Dyadic.evalUnchecked e ρ cfg).upperBoundedBy hi)

Domain-aware automatic differentiation with Dyadic intervals

This module is the bounded-denominator counterpart of AD.DomainChecked. Polynomial dual arithmetic is performed with Dyadic endpoints and outward rounding after every addition and multiplication. Transcendental values use the same verified rational Taylor kernels as the Dyadic value evaluator and are rounded back to Dyadic endpoints.

The public entry points are checked: unsupported syntax, invalid reciprocal or logarithm domains, and positive rounding precisions return EvalError rather than a finite interval.

structure LeanCert.Engine.DualIntervalDyadic : Type

A value interval and one directional derivative interval, both Dyadic.

• val : Core.IntervalDyadic

  The interval enclosing the function value.

• der : Core.IntervalDyadic

  The interval enclosing the derivative.

@[instance_reducible]

instance LeanCert.Engine.instReprDualIntervalDyadic : Repr DualIntervalDyadic

Equations

• LeanCert.Engine.instReprDualIntervalDyadic = { reprPrec := LeanCert.Engine.instReprDualIntervalDyadic.repr }

def LeanCert.Engine.instReprDualIntervalDyadic.repr : DualIntervalDyadic → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Engine.instInhabitedDualIntervalDyadic : Inhabited DualIntervalDyadic

Equations

• LeanCert.Engine.instInhabitedDualIntervalDyadic = { default := { val := default, der := default } }

@[reducible, inline]

abbrev LeanCert.Engine.DualDyadicEnv : Type

An environment of Dyadic dual intervals.

Equations

• LeanCert.Engine.DualDyadicEnv = (ℕ → LeanCert.Engine.DualIntervalDyadic)

def LeanCert.Engine.DualIntervalDyadic.zero : Core.IntervalDyadic

The singleton dyadic interval at zero.

Equations

• LeanCert.Engine.DualIntervalDyadic.zero = LeanCert.Core.IntervalDyadic.singleton LeanCert.Core.Dyadic.zero

def LeanCert.Engine.DualIntervalDyadic.one : Core.IntervalDyadic

The singleton dyadic interval at one.

Equations

• LeanCert.Engine.DualIntervalDyadic.one = LeanCert.Core.IntervalDyadic.singleton (LeanCert.Core.Dyadic.ofInt 1)

def LeanCert.Engine.DualIntervalDyadic.const (q : ℚ) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Enclose a rational constant in a dyadic interval with zero derivative.

Equations

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

def LeanCert.Engine.DualIntervalDyadic.varActive (I : Core.IntervalDyadic) : DualIntervalDyadic

An input interval whose derivative is the singleton one.

Equations

• LeanCert.Engine.DualIntervalDyadic.varActive I = { val := I, der := LeanCert.Engine.DualIntervalDyadic.one }

def LeanCert.Engine.DualIntervalDyadic.varPassive (I : Core.IntervalDyadic) : DualIntervalDyadic

An input interval held constant, with singleton zero derivative.

Equations

• LeanCert.Engine.DualIntervalDyadic.varPassive I = { val := I, der := LeanCert.Engine.DualIntervalDyadic.zero }

def LeanCert.Engine.DualIntervalDyadic.add (a b : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Addition with dyadic interval propagation of values and derivatives.

Equations

• a.add b cfg = { val := a.val.addRounded b.val cfg.precision, der := a.der.addRounded b.der cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.mul (a b : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Multiplication with dyadic interval propagation of values and derivatives.

Equations

• a.mul b cfg = { val := a.val.mulRounded b.val cfg.precision, der := (a.der.mulRounded b.val cfg.precision).addRounded (a.val.mulRounded b.der cfg.precision) cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.neg (a : DualIntervalDyadic) : DualIntervalDyadic

Negation with dyadic interval propagation of values and derivatives.

Equations

• a.neg = { val := a.val.neg, der := a.der.neg }

def LeanCert.Engine.DualIntervalDyadic.inv (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Reciprocal with dyadic interval propagation of values and derivatives.

Equations

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

def LeanCert.Engine.DualIntervalDyadic.exp (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Exponential with dyadic interval propagation of values and derivatives.

Equations

• a.exp cfg = { val := LeanCert.Engine.expIntervalDyadic a.val cfg, der := (LeanCert.Engine.expIntervalDyadic a.val cfg).mulRounded a.der cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.sin (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Sine with dyadic interval propagation of values and derivatives.

Equations

• a.sin cfg = { val := LeanCert.Engine.sinIntervalDyadic a.val cfg, der := (LeanCert.Engine.cosIntervalDyadic a.val cfg).mulRounded a.der cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.cos (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Cosine with dyadic interval propagation of values and derivatives.

Equations

• a.cos cfg = { val := LeanCert.Engine.cosIntervalDyadic a.val cfg, der := (LeanCert.Engine.sinIntervalDyadic a.val cfg).neg.mulRounded a.der cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.log (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Natural logarithm with dyadic interval propagation of values and derivatives.

Equations

• a.log cfg = { val := LeanCert.Engine.logIntervalDyadic a.val cfg, der := (LeanCert.Engine.invIntervalDyadic a.val cfg).mulRounded a.der cfg.precision }

def LeanCert.Internal.AD.Dyadic.evalTotal (e : Core.Expr) (rho : Engine.DualDyadicEnv) (cfg : Engine.DyadicConfig := { }) : Engine.DualIntervalDyadic

Total computational kernel. Sound public use goes through the checked entry points below.

Equations

• LeanCert.Internal.AD.Dyadic.evalTotal (LeanCert.Core.Expr.const q) rho cfg = LeanCert.Engine.DualIntervalDyadic.const q cfg
• LeanCert.Internal.AD.Dyadic.evalTotal (LeanCert.Core.Expr.var i) rho cfg = rho i
• LeanCert.Internal.AD.Dyadic.evalTotal (a.add b) rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).add (LeanCert.Internal.AD.Dyadic.evalTotal b rho cfg) cfg
• LeanCert.Internal.AD.Dyadic.evalTotal (a.mul b) rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).mul (LeanCert.Internal.AD.Dyadic.evalTotal b rho cfg) cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.neg rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).neg
• LeanCert.Internal.AD.Dyadic.evalTotal a.inv rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).inv cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.exp rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).exp cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.sin rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).sin cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.cos rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).cos cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.log rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).log cfg
• LeanCert.Internal.AD.Dyadic.evalTotal e rho cfg = default

def LeanCert.Engine.DualDyadicEnv.values (rho : DualDyadicEnv) : IntervalDyadicEnv

Value projection of a Dyadic dual environment.

Equations

• rho.values i = (rho i).val

def LeanCert.Engine.mkDualDyadicEnv (rho : IntervalDyadicEnv) (idx : ℕ) : DualDyadicEnv

Dual environment selecting coordinate idx.

Equations

• LeanCert.Engine.mkDualDyadicEnv rho idx i = if i = idx then LeanCert.Engine.DualIntervalDyadic.varActive (rho i) else LeanCert.Engine.DualIntervalDyadic.varPassive (rho i)

@[simp]

theorem LeanCert.Engine.mkDualDyadicEnv_values (rho : IntervalDyadicEnv) (idx : ℕ) : (mkDualDyadicEnv rho idx).values = rho

def LeanCert.Engine.checkDyadicADFragment : Core.Expr → Bool

The deliberately small v1 Dyadic AD fragment.

Equations

• LeanCert.Engine.checkDyadicADFragment (LeanCert.Core.Expr.const q) = true
• LeanCert.Engine.checkDyadicADFragment (LeanCert.Core.Expr.var i) = true
• LeanCert.Engine.checkDyadicADFragment (a.add b) = (LeanCert.Engine.checkDyadicADFragment a && LeanCert.Engine.checkDyadicADFragment b)
• LeanCert.Engine.checkDyadicADFragment (a.mul b) = (LeanCert.Engine.checkDyadicADFragment a && LeanCert.Engine.checkDyadicADFragment b)
• LeanCert.Engine.checkDyadicADFragment a.neg = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.inv = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.exp = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.sin = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.cos = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.log = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment x✝ = false

def LeanCert.Engine.checkDyadicADDomain (e : Core.Expr) (rho : DualDyadicEnv) (cfg : DyadicConfig := { }) : Bool

Box-dependent domain check for the Dyadic AD kernel.

Equations

• LeanCert.Engine.checkDyadicADDomain e rho cfg = (LeanCert.Engine.checkDyadicADFragment e && (LeanCert.Internal.Dyadic.evalCached e rho.values cfg).2)

def LeanCert.Engine.diagnoseDyadicADFailure (e : Core.Expr) (rho : DualDyadicEnv) (cfg : DyadicConfig := { }) : EvalError

Explain the first failed support or domain check.

Equations

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

def LeanCert.Engine.evalDualDyadicChecked (e : Core.Expr) (rho : DualDyadicEnv) (cfg : DyadicConfig := { }) : EvalResult DualIntervalDyadic

Checked Dyadic dual evaluation.

Equations

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

def LeanCert.Engine.evalWithDerivDyadicChecked (e : Core.Expr) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig := { }) : EvalResult DualIntervalDyadic

Checked value-and-derivative evaluation along coordinate idx.

Equations

• LeanCert.Engine.evalWithDerivDyadicChecked e rho idx cfg = LeanCert.Engine.evalDualDyadicChecked e (LeanCert.Engine.mkDualDyadicEnv rho idx) cfg

def LeanCert.Engine.derivIntervalDyadicChecked (e : Core.Expr) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig := { }) : EvalResult Core.IntervalDyadic

Checked Dyadic derivative enclosure along coordinate idx.

Equations

• LeanCert.Engine.derivIntervalDyadicChecked e rho idx cfg = do let __do_lift ← LeanCert.Engine.evalWithDerivDyadicChecked e rho idx cfg pure __do_lift.der

def LeanCert.Engine.derivIntervalDyadicChecked1 (e : Core.Expr) (I : Core.IntervalDyadic) (cfg : DyadicConfig := { }) : EvalResult Core.IntervalDyadic

Checked Dyadic derivative enclosure for a single-variable expression.

Equations

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

def LeanCert.Engine.derivIntervalDyadicCheckedOfRat (e : Core.Expr) (rho : IntervalEnv) (idx : ℕ) (cfg : DyadicConfig := { }) : EvalResult Core.IntervalDyadic

Convenience boundary for callers whose boxes use rational endpoints.

Equations

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

def LeanCert.Engine.derivIntervalDyadicChecked1OfRat (e : Core.Expr) (I : Core.IntervalRat) (cfg : DyadicConfig := { }) : EvalResult Core.IntervalDyadic

Single-variable rational-input convenience boundary.

Equations

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

theorem LeanCert.Engine.evalTotalDyadic_val_of_fragment (e : Core.Expr) (rho : DualDyadicEnv) (cfg : DyadicConfig) (hsupp : checkDyadicADFragment e = true) : (Internal.AD.Dyadic.evalTotal e rho cfg).val = Internal.Dyadic.evalUnchecked e rho.values cfg

The value projection of the dual kernel is exactly the ordinary Dyadic value kernel.

theorem LeanCert.Engine.evalDualDyadicChecked_val_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : DualDyadicEnv) (cfg : DyadicConfig) (D : DualIntervalDyadic) (hrho : ∀ (i : ℕ), rhoReal i ∈ (rho i).val) (hok : evalDualDyadicChecked e rho cfg = Except.ok D) : Core.Expr.eval rhoReal e ∈ D.val

Golden theorem for successful checked Dyadic dual evaluation.

theorem LeanCert.Engine.evalWithDerivDyadicChecked_differentiableAt (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig) (D : DualIntervalDyadic) (x : ℝ) (hx : x ∈ rho idx) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (hok : evalWithDerivDyadicChecked e rho idx cfg = Except.ok D) : DifferentiableAt ℝ (e.evalAlong rhoReal idx) x

Successful checked Dyadic indexed AD proves differentiability throughout the selected input interval.

theorem LeanCert.Engine.evalWithDerivDyadicChecked_der_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig) (D : DualIntervalDyadic) (x : ℝ) (hx : x ∈ rho idx) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (hok : evalWithDerivDyadicChecked e rho idx cfg = Except.ok D) : deriv (e.evalAlong rhoReal idx) x ∈ D.der

Golden theorem: successful checked Dyadic indexed AD encloses the true partial derivative.

theorem LeanCert.Engine.derivIntervalDyadicChecked_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig) (dI : Core.IntervalDyadic) (x : ℝ) (hx : x ∈ rho idx) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (hok : derivIntervalDyadicChecked e rho idx cfg = Except.ok dI) : deriv (e.evalAlong rhoReal idx) x ∈ dI

Golden theorem for the derivative-only Dyadic API.

theorem LeanCert.Engine.derivIntervalDyadicCheckedOfRat_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalEnv) (idx : ℕ) (cfg : DyadicConfig) (dI : Core.IntervalDyadic) (x : ℝ) (hx : x ∈ rho idx) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (hok : derivIntervalDyadicCheckedOfRat e rho idx cfg = Except.ok dI) : deriv (e.evalAlong rhoReal idx) x ∈ dI

Golden theorem for rational input boxes converted to the Dyadic backend.

def LeanCert.Engine.gradientIntervalDyadicChecked (e : Core.Expr) (rho : IntervalDyadicEnv) (n : ℕ) (cfg : DyadicConfig := { }) : EvalResult (List Core.IntervalDyadic)

Compute the first n partial derivatives with the checked Dyadic backend.

Equations

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

def LeanCert.Engine.gradientIntervalDyadicCheckedOfRat (e : Core.Expr) (rho : IntervalEnv) (n : ℕ) (cfg : DyadicConfig := { }) : EvalResult (List Core.IntervalDyadic)

Rational-input convenience boundary for the first n Dyadic partials.

Equations

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

theorem LeanCert.Engine.gradientIntervalDyadicChecked_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalDyadicEnv) (n : ℕ) (cfg : DyadicConfig) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (gradient : List Core.IntervalDyadic) (hok : gradientIntervalDyadicChecked e rho n cfg = Except.ok gradient) : List.Forall₂ (fun (i : ℕ) (dI : Core.IntervalDyadic) => deriv (e.evalAlong rhoReal i) (rhoReal i) ∈ dI) (List.range n) gradient

Golden theorem for the checked Dyadic gradient API.

theorem LeanCert.Engine.gradientIntervalDyadicCheckedOfRat_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalEnv) (n : ℕ) (cfg : DyadicConfig) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (gradient : List Core.IntervalDyadic) (hok : gradientIntervalDyadicCheckedOfRat e rho n cfg = Except.ok gradient) : List.Forall₂ (fun (i : ℕ) (dI : Core.IntervalDyadic) => deriv (e.evalAlong rhoReal i) (rhoReal i) ∈ dI) (List.range n) gradient

Golden theorem for checked Dyadic gradients over rational input boxes.

Automatic Differentiation via Intervals

This module provides forward-mode automatic differentiation using interval arithmetic. We compute both the value and derivative of an expression, with rigorous bounds on both.

Module Structure

• AD.Basic - Core types: DualInterval, basic operations (add, mul, neg)
• AD.Transcendental - Transcendental functions (sin, cos, exp, etc.)
• AD.Eval - Evaluators: LeanCert.Internal.AD.evalUnchecked, evalDualOption, derivInterval
• AD.Correctness - Correctness theorems for supported expressions
• AD.PartialCorrectness - Correctness for partial functions (inv, log, sqrt)
• AD.Computable - Taylor-based computable evaluators
• AD.DomainChecked - Computable AD with box-dependent checks for inv and log
• AD.Dyadic - Domain-aware AD with bounded-denominator Dyadic arithmetic

Main definitions

• DualInterval - A pair of intervals representing (value, derivative)
• LeanCert.Internal.AD.evalUnchecked - Evaluate expression to get value and derivative intervals
• evalDualOption - Partial evaluator supporting inv, log, sqrt
• LeanCert.Internal.AD.evalTotalCore - Computable evaluator for native_decide
• evalDualChecked, derivIntervalChecked - Computable, structured-failure APIs for inv/log
• evalDualDyadicChecked, derivIntervalDyadicChecked - Checked Dyadic counterparts

Main theorems

• LeanCert.Engine.evalDualUnchecked_val_correct - Value component is correct for supported expressions
• LeanCert.Engine.evalDualUnchecked_der_correct - Derivative component is correct for supported expressions
• evalDualOption_val_correct, evalDualOption_der_correct - Correctness with domain checks
• LeanCert.Internal.AD.evalTotalCore_val_correct, LeanCert.Internal.AD.evalTotalCore_der_correct

• Computable correctness

• evalWithDerivChecked_der_correct, derivIntervalChecked_correct - Golden theorems for successful domain-aware computation

All theorems are FULLY PROVED with no sorry or axioms.

N-Dimensional Boxes for Global Optimization

This file provides the Box type for representing n-dimensional domains as products of intervals, along with helper functions for branch-and-bound optimization.

Main definitions

• Box - A list of intervals representing an n-dimensional box
• Box.toEnv - Convert a box to an interval environment
• Box.mem - Membership: a point (list of reals) is in a box
• Box.widestDim - Find the dimension with the largest width (for splitting)
• Box.split - Split a box along a given dimension
• Box.volume - Product of interval widths (heuristic measure)

Design

A Box is represented as List IntervalRat, where the i-th element is the interval for the i-th variable. This allows boxes of any dimension.

For expressions with n variables (var 0 through var n-1), a box should have at least n intervals. The conversion Box.toEnv returns default for out-of-bounds indices.

Box type and basic operations

@[reducible, inline]

abbrev LeanCert.Engine.Optimization.Box : Type

An n-dimensional box as a list of intervals. The i-th element is the interval for variable i.

Equations

• LeanCert.Engine.Optimization.Box = List LeanCert.Core.IntervalRat

@[reducible, inline]

abbrev LeanCert.Engine.Optimization.Point : Type

A point in ℝⁿ represented as a list of reals

Equations

• LeanCert.Engine.Optimization.Point = List ℝ

@[reducible, inline]

abbrev LeanCert.Engine.Optimization.PointQ : Type

A rational point in ℚⁿ

Equations

• LeanCert.Engine.Optimization.PointQ = List ℚ

def LeanCert.Engine.Optimization.Box.ofInterval (I : Core.IntervalRat) : Box

Create a one-dimensional box from a single interval.

Equations

• LeanCert.Engine.Optimization.Box.ofInterval I = [I]

def LeanCert.Engine.Optimization.Box.toEnv (B : Box) : IntervalEnv

Convert a box to an interval environment. Returns default for out-of-bounds indices (i.e., the whole real line approximation).

Equations

• B.toEnv i = List.getD B i default

def LeanCert.Engine.Optimization.Box.dim (B : Box) : ℕ

The dimension (number of intervals) of a box

Equations

• B.dim = List.length B

def LeanCert.Engine.Optimization.Box.mem (p : Point) (B : Box) : Prop

Check if a point is in a box. A point is in a box if each coordinate is in the corresponding interval.

Equations

• LeanCert.Engine.Optimization.Box.mem p B = ∃ (h : List.length p = List.length B), ∀ (i : Fin (List.length B)), p[↑i] ∈ B[↑i]

def LeanCert.Engine.Optimization.Box.envMem (ρ : ℕ → ℝ) (B : Box) : Prop

Membership for a real function (environment) in a box. This is the key notion for correctness: ρ ∈ B means ρ i ∈ B[i] for all i < B.length.

Equations

• LeanCert.Engine.Optimization.Box.envMem ρ B = ∀ (i : Fin (List.length B)), ρ ↑i ∈ B[↑i]

theorem LeanCert.Engine.Optimization.Box.envMem_toEnv (ρ : ℕ → ℝ) (B : Box) (h : envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) : Engine.envMem ρ B.toEnv

envMem implies the general IntervalEnv membership for toEnv NOTE: For indices beyond the box dimension, we use the default interval [0,0]. This means expressions should only use variables 0..B.length-1 for correct results.

Width and dimension selection

def LeanCert.Engine.Optimization.Box.intervalWidth (I : Core.IntervalRat) : ℚ

Width of an interval

Equations

• LeanCert.Engine.Optimization.Box.intervalWidth I = I.hi - I.lo

def LeanCert.Engine.Optimization.Box.widths (B : Box) : List ℚ

Get the width of each dimension

Equations

• B.widths = List.map LeanCert.Engine.Optimization.Box.intervalWidth B

def LeanCert.Engine.Optimization.Box.maxIdx (xs : List ℚ) : ℕ

Find the index of the maximum element in a list (returns 0 for empty list)

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.Optimization.Box.maxIdx [] = 0
• LeanCert.Engine.Optimization.Box.maxIdx [head] = 0

def LeanCert.Engine.Optimization.Box.widestDim (B : Box) : ℕ

Find the dimension with the widest interval (heuristic for splitting). Returns 0 if the box is empty.

Equations

• B.widestDim = LeanCert.Engine.Optimization.Box.maxIdx B.widths

def LeanCert.Engine.Optimization.Box.widestDim' (B : Box) : ℕ

Alternative: find widest dimension with explicit fold

Equations

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

Box splitting

def LeanCert.Engine.Optimization.Box.split (B : Box) (dim : ℕ) : Box × Box

Split a box along a given dimension by bisecting that interval. Returns the original box if the dimension is out of bounds.

Equations

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

def LeanCert.Engine.Optimization.Box.splitWidest (B : Box) : Box × Box

Split along the widest dimension

Equations

• B.splitWidest = B.split B.widestDim

theorem LeanCert.Engine.Optimization.Box.split_length_eq (B : Box) (d : ℕ) : List.length (B.split d).1 = List.length B ∧ List.length (B.split d).2 = List.length B

Splitting preserves the number of box coordinates.

theorem LeanCert.Engine.Optimization.Box.envMem_of_envMem_split (B : Box) (d : ℕ) (ρ : ℕ → ℝ) : envMem ρ (B.split d).1 → envMem ρ B

The lower child of a split is a semantic sub-box of its parent.

theorem LeanCert.Engine.Optimization.Box.envMem_of_envMem_split_right (B : Box) (d : ℕ) (ρ : ℕ → ℝ) : envMem ρ (B.split d).2 → envMem ρ B

The upper child of a split is a semantic sub-box of its parent.

Volume and size heuristics

def LeanCert.Engine.Optimization.Box.volume (B : Box) : ℚ

Volume of a box (product of widths). Returns 0 for empty box.

Equations

• B.volume = List.foldl (fun (x1 x2 : ℚ) => x1 * x2) 1 B.widths

def LeanCert.Engine.Optimization.Box.maxWidth (B : Box) : ℚ

Maximum width across all dimensions

Equations

• B.maxWidth = List.foldl max 0 B.widths

def LeanCert.Engine.Optimization.Box.isSmall (B : Box) (threshold : ℚ) : Bool

Check if a box is "small" (max width below threshold)

Equations

• B.isSmall threshold = decide (B.maxWidth ≤ threshold)

Box construction helpers

def LeanCert.Engine.Optimization.Box.ofPairs (pairs : List (ℚ × ℚ)) : Box

Create a box from a list of (lo, hi) pairs

Equations

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

def LeanCert.Engine.Optimization.Box.unit (n : ℕ) : Box

Create a unit box [0,1]ⁿ

Equations

• LeanCert.Engine.Optimization.Box.unit n = List.replicate n { lo := 0, hi := 1, le := LeanCert.Engine.Optimization.Box.unit._proof_1 }

def LeanCert.Engine.Optimization.Box.symmetric (n : ℕ) : Box

Create a symmetric box [-1,1]ⁿ

Equations

• LeanCert.Engine.Optimization.Box.symmetric n = List.replicate n { lo := -1, hi := 1, le := LeanCert.Engine.Optimization.Box.symmetric._proof_1 }

def LeanCert.Engine.Optimization.Box.ofBounds (los his : List ℚ) (_h : los.length = his.length) : Box

Create a box from bounds: [lo₀, hi₀] × ... × [loₙ₋₁, hiₙ₋₁]

Equations

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

Membership lemmas

theorem LeanCert.Engine.Optimization.Box.coord_mem_of_mem (p : Point) (B : Box) (h : mem p B) (i : Fin (List.length B)) : p[↑i] ∈ B[↑i]

If a point is in a box, its i-th coordinate is in the i-th interval

theorem LeanCert.Engine.Optimization.Box.mem_split_cases (B : Box) (d : ℕ) (hd : d < List.length B) (p : Point) (hp : mem p B) : mem p (B.split d).1 ∨ mem p (B.split d).2

After splitting, any point in the original box is in one of the halves.

theorem LeanCert.Engine.Optimization.Box.envMem_split_cases (B : Box) (d : ℕ) (hd : d < List.length B) (ρ : ℕ → ℝ) (hρ : envMem ρ B) : envMem ρ (B.split d).1 ∨ envMem ρ (B.split d).2

Environment membership after splitting.

Global Optimization via Branch-and-Bound

This file implements verified global optimization over intervals using branch-and-bound with interval arithmetic and derivative bounds.

Phase Status

This module is now largely Phase 1 (verified). The core correctness theorems are fully proved for the ADSupported subset.

Main definitions

• minimizeInterval - Find a lower bound on min f over an interval
• maximizeInterval - Find an upper bound on max f over an interval
• Correctness theorems (fully proved for ADSupported)

Algorithm

Branch-and-bound with the following pruning rules:

1. Interval evaluation: If f([a,b]) = [lo, hi], then min f ≥ lo
2. Monotonicity: If f'([a,b]) > 0, f is increasing, so min is at a
3. Subdivision: Split interval and recurse

Optimization result

structure LeanCert.Engine.OptResult : Type

Result of an optimization computation

• valueBound : Core.IntervalRat

  Interval containing the optimum value

• argBound : Option Core.IntervalRat

  Interval containing an optimizing point (if found)

• depth : ℕ

  Depth of search performed

noncomputable def LeanCert.Engine.OptResult.merge (r₁ r₂ : OptResult) : OptResult

Combine two subinterval bounds, preserving their lower and upper bounds.

Equations

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

Minimization

noncomputable def LeanCert.Engine.derivStrictlyPositive (e : Core.Expr) (I : Core.IntervalRat) (varIdx : ℕ) : Bool

Check if derivative interval is strictly positive

Equations

• LeanCert.Engine.derivStrictlyPositive e I varIdx = decide (0 < (LeanCert.Engine.derivInterval e (fun (x : ℕ) => I) varIdx).lo)

noncomputable def LeanCert.Engine.derivStrictlyNegative (e : Core.Expr) (I : Core.IntervalRat) (varIdx : ℕ) : Bool

Check if derivative interval is strictly negative

Equations

• LeanCert.Engine.derivStrictlyNegative e I varIdx = decide ((LeanCert.Engine.derivInterval e (fun (x : ℕ) => I) varIdx).hi < 0)

noncomputable def LeanCert.Engine.minimizeInterval (e : Core.Expr) (I : Core.IntervalRat) (varIdx maxDepth : ℕ) : OptResult

Simple branch-and-bound minimization.

Returns an interval [lo, hi] such that:

• lo ≤ min_{x ∈ I} f(x)
• hi ≥ min_{x ∈ I} f(x)

Equations

• LeanCert.Engine.minimizeInterval e I varIdx maxDepth = LeanCert.Engine.minimizeInterval.go e varIdx maxDepth I maxDepth

@[irreducible]

noncomputable def LeanCert.Engine.minimizeInterval.go (e : Core.Expr) (varIdx maxDepth : ℕ) (J : Core.IntervalRat) (depth : ℕ) : OptResult

Recursive interval minimization with a decreasing subdivision budget.

Equations

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

theorem LeanCert.Engine.minimizeInterval_base_correct (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (x : ℝ) : x ∈ I → ↑(Internal.Rational.evalUnchecked1 e I).lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Base case correctness: interval evaluation gives a valid lower bound. This theorem is FULLY PROVED - no sorry, no axioms.

Derivative bounds and monotonicity

theorem LeanCert.Engine.derivInterval_correct_evalWithDeriv1 (e : Core.Expr) (hsupp : ADSupported e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) : deriv (evalFunc1 e) x ∈ (evalWithDeriv1 e I).der

For single-variable expressions evaluated with (fun _ => I), derivative is correct. We use evalWithDeriv1 which directly uses varActive for all variables.

theorem LeanCert.Engine.derivInterval_correct_single (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) : deriv (evalFunc1 e) x ∈ derivInterval e (fun (x : ℕ) => I) 0

Derivative is in derivInterval for expressions that only use var 0. FULLY PROVED - no sorry.

theorem LeanCert.Engine.deriv_pos_on_interval (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hpos : 0 < (derivInterval e (fun (x : ℕ) => I) 0).lo) (x : ℝ) : x ∈ I → 0 < deriv (evalFunc1 e) x

If the derivative interval is strictly positive, derivative is positive everywhere

theorem LeanCert.Engine.deriv_neg_on_interval (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hneg : (derivInterval e (fun (x : ℕ) => I) 0).hi < 0) (x : ℝ) : x ∈ I → deriv (evalFunc1 e) x < 0

If the derivative interval is strictly negative, derivative is negative everywhere

theorem LeanCert.Engine.strictMonoOn_of_deriv_pos_interval (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hpos : 0 < (derivInterval e (fun (x : ℕ) => I) 0).lo) : StrictMonoOn (evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)

Strictly positive derivative implies strict monotonicity

theorem LeanCert.Engine.strictAntiOn_of_deriv_neg_interval (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hneg : (derivInterval e (fun (x : ℕ) => I) 0).hi < 0) : StrictAntiOn (evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)

Strictly negative derivative implies strict antitonicity

Monotonicity-based bounds

theorem LeanCert.Engine.increasing_min_at_left (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hpos : 0 < (derivInterval e (fun (x : ℕ) => I) 0).lo) (x : ℝ) : x ∈ I → evalFunc1 e ↑I.lo ≤ evalFunc1 e x

For increasing functions, minimum is at the left endpoint

theorem LeanCert.Engine.decreasing_min_at_right (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hneg : (derivInterval e (fun (x : ℕ) => I) 0).hi < 0) (x : ℝ) : x ∈ I → evalFunc1 e ↑I.hi ≤ evalFunc1 e x

For decreasing functions, minimum is at the right endpoint

theorem LeanCert.Engine.increasing_endpoint_bound (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hpos : 0 < (derivInterval e (fun (x : ℕ) => I) 0).lo) (x : ℝ) : x ∈ I → ↑(Internal.Rational.evalUnchecked1 e (Core.IntervalRat.singleton I.lo)).lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Interval at left endpoint gives valid lower bound for increasing functions

theorem LeanCert.Engine.decreasing_endpoint_bound (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hneg : (derivInterval e (fun (x : ℕ) => I) 0).hi < 0) (x : ℝ) : x ∈ I → ↑(Internal.Rational.evalUnchecked1 e (Core.IntervalRat.singleton I.hi)).lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Interval at right endpoint gives valid lower bound for decreasing functions

Full optimization correctness

theorem LeanCert.Engine.minimizeInterval_go_correct (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (maxDepth depth : ℕ) (J : Core.IntervalRat) (x : ℝ) : x ∈ J → ↑(minimizeInterval.go e 0 maxDepth J depth).valueBound.lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Helper lemma for go correctness. FULLY PROVED for varIdx = 0 and UsesOnlyVar0 expressions.

theorem LeanCert.Engine.minimizeInterval_correct (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (maxDepth : ℕ) (x : ℝ) : x ∈ I → ↑(minimizeInterval e I 0 maxDepth).valueBound.lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Correctness: the minimum is in the computed interval. FULLY PROVED for varIdx = 0 and UsesOnlyVar0 expressions.

Maximization

noncomputable def LeanCert.Engine.maximizeInterval (e : Core.Expr) (I : Core.IntervalRat) (varIdx maxDepth : ℕ) : OptResult

Maximize by minimizing the negation

Equations

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

theorem LeanCert.Engine.maximizeInterval_correct (e : Core.Expr) (hsupp : ADSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (maxDepth : ℕ) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑(maximizeInterval e I 0 maxDepth).valueBound.hi

Correctness: the maximum is in the computed interval. FULLY PROVED for varIdx = 0 and UsesOnlyVar0 expressions.

Bounds checking

noncomputable def LeanCert.Engine.checkLowerBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (varIdx maxDepth : ℕ) : Bool

Check if f(x) ≥ c for all x in I

Equations

• LeanCert.Engine.checkLowerBound e I c varIdx maxDepth = decide (c ≤ (LeanCert.Engine.minimizeInterval e I varIdx maxDepth).valueBound.lo)

noncomputable def LeanCert.Engine.checkUpperBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (varIdx maxDepth : ℕ) : Bool

Check if f(x) ≤ c for all x in I

Equations

• LeanCert.Engine.checkUpperBound e I c varIdx maxDepth = decide ((LeanCert.Engine.maximizeInterval e I varIdx maxDepth).valueBound.hi ≤ c)

N-Variable Optimization Infrastructure

The following section provides generalized optimization infrastructure that works with arbitrary variable indices and multi-variable environments. This allows optimizing along any coordinate while holding other variables fixed.

Key types:

• IntervalEnv := Nat → IntervalRat - maps variable indices to intervals
• evalAlong e ρ idx - evaluates e as a function of variable idx

The main advantage is that we can now optimize expressions with multiple variables by fixing all but one variable and optimizing along that coordinate.

N-variable derivative bounds

theorem LeanCert.Engine.deriv_pos_on_interval_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hpos : 0 < (derivInterval e ρ_int idx).lo) (x : ℝ) : x ∈ ρ_int idx → 0 < deriv (e.evalAlong ρ_real idx) x

If the derivative interval along idx is strictly positive, derivative is positive everywhere. Generalized version that works with any variable index and environment.

theorem LeanCert.Engine.deriv_neg_on_interval_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hneg : (derivInterval e ρ_int idx).hi < 0) (x : ℝ) : x ∈ ρ_int idx → deriv (e.evalAlong ρ_real idx) x < 0

If the derivative interval along idx is strictly negative, derivative is negative everywhere. Generalized version that works with any variable index and environment.

theorem LeanCert.Engine.strictMonoOn_of_deriv_pos_interval_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hpos : 0 < (derivInterval e ρ_int idx).lo) : StrictMonoOn (e.evalAlong ρ_real idx) (Set.Icc ↑(ρ_int idx).lo ↑(ρ_int idx).hi)

Strictly positive derivative along idx implies strict monotonicity. Generalized n-variable version.

theorem LeanCert.Engine.strictAntiOn_of_deriv_neg_interval_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hneg : (derivInterval e ρ_int idx).hi < 0) : StrictAntiOn (e.evalAlong ρ_real idx) (Set.Icc ↑(ρ_int idx).lo ↑(ρ_int idx).hi)

Strictly negative derivative along idx implies strict antitonicity. Generalized n-variable version.

N-variable monotonicity-based bounds

theorem LeanCert.Engine.increasing_min_at_left_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hpos : 0 < (derivInterval e ρ_int idx).lo) (x : ℝ) : x ∈ ρ_int idx → e.evalAlong ρ_real idx ↑(ρ_int idx).lo ≤ e.evalAlong ρ_real idx x

For increasing functions along idx, minimum is at the left endpoint. Generalized n-variable version.

theorem LeanCert.Engine.decreasing_min_at_right_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hneg : (derivInterval e ρ_int idx).hi < 0) (x : ℝ) : x ∈ ρ_int idx → e.evalAlong ρ_real idx ↑(ρ_int idx).hi ≤ e.evalAlong ρ_real idx x

For decreasing functions along idx, minimum is at the right endpoint. Generalized n-variable version.

N-variable minimization algorithm

noncomputable def LeanCert.Engine.derivStrictlyPositiveIdx (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) : Bool

Check if derivative interval along idx is strictly positive

Equations

• LeanCert.Engine.derivStrictlyPositiveIdx e ρ idx = decide (0 < (LeanCert.Engine.derivInterval e ρ idx).lo)

noncomputable def LeanCert.Engine.derivStrictlyNegativeIdx (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) : Bool

Check if derivative interval along idx is strictly negative

Equations

• LeanCert.Engine.derivStrictlyNegativeIdx e ρ idx = decide ((LeanCert.Engine.derivInterval e ρ idx).hi < 0)

def LeanCert.Engine.updateIntervalEnv (ρ : IntervalEnv) (idx : ℕ) (J : Core.IntervalRat) : IntervalEnv

Update an interval environment at a specific index

Equations

• LeanCert.Engine.updateIntervalEnv ρ idx J i = if i = idx then J else ρ i

noncomputable def LeanCert.Engine.minimizeIntervalIdx (e : Core.Expr) (ρ : IntervalEnv) (idx maxDepth : ℕ) : OptResult

N-variable branch-and-bound minimization along coordinate idx.

Returns an interval [lo, hi] such that for any ρ_real with ρ_real i ∈ ρ i:

• lo ≤ min_{t ∈ ρ idx} evalAlong e ρ_real idx t
• hi ≥ min_{t ∈ ρ idx} evalAlong e ρ_real idx t

Equations

• LeanCert.Engine.minimizeIntervalIdx e ρ idx maxDepth = LeanCert.Engine.minimizeIntervalIdx.go e ρ idx maxDepth (ρ idx) maxDepth

@[irreducible]

noncomputable def LeanCert.Engine.minimizeIntervalIdx.go (e : Core.Expr) (ρ : IntervalEnv) (idx maxDepth : ℕ) (J : Core.IntervalRat) (depth : ℕ) : OptResult

Recursive coordinate minimization with a decreasing subdivision budget.

Equations

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

N-variable minimization correctness

theorem LeanCert.Engine.minimizeIntervalIdx_base_correct (e : Core.Expr) (hsupp : ADSupported e) (ρ_int : IntervalEnv) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ↑(Internal.Rational.evalUnchecked e ρ_int).lo ≤ Core.Expr.eval ρ_real e

Base case correctness for n-variable optimization. Interval evaluation gives a valid lower bound.

theorem LeanCert.Engine.minimizeIntervalIdx_go_correct (e : Core.Expr) (hsupp : ADSupported e) (ρ_int : IntervalEnv) (idx maxDepth depth : ℕ) (J : Core.IntervalRat) (hJ_sub : ∀ t ∈ J, t ∈ ρ_int idx) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ∀ t ∈ J, ↑(minimizeIntervalIdx.go e ρ_int idx maxDepth J depth).valueBound.lo ≤ Core.Expr.eval (ρ_real[idx ↦ t]) e

Helper lemma for go correctness in n-variable setting

theorem LeanCert.Engine.minimizeIntervalIdx_correct (e : Core.Expr) (hsupp : ADSupported e) (ρ_int : IntervalEnv) (idx maxDepth : ℕ) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ∀ t ∈ ρ_int idx, ↑(minimizeIntervalIdx e ρ_int idx maxDepth).valueBound.lo ≤ Core.Expr.eval (ρ_real[idx ↦ t]) e

Correctness theorem for n-variable minimization: For any real environment ρ_real satisfying ρ_int, and any t in ρ_int idx, the computed lower bound is valid.

FULLY PROVED - no sorry, no axioms.

noncomputable def LeanCert.Engine.maximizeIntervalIdx (e : Core.Expr) (ρ : IntervalEnv) (idx maxDepth : ℕ) : OptResult

N-variable maximization via minimization of negation

Equations

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

theorem LeanCert.Engine.maximizeIntervalIdx_correct (e : Core.Expr) (hsupp : ADSupported e) (ρ_int : IntervalEnv) (idx maxDepth : ℕ) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ∀ t ∈ ρ_int idx, Core.Expr.eval (ρ_real[idx ↦ t]) e ≤ ↑(maximizeIntervalIdx e ρ_int idx maxDepth).valueBound.hi

Correctness theorem for n-variable maximization

Gradient Interval Computation for Optimization

This file provides functions to compute interval bounds on the gradient ∇f(B) of an expression over a box B. This is used for monotonicity-based pruning in branch-and-bound global optimization.

Main definitions

• gradientInterval - Compute interval bounds on all partial derivatives over a box
• gradientSignature - Determine the sign of each partial derivative
• canPruneToLo / canPruneToHi - Check if a coordinate can be pruned by monotonicity

Design

The gradient is computed by running forward-mode AD (from AD.lean) for each coordinate direction. The result is a list of intervals, one per variable.

Monotonicity pruning: If ∂f/∂xᵢ > 0 on the entire box B, then f is minimized when xᵢ = B[i].lo. We can shrink the box in that dimension to a point.

Gradient computation

noncomputable def LeanCert.Engine.Optimization.gradientInterval (e : Core.Expr) (B : Box) : List Core.IntervalRat

Compute the gradient interval: bounds on each partial derivative over a box. Returns a list of intervals, where the i-th interval contains ∂f/∂xᵢ for all x ∈ B.

Equations

• LeanCert.Engine.Optimization.gradientInterval e B = List.ofFn fun (i : Fin (List.length B)) => LeanCert.Engine.derivInterval e B.toEnv ↑i

noncomputable def LeanCert.Engine.Optimization.gradientIntervalN (e : Core.Expr) (B : Box) (n : ℕ) : List Core.IntervalRat

Compute gradient for n variables (explicit dimension)

Equations

• LeanCert.Engine.Optimization.gradientIntervalN e B n = List.map (fun (i : ℕ) => LeanCert.Engine.derivInterval e B.toEnv i) (List.range n)

Computable versions

def LeanCert.Engine.Optimization.mkDualEnvCore (ρ : IntervalEnv) (idx : ℕ) : DualEnv

Create dual environment for differentiating with respect to variable idx (computable). Active variable gets der = 1, passive variables get der = 0.

Equations

• LeanCert.Engine.Optimization.mkDualEnvCore ρ idx i = if i = idx then LeanCert.Engine.DualInterval.varActive (ρ i) else LeanCert.Engine.DualInterval.varPassive (ρ i)

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

Evaluate with derivative with respect to variable idx (computable version)

Equations

• LeanCert.Engine.Optimization.evalWithDerivCore e ρ idx cfg = LeanCert.Internal.AD.evalTotalCore e (LeanCert.Engine.Optimization.mkDualEnvCore ρ idx) cfg

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

Computable derivative interval for multi-variable expressions. Computes the interval containing ∂f/∂xᵢ over the box.

Equations

• LeanCert.Engine.Optimization.derivIntervalCoreN e ρ idx cfg = (LeanCert.Engine.Optimization.evalWithDerivCore e ρ idx cfg).der

theorem LeanCert.Engine.Optimization.evalDualTotalCore_der_correct_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (x : ℝ) (hx : x ∈ ρ_int idx) (cfg : EvalConfig) : deriv (e.evalAlong ρ_real idx) x ∈ (Internal.AD.evalTotalCore e (mkDualEnvCore ρ_int idx) cfg).der

Correctness of the computable derivative evaluator for an arbitrary coordinate of a multivariate expression.

def LeanCert.Engine.Optimization.gradientIntervalCore (e : Core.Expr) (B : Box) (cfg : EvalConfig := { }) : List Core.IntervalRat

Computable version of gradient interval for Core expressions. This can be used with native_decide for verified optimization.

Equations

• LeanCert.Engine.Optimization.gradientIntervalCore e B cfg = List.map (fun (i : ℕ) => LeanCert.Engine.Optimization.derivIntervalCoreN e B.toEnv i cfg) (List.range (List.length B))

def LeanCert.Engine.Optimization.gradientIntervalChecked (e : Core.Expr) (B : Box) (cfg : EvalConfig := { }) : EvalResult (List Core.IntervalRat)

Compute every partial derivative using the domain-aware checked AD path. Unlike gradientIntervalCore, this rejects unsupported syntax, reciprocal arguments containing zero, and nonpositive logarithm arguments instead of returning a finite interval that could be mistaken for a certificate.

Equations

• LeanCert.Engine.Optimization.gradientIntervalChecked e B cfg = List.mapM (fun (i : ℕ) => LeanCert.Engine.derivIntervalChecked e B.toEnv i cfg) (List.range (List.length B))

theorem LeanCert.Engine.Optimization.gradientIntervalChecked_correct (e : Core.Expr) (B : Box) (cfg : EvalConfig) (ρReal : ℕ → ℝ) (hρ : Box.envMem ρReal B) (hzero : ∀ i ≥ List.length B, ρReal i = 0) (gradient : List Core.IntervalRat) (hok : gradientIntervalChecked e B cfg = Except.ok gradient) : List.Forall₂ (fun (i : ℕ) (dI : Core.IntervalRat) => deriv (e.evalAlong ρReal i) (ρReal i) ∈ dI) (List.range (List.length B)) gradient

Golden soundness theorem for a successfully computed checked gradient. The output list is aligned with coordinates 0, …, B.length - 1.

Sign classification

inductive LeanCert.Engine.Optimization.IntervalSign : Type

Classification of an interval's sign

• positive : IntervalSign
• negative : IntervalSign
• nonpositive : IntervalSign
• nonnegative : IntervalSign
• indefinite : IntervalSign

def LeanCert.Engine.Optimization.instReprIntervalSign.repr : IntervalSign → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Engine.Optimization.instReprIntervalSign : Repr IntervalSign

Equations

• LeanCert.Engine.Optimization.instReprIntervalSign = { reprPrec := LeanCert.Engine.Optimization.instReprIntervalSign.repr }

@[instance_reducible]

instance LeanCert.Engine.Optimization.instDecidableEqIntervalSign : DecidableEq IntervalSign

Equations

• LeanCert.Engine.Optimization.instDecidableEqIntervalSign x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanCert.Engine.Optimization.classifySign (I : Core.IntervalRat) : IntervalSign

Classify the sign of an interval

Equations

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

noncomputable def LeanCert.Engine.Optimization.gradientSignature (e : Core.Expr) (B : Box) : List IntervalSign

The gradient signature: sign of each partial derivative (noncomputable wrapper)

Equations

• LeanCert.Engine.Optimization.gradientSignature e B = List.map LeanCert.Engine.Optimization.classifySign (LeanCert.Engine.Optimization.gradientIntervalN e B (List.length B))

Monotonicity predicates

def LeanCert.Engine.Optimization.isStrictlyPositive (I : Core.IntervalRat) : Bool

Check if interval is strictly positive

Equations

• LeanCert.Engine.Optimization.isStrictlyPositive I = decide (I.lo > 0)

def LeanCert.Engine.Optimization.isStrictlyNegative (I : Core.IntervalRat) : Bool

Check if interval is strictly negative

Equations

• LeanCert.Engine.Optimization.isStrictlyNegative I = decide (I.hi < 0)

def LeanCert.Engine.Optimization.isNonnegative (I : Core.IntervalRat) : Bool

Check if interval is nonnegative

Equations

• LeanCert.Engine.Optimization.isNonnegative I = decide (I.lo ≥ 0)

def LeanCert.Engine.Optimization.isNonpositive (I : Core.IntervalRat) : Bool

Check if interval is nonpositive

Equations

• LeanCert.Engine.Optimization.isNonpositive I = decide (I.hi ≤ 0)

Pruning queries

def LeanCert.Engine.Optimization.canPruneToLo (deriv_i : Core.IntervalRat) : Bool

Can we prune coordinate i to its low endpoint for minimization? True if ∂f/∂xᵢ > 0 on B (f is increasing in xᵢ, so min is at lo).

Equations

• LeanCert.Engine.Optimization.canPruneToLo deriv_i = LeanCert.Engine.Optimization.isStrictlyPositive deriv_i

def LeanCert.Engine.Optimization.canPruneToHi (deriv_i : Core.IntervalRat) : Bool

Can we prune coordinate i to its high endpoint for minimization? True if ∂f/∂xᵢ < 0 on B (f is decreasing in xᵢ, so min is at hi).

Equations

• LeanCert.Engine.Optimization.canPruneToHi deriv_i = LeanCert.Engine.Optimization.isStrictlyNegative deriv_i

def LeanCert.Engine.Optimization.pruneBoxForMin (B : Box) (grad : List Core.IntervalRat) : Box × List ℕ

Prune a box for minimization by fixing monotonic coordinates. Returns a (potentially smaller) box and a list of fixed coordinates.

Equations

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

Correctness theorems

theorem LeanCert.Engine.Optimization.gradientInterval_correct (e : Core.Expr) (hsupp : ADSupported e) (B : Box) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) (i : Fin (List.length B)) : deriv (e.evalAlong ρ ↑i) (ρ ↑i) ∈ (gradientIntervalN e B (List.length B))[↑i]?.getD default

The computed gradient interval contains the true partial derivatives. This follows from evalDual_der_correct_idx in AD.lean.

theorem LeanCert.Engine.Optimization.pruneToLo_preserves_min (e : Core.Expr) (hsupp : ADSupported e) (B : Box) (i : Fin (List.length B)) (hgrad : isStrictlyPositive (derivInterval e B.toEnv ↑i) = true) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ j ≥ List.length B, ρ j = 0) → ∃ (ρ' : ℕ → ℝ), Box.envMem ρ' B ∧ (∀ j ≥ List.length B, ρ' j = 0) ∧ ρ' ↑i = ↑B[↑i].lo ∧ Core.Expr.eval ρ' e ≤ Core.Expr.eval ρ e

If we prune a coordinate to lo because ∂f/∂xᵢ > 0, the minimum is preserved. Informal: if f is increasing in xᵢ on B, then min{f(x) : x ∈ B} = min{f(x) : xᵢ = B[i].lo}. NOTE: Requires ρ j = 0 for j ≥ B.length (standard assumption for box membership).

theorem LeanCert.Engine.Optimization.pruneToHi_preserves_min (e : Core.Expr) (hsupp : ADSupported e) (B : Box) (i : Fin (List.length B)) (hgrad : isStrictlyNegative (derivInterval e B.toEnv ↑i) = true) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ j ≥ List.length B, ρ j = 0) → ∃ (ρ' : ℕ → ℝ), Box.envMem ρ' B ∧ (∀ j ≥ List.length B, ρ' j = 0) ∧ ρ' ↑i = ↑B[↑i].hi ∧ Core.Expr.eval ρ' e ≤ Core.Expr.eval ρ e

If we prune a coordinate to hi because ∂f/∂xᵢ < 0, the minimum is preserved. NOTE: Requires ρ j = 0 for j ≥ B.length (standard assumption for box membership).

Pruned box membership and correctness

theorem LeanCert.Engine.Optimization.pruneBoxForMin_subset (B : Box) (grad : List Core.IntervalRat) (ρ : ℕ → ℝ) : Box.envMem ρ (pruneBoxForMin B grad).1 → Box.envMem ρ B

Helper: membership in the pruned box implies membership in the original box. The pruned box only shrinks coordinates, never expands them.

theorem LeanCert.Engine.Optimization.pruneBoxForMin_length (B : Box) (grad : List Core.IntervalRat) : List.length (pruneBoxForMin B grad).1 = List.length B

The pruned box has the same length as the original box

theorem LeanCert.Engine.Optimization.increasing_min_at_left_idx_core (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (cfg : EvalConfig) (hpos : 0 < (derivIntervalCoreN e ρ_int idx cfg).lo) (x : ℝ) : x ∈ ρ_int idx → e.evalAlong ρ_real idx ↑(ρ_int idx).lo ≤ e.evalAlong ρ_real idx x

A positive computable derivative enclosure makes the objective increasing along the selected coordinate.

theorem LeanCert.Engine.Optimization.decreasing_min_at_right_idx_core (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (cfg : EvalConfig) (hneg : (derivIntervalCoreN e ρ_int idx cfg).hi < 0) (x : ℝ) : x ∈ ρ_int idx → e.evalAlong ρ_real idx ↑(ρ_int idx).hi ≤ e.evalAlong ρ_real idx x

A negative computable derivative enclosure makes the objective decreasing along the selected coordinate.

theorem LeanCert.Engine.Optimization.pruneBoxForMin_correct (e : Core.Expr) (hsupp : ADSupported e) (B : Box) (cfg : EvalConfig := { }) : have grad := gradientIntervalCore e B cfg; have B' := (pruneBoxForMin B grad).1; ∀ (ρ : ℕ → ℝ), Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ∃ (ρ' : ℕ → ℝ), Box.envMem ρ' B' ∧ (∀ i ≥ List.length B', ρ' i = 0) ∧ Core.Expr.eval ρ' e ≤ Core.Expr.eval ρ e

Certified roots of differentiable systems

This module implements a strong, norm-form Krawczyk test for square systems in LeanCert's ADSupported expression fragment. The center and rational preconditioner are untrusted certificate data; krawczykCheck verifies AD support, center containment, invertibility, a strict infinity-norm contraction bound, and a strict self-map enclosure.

The golden theorem krawczykCheck_sound turns a successful Boolean check into existence and uniqueness of a real root in the supplied box.

@[instance_reducible]

def LeanCert.Engine.intervalRatZero : Zero Core.IntervalRat

Use the singleton zero interval as the additive identity.

Equations

• LeanCert.Engine.intervalRatZero = { zero := LeanCert.Core.IntervalRat.singleton 0 }

@[instance_reducible]

def LeanCert.Engine.intervalRatAdd : Add Core.IntervalRat

Use endpoint-wise interval addition for finite interval sums.

Equations

• LeanCert.Engine.intervalRatAdd = { add := LeanCert.Core.IntervalRat.add }

@[instance_reducible]

def LeanCert.Engine.instSMulNatIntervalRat : SMul ℕ Core.IntervalRat

Natural scalar multiplication by repeated interval addition.

Equations

• LeanCert.Engine.instSMulNatIntervalRat = { smul := fun (n : ℕ) (a : LeanCert.Core.IntervalRat) => { lo := ↑n * a.lo, hi := ↑n * a.hi, le := ⋯ } }

@[instance_reducible]

def LeanCert.Engine.instAddCommMonoidIntervalRat : AddCommMonoid Core.IntervalRat

The additive commutative monoid of rational intervals.

Equations

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

noncomputable def LeanCert.Engine.finEnv {n : ℕ} (x : Fin n → ℝ) : ℕ → ℝ

Extend a finite real coordinate vector to an expression environment with zero defaults.

Equations

• LeanCert.Engine.finEnv x i = if h : i < n then x ⟨i, h⟩ else 0

noncomputable def LeanCert.Engine.evalFin {n : ℕ} (e : Core.Expr) (x : Fin n → ℝ) : ℝ

Evaluate an expression in the environment of a finite real coordinate vector.

Equations

• LeanCert.Engine.evalFin e x = LeanCert.Core.Expr.eval (LeanCert.Engine.finEnv x) e

theorem LeanCert.Engine.evalFin_differentiable {n : ℕ} (e : Core.Expr) (h : ADSupported e) : Differentiable ℝ (evalFin e)

theorem LeanCert.Engine.finEnv_update {n : ℕ} (x : Fin n → ℝ) (j : Fin n) (t : ℝ) : finEnv (Function.update x j t) = finEnv x[↑j ↦ t]

theorem LeanCert.Engine.fderiv_single_eq_deriv_evalAlong {n : ℕ} (e : Core.Expr) (h : ADSupported e) (x : Fin n → ℝ) (j : Fin n) : (fderiv ℝ (evalFin e) x) (Pi.single j 1) = deriv (e.evalAlong (finEnv x) ↑j) (x j)

noncomputable def LeanCert.Engine.systemEval {n : ℕ} (F : Fin n → Core.Expr) (x : Fin n → ℝ) : Fin n → ℝ

Evaluate all coordinate expressions of a finite system.

Equations

• LeanCert.Engine.systemEval F x i = LeanCert.Engine.evalFin (F i) x

theorem LeanCert.Engine.systemEval_differentiable {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) : Differentiable ℝ (systemEval F)

noncomputable def LeanCert.Engine.jacobianAt {n : ℕ} (F : Fin n → Core.Expr) (x : Fin n → ℝ) : Matrix (Fin n) (Fin n) ℝ

The matrix of coordinate partial derivatives of an expression system.

Equations

• LeanCert.Engine.jacobianAt F x = LinearMap.toMatrix' ↑(fderiv ℝ (LeanCert.Engine.systemEval F) x)

theorem LeanCert.Engine.jacobianAt_apply {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (x : Fin n → ℝ) (i j : Fin n) : jacobianAt F x i j = deriv ((F i).evalAlong (finEnv x) ↑j) (x j)

def LeanCert.Engine.finBoxEnv {n : ℕ} (X : Fin n → Core.IntervalRat) : IntervalEnv

Extend a finite interval box to the evaluator’s indexed environment.

Equations

• LeanCert.Engine.finBoxEnv X i = if h : i < n then X ⟨i, h⟩ else LeanCert.Core.IntervalRat.singleton 0

def LeanCert.Engine.FinBoxMem {n : ℕ} (x : Fin n → ℝ) (X : Fin n → Core.IntervalRat) : Prop

Coordinatewise membership of a real vector in a rational interval box.

Equations

• LeanCert.Engine.FinBoxMem x X = ∀ (i : Fin n), x i ∈ X i

def LeanCert.Engine.intervalJacobian {n : ℕ} (F : Fin n → Core.Expr) (X : Fin n → Core.IntervalRat) (cfg : EvalConfig := { }) : Matrix (Fin n) (Fin n) Core.IntervalRat

Enclose the Jacobian entries by interval automatic differentiation.

Equations

• LeanCert.Engine.intervalJacobian F X cfg i j = LeanCert.Engine.Optimization.derivIntervalCoreN (F i) (LeanCert.Engine.finBoxEnv X) (↑j) cfg

theorem LeanCert.Engine.finEnv_mem_finBoxEnv {n : ℕ} {x : Fin n → ℝ} {X : Fin n → Core.IntervalRat} (hx : FinBoxMem x X) (i : ℕ) : finEnv x i ∈ finBoxEnv X i

theorem LeanCert.Engine.jacobianAt_mem_intervalJacobian {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (X : Fin n → Core.IntervalRat) (x : Fin n → ℝ) (hx : FinBoxMem x X) (cfg : EvalConfig) (i j : Fin n) : jacobianAt F x i j ∈ intervalJacobian F X cfg i j

noncomputable def LeanCert.Engine.matrixCLM {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) : (Fin n → ℝ) →L[ℝ] Fin n → ℝ

Interpret a real matrix as a continuous linear map on finite coordinate vectors.

Equations

• LeanCert.Engine.matrixCLM A = { toLinearMap := A.mulVecLin, cont := ⋯ }

noncomputable def LeanCert.Engine.newtonMap {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℝ) (F : Fin n → Core.Expr) (x : Fin n → ℝ) : Fin n → ℝ

The preconditioned Newton map x ↦ x - Y (F x).

Equations

• LeanCert.Engine.newtonMap Y F x = x - Y.mulVec (LeanCert.Engine.systemEval F x)

theorem LeanCert.Engine.newtonMap_differentiable {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℝ) (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) : Differentiable ℝ (newtonMap Y F)

theorem LeanCert.Engine.newtonMap_fderiv_matrix {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℝ) (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (x : Fin n → ℝ) : LinearMap.toMatrix' ↑(fderiv ℝ (newtonMap Y F) x) = 1 - Y * jacobianAt F x

def LeanCert.Engine.finBoxSet {n : ℕ} (X : Fin n → Core.IntervalRat) : Set (Fin n → ℝ)

The set of real vectors lying coordinatewise in the interval box.

Equations

• LeanCert.Engine.finBoxSet X = {x : Fin n → ℝ | LeanCert.Engine.FinBoxMem x X}

theorem LeanCert.Engine.finBoxSet_closed {n : ℕ} (X : Fin n → Core.IntervalRat) : IsClosed (finBoxSet X)

theorem LeanCert.Engine.finBoxSet_convex {n : ℕ} (X : Fin n → Core.IntervalRat) : Convex ℝ (finBoxSet X)

theorem LeanCert.Engine.contraction_unique_fixedPoint_in_finBox {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℝ) (hm : FinBoxMem m X) (g : (Fin n → ℝ) → Fin n → ℝ) (hmap : Set.MapsTo g (finBoxSet X) (finBoxSet X)) (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q < 1) (hdiff : ∀ x ∈ finBoxSet X, DifferentiableAt ℝ g x) (hderiv : ∀ x ∈ finBoxSet X, ‖fderiv ℝ g x‖ ≤ q) : ∃! x : Fin n → ℝ, FinBoxMem x X ∧ g x = x

def LeanCert.Engine.intervalIdentity {n : ℕ} : Matrix (Fin n) (Fin n) Core.IntervalRat

The identity matrix represented by singleton rational intervals.

Equations

• LeanCert.Engine.intervalIdentity i j = LeanCert.Core.IntervalRat.singleton (if i = j then 1 else 0)

def LeanCert.Engine.ratMulInterval {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (J : Matrix (Fin n) (Fin n) Core.IntervalRat) : Matrix (Fin n) (Fin n) Core.IntervalRat

Multiply a rational matrix by an interval matrix using interval sums.

Equations

• LeanCert.Engine.ratMulInterval Y J i j = ∑ k : Fin n, LeanCert.Core.IntervalRat.scale (Y i k) (J k j)

def LeanCert.Engine.preconditionedJacobian {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (J : Matrix (Fin n) (Fin n) Core.IntervalRat) : Matrix (Fin n) (Fin n) Core.IntervalRat

The interval matrix I - Y J enclosing the Newton-map derivative.

Equations

• LeanCert.Engine.preconditionedJacobian Y J i j = (LeanCert.Engine.intervalIdentity i j).sub (LeanCert.Engine.ratMulInterval Y J i j)

theorem LeanCert.Engine.mem_interval_sum {ι : Type u_1} (s : Finset ι) (x : ι → ℝ) (I : ι → Core.IntervalRat) (h : ∀ i ∈ s, x i ∈ I i) : ∑ i ∈ s, x i ∈ ∑ i ∈ s, I i

theorem LeanCert.Engine.mem_ratMulInterval {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (Jreal : Matrix (Fin n) (Fin n) ℝ) (J : Matrix (Fin n) (Fin n) Core.IntervalRat) (hJ : ∀ (i j : Fin n), Jreal i j ∈ J i j) (i j : Fin n) : ((Y.map fun (q : ℚ) => ↑q) * Jreal) i j ∈ ratMulInterval Y J i j

theorem LeanCert.Engine.mem_preconditionedJacobian {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (Jreal : Matrix (Fin n) (Fin n) ℝ) (J : Matrix (Fin n) (Fin n) Core.IntervalRat) (hJ : ∀ (i j : Fin n), Jreal i j ∈ J i j) (i j : Fin n) : (1 - (Y.map fun (q : ℚ) => ↑q) * Jreal) i j ∈ preconditionedJacobian Y J i j

def LeanCert.Engine.intervalAbsBound (I : Core.IntervalRat) : ℚ

The larger absolute endpoint, bounding absolute values in the interval.

Equations

• LeanCert.Engine.intervalAbsBound I = max |I.lo| |I.hi|

def LeanCert.Engine.intervalMatrixRowBound {n : ℕ} (A : Matrix (Fin n) (Fin n) Core.IntervalRat) (i : Fin n) : ℚ

The sum of absolute interval bounds in a selected matrix row.

Equations

• LeanCert.Engine.intervalMatrixRowBound A i = ∑ j : Fin n, LeanCert.Engine.intervalAbsBound (A i j)

def LeanCert.Engine.intervalMatrixBound {n : ℕ} (A : Matrix (Fin n) (Fin n) Core.IntervalRat) : ℚ

The maximum interval row sum, bounding the matrix’s sup-norm operator norm.

Equations

• LeanCert.Engine.intervalMatrixBound A = List.foldl max 0 (List.ofFn fun (i : Fin n) => LeanCert.Engine.intervalMatrixRowBound A i)

theorem LeanCert.Engine.abs_le_intervalAbsBound {x : ℝ} {I : Core.IntervalRat} (hx : x ∈ I) : |x| ≤ ↑(intervalAbsBound I)

theorem LeanCert.Engine.intervalMatrixRowBound_le_bound {n : ℕ} (A : Matrix (Fin n) (Fin n) Core.IntervalRat) (i : Fin n) : intervalMatrixRowBound A i ≤ intervalMatrixBound A

theorem LeanCert.Engine.matrix_norm_le_intervalMatrixBound {n : ℕ} (R : Matrix (Fin n) (Fin n) ℝ) (A : Matrix (Fin n) (Fin n) Core.IntervalRat) (hmem : ∀ (i j : Fin n), R i j ∈ A i j) : ‖R‖ ≤ ↑(intervalMatrixBound A)

theorem LeanCert.Engine.newtonMap_fderiv_norm_le {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (X : Fin n → Core.IntervalRat) (x : Fin n → ℝ) (hx : FinBoxMem x X) (cfg : EvalConfig) : ‖fderiv ℝ (newtonMap (Y.map fun (q : ℚ) => ↑q) F) x‖ ≤ ↑(intervalMatrixBound (preconditionedJacobian Y (intervalJacobian F X cfg)))

def LeanCert.Engine.pointIntervalEnv {n : ℕ} (m : Fin n → ℚ) : IntervalEnv

Represent a rational center by singleton intervals in the evaluation environment.

Equations

• LeanCert.Engine.pointIntervalEnv m i = if h : i < n then LeanCert.Core.IntervalRat.singleton (m ⟨i, h⟩) else LeanCert.Core.IntervalRat.singleton 0

def LeanCert.Engine.pointEvalIntervals {n : ℕ} (F : Fin n → Core.Expr) (m : Fin n → ℚ) (cfg : EvalConfig := { }) : Fin n → Core.IntervalRat

Enclose the expression system at a rational center by interval evaluation.

Equations

• LeanCert.Engine.pointEvalIntervals F m cfg i = LeanCert.Internal.Rational.evalTotalCore (F i) (LeanCert.Engine.pointIntervalEnv m) cfg

def LeanCert.Engine.intervalRatMatVec {n : ℕ} (Y : Matrix (Fin n) (Fin n) ℚ) (v : Fin n → Core.IntervalRat) : Fin n → Core.IntervalRat

Multiply a rational matrix by an interval vector.

Equations

• LeanCert.Engine.intervalRatMatVec Y v i = ∑ j : Fin n, LeanCert.Core.IntervalRat.scale (Y i j) (v j)

def LeanCert.Engine.newtonCenterInterval {n : ℕ} (F : Fin n → Core.Expr) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : EvalConfig := { }) : Fin n → Core.IntervalRat

An interval enclosure of the preconditioned Newton map at the chosen center.

Equations

• LeanCert.Engine.newtonCenterInterval F m Y cfg i = (LeanCert.Core.IntervalRat.singleton (m i)).sub (LeanCert.Engine.intervalRatMatVec Y (LeanCert.Engine.pointEvalIntervals F m cfg) i)

theorem LeanCert.Engine.finEnv_ratCast_mem_pointIntervalEnv {n : ℕ} (m : Fin n → ℚ) (i : ℕ) : finEnv (fun (j : Fin n) => ↑(m j)) i ∈ pointIntervalEnv m i

theorem LeanCert.Engine.systemEval_mem_pointEvalIntervals {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (m : Fin n → ℚ) (cfg : EvalConfig) (i : Fin n) : systemEval F (fun (j : Fin n) => ↑(m j)) i ∈ pointEvalIntervals F m cfg i

theorem LeanCert.Engine.newtonMap_center_mem {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : EvalConfig) (i : Fin n) : newtonMap (Y.map fun (q : ℚ) => ↑q) F (fun (j : Fin n) => ↑(m j)) i ∈ newtonCenterInterval F m Y cfg i

def LeanCert.Engine.coordinateRadius {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) (i : Fin n) : ℚ

The greater endpoint distance from the center in a selected coordinate.

Equations

• LeanCert.Engine.coordinateRadius X m i = max (m i - (X i).lo) ((X i).hi - m i)

def LeanCert.Engine.boxRadius {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) : ℚ

The maximum coordinate radius of the box around the chosen center.

Equations

• LeanCert.Engine.boxRadius X m = List.foldl max 0 (List.ofFn fun (i : Fin n) => LeanCert.Engine.coordinateRadius X m i)

theorem LeanCert.Engine.coordinateRadius_le_boxRadius {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) (i : Fin n) : coordinateRadius X m i ≤ boxRadius X m

theorem LeanCert.Engine.abs_sub_center_le_coordinateRadius {n : ℕ} {X : Fin n → Core.IntervalRat} {m : Fin n → ℚ} {x : Fin n → ℝ} (hx : FinBoxMem x X) (i : Fin n) : |x i - ↑(m i)| ≤ ↑(coordinateRadius X m i)

theorem LeanCert.Engine.boxRadius_nonneg {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) : 0 ≤ boxRadius X m

theorem LeanCert.Engine.norm_sub_center_le_boxRadius {n : ℕ} {X : Fin n → Core.IntervalRat} {m : Fin n → ℚ} {x : Fin n → ℝ} (hx : FinBoxMem x X) : ‖x - fun (i : Fin n) => ↑(m i)‖ ≤ ↑(boxRadius X m)

def LeanCert.Engine.symmetricInterval (d : ℚ) : Core.IntervalRat

The rational interval with endpoints -d and d.

Equations

• LeanCert.Engine.symmetricInterval d = { lo := -|d|, hi := |d|, le := ⋯ }

def LeanCert.Engine.newtonImageEnclosure {n : ℕ} (F : Fin n → Core.Expr) (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : EvalConfig := { }) : Fin n → Core.IntervalRat

Enclose the Newton image using its center value and a uniform derivative bound.

Equations

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

def LeanCert.Engine.intervalStrictInside (I X : Core.IntervalRat) : Bool

Test whether both endpoints lie strictly inside another interval.

Equations

• LeanCert.Engine.intervalStrictInside I X = (decide (X.lo < I.lo) && decide (I.hi < X.hi))

theorem LeanCert.Engine.intervalStrictInside_sound {I X : Core.IntervalRat} (h : intervalStrictInside I X = true) (x : ℝ) : x ∈ I → x ∈ X

theorem LeanCert.Engine.newtonMap_mapsTo_of_imageEnclosure {n : ℕ} (F : Fin n → Core.Expr) (h : ∀ (i : Fin n), ADSupported (F i)) (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) (hm : FinBoxMem (fun (i : Fin n) => ↑(m i)) X) (Y : Matrix (Fin n) (Fin n) ℚ) (cfg : EvalConfig) (hencl : ∀ (i : Fin n), intervalStrictInside (newtonImageEnclosure F X m Y cfg i) (X i) = true) : Set.MapsTo (newtonMap (Y.map fun (q : ℚ) => ↑q) F) (finBoxSet X) (finBoxSet X)

structure LeanCert.Engine.KrawczykCert (n : ℕ) : Type

Rational center and preconditioner data for a checkable Krawczyk certificate.

• center : Fin n → ℚ

  The rational center used by the Newton-image enclosure.

• preconditioner : Matrix (Fin n) (Fin n) ℚ

  The rational matrix used to precondition the equation system.

def LeanCert.Engine.centerInside {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) : Prop

Coordinatewise containment of the rational center in the interval box.

Equations

• LeanCert.Engine.centerInside X m = ∀ (i : Fin n), (X i).lo ≤ m i ∧ m i ≤ (X i).hi

@[instance_reducible]

instance LeanCert.Engine.instDecidableCenterInside {n : ℕ} (X : Fin n → Core.IntervalRat) (m : Fin n → ℚ) : Decidable (centerInside X m)

Equations

• LeanCert.Engine.instDecidableCenterInside X m = id inferInstance

def LeanCert.Engine.krawczykCheck {n : ℕ} (F : Fin n → Core.Expr) (X : Fin n → Core.IntervalRat) (cert : KrawczykCert n) (cfg : EvalConfig := { }) : Bool

Check supported derivatives, center containment, invertibility, contraction and self-map bounds.

Equations

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

def LeanCert.Engine.SystemZero {n : ℕ} (F : Fin n → Core.Expr) (x : Fin n → ℝ) : Prop

Every expression in the finite system evaluates to zero at the given point.

Equations

• LeanCert.Engine.SystemZero F x = ∀ (i : Fin n), LeanCert.Engine.evalFin (F i) x = 0

theorem LeanCert.Engine.centerInside_sound {n : ℕ} {X : Fin n → Core.IntervalRat} {m : Fin n → ℚ} (h : centerInside X m) : FinBoxMem (fun (i : Fin n) => ↑(m i)) X

theorem LeanCert.Engine.fixedPoint_iff_systemZero {n : ℕ} (F : Fin n → Core.Expr) (Y : Matrix (Fin n) (Fin n) ℚ) (hdet : Y.det ≠ 0) (x : Fin n → ℝ) : newtonMap (Y.map fun (q : ℚ) => ↑q) F x = x ↔ SystemZero F x

theorem LeanCert.Engine.krawczykCheck_sound {n : ℕ} (F : Fin n → Core.Expr) (X : Fin n → Core.IntervalRat) (cert : KrawczykCert n) (cfg : EvalConfig) (hcheck : krawczykCheck F X cert cfg = true) : ∃! x : Fin n → ℝ, FinBoxMem x X ∧ SystemZero F x