Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-30
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.

Schottky's theorem

Statement

For every R>0 and every 0<r<1 there exists a constant C(R,r)>0 such that every holomorphic map f:DC{0,1} with f(0)R satisfies

f(z)C(R,r)(zr).

Facts & Assumptions

Given: Real numbers R>0 and 0<r<1, and a holomorphic map f:DC{0,1} with f(0)R.

[L1]

The functions f and 1f admit holomorphic logarithms on D (Disc functions omitting 0 and 1 admit holomorphic logarithms for f and 1-f).

[L3]

Bloch's theorem gives an absolute lower bound b:=1/48 for normalized Bloch discs (Bloch's theorem).

Proof

technique · direct
1.1

By [L1], choose h with e2πih=f. Since f omits 1, the function h omits every integer. In particular h and h1 are nowhere zero, so [L2] gives holomorphic u,v on D with u2=h and v2=h1. Then (uv)(u+v)=1, so uv is nowhere zero, and [L2] gives a holomorphic g with eg=uv.

L1L2givenconstruct
2.1

Using [L4] and (uv)(u+v)=1, one gets u+v=eg and hence 2u=eg+eg=2coshg. Therefore u=coshg, h=u2=cosh2g=(1+cosh(2g))/2, and f=e2πih=eπicosh(2g).

L4step 1.1algebra
2.2

Put R0:=max{2,R}. First suppose R01f(0)R0. In step 1.1 choose the logarithm h so that Reh(0)1/2, which is possible because h is determined up to an integer. Since f(0)=e2πImh(0), this also gives Imh(0)(logR0)/(2π) and hence h(0)H(R0) for a fixed bound H(R0). Now u(0)=h(0) and v(0)=h(0)1, so for P(R0):=H(R0)+H(R0)+1 one has u(0)v(0)P(R0). Because (uv)(u+v)=1 and u(0)+v(0)P(R0), one also has u(0)v(0)P(R0)1. Finally choose the logarithm g of uv so that Img(0)π; then Reg(0)logP(R0) and therefore g(0)A(R0):=logP(R0)+π.

step 1.1choosealgebra
3.1

Let αn:=12arcosh(2n+1) for n0, and set E:={±αn+mπi:n0, mZ}{±αn+(m+12)πi:n0, mZ}. If g(z)=ζE, then cosh(2ζ) is an odd integer, so step 2.1 gives f(z)=1, impossible. Hence g(D)E=. The horizontal gaps between consecutive αn are less than 1, and the two vertical translates reduce the vertical gap to π/2, so every open Euclidean disc of radius 2 in C meets E.

step 2.1algebra
4.1

Fix wD and rescale g from the disc D(w,1w) to the unit disc. If g(w)>2/(b(1w)), then [L3] would produce a schlicht disc of radius greater than 2 inside g(D), contradicting step 3.1. Therefore g(w)2/(b(1w)) for every wD.

L3step 3.1assume-contradischarge-contradiction
5.1

If f(0)R01, integrate step 4.1 radially and use step 2.2 to get g(z)A(R0)+(2/b)log ⁣(1/(1r)) for zr. The formula in step 2.1 then bounds f(z) by a constant depending only on R and r. If f(0)<R011/2, apply the same construction to 1f: its center value lies between 1/2 and 3/2, so the preceding case with center parameter 2 uniformly bounds 1f(z) and hence f(z)1+1f(z). Taking the larger of the two bounds gives the required C(R,r).

step 2.1step 4.1step 2.2casesalgebra

Depends on

Used by

Dependency tree · two levels

55 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