Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24
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 nonvanishing holomorphic function on a disc has a holomorphic logarithm

Statement

If h is nowhere zero and holomorphic on a disc, then there is a holomorphic L on that disc with expL=h.

Precisely, 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 function L:D(a,r)C satisfying exp(L(z))=h(z) for every zD(a,r).

Facts & Assumptions

Given: A disc D(a,r) with r>0 and a nowhere-zero holomorphic function h on it. For z,wD(a,r) and t[0,1] the triangle inequality gives ((1t)z+tw)a(1t)za+twa<r, so every segment between two points of the disc stays in it; taking z=a makes the disc star-shaped with respect to a in the sense of Complex star-shaped and convex domains are the published Euclidean notions under the identification C=R2 and Star-shaped open subsets of Euclidean space, and [L4] makes the disc a connected, hence a complex, domain. Also h is itself holomorphic on the disc, because a holomorphic function has complex derivatives of all orders locally (All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle), so the quotient rule makes h/h holomorphic there, h being nowhere zero (Linearity, product, reciprocal, and quotient rules for complex derivatives); and the complex chain rule, the derivative of exp, and the exponential addition law are supplied by The chain rule for complex derivatives, The complex exponential is entire and its complex derivative is itself, and exp(z+w)=expzexpw, and the complex exponential extends the real exponential.

[L1]

Every holomorphic function on an open set star-shaped with respect to a has a primitive there (Every holomorphic function on a star-shaped domain has a primitive).

[L2]

A holomorphic function whose derivative vanishes everywhere on a complex domain is constant (A holomorphic function with zero derivative on a domain is constant).

[L3]

For every nonzero complex number z, the solutions of expw=z are exactly Logz+2πik with kZ (All logarithms of z0 are Logz+2πik, kZ).

[L4]

A segment t(1t)v0+tv1 that lies in a subset A is a continuous path in A, and a path-connected subset of a topological space is a connected subset (A finite concatenation of straight segments in Rn is a continuous path, Every path-connected space is connected, and every path component lies inside a component, claim 2).

Proof

technique · direct
1.1

By the star-shapedness in the Given and [L1], h/h has a holomorphic primitive K on the disc. Put H(z):=K(z)K(a); then H(a)=0 and H=h/h.

L1givenalgebra
2.1

The complex product and chain rules give (hexp(H))=hexp(H)hHexp(H)=0, so, the disc being a complex domain by [L4], [L2] makes hexp(H) constant; its value at a is h(a).

step 1.1L2L4givenalgebra
3.1

Since h(a)0, choose by [L3] a complex number c with expc=h(a), and set L:=H+c.

step 2.1L3choose
4.1

The exponential addition law and step 2.1 give expL=expHexpc=expHh(a)=h throughout the disc, so L is the required holomorphic logarithm.

step 2.1step 3.1givenalgebra

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