Edge Case Stress Tests

This file tests boundary conditions, singularities, and "tricky" mathematical scenarios to ensure the library behaves safely (soundly) even when exact answers are impossible.

1. The "Division by Zero" Singularity

The interval evaluator evalIntervalCoreWithDiv has a fallback for intervals containing 0. It should return a massive safe interval rather than crashing or proving False.

def LeanCert.Examples.EdgeCases.I_cross_zero : Core.IntervalRat

Equations

• LeanCert.Examples.EdgeCases.I_cross_zero = { lo := -1, hi := 1, le := LeanCert.Examples.EdgeCases.I_cross_zero._proof_1 }

theorem LeanCert.Examples.EdgeCases.inv_zero_safe : have result := Engine.evalIntervalCoreWithDiv (Core.Expr.var 0).inv fun (x : ℕ) => I_cross_zero; result.lo ≤ -1000000 ∧ 1000000 ≤ result.hi

2. The "Square Root of Negative" Edge Case

Mathlib defines Real.sqrt x = 0 for x < 0. LeanCert's interval arithmetic must respect this convention to remain sound with respect to the standard library.

def LeanCert.Examples.EdgeCases.I_negative : Core.IntervalRat

Equations

• LeanCert.Examples.EdgeCases.I_negative = { lo := -5, hi := -1, le := LeanCert.Examples.EdgeCases.I_negative._proof_1 }

def LeanCert.Examples.EdgeCases.exprSqrt : Core.Expr

Equations

• LeanCert.Examples.EdgeCases.exprSqrt = (LeanCert.Core.Expr.var 0).sqrt

def LeanCert.Examples.EdgeCases.exprSqrt_core : Core.ExprSupportedCore exprSqrt

Equations

• LeanCert.Examples.EdgeCases.exprSqrt_core = ⋯

theorem LeanCert.Examples.EdgeCases.sqrt_neg_contains_zero : have result := Engine.evalIntervalCore1 exprSqrt I_negative; result.lo = 0

def LeanCert.Examples.EdgeCases.I_mixed : Core.IntervalRat

Equations

• LeanCert.Examples.EdgeCases.I_mixed = { lo := -1, hi := 4, le := LeanCert.Examples.EdgeCases.I_mixed._proof_1 }

theorem LeanCert.Examples.EdgeCases.sqrt_mixed_contains_two : have result := Engine.evalIntervalCore1 exprSqrt I_mixed; result.lo = 0 ∧ result.hi ≥ 2

3. Root Finding: Tangential Roots (Multiplicity > 1)

Bisection relies on sign change (IVT). It works for crossings (x³) but fails for touching roots (x²). This test confirms the library handles "no sign change" correctly.

NOTE: Interval arithmetic overestimates: [-1, 1] * [-1, 1] = [-1, 1], not [0, 1]. So x² on [-1, 1] gives interval [-1, 1], which includes negative values. This is sound (conservative) but not tight.

def LeanCert.Examples.EdgeCases.exprX2 : Core.Expr

Equations

• LeanCert.Examples.EdgeCases.exprX2 = (LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0)

def LeanCert.Examples.EdgeCases.exprX2_core : Core.ExprSupportedCore exprX2

Equations

• LeanCert.Examples.EdgeCases.exprX2_core = ⋯

theorem LeanCert.Examples.EdgeCases.x_sq_bounded_above (x : ℝ) : x ∈ I_cross_zero → Core.Expr.eval (fun (x_1 : ℕ) => x) exprX2 ≤ ↑1

def LeanCert.Examples.EdgeCases.I_positive : Core.IntervalRat

Equations

• LeanCert.Examples.EdgeCases.I_positive = { lo := 0, hi := 1, le := LeanCert.Examples.EdgeCases.I_positive._proof_1 }

theorem LeanCert.Examples.EdgeCases.x_sq_nonneg_on_positive (x : ℝ) : x ∈ I_positive → ↑0 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprX2

def LeanCert.Examples.EdgeCases.exprX3 : Core.Expr

Equations

• LeanCert.Examples.EdgeCases.exprX3 = (LeanCert.Core.Expr.var 0).mul ((LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0))

def LeanCert.Examples.EdgeCases.exprX3_core : Core.ExprSupportedCore exprX3

Equations

• LeanCert.Examples.EdgeCases.exprX3_core = ⋯

theorem LeanCert.Examples.EdgeCases.x_cube_spans_zero : have result := Engine.evalIntervalCore1 exprX3 I_cross_zero; result.lo < 0 ∧ 0 < result.hi

4. The "Sinc" Singularity at 0

sin(x)/x has a removable singularity at 0. Expr.div (sin x) x will give wide bounds at 0, but Expr.sinc x is safe.

NOTE: sinc is not in ExprSupportedCore, so we test using ExprSupportedWithInv or direct evaluation.

def LeanCert.Examples.EdgeCases.exprSinDivX : Core.Expr

Equations

• LeanCert.Examples.EdgeCases.exprSinDivX = (LeanCert.Core.Expr.var 0).sin.mul (LeanCert.Core.Expr.var 0).inv

theorem LeanCert.Examples.EdgeCases.sin_div_x_wide_at_zero : have result := Engine.evalIntervalCoreWithDiv exprSinDivX fun (x : ℕ) => I_cross_zero; result.hi > 1000 ∨ result.lo < -1000

def LeanCert.Examples.EdgeCases.exprSinc : Core.Expr

Equations

• LeanCert.Examples.EdgeCases.exprSinc = (LeanCert.Core.Expr.var 0).sinc

theorem LeanCert.Examples.EdgeCases.sinc_at_zero : Core.Expr.eval (fun (x : ℕ) => 0) exprSinc = 1

theorem LeanCert.Examples.EdgeCases.sinc_bounded_check : have result := Engine.evalIntervalCoreWithDiv exprSinc fun (x : ℕ) => I_cross_zero; result.lo ≥ -2 ∧ result.hi ≤ 2

5. Precision Stress Test (Deep Polynomial)

Deep composition of polynomials causes rational denominators to explode in size. We test if the evaluator can handle depths that might choke naive implementations.

def LeanCert.Examples.EdgeCases.exprDeepPoly : Core.Expr

Equations

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

def LeanCert.Examples.EdgeCases.exprDeepPoly_core : Core.ExprSupportedCore exprDeepPoly

Equations

• LeanCert.Examples.EdgeCases.exprDeepPoly_core = ⋯

def LeanCert.Examples.EdgeCases.I_half_one : Core.IntervalRat

Equations

• LeanCert.Examples.EdgeCases.I_half_one = { lo := 1 / 2, hi := 1, le := LeanCert.Examples.EdgeCases.I_half_one._proof_1 }

theorem LeanCert.Examples.EdgeCases.deep_poly_bounded (x : ℝ) : x ∈ I_half_one → Core.Expr.eval (fun (x_1 : ℕ) => x) exprDeepPoly ≤ ↑1

theorem LeanCert.Examples.EdgeCases.deep_poly_nonneg (x : ℝ) : x ∈ I_half_one → ↑0 ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprDeepPoly

6. The "Wiggle" Function

Test a function with oscillating behavior: x · sin(10x) on [0.1, 1].

def LeanCert.Examples.EdgeCases.exprWiggle : Core.Expr

Equations

• LeanCert.Examples.EdgeCases.exprWiggle = (LeanCert.Core.Expr.var 0).mul ((LeanCert.Core.Expr.const 10).mul (LeanCert.Core.Expr.var 0)).sin

def LeanCert.Examples.EdgeCases.exprWiggle_core : Core.ExprSupportedCore exprWiggle

Equations

• LeanCert.Examples.EdgeCases.exprWiggle_core = ⋯

def LeanCert.Examples.EdgeCases.I_wiggle : Core.IntervalRat

Equations

• LeanCert.Examples.EdgeCases.I_wiggle = { lo := 1 / 10, hi := 1, le := LeanCert.Examples.EdgeCases.I_wiggle._proof_1 }

theorem LeanCert.Examples.EdgeCases.wiggle_bounded (x : ℝ) : x ∈ I_wiggle → Core.Expr.eval (fun (x_1 : ℕ) => x) exprWiggle ≤ ↑1

theorem LeanCert.Examples.EdgeCases.wiggle_bounded_below (x : ℝ) : x ∈ I_wiggle → ↑(-1) ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) exprWiggle

7. Type Safety of IntervalRat

The IntervalRat structure requires lo ≤ hi as a field, so invalid intervals cannot be constructed. This is proven by the type system itself.

8. Zero-Dimensional Evaluation

Evaluating a constant expression (0 variables) on an empty domain.

def LeanCert.Examples.EdgeCases.exprConst5 : Core.Expr

Equations

• LeanCert.Examples.EdgeCases.exprConst5 = LeanCert.Core.Expr.const 5

def LeanCert.Examples.EdgeCases.exprConst5_core : Core.ExprSupportedCore exprConst5

Equations

• LeanCert.Examples.EdgeCases.exprConst5_core = ⋯

theorem LeanCert.Examples.EdgeCases.const_eval_correct : Core.Expr.eval (fun (x : ℕ) => 0) exprConst5 = 5

def LeanCert.Examples.EdgeCases.I_any : Core.IntervalRat

Equations

• LeanCert.Examples.EdgeCases.I_any = { lo := 0, hi := 1, le := LeanCert.Examples.EdgeCases.I_positive._proof_1 }

theorem LeanCert.Examples.EdgeCases.const_interval_correct : have result := Engine.evalIntervalCore1 exprConst5 I_any; result.lo = 5 ∧ result.hi = 5

9. Dyadic Interval Evaluation

Test the dyadic (floating-point style) evaluator for performance comparison.

def LeanCert.Examples.EdgeCases.I_unit_dyadic : Core.IntervalDyadic

Equations

• LeanCert.Examples.EdgeCases.I_unit_dyadic = { lo := { mantissa := 0, exponent := 0 }, hi := { mantissa := 1, exponent := 0 }, le := LeanCert.Examples.EdgeCases.I_unit_dyadic._proof_1 }

theorem LeanCert.Examples.EdgeCases.dyadic_x2_bounded : have result := Engine.evalIntervalDyadic exprX2 fun (x : ℕ) => I_unit_dyadic; result.lo.toRat ≥ 0

10. Global Optimization Edge Cases

def LeanCert.Examples.EdgeCases.box_sym : Engine.Optimization.Box

Equations

• LeanCert.Examples.EdgeCases.box_sym = [LeanCert.Examples.EdgeCases.I_cross_zero]

theorem LeanCert.Examples.EdgeCases.x2_max_correct : have result := Engine.Optimization.globalMaximizeCore exprX2 box_sym; result.bound.hi ≤ 1

def LeanCert.Examples.EdgeCases.box_positive : Engine.Optimization.Box

Equations

• LeanCert.Examples.EdgeCases.box_positive = [LeanCert.Examples.EdgeCases.I_positive]

theorem LeanCert.Examples.EdgeCases.x2_min_on_positive : have result := Engine.Optimization.globalMinimizeCore exprX2 box_positive; result.bound.lo ≥ 0

theorem LeanCert.Examples.EdgeCases.x3_min_at_neg_one : have result := Engine.Optimization.globalMinimizeCore exprX3 box_sym; result.bound.lo ≥ -1