Root Finding: Newton Method

This file implements the interval Newton method for root finding.

Main definitions

• newtonStepTM - TM-based interval Newton step
• newtonStepSimple - Simple interval Newton step (fallback)
• newtonStep - Combined Newton step (tries TM first)
• newtonIntervalGo - Main Newton iteration loop
• newtonIntervalTM - Newton interval iteration using TM

Main theorems

• newton_preserves_root - Roots are preserved by Newton refinement (via MVT)
• newton_step_at_most_one_root - At most one root when Newton step succeeds (via Rolle)
• newtonIntervalGo_preserves_root - If root exists, noRoot cannot be returned

All Newton theorems for root preservation are FULLY PROVED with no sorry.

Newton step definitions

noncomputable def LeanCert.Engine.newtonStepTM (e : Core.Expr) (I : Core.IntervalRat) (varIdx : ℕ) (degree : ℕ := 1) : Option Core.IntervalRat

One TM-based interval Newton step for e on I w.r.t. variable varIdx.

The Newton operator is: N(I) = c - f(c)/f'(I) where c is the center (midpoint) of I.

We use Taylor model evaluation to get a sharper bound on f(c) than plain interval evaluation, and AD for the derivative interval f'(I).

Returns the intersection I ∩ N(I), or none if:

• The Taylor model build fails (e.g., division by interval containing 0)
• The derivative interval contains 0 (cannot safely divide)
• The intersection is empty

degree is the Taylor model degree (1 is usually enough for Newton).

Equations

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

noncomputable def LeanCert.Engine.newtonStepSimple (e : Core.Expr) (I : Core.IntervalRat) (varIdx : ℕ) : Option Core.IntervalRat

Simple Newton step using plain interval arithmetic (fallback). Less precise than TM-based but always available.

Equations

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

noncomputable def LeanCert.Engine.newtonStep (e : Core.Expr) (I : Core.IntervalRat) (varIdx : ℕ) (degree : ℕ := 1) : Option Core.IntervalRat

Combined Newton step: tries TM-based first, falls back to simple. This is the main entry point for the Newton iteration.

Equations

• LeanCert.Engine.newtonStep e I varIdx degree = match LeanCert.Engine.newtonStepTM e I varIdx degree with | some N => some N | none => LeanCert.Engine.newtonStepSimple e I varIdx

@[irreducible]

noncomputable def LeanCert.Engine.newtonIntervalGo (e : Core.Expr) (varIdx degree : ℕ) (J : Core.IntervalRat) (iter : ℕ) (contracted : Bool) : Core.IntervalRat × RootStatus

Main Newton iteration loop. Extracted from newtonIntervalTM for proof purposes.

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.newtonIntervalGo e varIdx degree J 0 contracted = if contracted = true then (J, LeanCert.Engine.RootStatus.uniqueRoot) else (J, LeanCert.Engine.checkRootStatus e J)

noncomputable def LeanCert.Engine.newtonIntervalTM (e : Core.Expr) (I : Core.IntervalRat) (varIdx maxIter : ℕ) (degree : ℕ := 1) : Core.IntervalRat × RootStatus

Interval Newton iteration using TM-based steps.

If Newton step contracts (result ⊂ input), we have uniqueness.

Parameters:

• e: the expression representing the function
• I: initial interval to search for root
• varIdx: variable index (typically 0 for single-variable)
• maxIter: maximum number of Newton iterations
• degree: Taylor model degree (default 1, higher for more precision)

Equations

• LeanCert.Engine.newtonIntervalTM e I varIdx maxIter degree = LeanCert.Engine.newtonIntervalGo e varIdx degree I maxIter false

noncomputable def LeanCert.Engine.newtonInterval (e : Core.Expr) (I : Core.IntervalRat) (varIdx maxIter : ℕ) : Core.IntervalRat × RootStatus

Original Newton iteration (for backwards compatibility). Now uses TM-based implementation with degree 1.

Equations

• LeanCert.Engine.newtonInterval e I varIdx maxIter = LeanCert.Engine.newtonIntervalTM e I varIdx maxIter

Auxiliary lemmas for Newton proofs

theorem LeanCert.Engine.deriv_in_derivInterval (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (ξ : ℝ) (hξ : ξ ∈ I) : deriv (evalFunc1 e) ξ ∈ derivInterval e (fun (x : ℕ) => I) 0

The derivative of evalFunc1 at any point in I is contained in derivInterval. This bridges our AD derivative bounds to actual derivatives. Requires UsesOnlyVar0, which we'll assume for root finding on single-variable expressions.

theorem LeanCert.Engine.mvt_for_eval (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (c x : ℝ) (_hcI : c ∈ I) (_hxI : x ∈ I) (hcx : c ≠ x) : ∃ (ξ : ℝ), (min c x < ξ ∧ ξ < max c x) ∧ evalFunc1 e x - evalFunc1 e c = deriv (evalFunc1 e) ξ * (x - c)

Mean Value Theorem application: for differentiable f, f(x) - f(c) = f'(ξ)(x - c) for some ξ between c and x.

theorem LeanCert.Engine.between_mem_interval (I : Core.IntervalRat) (c x ξ : ℝ) (hcI : c ∈ I) (hxI : x ∈ I) (hξ_between : min c x < ξ ∧ ξ < max c x) : ξ ∈ I

If ξ is between c and x, and both c and x are in I, then ξ is in I.

theorem LeanCert.Engine.newton_operator_preserves_root (e : Core.Expr) (hsupp : ExprSupported e) (_hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (c : ℚ) (fc dI : Core.IntervalRat) (hc_in_I : ↑c ∈ I) (hfc : evalFunc1 e ↑c ∈ fc) (hdI : ∀ ξ ∈ I, deriv (evalFunc1 e) ξ ∈ dI) (hdI_nonzero : ¬dI.containsZero) (x : ℝ) (hx : x ∈ I) (hroot : evalFunc1 e x = 0) : have dNonzero := { toIntervalRat := dI, nonzero := hdI_nonzero }; have dInv := Core.IntervalRat.invNonzero dNonzero; have Q := fc.mul dInv; have Newton := { lo := c - Q.hi, hi := c - Q.lo, le := ⋯ }; x ∈ Newton

Abstract Newton preservation lemma: if x is a root in I, and we compute N = I ∩ (c - fc/dI) where fc contains f(c) and dI contains f'(I), then x ∈ N.

This captures the mathematical essence without dealing with the monadic structure of newtonStepTM/newtonStepSimple.

theorem LeanCert.Engine.newton_preserves_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) (x : ℝ) (hx : x ∈ I) (hroot : Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0) : x ∈ N

If a root exists in I and Newton step produces N, then the root is in N. This is the key soundness property: Newton refinement preserves roots.

Requires UsesOnlyVar0 e to connect our AD derivative bounds to actual derivatives. This is a reasonable assumption for root finding on single-variable expressions.

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

At most one root when Newton step succeeds (regardless of contraction).

If a Newton step succeeds (returns some N), then the derivative interval excludes zero. By MVT, this means f is strictly monotonic on I, hence at most one root.

This lemma is independent of existence - it just proves uniqueness given any two roots.

Helper lemmas for Newton contraction existence proof

structure LeanCert.Engine.NewtonContractionData (I N : Core.IntervalRat) : Type

Structure extracted from a contracting Newton step. When newtonStepSimple contracts, we can extract bounds on the quotient Q = fc/dI.

• c : ℚ
• fc : Core.IntervalRat
• dI : Core.IntervalRat
• Q : Core.IntervalRat
• hc_eq : self.c = I.midpoint
• hdI_nonzero : ¬self.dI.containsZero
• hQ_lo_bound : self.Q.lo > self.c - I.hi
• hQ_hi_bound : self.Q.hi < self.c - I.lo
• hN_lo : N.lo = max I.lo (self.c - self.Q.hi)
• hN_hi : N.hi = min I.hi (self.c - self.Q.lo)

theorem LeanCert.Engine.contraction_newton_bounds {I N : Core.IntervalRat} {c : ℚ} {Q : Core.IntervalRat} (hContract : N.lo > I.lo ∧ N.hi < I.hi) (hN_lo : N.lo = max I.lo (c - Q.hi)) (hN_hi : N.hi = min I.hi (c - Q.lo)) : N.lo = c - Q.hi ∧ N.hi = c - Q.lo

When Newton contracts strictly, the Newton bounds dominate the intersection. That is, N.lo = c - Q.hi (not I.lo) and N.hi = c - Q.lo (not I.hi).

theorem LeanCert.Engine.newtonStepSimple_extract (e : Core.Expr) (I N : Core.IntervalRat) (hSimple : newtonStepSimple e I 0 = some N) : have c := I.midpoint; have fc := evalInterval1 e (Core.IntervalRat.singleton c); have dI := derivInterval e (fun (x : ℕ) => I) 0; ∃ (hdI_nonzero : ¬dI.containsZero), have dNonzero := { toIntervalRat := dI, nonzero := hdI_nonzero }; have Q := fc.mul (Core.IntervalRat.invNonzero dNonzero); N.lo = max I.lo (c - Q.hi) ∧ N.hi = min I.hi (c - Q.lo)

Extract the Newton step structure from newtonStepSimple. This lemma isolates the definitional unfolding of newtonStepSimple.

theorem LeanCert.Engine.newtonStepTM_structure (e : Core.Expr) (I N : Core.IntervalRat) (hTM : newtonStepTM e I 0 = some N) : ∃ (tm : TaylorModel) (hdI_nonzero : ¬(derivInterval e (fun (x : ℕ) => I) 0).containsZero), TaylorModel.fromExpr? e I 1 = some tm ∧ tm.center = I.midpoint ∧ have c := I.midpoint; have fc := tm.valueAtCenterInterval; let dI := derivInterval e (fun (x : ℕ) => I) 0; have dNonzero := { toIntervalRat := dI, nonzero := hdI_nonzero }; have Q := fc.mul (Core.IntervalRat.invNonzero dNonzero); N.lo = max I.lo (c - Q.hi) ∧ N.hi = min I.hi (c - Q.lo)

Extract structure from newtonStepTM. This extracts the TM and proves the key structural facts.

theorem LeanCert.Engine.newtonStepTM_fc_correct (e : Core.Expr) (I : Core.IntervalRat) (tm : TaylorModel) (htmeq : TaylorModel.fromExpr? e I 1 = some tm) : have c := I.midpoint; have fc := tm.valueAtCenterInterval; evalFunc1 e ↑c ∈ fc

Key correctness lemma: for TM Newton step, f(c) ∈ the TM-computed fc interval. This is what allows us to use the generic contraction contradiction lemmas.