CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Constant boundary modulus forces an interior zero or constancy

Statement

If a holomorphic function has constant modulus on the boundary of a bounded domain, then it is constant or has a zero in the domain.

Precisely, let $Ω$ be a bounded complex domain and let $f$ be continuous on $\overline{Ω}$ and holomorphic on $Ω$ . If $∣ f (ζ) ∣ = M$ for every $ζ \in \partial Ω$ , then either $f$ is constant on $Ω$ or some $a \in Ω$ satisfies $f (a) = 0$ .

Facts & Assumptions

Given: A bounded complex domain $Ω$ , a function $f$ continuous on $\overline{Ω}$ and holomorphic on $Ω$ , and a real $M \geq 0$ such that $∣ f ∣ = M$ on $\partial Ω$ . A nonvanishing holomorphic function has a holomorphic reciprocal (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L1]

If $Ω$ is a bounded complex domain and $f$ is continuous on $\overline{Ω}$ and holomorphic on $Ω$ , then $∣ f ∣$ attains its maximum on $\partial Ω$ (Boundary maximum modulus principle on a bounded domain).

[L2]

A nowhere-zero holomorphic function on a complex domain cannot have an interior local modulus minimum unless it is constant (Minimum modulus principle for a nowhere-zero holomorphic function).

Proof

technique · direct

1.1L1given

If $M = 0$ , then [L1] gives $∣ f ∣ \leq 0$ on $\overline{Ω}$ , so $f$ is the zero function and is constant.

1.2L1givenalgebra

Suppose $M > 0$ and $f$ has no zero in $Ω$ . On $\partial Ω$ one has $∣ f ∣ = M > 0$ , so $f$ has no zero on $\overline{Ω}$ . At a point $c \in \overline{Ω}$ the identity $1 / f (z) - 1 / f (c) = (f (c) - f (z)) / (f (z) f (c))$ together with $∣ f (z) ∣ \geq ∣ f (c) ∣ / 2$ for $z$ near $c$ bounds $∣ 1 / f (z) - 1 / f (c) ∣$ by $2 ∣ f (z) - f (c) ∣ / ∣ f (c) ∣^{2}$ , so $1 / f$ is continuous on $\overline{Ω}$ ; the given reciprocal law makes it holomorphic on $Ω$ . Applying [L1] to $f$ and to $1 / f$ gives $∣ f ∣ \leq M$ and $1 / ∣ f ∣ \leq 1 / M$ on $\overline{Ω}$ . Hence $∣ f ∣ = M$ throughout $Ω$ .

2.1step 1.2L2

The equality in step 1.2 makes every interior point a local minimum of $∣ f ∣$ , so [L2] makes $f$ constant.

3.1step 1.1step 1.2step 2.1∎

Thus the zero-boundary case is constant, and in the positive-boundary case either $f$ is constant or the supposition in step 1.2 fails and $f$ has a zero in $Ω$ .

Depends on

Used by

A nonconstant Blaschke factor has constant boundary modulus Counterexample

Dependency tree · two levels

12 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

J. Lebl, Guide to Cultivating Complex Analysis, Exercise 3.3.20 (standard reference, not scraped)