Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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.

Zero free entire function of exponential type is an exponential

Statement

Let f:CC be entire and zero-free, and suppose there are real constants M>0 and C0 with

f(z)    MeCz(zC).

Then f(z)=f(0)eaz for all zC, where a:=f(0)/f(0). In particular, if f(0)=1 then f(z)=ef(0)z.

The statement is deliberately formulated with the constant M present: in applications the bound arises from a product eCzeBw in which the w-dependent factor cannot be absorbed into the exponent without losing linearity in z, and the constant factor is exactly what survives.

Facts & Assumptions

Given: The zero-free entire function and constants M>0, C0 of the statement.

[F1]

On a convex complex domain every closed rectifiable contour integral of a holomorphic function vanishes; vanishing of these integrals for a continuous function is equivalent to existence of a primitive. (Cauchy's theorem on a convex complex domain, For a continuous function on a complex domain, endpoint independence, zero closed-contour integrals, and existence of a primitive are equivalent).

[F2]

Holomorphic functions are exactly the locally analytic functions. Power-series sums are analytic and admit derivatives of every order by termwise differentiation; analytic functions are closed under algebraic operations, nonvanishing quotients and composition. (A complex function is holomorphic if and only if it is analytic, The sum of a complex power series is analytic throughout its open disc of convergence, A complex power-series sum has complex derivatives of every order, obtained by repeated termwise differentiation, Complex analytic functions are closed under finite linear combinations, products, quotients with nonzero denominator, and composition).

[F3]

Complex derivatives satisfy the linear, product, quotient and chain rules; a holomorphic function with derivative zero on a domain is constant. (Linearity, product, reciprocal, and quotient rules for complex derivatives, The chain rule for complex derivatives, A holomorphic function with zero derivative on a domain is constant).

[F4]

The complex exponential is entire with derivative itself, satisfies exp(z+w)=expzexpw, agrees with the real exponential on the real axis and has modulus expz=eRez. The real exponential is a strictly increasing bijection onto the positive reals. (The complex exponential is entire and its complex derivative is itself, exp(z+w)=expzexpw, and the complex exponential extends the real exponential, exp(x+iy)=ex(cosy+isiny), exp(x+iy)=ex, and eiπ+1=0, The exponential is a continuous bijection from R onto (0,), The exponential function is strictly increasing).

[F5]

A function continuous on the closure of a bounded domain and holomorphic inside attains its maximum modulus on the boundary. Every bounded entire function is constant. (Boundary maximum modulus principle on a bounded domain, Liouville's theorem: every bounded entire function is constant).

Proof

technique · direct
1.1

A disk estimate including zero growth. Suppose H is entire, H(0)=0, and ReH(w)A+Bw with A,B0. Fix w0 and 0<t<1, put R=w/t and K=A+BR+1>0. For ζ<1, the denominator 2KH(Rζ) has real part at least K+1>0. Thus G(ζ)=H(Rζ)/(2KH(Rζ)) is holomorphic by [F2] and satisfies G(0)=0. For η=H(Rζ), 2Kη2η2=4K(KReη)>0, so G(ζ)<1. The local power series at zero shows that G(ζ)/ζ extends holomorphically through zero. For 0<r<1, [F5] applied on ζr gives G(ζ)/ζ1/r there; fixing ζ and letting r increase to one proves G(ζ)ζ. Hence H(Rζ)ζ(2K+H(Rζ)). At ζ=tw/w this becomes H(w)[2t(A+1)+2Bw]/(1t). Let t decrease to zero to conclude H(w)2Bw; at w=0 the same holds. In particular A=B=0 never produces division by zero, and B=0 forces H=0.

F2F5algebra
1.2

Construct the entire logarithm. By the local power series and derivative statements of [F2], f is holomorphic, and because f is zero-free, g=f/f is holomorphic. On the convex plane [F1] gives a primitive h; subtract its value at zero so h(0)=0 and h=f/f. A primitive is holomorphic by definition, so [F2] also supplies its local power series.

F1F2F3
2.1

By [F3] and [F4], (feh)=fehfheh=0. Hence feh is constant with value f(0), and the exponential addition formula gives f=f(0)eh. Here f(0)0 by zero-freeness.

F3F4step 1.2algebra
3.1

The growth bound at zero gives M/f(0)1. Let A be the unique real number with eA=M/f(0), supplied by [F4]. Since the exponential is increasing and e0=1, A0. Taking moduli in step 2.1 and using [F4] gives eReh(z)eA+Cz, so Reh(z)A+Cz. The disk estimate of step 1.1, applied directly to h, yields h(z)2Cz for all z.

F4step 1.1step 2.1algebra
4.1

Near zero write the convergent power series h(z)=k1bkzk, with no constant term because h(0)=0. Then h(z)/z=k1bkzk1 extends analytically through zero, with value b1=h(0); the shifted series converges on the same disk by comparison on any smaller radius. Away from zero the quotient is holomorphic by [F2]. This defines an entire function q, bounded by 2C off zero by step 3.1 and at zero by continuity. By [F5], q is constant and equals h(0)=f(0)/f(0) from step 1.2. Consequently h(z)=az with the stated a, and step 2.1 gives f(z)=f(0)eaz.

F2F5step 1.2step 2.1step 3.1algebra
5.1

If C=0 the bound in step 3.1 forces h=0 and hence a=0 and f=f(0), including f=1,M=1. If f(0)=1, step 4.1 gives the advertised normalized formula. The assumptions exclude M=0 and f(0)=0; the removable value at zero and the open parameter limit t0 have both been checked. All constructions use uniquely determined analytic operations or one primitive, not any simultaneous choice of arbitrary witnesses.

F3step 1.1step 3.1step 4.1

Depends on

Used by

Dependency tree · two levels

71 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