Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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 disc missing p carries a holomorphic logarithm of z−p

Statement

Let D(c,ρ)=B(c,ρ) be an open disc in C with ρ>0 and let p∈C with p∉D(c,ρ). Then there is a holomorphic L:D(c,ρ)→C with

exp⁡(L(z))=z−pfor every z∈D(c,ρ),

and every such L satisfies L′(z)=1/(z−p) there. If L1 and L2 both have this property, then L1−L2 is a constant lying in 2πiZ.

Facts & Assumptions

Given: An open disc D(c,ρ) with ρ>0 and a point p∉D(c,ρ).

[L1]

If D(a,r) is an open disc with r>0 and h:D(a,r)→C is holomorphic and nowhere zero, then there is a holomorphic L:D(a,r)→C with exp⁡(L(z))=h(z) for every z∈D(a,r) (A nonvanishing holomorphic function on a disc has a holomorphic logarithm).

[L2]

If L and h are holomorphic on an open U with exp⁡∘L=h, then h is nowhere zero and L′=h′/h; if U misses p and h(z)=z−p, then L′(z)=1/(z−p) (A holomorphic logarithm is a primitive of the logarithmic derivative).

[L3]

ker⁡(exp⁡)=2πiZ, and exp⁡z=exp⁡w exactly when z−w∈2πiZ (ker⁡(exp⁡)=2πiZ, and exp⁡z=exp⁡w exactly when z−w∈2πiZ).

[L4]

The continuous image of a connected subset is a connected subset (A continuous image of a connected space is connected, and connectedness is a topological property).

[L6]

A path-connected subset of a topological space is a connected subset (Every path-connected space is connected, and every path component lies inside a component); a subset is path-connected when any two of its points are joined by a continuous map from [0,1] with image inside it (Paths, path-connected spaces and path components).

[L7]

A subset U⊆Rm is convex when (1−t)x+ty∈U for all x,y∈U and t∈[0,1] (A convex subset of Rm contains every line segment between two of its points).

[L8]

B(x,r)={y:d(x,y)<r} (Open ball, closed ball and sphere in a metric space).

[L9]

Linear combinations, products and nonvanishing quotients of functions complex differentiable at a point are complex differentiable there; constants have derivative 0 and the identity has derivative 1 (Linearity, product, reciprocal, and quotient rules for complex derivatives).

[L10]

A function complex differentiable at a point is continuous there (Complex differentiability at a point implies continuity there).

[L11]

∣zw∣=∣z∣∣w∣ and ∣z+w∣≤∣z∣+∣w∣ for complex z,w (Conjugation is an involutive real-field automorphism, zz‾=∣z∣2, and modulus is definite, multiplicative, and subadditive).

[L12]

For z=a+bi with a,b real, Im⁡z=b and ∣z∣=a2+b2 (Real and imaginary parts, complex conjugation, and modulus).

[L13]

The integers form an ordered commutative ring, and their canonical image in R is discrete; hence if m<n then m+12 lies strictly between them and is not an integer (The integers form a commutative ring, The integers form a totally ordered ring, Integer part: for every real x there is exactly one integer m with m≤x<m+1).

Proof

technique · direct
1.1givenL1L2L9

The function h(z)=z−p is holomorphic on D(c,ρ) by [L9], and it is nowhere zero there because p∉D(c,ρ); so [L1] supplies a holomorphic L on D(c,ρ) with exp⁡∘L=h, and [L2] gives L′(z)=1/(z−p) for every such L.

1.2L6L7L8L11

D(c,ρ) is convex in the sense of [L7]: for z,w in it and t∈[0,1], [L8] and [L11] give ∣(1−t)z+tw−c∣=∣(1−t)(z−c)+t(w−c)∣≤(1−t)∣z−c∣+t∣w−c∣<ρ. Hence any two of its points are joined by the continuous map t↦(1−t)z+tw of [0,1] into it, so D(c,ρ) is path-connected and therefore a connected subset of C by [L6].

2.1step 1.1L3L9L10L12

Let L1,L2 both be holomorphic on D(c,ρ) with exp⁡∘Lj=h. Then exp⁡(L1(z))=exp⁡(L2(z)) for every z, so L1(z)−L2(z)∈2πiZ by [L3]; in particular Re⁡(L1−L2)=0 and the function g:=Im⁡(L1−L2)/(2π) takes values in Z. By [L9] and [L10] the difference L1−L2 is continuous, and ∣Im⁡v∣≤∣v∣ by [L12], so g is a continuous real-valued function on D(c,ρ).

3.1step 1.2step 2.1L4L5L13∎

By step 1.2 and [L4] the image g[D(c,ρ)] is a connected subset of R, hence order-convex by [L5]; if it contained two distinct integers m<n it would contain m+12, which is not an integer, contradicting step 2.1 and [L13]. So g is constant, and L1−L2 is the constant 2πig∈2πiZ.

Depends on

Used by

Dependency tree · two levels

93 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