All roots lie in the circle of radius $1 + A/|a_0|$

Proved

MetodosNumericos.cauchy_root_bound

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

numerical-analysispolynomials

Let $P(z) = a_0z^n + a_1z^{n-1} + \\dots + a_n$ have real coefficients with $a_0 \\neq 0$ and $n \\ge 1$ , and let $A = \\max\\{|a_1|, \\dots, |a_n|\\}$ . Then every complex root of $P$ satisfies $|z| \\le 1 + A/|a_0|$ . This is Proposição 4.2.1, the localization result the chapter uses to bound the search region for the zeros of a polynomial.

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_polinomiosDefs

Formal statement

namespace MetodosNumericos

theorem cauchy_root_bound (a : ℕ → ℝ) (n : ℕ) (hn : 1 ≤ n) (ha0 : a 0 ≠ 0)
    (A : ℝ) (hA : A = Finset.sup' (Finset.Icc 1 n) (by simp [Finset.nonempty_Icc, hn])
      (fun i => |a i|))
    (z : ℂ) (hz : polyValC a n z = 0) :
    ‖z‖ ≤ 1 + A / |a 0| := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 4, Proposição 4.2.1, p. 74.

Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Disclosure: this read-back is not blind. It was written by the same agent that drafted the Lean statement, at the explicit instruction of the mission's human owner, and not by an independent auditor with fresh context.

The statement fixes $a : \\mathbb{N} \\to \\mathbb{R}$ , a natural number $n$ with $n \\ge 1$ , and a real number $A$ , under the hypotheses $a_0 \\neq 0$ and

A = \\max_{1 \\le i \\le n} |a_i|,

the maximum being over the nonempty finite index set $\\{1, \\dots, n\\}$ . For a complex number $z$ satisfying

\\sum_{i=0}^{n} a_i\\, z^{\\,n-i} = 0,

the conclusion is

\\lVert z \\rVert \\;\\le\\; 1 + \\frac{A}{|a_0|},

with $\\lVert z \\rVert$ the modulus of $z$ and a non-strict inequality. The coefficients $a_i$ for $i > n$ play no role. The bound is asserted for every root, and the right-hand side is at least $1$ because $A \\ge 0$ and $|a_0| > 0$ .

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

All roots lie in the circle of radius 1+A/∣a0∣1 + A/|a_0|1+A/∣a0​∣

All roots lie in the circle of radius $1 + A/|a_0|$