LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A nonconstant complex polynomial tends to infinite modulus and attains a global minimum modulus

Statement

If $p$ is a nonconstant complex polynomial, then $|p(z)|\to\infty$ as $|z|\to\infty$ , and $|p|$ attains a global minimum on $\mathbb C$ . The conventions and prerequisite facts used below are recorded in Formal complex polynomials, evaluation, degree, leading coefficient, and monic polynomials, Conjugation laws, $z\overline z=|z|^2$ , multiplicativity of modulus, and the triangle inequality, Heine-Borel in $\mathbb{R}^n$ : with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, Laws of finite sums and finite products.

Facts & Assumptions

Given: A nonconstant polynomial $p(z)=a_nz^n+\sum_{k<n}a_kz^k$ with $a_n\ne0$ .

[L1]

Conjugation laws, $z\overline z=|z|^2$ , multiplicativity of modulus, and the triangle inequality gives $|uv|=|u||v|$ and $|u+v|\le|u|+|v|$ .

[L2]

Heine-Borel in $\mathbb{R}^n$ : with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line says that every closed box in $\mathbb R^2$ is compact.

[L3]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value gives a minimum for a continuous real-valued function on a nonempty compact metric space.

[L4]

A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions makes a map into $\mathbb R^2$ continuous exactly when its two components are continuous.

Proof

technique · direct

1.1

Put $C:=\sum_{k<n}|a_k|$ . For $r=|z|\ge1$ , [L1] gives $|p(z)|\ge |a_n|r^n-\sum_{k<n}|a_k|r^k\ge r^n\bigl(|a_n|-C/r\bigr).$ Thus for $r\ge2C/|a_n|$ the right side is at least $(|a_n|/2)r^n$ , which tends to $+\infty$ .

L1algebra

1.2

Writing $z=x+iy$ , each coordinate projection is continuous because $|x-x_0|,|y-y_0|\le\|(x,y)-(x_0,y_0)\|$ . The identity $uv-u_0v_0=u(v-v_0)+v_0(u-u_0)$ proves continuity of products, so induction over the finite expression makes both coordinate polynomials of $p(x+iy)$ continuous. Then [L4] makes $p$ and $|p|$ continuous.

2.1

Choose $R\ge1$ so that the lower bound of step 1.1 is $>|p(0)|$ when $|z|>R$ . The closed square $K=[-R,R]^2\subseteq\mathbb R^2=\mathbb C$ is nonempty and compact by [L2]; outside $K$ one has $|z|>R$ . By [L3] and step 1.2, let $a\in K$ minimize $|p|$ on $K$ .

L2L3step 1.1step 1.2

3.1

Since $0\in K$ , this minimizer satisfies $|p(a)|\le|p(0)|$ . Step 2.1 makes every point outside $K$ have strictly larger modulus, so $a$ is a global minimizer.

step 2.1∎

Depends on

Used by

Fundamental theorem of algebra: every nonconstant complex polynomial has a complex root Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 159 results over 26 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Lebl, Basic Analysis I: The Fundamental Theorem of Algebra (standard reference, not scraped)