Root Finding: Main Module

This module re-exports all components of the root finding library.

Module Structure

• Basic.lean - Core definitions (RootStatus, excludesZero, signChange, checkRootStatus) and basic correctness lemmas (excludesZero_correct, signChange_correct)

• Bisection.lean - Bisection algorithm (bisectRootGo, bisectRoot) and correctness theorems (bisectRoot_hasRoot_correct, bisectRoot_noRoot_correct)

• Newton.lean - Interval Newton method (newtonStepTM, newtonStepSimple, newtonStep, newtonIntervalGo, newtonIntervalTM) and core preservation theorems (newton_preserves_root, newton_step_at_most_one_root)

• MVTBounds.lean - Mean Value Theorem wrappers and quotient bound lemmas used for proving Newton contraction correctness

• Contraction.lean - Main contraction theorems (newton_contraction_has_root, newton_contraction_unique_root, newtonIntervalGo_preserves_root)

Usage

For most applications, import this module to get access to all root finding functionality:

import LeanCert.Engine.RootFinding.Main

Or import specific submodules as needed.

Verification Status

Fully Verified (no sorry):

• All root finding theorems are now fully proved with no sorry statements
• Bisection: bisectRoot_hasRoot_correct, bisectRoot_noRoot_correct
• Newton: newton_preserves_root, newton_step_at_most_one_root, newton_contraction_has_root, newton_contraction_unique_root, newtonIntervalGo_preserves_root
• MVT wrapper lemmas and all contraction contradiction lemmas