Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-29
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.

Schwarz lemma with the equality cases

Statement

Let f:DD be holomorphic and satisfy f(0)=0. Then

f(z)z(zD),f(0)1.

Moreover, if either f(z0)=z0 for some z0D{0} or f(0)=1, then

f(z)=eiθz

for some real θ; conversely every rotation zeiθz satisfies equality in both conclusions.

Facts & Assumptions

Given: A holomorphic map f:DD with f(0)=0.

[F1]

The unit disc is D={zC:z<1} (The unit disc, the upper half-plane, and Blaschke factors).

[F2]

If a holomorphic function on a punctured disc has a finite limit at the centre, then the singularity is removable (Characterizations of removable singularities).

[F3]

Boundary modulus control on a bounded domain bounds the modulus throughout the domain (Maximum modulus principle with boundary and infinity control).

[F4]

If the modulus of a holomorphic function has an interior local maximum, then the function is constant (Local maximum modulus principle).

Proof

technique · direct
1.1

If f0 then the two inequalities and the equality characterization are immediate, so assume f is not identically zero and define g(z)=f(z)/z for z0 on the punctured disc.

F1givencases
2.1

Since f(0)=limz0f(z)/z, the function g has finite limit f(0) at 0; by [F2] it extends holomorphically to D, still denoted g, with g(0)=f(0).

F2step 1.1algebra
3.1

Fix 0<r<1. On z=r one has g(z)=f(z)/r1/r because f(D)D; applying [F3] on the radius-r disc gives g(z)1/r whenever zr.

F1F3step 2.1algebra
4.1

For any wD, step 3.1 holds for every r with w<r<1, so letting r1 gives g(w)1; therefore f(w)=wg(w)w for all wD, and at w=0 this also gives f(0)=g(0)1.

step 2.1step 3.1algebra
5.1

If f(z0)=z0 for some z00, then step 4.1 gives g(z0)=1, an interior maximum for g, so [F4] makes g constant of modulus 1; if instead f(0)=1, then g(0)=1 and the same argument applies. Thus in either equality case g(z)eiθ for some real θ, so f(z)=eiθz on D.

F4step 2.1step 4.1casesalgebra
6.1

Conversely, for f(z)=eiθz one has f(z)=z for all z and f(0)=eiθ=1.

step 5.1algebra

Depends on

Used by

Dependency tree · two levels

18 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