Root Finding: Newton Contraction Existence Theorem

This file contains the main theorem proving that Newton contraction implies root existence, along with the uniqueness theorem.

Main theorems

• newton_contraction_has_root - If Newton step contracts, a root exists
• newton_contraction_unique_root - If Newton step contracts, exactly one root exists
• newtonIntervalGo_preserves_root - Newton iteration preserves roots

Verification Status

All theorems in this file are fully proved with no sorry statements.

Newton contraction existence theorem

theorem LeanCert.Engine.newton_contraction_has_root (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I N : Core.IntervalRat) (hN : newtonStepTM e I 0 = some N ∨ newtonStepSimple e I 0 = some N) (hContract : N.lo > I.lo ∧ N.hi < I.hi) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) : ∃ x ∈ N, Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

If Newton iteration detects contraction (N ⊂ I strictly), existence of root. Combined with newton_preserves_root, this gives uniqueness.

The key insight is that contraction of the Newton operator implies that f must change sign within the interval (otherwise the operator wouldn't contract). This uses the structure of Newton's method, not just general contraction.

theorem LeanCert.Engine.newton_contraction_unique_root (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I N : Core.IntervalRat) (hN : newtonStepTM e I 0 = some N ∨ newtonStepSimple e I 0 = some N) (hContract : N.lo > I.lo ∧ N.hi < I.hi) (hCont : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)) : ∃! x : ℝ, x ∈ I ∧ Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

If Newton iteration detects contraction, the root is unique in I. This is THE key uniqueness theorem for Newton's method.

Newton iteration loop correctness

theorem LeanCert.Engine.newtonIntervalGo_preserves_root (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (J : Core.IntervalRat) (iter : ℕ) (contracted : Bool) (x : ℝ) (hxJ : x ∈ J) (hroot : Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0) : (newtonIntervalGo e 0 1 J iter contracted).2 ≠ RootStatus.noRoot

If a root exists in J and Newton iteration doesn't return noRoot, the root is preserved. Key lemma for proving noRoot correctness.

Note: Uses newton_preserves_root which puts x in both J and N