Root Finding: Bisection Algorithm

This file implements the bisection method for root isolation.

Main definitions

• BisectionResult - Result structure from bisection
• bisectRootGo - Worker function for bisection
• bisectRoot - Main bisection entry point

Main theorems

• bisectRoot_hasRoot_correct - If status is hasRoot, there exists a root (via IVT)
• bisectRoot_noRoot_correct - If status is noRoot, there are no roots

All bisection theorems are FULLY PROVED with no sorry.

Bisection result structure

structure LeanCert.Engine.BisectionResult : Type

Result of bisection root finding

• intervals : List (Core.IntervalRat × RootStatus)

  Interval-status pairs

• iterations : ℕ

  Number of bisections performed

def LeanCert.Engine.BisectionResult.candidates (r : BisectionResult) : List Core.IntervalRat

Get just the candidate intervals

Equations

• r.candidates = List.map Prod.fst r.intervals

def LeanCert.Engine.BisectionResult.statuses (r : BisectionResult) : List RootStatus

Get just the statuses

Equations

• r.statuses = List.map Prod.snd r.intervals

Bisection algorithm

noncomputable def LeanCert.Engine.bisectRootGo (e : Core.Expr) (tol : ℚ) (maxIter : ℕ) (work : List (Core.IntervalRat × RootStatus)) (iter : ℕ) (done : List (Core.IntervalRat × RootStatus)) : BisectionResult

Worker function for bisection root finding.

Processes a worklist, discarding intervals that provably contain no roots, bisecting intervals that may contain roots until they are small enough.

Lifted to top-level so we can state correctness lemmas about it.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.bisectRootGo e tol maxIter work 0 done = { intervals := done ++ work, iterations := maxIter }
• LeanCert.Engine.bisectRootGo e tol maxIter [] iter done = { intervals := done, iterations := maxIter - iter }

noncomputable def LeanCert.Engine.bisectRoot (e : Core.Expr) (I : Core.IntervalRat) (maxIter : ℕ) (tol : ℚ) (_htol : 0 < tol) : BisectionResult

Bisection root finding.

Repeatedly bisects the interval, discarding subintervals that provably contain no roots.

Equations

• LeanCert.Engine.bisectRoot e I maxIter tol _htol = LeanCert.Engine.bisectRootGo e tol maxIter [(I, LeanCert.Engine.RootStatus.unknown)] maxIter []

Bisection correctness

theorem LeanCert.Engine.checkRootStatus_noRoot_implies_excludesZero (e : Core.Expr) (J : Core.IntervalRat) : checkRootStatus e J = RootStatus.noRoot → excludesZero (evalInterval1 e J) = true

Key lemma: checkRootStatus returns noRoot only when excludesZero is true

theorem LeanCert.Engine.checkRootStatus_hasRoot_implies_signChange (e : Core.Expr) (J : Core.IntervalRat) : checkRootStatus e J = RootStatus.hasRoot → signChange e J = true

Key lemma: checkRootStatus returns hasRoot only when signChange is true

Invariants for bisection proofs

def LeanCert.Engine.BisectInv (e : Core.Expr) (pairs : List (Core.IntervalRat × RootStatus)) : Prop

Invariant for bisection: every interval with hasRoot status has signChange = true. Note: noRoot intervals are discarded by the algorithm, so they never appear in output.

Equations

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

def LeanCert.Engine.SubIntervalInv (I : Core.IntervalRat) (pairs : List (Core.IntervalRat × RootStatus)) : Prop

Invariant for tracking sub-intervals: all intervals in the list are sub-intervals of I

Equations

• LeanCert.Engine.SubIntervalInv I pairs = ∀ (J : LeanCert.Core.IntervalRat) (s : LeanCert.Engine.RootStatus), (J, s) ∈ pairs → I.lo ≤ J.lo ∧ J.hi ≤ I.hi

theorem LeanCert.Engine.bisect_inv_initial (e : Core.Expr) (I : Core.IntervalRat) : BisectInv e [(I, RootStatus.unknown)]

The invariant holds for the initial work list

theorem LeanCert.Engine.subinterval_inv_initial (I : Core.IntervalRat) : SubIntervalInv I [(I, RootStatus.unknown)]

The sub-interval invariant holds initially

theorem LeanCert.Engine.bisect_inv_cons_hasRoot (e : Core.Expr) (J : Core.IntervalRat) (pairs : List (Core.IntervalRat × RootStatus)) (hInv : BisectInv e pairs) (hsign : signChange e J = true) : BisectInv e ((J, RootStatus.hasRoot) :: pairs)

BisectInv is preserved when adding a hasRoot interval with signChange = true

theorem LeanCert.Engine.bisect_inv_cons_other (e : Core.Expr) (J : Core.IntervalRat) (s : RootStatus) (pairs : List (Core.IntervalRat × RootStatus)) (hInv : BisectInv e pairs) (hne : s ≠ RootStatus.hasRoot) : BisectInv e ((J, s) :: pairs)

BisectInv is preserved when adding non-hasRoot intervals

theorem LeanCert.Engine.bisect_inv_append (e : Core.Expr) (l₁ l₂ : List (Core.IntervalRat × RootStatus)) (h₁ : BisectInv e l₁) (h₂ : BisectInv e l₂) : BisectInv e (l₁ ++ l₂)

BisectInv holds for list append

theorem LeanCert.Engine.subinterval_inv_append (I : Core.IntervalRat) (l₁ l₂ : List (Core.IntervalRat × RootStatus)) (h₁ : SubIntervalInv I l₁) (h₂ : SubIntervalInv I l₂) : SubIntervalInv I (l₁ ++ l₂)

SubIntervalInv holds for list append

theorem LeanCert.Engine.subinterval_inv_cons (I J : Core.IntervalRat) (s : RootStatus) (pairs : List (Core.IntervalRat × RootStatus)) (hInv : SubIntervalInv I pairs) (hJ : I.lo ≤ J.lo ∧ J.hi ≤ I.hi) : SubIntervalInv I ((J, s) :: pairs)

SubIntervalInv is preserved when adding a sub-interval

theorem LeanCert.Engine.bisect_subinterval (I J : Core.IntervalRat) (hJ : I.lo ≤ J.lo ∧ J.hi ≤ I.hi) : match J.bisect with | (J₁, J₂) => (I.lo ≤ J₁.lo ∧ J₁.hi ≤ I.hi) ∧ I.lo ≤ J₂.lo ∧ J₂.hi ≤ I.hi

Bisecting preserves the sub-interval property

Main correctness proofs

theorem LeanCert.Engine.go_noRoot_not_in_output (e : Core.Expr) (tol : ℚ) (maxIter : ℕ) (work : List (Core.IntervalRat × RootStatus)) (iter : ℕ) (done : List (Core.IntervalRat × RootStatus)) (hDone : ∀ (J : Core.IntervalRat) (s : RootStatus), (J, s) ∈ done → s ≠ RootStatus.noRoot) (hWork : ∀ (J : Core.IntervalRat) (s : RootStatus), (J, s) ∈ work → s ≠ RootStatus.noRoot) (J : Core.IntervalRat) (s : RootStatus) : (J, s) ∈ (bisectRootGo e tol maxIter work iter done).intervals → s ≠ RootStatus.noRoot

noRoot never appears in output - the algorithm discards such intervals. We prove this by induction on iter.

theorem LeanCert.Engine.go_hasRoot_has_signChange (e : Core.Expr) (tol : ℚ) (maxIter : ℕ) (work : List (Core.IntervalRat × RootStatus)) (iter : ℕ) (done : List (Core.IntervalRat × RootStatus)) (hWork : BisectInv e work) (hDone : BisectInv e done) : BisectInv e (bisectRootGo e tol maxIter work iter done).intervals

Every hasRoot interval in output has signChange = true. We prove this by induction on iter. Note: We need BisectInv for work too, since at iter=0 we output work as-is.

theorem LeanCert.Engine.go_subinterval (e : Core.Expr) (tol : ℚ) (maxIter : ℕ) (I : Core.IntervalRat) (work : List (Core.IntervalRat × RootStatus)) (iter : ℕ) (done : List (Core.IntervalRat × RootStatus)) (hWork : SubIntervalInv I work) (hDone : SubIntervalInv I done) : SubIntervalInv I (bisectRootGo e tol maxIter work iter done).intervals

Every interval in output is a sub-interval of the original. We prove this by induction on iter.

theorem LeanCert.Engine.bisectRoot_hasRoot_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (maxIter : ℕ) (tol : ℚ) (htol : 0 < tol) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) : have result := bisectRoot e I maxIter tol htol; ∀ (J : Core.IntervalRat) (s : RootStatus), (J, s) ∈ result.intervals → s = RootStatus.hasRoot → ∃ x ∈ J, Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

If bisection returns hasRoot for an interval, there exists a root (by IVT).

The proof works by showing that every (J, hasRoot) pair in the output has signChange e J = true, then applying signChange_correct.

Note about noRoot: The algorithm discards noRoot intervals, so they never appear in the output. Thus bisectRoot_noRoot_correct is vacuously true.

theorem LeanCert.Engine.bisectRoot_noRoot_correct (e : Core.Expr) (_hsupp : ExprSupported e) (I : Core.IntervalRat) (maxIter : ℕ) (tol : ℚ) (htol : 0 < tol) : have result := bisectRoot e I maxIter tol htol; ∀ (J : Core.IntervalRat) (s : RootStatus), (J, s) ∈ result.intervals → s = RootStatus.noRoot → ∀ x ∈ J, Core.Expr.eval (fun (x_1 : ℕ) => x) e ≠ 0

If bisection returns noRoot for an interval, there really is no root.

Note: The bisection algorithm discards noRoot intervals - when checkRootStatus returns noRoot, we call go rest n done without adding J to done. So noRoot never appears in the output intervals list.

This means the theorem is vacuously true: there are no (J, noRoot) pairs in the output.