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
• ln2 : Core.IntervalRat
• expCoeffs : List ℚ
• sinCoeffs : List ℚ
• cosCoeffs : List ℚ
• atanhCoeffs : List ℚ

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)