CorollaryStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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 holomorphic function of constant modulus on a domain is constant

Statement

Let $U$ be a complex domain and let $f : U \to C$ be holomorphic. If $∣ f ∣$ is constant on $U$ , then $f$ is constant.

Facts & Assumptions

Given: A domain $U$ , a holomorphic $f = u + i v$ on $U$ , and a real $c \geq 0$ with $∣ f (z) ∣ = c$ for every $z \in U$ .

[L1]

Complex modulus is definite and satisfies $∣ u + i v ∣^{2} = u^{2} + v^{2}$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L2]

A holomorphic map satisfies $u_{x} = v_{y}$ , $u_{y} = - v_{x}$ , and $f^{'} = u_{x} + i v_{x}$ (Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with $\partial_{\overset{ˉ}{z}} f = 0$ , or with the Cauchy–Riemann equations).

[L3]

A holomorphic function with zero derivative on a domain is constant (A holomorphic function with zero derivative on a domain is constant).

Proof

technique · cases

1.1

Suppose first that $c = 0$ . Then $∣ f ∣ = 0$ , so $f = 0$ by [L1] and is constant.

assume-case zerogivenL1

1.2

Suppose next that $c > 0$ . Differentiating $u^{2} + v^{2} = c^{2}$ in the two real coordinates gives $u u_{x} + v v_{x} = 0$ and $u u_{y} + v v_{y} = 0$ .

assume-case posgivenL1algebra

2.1

Using [L2], the equations of step 1.2 become $u u_{x} - v u_{y} = 0$ and $v u_{x} + u u_{y} = 0$ . Their coefficient determinant is $u^{2} + v^{2} = c^{2} > 0$ , so $u_{x} = u_{y} = 0$ .

step 1.2L2algebra

3.1

Again by [L2], $v_{x} = - u_{y} = 0$ and $f^{'} = u_{x} + i v_{x} = 0$ throughout $U$ . Hence [L3] makes $f$ constant in the positive-modulus case.

step 2.1L2L3

4.1

The cases $c = 0$ and $c > 0$ exhaust $c \geq 0$ , and both give constancy.

step 1.1step 3.1cases-exhaustive∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 66 results over 15 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

R. Howell and J. Mathews, Complex Analysis, Theorem 3.2.12 (standard reference, not scraped)