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

The Riemann surface of the logarithm is the complex plane over the punctured plane via exp

Statement

Let Rlog⁡ be the Riemann surface of the complete analytic function generated by the principal logarithm germ at 1 over C×. Define

Λ:Rlog⁡→C,Λ([ℓ]z):=ℓ(z).

Then Λ is a biholomorphism, and if p:Rlog⁡→C× is the germ projection, then

p=exp⁡∘Λ.

So, after identifying Rlog⁡ with C through Λ, the projection is the exponential covering exp⁡:C→C×.

Facts & Assumptions

Given: The logarithm germ surface Rlog⁡ and its projection p.

[L1]

On the principal strip P={w:−π<Im⁡w<π}, the exponential is a biholomorphism onto the slit plane S=C∖(−∞,0], with inverse the principal logarithm (The exponential is the inverse biholomorphism from the principal strip to the slit plane).

[L2]
[L3]

The germ projection on a complete analytic function is a local biholomorphism (The germ projection is a local biholomorphism).

Proof

technique · direct
1.1L1algebra

For each w∈C, let Vw:=ewB(1,1/2) and define ℓw(u):=w+Log⁡(e−wu) for u∈Vw. Because B(1,1/2)⊆S, fact [L1] makes ℓw holomorphic on Vw, with exp⁡(ℓw(u))=eweLog⁡(e−wu)=u and ℓw(ew)=w. Thus Φ(w):=[ℓw]ew is a well-defined logarithm germ over ew.

1.2L1choose

The germ Φ(w) lies on Rlog⁡. Indeed, along the path γw(t)=etw from 1 to ew, choose a subdivision fine enough that for every adjacent pair tj,tj+1 and every t∈[tj,tj+1] one has ∣e(t−tj)w−1∣<12, and also ∣Im⁡((tj+1−tj)w)∣<π. The first condition puts the entire subpath γw([tj,tj+1]) inside Vtjw. At the joining point, the second condition gives ℓtjw(etj+1w)=tjw+Log⁡(e(tj+1−tj)w)=tj+1w, so consecutive branches agree there as germs. Starting at t0=0 gives the principal logarithm germ at 1, and the final germ is Φ(w).

2.1step 1.1algebra

If Φ(w)=Φ(v), then the two germs have the same base point and the same value at that base point. Therefore ew=ev and w=v. So Φ is injective.

2.2L2step 1.1algebra

Let ξ=[ℓ]z be any point of Rlog⁡ and put w:=ℓ(z). Shrink the representative domain of ℓ to a disc U⊆Vw on which ℓ(U)⊆B(w,π). On U one has exp⁡(ℓ(u))=u=exp⁡(ℓw(u)), so [L2] gives ℓ(u)−ℓw(u)∈2πiZ for every u∈U. The difference is continuous, takes the value 0 at z, and its image lies in the discrete set 2πiZ; because U is connected, the difference is identically 0. Hence ξ=Φ(w), and Φ is surjective.

3.1L3step 1.1step 2.1step 2.2

The map Λ is the inverse of Φ by steps 2.1 and 2.2. In a chart N(ℓ,U) on the germ surface one has Λ∘ϕℓ,U−1(u)=ℓ(u), so [L3] makes Λ holomorphic. Near any w0∈C, if ∣w−w0∣<1/4 then Φ(w)∈N(ℓw0,Vw0) and ϕℓw0,Vw0(Φ(w))=ew, which is holomorphic in w; so Φ is holomorphic as well. Therefore Λ is a biholomorphism.

4.1step 3.1algebra∎

For every [ℓ]z∈Rlog⁡ one has p([ℓ]z)=z=exp⁡(ℓ(z))=exp⁡(Λ([ℓ]z)), so p=exp⁡∘Λ.

Depends on

Used by

Dependency tree · two levels

27 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