Root Finding Algorithms

LeanCert provides verified root finding with proofs of existence and uniqueness.

Overview

Algorithm	Proves	Method	Tactic
Sign-change certification	Existence	Check the supplied interval + IVT	`interval_roots`
Recursive bisection	Candidate isolation	Repeated sign-change search	advanced engine API
Newton Contraction	Uniqueness	Fixed-point theorem	`interval_unique_root`
Norm-form Krawczyk	Existence + uniqueness for square differentiable systems	Interval Jacobian + Banach	certificate API
Bézout derivative	Global simplicity of all roots of a rational polynomial	Exact identity `A P + B P' = c ≠ 0`	certificate API
Discriminant count	Uniform 1-or-3 real-root count for cubic coefficient families	Interval sign of leading coefficient and discriminant, with adaptive subdivision	certificate API
Complete cubic isolation	Three unique roots and proof that no others exist	Positive discriminant + three ordered Newton contractions	certificate API
Cauchy/separation mesh	A-priori root radius and pairwise gap	Exact rational coefficient and discriminant inequalities	certificate API

The Bézout layer is algebraic rather than isolating: it proves that roots are simple globally. Its QPoly.toExpr bridge lets that fact compose with the interval algorithms below. See Algebraic Root Certificates.

The discriminant layer is global rather than isolating. Its coefficients may be Expr families over a parameter box, and its subdivision checker resolves interval dependency by proving the same strict sign on every child box.

For fixed rational cubics, the complete-isolation layer joins these worlds: count globally, isolate locally, then use cardinality to prove exhaustion. The companion Cauchy-radius and separation-mesh checker can choose a certified search domain and a safe mesh width before local isolation starts. Pure cubic representations and interval ordering remain under Engine; the composition with the Newton Golden Theorem is intentionally located under Validity.Algebra.

Nonlinear Systems (Krawczyk)

For a square system F : Fin n → Expr in LeanCert's ADSupported fragment, LeanCert can check an untrusted rational center m and rational preconditioner Y. It computes an interval Jacobian on the box, bounds the infinity operator norm of I - Y J(X), and checks a strict self-map enclosure. A successful check certifies exactly one real root in the box.

import LeanCert.Validity.Krawczyk

open LeanCert.Core LeanCert.Engine LeanCert.Validity

example (F : Fin n → Expr) (X : Fin n → IntervalRat)
    (cert : KrawczykCert n)
    (h : krawczykCheck F X cert = true) :
    ∃! x, FinBoxMem x X ∧ SystemZero F x := by
  exact verify_unique_system_root F X cert {} h

KrawczykCert is dimension-safe: malformed vector and matrix shapes cannot be constructed. The checker accepts constants, variables, addition, multiplication, negation, sin, cos, and exp. It uses a strong norm-form condition, which is sometimes more conservative than the componentwise textbook Krawczyk operator but gives a direct Banach proof.

Three golden theorems expose the same successful check in the common goal shapes: verify_system_root_exists, verify_system_root_unique, and verify_unique_system_root.

The automatic I2 front end exposes the last shape directly:

import LeanCert.Examples.Krawczyk
import LeanCert.Tactic

open LeanCert.Core LeanCert.Engine LeanCert.Validity
open LeanCert.Examples.Krawczyk

example : ∃! x, FinBoxMem x box ∧ SystemZero system x := by
  system_unique_root (trust := auto)

The generated center and preconditioner remain untrusted candidate data. The search uses a box midpoint, singleton checked-AD Jacobian, pivoted rational Gauss--Jordan inversion, and bounded interval-Newton refinement. It then runs the same monolithic checker as system_unique_root using certificate and reaches the theorem only through the configured verification route.

Current limits

Systems must be square and use the ADSupported expression fragment.
Boxes, centers, and preconditioners use exact rational data.
The norm-form enclosure is intentionally conservative; a rejected certificate is inconclusive.
Automatic generation defaults to dimensions at most four; explicit certificates remain dimension-generic.
Candidate refinement uses fixed dyadic precision to prevent denominator explosion in untrusted search data.
Automatic search does not subdivide the target box. A certificate on one sub-box would not prove uniqueness over the original box.
The theorem is over real boxes. Complex systems must first be represented as coupled real and imaginary coordinates.

Sign-Change Certification And Recursive Bisection

The public interval_roots tactic checks for a sign change on the interval in the goal and proves existence there. It does not recursively isolate roots. The lower-level bisection engine can subdivide a search interval and return several candidates.

Public Tactic

Evaluate f at interval endpoints
If signs differ, IVT guarantees a root exists

f(a) < 0                    f(b) > 0
  ●━━━━━━━━━━━━━━━━━━━━━━━━━●
  a          root          b
             somewhere
             in here

The Theorem

#check verify_sign_change

Key insight: The checker checkSignChange is computable, while the conclusion is a semantic statement about real numbers. Its successful result may be established through LeanCert's native, kernel, or automatic verification route.

Usage

import LeanCert.Tactic.Discovery

open LeanCert.Core

def I12 : IntervalRat := ⟨1, 2, by norm_num⟩

-- Prove √2 exists (root of x² - 2)
example : ∃ x ∈ I12, Expr.eval (fun _ => x)
    (Expr.add (Expr.mul (Expr.var 0) (Expr.var 0)) (Expr.neg (Expr.const 2))) = 0 := by
  interval_roots

Advanced Engine Algorithm

The advanced Engine.RootFinding.Bisection API recursively subdivides and can return several candidate intervals. Its shape is:

bisectRoot(f, [a, b], depth):
  if depth = 0:
    return [a, b] if sign_change(f, a, b) else ∅

  mid = (a + b) / 2
  roots = []

  if sign_change(f, a, mid):
    roots += bisectRoot(f, [a, mid], depth - 1)

  if sign_change(f, mid, b):
    roots += bisectRoot(f, [mid, b], depth - 1)

  return roots

The interval_roots tactic is intentionally simpler: it checks for a sign change on the interval stated in the goal and proves existence there. It does not expose the engine's list of recursively isolated candidates.

Limitations

Only finds roots where sign changes (misses tangent roots like x² at 0)
Requires continuity (cannot handle discontinuous functions)
The advanced bisection engine may return multiple candidate intervals; the interval_roots tactic proves one existence statement on the supplied interval

Newton Contraction (Uniqueness)

How It Works

The Newton operator is:

\[ N(x) = x - \frac{f(x)}{f'(x)} \]

If we can show: 1. N maps interval I into itself: N(I) ⊆ I 2. N is a contraction: |N'(x)| < 1 for all x ∈ I

Then Banach fixed-point theorem guarantees exactly one root in I.

The Theorem

The exact engine theorem is:

#check LeanCert.Engine.newton_contraction_unique_root

It accepts an ADSupported expression, a UsesOnlyVar0 proof, the original interval and a checked Newton image, evidence that either the Taylor-model or simple Newton step produced that image, strict containment, and continuity. The conclusion is uniqueness of a root in the original interval. Prefer interval_unique_root unless you are building an engine-level certificate.

Usage

def rootInterval : IntervalRat := ⟨1, 2, by norm_num⟩

def squareMinusTwo : Expr :=
  Expr.add (Expr.mul (Expr.var 0) (Expr.var 0)) (Expr.neg (Expr.const 2))

example : ∃! x, x ∈ rootInterval ∧
    Expr.eval (fun _ => x) squareMinusTwo = 0 := by
  unfold squareMinusTwo
  interval_unique_root

Contraction Verification

To verify contraction, we bound |N'(x)|:

\[ N'(x) = 1 - \frac{f'(x)^2 - f(x) \cdot f''(x)}{f'(x)^2} = \frac{f(x) \cdot f''(x)}{f'(x)^2} \]

Using interval arithmetic: 1. Compute interval bounds on f(I), f'(I), f''(I) 2. Check if |f(I) · f''(I)| / |f'(I)|² < 1

Checker shape

The following is schematic pseudocode, not a Lean declaration:

checkNewtonContracts(f, I):
  # Compute function and derivatives on interval
  f_I   = evalInterval(f, I)
  f'_I  = evalInterval(derivative(f), I)
  f''_I = evalInterval(derivative(derivative(f)), I)

  # Check f' doesn't contain 0 (otherwise N undefined)
  if 0 ∈ f'_I:
    return false

  # Compute Newton image
  N_I = I - f_I / f'_I

  # Check maps into
  if not (N_I ⊆ I):
    return false

  # Check contraction (|N'| < 1)
  N'_bound = |f_I * f''_I| / (f'_I)²
  return N'_bound.hi < 1

The engine exposes newtonStep, which returns Option IntervalRat, and iteration APIs such as newtonIntervalGo. A simplified loop has this shape:

newtonRefine(e, I, n):
  match n with
  | 0       => I
  | n + 1   => if newtonStep(e, I) succeeds with J
               then newtonRefine(e, J, n)
               else I

Once sufficiently close to a simple root, classical Newton iteration is quadratically convergent and often approximately doubles the number of correct digits per successful step. That rate is not unconditional for every interval Newton run.

Comparison

Aspect	Bisection	Newton
Proves	Existence	Uniqueness
Requires	Sign change	f' ≠ 0, contraction
Convergence	Linear	Quadratic
Multiple roots	Advanced engine can return several sign-change candidates	Certifies at most one root in the checked interval
Tangent roots	Misses	Can verify if f' ≠ 0 nearby

Combined Workflow

For full root verification, first prove existence with interval_roots, then prove uniqueness with interval_unique_root. Tighten the input interval and rerun the existence proof when a narrower certified location is needed. The complete compiled squareMinusTwo example above demonstrates both steps.

Mean Value Theorem Bounds

For project-specific estimates, combine the certified derivative enclosure with Mathlib's mean-value theorems. The exact hypotheses depend on whether the development uses HasDerivAt, DifferentiableOn, or a convex-set formulation. This is used internally for: - Bounding how much f can change between sample points - Verifying monotonicity - Lipschitz constant estimation

Files

File	Description
`Engine/RootFinding/Basic.lean`	Core predicates (`signChange`, `excludesZero`)
`Engine/RootFinding/Bisection.lean`	Bisection algorithm
`Engine/RootFinding/Contraction.lean`	Newton contraction verification
`Engine/RootFinding/MVTBounds.lean`	Mean value theorem utilities
`Engine/RootFinding/Krawczyk.lean`	Nonlinear-system checker and soundness bridge
`Engine/RootFinding/KrawczykCandidate.lean`	Untrusted rational candidate generation and refinement
`Validity/Krawczyk.lean`	Stable golden theorem
`Tactic/Discovery.lean`	`interval_roots`, `interval_unique_root` tactics

Root Finding Algorithms

Overview

Nonlinear Systems (Krawczyk)

Current limits

Sign-Change Certification And Recursive Bisection

Public Tactic

The Theorem

Usage

Advanced Engine Algorithm

Limitations

Newton Contraction (Uniqueness)

How It Works

The Theorem

Usage

Contraction Verification

Checker shape

Refinement

Comparison

Combined Workflow

Mean Value Theorem Bounds

Files