Root Finding: Basic Definitions

This file provides the core definitions and basic correctness lemmas for root finding.

Main definitions

• RootStatus - Result of checking an interval for roots
• excludesZero - Check if an interval excludes zero
• signChange - Check if function has opposite signs at endpoints
• checkRootStatus - Determine initial root status

Main theorems

• excludesZero_correct - If interval excludes zero, no roots exist
• signChange_correct - If sign change exists, a root exists (IVT)

Root status

inductive LeanCert.Engine.RootStatus : Type

Result of checking an interval for roots

• noRoot : RootStatus

  No root in this interval (interval evaluation doesn't contain 0)

• hasRoot : RootStatus

  At least one root exists (by intermediate value theorem)

• uniqueRoot : RootStatus

  Exactly one root exists (Newton contraction)

• unknown : RootStatus

  Cannot determine

instance LeanCert.Engine.instReprRootStatus : Repr RootStatus

Equations

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

def LeanCert.Engine.instReprRootStatus.repr : RootStatus → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.instDecidableEqRootStatus : DecidableEq RootStatus

Equations

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

Basic root checks

def LeanCert.Engine.excludesZero (I : Core.IntervalRat) : Bool

Check if interval evaluation excludes zero

Equations

• LeanCert.Engine.excludesZero I = decide (I.hi < 0 ∨ 0 < I.lo)

noncomputable def LeanCert.Engine.signChange (e : Core.Expr) (I : Core.IntervalRat) : Bool

Check if function values have opposite signs at endpoints (IVT applicable)

Equations

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

noncomputable def LeanCert.Engine.checkRootStatus (e : Core.Expr) (I : Core.IntervalRat) : RootStatus

Initial root status check

Equations

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

Core correctness lemmas

theorem LeanCert.Engine.excludesZero_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (hexcl : excludesZero (evalInterval1 e I) = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≠ 0

If interval evaluation excludes zero, then f(x) ≠ 0 for all x in I. This is the key lemma for proving noRoot correctness.

theorem LeanCert.Engine.signChange_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (hsign : signChange e I = true) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) : ∃ x ∈ I, Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

If there is a sign change, then by IVT there exists a root. This uses Mathlib's intermediate_value_Icc theorem.

Proof strategy:

1. signChange means f(lo) < 0 < f(hi) or f(hi) < 0 < f(lo)
2. Use evalInterval1_correct on singletons to get actual values at endpoints
3. Apply intermediate_value_Icc to conclude 0 is in the image

N-Variable Root Finding Infrastructure

The following section provides infrastructure for root finding in multi-variable expressions. The key idea is that we search for roots along a specific coordinate while holding other variables fixed.

For a multi-variable expression e with environment ρ, we can find roots of evalAlong e ρ idx - the function obtained by varying coordinate idx while keeping all other coordinates fixed according to ρ.

N-variable root checks

noncomputable def LeanCert.Engine.excludesZero_idx (e : Core.Expr) (ρ_int : IntervalEnv) (_idx : ℕ) : Bool

Check if interval evaluation along coordinate idx excludes zero. Note: idx is kept for API consistency though the full box is checked.

Equations

• LeanCert.Engine.excludesZero_idx e ρ_int _idx = LeanCert.Engine.excludesZero (LeanCert.Engine.evalInterval e ρ_int)

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

Check if function has opposite signs at endpoints along coordinate idx

Equations

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

noncomputable def LeanCert.Engine.checkRootStatus_idx (e : Core.Expr) (ρ_int : IntervalEnv) (idx : ℕ) : RootStatus

Initial root status check along coordinate idx

Equations

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

N-variable correctness lemmas

theorem LeanCert.Engine.excludesZero_correct_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_int : IntervalEnv) (hexcl : excludesZero (evalInterval e ρ_int) = true) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → Core.Expr.eval ρ_real e ≠ 0

If interval evaluation excludes zero, then f(x) ≠ 0 for all x in the box. N-variable version: the function has no zeros in the entire box.

theorem LeanCert.Engine.signChange_correct_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_int : IntervalEnv) (idx : ℕ) (ρ_real : ℕ → ℝ) (hρ : ∀ (i : ℕ), i ≠ idx → ρ_real i ∈ ρ_int i) (hsign : signChange_idx e ρ_int idx = true) (hCont : ContinuousOn (e.evalAlong ρ_real idx) (Set.Icc ↑(ρ_int idx).lo ↑(ρ_int idx).hi)) : ∃ x ∈ ρ_int idx, e.evalAlong ρ_real idx x = 0

If there is a sign change along coordinate idx, then by IVT there exists a root along that coordinate. N-variable version: for any fixed values of other coordinates satisfying ρ_int, there exists a value of coordinate idx where the function is zero.

N-variable bisection root finding

inductive LeanCert.Engine.BisectResult : Type

Result of bisection root finding

• found (I : Core.IntervalRat) (depth : ℕ) : BisectResult

  Found interval containing root with a sign change

• noRoot : BisectResult

  No root in this interval

• uncertain (I : Core.IntervalRat) (depth : ℕ) : BisectResult

  Could not determine (no sign change detected)

instance LeanCert.Engine.instReprBisectResult : Repr BisectResult

Equations

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

def LeanCert.Engine.instReprBisectResult.repr : BisectResult → ℕ → Std.Format

Equations

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

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

theorem LeanCert.Engine.mem_bisect_cases (J : Core.IntervalRat) (t : ℝ) (ht : t ∈ J) : t ∈ J.bisect.1 ∨ t ∈ J.bisect.2

Helper: membership in bisected intervals

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

N-variable bisection root finding along coordinate idx.

This searches for a root of e by bisecting the interval ρ idx while keeping other coordinates fixed. It uses interval arithmetic to:

1. Exclude intervals where the function cannot be zero
2. Detect sign changes indicating a root exists (by IVT)
3. Bisect when neither condition is met

Returns a BisectResult indicating whether a root was found, excluded, or uncertain.

Equations

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

@[irreducible]

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

Equations

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

theorem LeanCert.Engine.bisectRootIdx_go_found_signChange (e : Core.Expr) (ρ_int : IntervalEnv) (idx maxDepth depth : ℕ) (J I : Core.IntervalRat) (d : ℕ) (hJ_sub : ∀ t ∈ J, t ∈ ρ_int idx) (hfound : bisectRootIdx.go e ρ_int idx maxDepth J depth = BisectResult.found I d) : signChange_idx e (updateIntervalEnv' ρ_int idx I) idx = true ∧ ∀ t ∈ I, t ∈ ρ_int idx

Helper: when go returns found, signChange_idx was true for that interval

theorem LeanCert.Engine.bisectRootIdx_found_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_int : IntervalEnv) (idx maxDepth : ℕ) (I : Core.IntervalRat) (d : ℕ) (hfound : bisectRootIdx e ρ_int idx maxDepth = BisectResult.found I d) (ρ_real : ℕ → ℝ) (hρ : ∀ (i : ℕ), i ≠ idx → ρ_real i ∈ ρ_int i) (hCont : ContinuousOn (e.evalAlong ρ_real idx) (Set.Icc ↑I.lo ↑I.hi)) : ∃ x ∈ I, e.evalAlong ρ_real idx x = 0

Correctness theorem for bisectRootIdx when it finds a root. If bisectRootIdx returns found I d, then for any ρ_real satisfying ρ_int, there exists a root of evalAlong e ρ_real idx in the returned interval I.

theorem LeanCert.Engine.bisectRootIdx_go_noRoot_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_int : IntervalEnv) (idx maxDepth depth : ℕ) (J : Core.IntervalRat) (hJ_sub : ∀ t ∈ J, t ∈ ρ_int idx) (hnoRoot : bisectRootIdx.go e ρ_int idx maxDepth J depth = BisectResult.noRoot) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ∀ t ∈ J, e.evalAlong ρ_real idx t ≠ 0

Helper: noRoot is preserved through bisection. The proof is complex due to the match structure in bisectRootIdx.go. The key insight is that noRoot can only be returned if excludesZero is true at some level of the recursion, and excludesZero implies the function is nonzero.

theorem LeanCert.Engine.bisectRootIdx_noRoot_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_int : IntervalEnv) (idx maxDepth : ℕ) (hnoRoot : bisectRootIdx e ρ_int idx maxDepth = BisectResult.noRoot) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ∀ t ∈ ρ_int idx, e.evalAlong ρ_real idx t ≠ 0

Correctness theorem for bisectRootIdx when it reports no root. If bisectRootIdx returns noRoot, then for any ρ_real satisfying ρ_int, the function evalAlong e ρ_real idx has no zeros in ρ_int idx.