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
• evalIntervalDyadic - 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.
• roundAfterOps - Round after this many operations (0 = after every op).

• precision : ℤ

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

• taylorDepth : ℕ

  Number of Taylor series terms for transcendental functions

• roundAfterOps : ℕ

  Round after this many arithmetic operations (0 = always)

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.

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 LeanCert.Engine.instDecidableEqDyadicConfig : DecidableEq DyadicConfig

Equations

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

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.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)]
• Conservative bound: use [-100, max(hi, 1)] as a wide safe interval

Equations

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

Main Evaluator

def LeanCert.Engine.evalIntervalDyadic (e : Core.Expr) (ρ : IntervalDyadicEnv) (cfg : 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.Engine.evalIntervalDyadic (LeanCert.Core.Expr.const q) ρ cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat (LeanCert.Core.IntervalRat.singleton q) cfg.precision
• LeanCert.Engine.evalIntervalDyadic (LeanCert.Core.Expr.var idx) ρ cfg = ρ idx
• LeanCert.Engine.evalIntervalDyadic (e₁.add e₂) ρ cfg = ((LeanCert.Engine.evalIntervalDyadic e₁ ρ cfg).add (LeanCert.Engine.evalIntervalDyadic e₂ ρ cfg)).roundOut cfg.precision
• LeanCert.Engine.evalIntervalDyadic (e₁.mul e₂) ρ cfg = ((LeanCert.Engine.evalIntervalDyadic e₁ ρ cfg).mul (LeanCert.Engine.evalIntervalDyadic e₂ ρ cfg)).roundOut cfg.precision
• LeanCert.Engine.evalIntervalDyadic e_2.neg ρ cfg = (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg).neg
• LeanCert.Engine.evalIntervalDyadic e_2.inv ρ cfg = LeanCert.Engine.invIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.exp ρ cfg = LeanCert.Engine.expIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.sin ρ cfg = LeanCert.Engine.sinIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.cos ρ cfg = LeanCert.Engine.cosIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.log ρ cfg = LeanCert.Engine.logIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.atan ρ cfg = LeanCert.Engine.atanIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.arsinh ρ cfg = default
• LeanCert.Engine.evalIntervalDyadic e_2.atanh ρ cfg = default
• LeanCert.Engine.evalIntervalDyadic e_2.sinc ρ cfg = LeanCert.Engine.sincIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.erf ρ cfg = LeanCert.Engine.erfIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.sinh ρ cfg = LeanCert.Engine.sinhIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.cosh ρ cfg = LeanCert.Engine.coshIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.tanh ρ cfg = LeanCert.Engine.tanhIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic e_2.sqrt ρ cfg = LeanCert.Engine.sqrtIntervalDyadic (LeanCert.Engine.evalIntervalDyadic e_2 ρ cfg) cfg
• LeanCert.Engine.evalIntervalDyadic LeanCert.Core.Expr.pi ρ cfg = LeanCert.Core.IntervalDyadic.ofIntervalRat LeanCert.Engine.piInterval 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 evalIntervalDyadic to ensure compatibility. For log, we require the argument interval (converted to Rat) to have positive lower bound.

Equations

• 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.inv ρ 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.Engine.evalIntervalDyadic 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.atanh ρ 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.pi ρ cfg = True

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

Domain validity is trivially true for ExprSupported 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 ∈ evalIntervalDyadic 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).

Convenience Functions

def LeanCert.Engine.evalDyadic (e : Core.Expr) (ρ : IntervalDyadicEnv) : Core.IntervalDyadic

Evaluate with standard (double-like) precision

Equations

• LeanCert.Engine.evalDyadic e ρ = LeanCert.Engine.evalIntervalDyadic e ρ

def LeanCert.Engine.evalDyadicHighPrec (e : Core.Expr) (ρ : IntervalDyadicEnv) : Core.IntervalDyadic

Evaluate with high precision

Equations

• LeanCert.Engine.evalDyadicHighPrec e ρ = LeanCert.Engine.evalIntervalDyadic e ρ LeanCert.Engine.DyadicConfig.highPrecision

def LeanCert.Engine.evalDyadicFast (e : Core.Expr) (ρ : IntervalDyadicEnv) : Core.IntervalDyadic

Evaluate with fast settings (lower precision)

Equations

• LeanCert.Engine.evalDyadicFast e ρ = LeanCert.Engine.evalIntervalDyadic e ρ LeanCert.Engine.DyadicConfig.fast

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.Engine.evalIntervalDyadic 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.Engine.evalIntervalDyadic 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.Engine.evalIntervalDyadic e ρ cfg).lowerBoundedBy lo && (LeanCert.Engine.evalIntervalDyadic e ρ cfg).upperBoundedBy hi)