TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

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.

An entire function of polynomial growth is a polynomial

Statement

Let $f : C \to C$ be entire. Suppose there are real numbers $C, N \geq 0$ such that

$∣ f (z) ∣ \leq C (1 + ∣ z ∣)^{N} (z \in C),$

where real powers have the convention of Real powers for positive bases, with the zero-base positive-exponent convention. Put $m = ⌊ N ⌋$ . Then there are complex coefficients $c_{0}, \dots, c_{m}$ such that

$f (z) = \sum_{k = 0}^{m} c_{k} z^{k} (z \in C) .$

Thus $f$ is a polynomial, and if it is nonzero its degree is at most $⌊ N ⌋$ .

Facts & Assumptions

Given: An entire function $f$ and real constants $C, N \geq 0$ satisfying the displayed growth bound.

[L1]

If $f$ is holomorphic on $D (a, R_{0})$ , $0 < r < R_{0}$ , and $∣ f (ζ) ∣ \leq M$ on $∣ ζ - a ∣ = r$ , then the $n$ th Taylor coefficient $c_{n}$ satisfies $∣ c_{n} ∣ \leq M / r^{n}$ (Cauchy's inequalities bound the Taylor coefficients by the circle supremum).

[L2]

For $a > 0$ and real $x$ , the real power is $a^{x} = \exp (x \log a)$ ; zero-base powers are defined only for positive exponents (Real powers for positive bases, with the zero-base positive-exponent convention).

[L3]

Positive-base real powers satisfy $a^{r + s} = a^{r} a^{s}$ and $(a b)^{r} = a^{r} b^{r}$ (The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents).

[L4]

The natural logarithm is the inverse of the exponential on the positive reals (The natural logarithm as the inverse of the exponential function).

[L5]

The exponential tends to $0$ at $- \infty$ and to $+ \infty$ at $+ \infty$ (The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ ).

[L6]

Every entire function equals its Taylor series at the origin on the whole complex plane (A holomorphic function equals its Taylor series throughout the largest centred disc in its domain).

[L7]

For every real $x$ there is a unique integer $⌊ x ⌋$ satisfying $⌊ x ⌋ \leq x < ⌊ x ⌋ + 1$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

[L8]

The exponential function is strictly increasing on $R$ (The exponential function is strictly increasing).

Proof

technique · direct

1.1

Let $f (z) = \sum_{n \geq 0} c_{n} z^{n}$ be its Taylor series at $0$ , fix a natural $n > N$ , and take any real $R \geq 1$ ; the growth hypothesis bounds $∣ f ∣$ on $∣ ζ ∣ = R$ by $C (1 + R)^{N}$ , so [L1], applied with outer radius $R + 1$ , gives $∣ c_{n} ∣ \leq C (1 + R)^{N} / R^{n}$ .

givenL1

2.1

Since $R \geq 1$ gives $1 + R \leq 2 R$ , [L2], [L3], [L4], and [L8] give $∣ c_{n} ∣ \leq C 2^{N} R^{N - n} = C 2^{N} \exp (- (n - N) \log R)$ ; by [L4], [L5], and [L8], $\log R \to + \infty$ as $R \to + \infty$ , so the right side tends to $0$ , forcing $c_{n} = 0$ .

step 1.1L2L3L4L5L8algebra

3.1

Step 2.1 applies to every natural $n > N$ , and [L6] represents $f$ globally by its Taylor series, so all terms with index exceeding $N$ vanish and the series truncates.

step 2.1L6

4.1

Put $m = ⌊ N ⌋$ . By [L7], $m \leq N < m + 1$ , so every natural $n \geq m + 1$ satisfies $n > N$ and has $c_{n} = 0$ by step 3.1; because $N \geq 0$ , the integer $m$ is a natural number, and the displayed finite polynomial has no term above $m$ .

step 3.1L7

5.1

If $C = 0$ , the hypothesis gives $f = 0$ directly; if $N = 0$ , step 4.1 gives $m = 0$ and $f$ is constant. In every case step 4.1 proves the stated polynomial representation, with the degree qualification interpreted only for a nonzero polynomial.

step 3.1step 4.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Steven G. Krantz, A Guide to Complex Variables, §3.1.3 (standard reference, not scraped)