TheoremStatement: Literature-sourcedProof: 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.

Every holomorphic function on a homologically simply connected domain has a primitive

Statement

Let $Ω$ be a homologically simply connected complex domain (Homologically simply connected complex domains). Then every holomorphic $f : Ω \to C$ has a primitive on $Ω$ (A primitive of a complex function on an open set): there is a holomorphic $F : Ω \to C$ with $F^{'} = f$ .

Facts & Assumptions

Given: A homologically simply connected complex domain $Ω$ and a holomorphic $f : Ω \to C$ .

[L1]

If $Γ$ is a cycle with trace in an open $Ω$ , null-homologous in $Ω$ , and $f$ is holomorphic on $Ω$ , then $\int_{Γ} f d z = 0$ (Cauchy's theorem for a null-homologous cycle).

[L2]

A complex domain is homologically simply connected when every cycle with trace in it is null-homologous in it (Homologically simply connected complex domains, Null-homologous cycles and homologous cycles in an open set).

[L3]

A list of closed complex contours is a cycle; in particular a single closed contour, taken as the list of length $1$ with coefficient $1$ , is a cycle, and its trace is the trace of that contour (Complex chains, their traces, and cycles).

[L4]

For a chain consisting of the single closed contour $γ$ with coefficient $1$ , $\int_{Γ} f d z = \int_{γ} f d z$ (Integration over a complex chain and the index of a chain).

[L5]

For a complex domain $U$ and a continuous $f : U \to C$ , the following are equivalent: $f$ has a primitive on $U$ ; the integral of $f$ along rectifiable contours in $U$ depends only on the endpoints; the integral of $f$ around every closed rectifiable contour in $U$ is $0$ (For a continuous function on a complex domain, endpoint independence, zero closed-contour integrals, and existence of a primitive are equivalent).

[L6]

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

[L7]

A complex domain is a nonempty, connected, open subset of $C$ (A complex domain is a nonempty connected open subset of $C$ ).

Proof

technique · direct

1.1givenL3

Let $γ$ be a closed rectifiable contour with trace in $Ω$ , and let $Γ$ be the chain consisting of $γ$ with coefficient $1$ . By [L3] that chain is a cycle whose trace is $γ^{*} \subseteq Ω$ .

2.1step 1.1L1L2L4

By [L2] the cycle $Γ$ is null-homologous in $Ω$ , so [L1] gives $\int_{Γ} f d z = 0$ , and [L4] rewrites this as $\int_{γ} f d z = 0$ .

3.1givenstep 2.1L5L6L7∎

The set $Ω$ is a complex domain by [L7] and $f$ is continuous on it by [L6], so [L5] applies; step 2.1 supplies its third condition for every closed rectifiable contour in $Ω$ , and the equivalence therefore yields a primitive $F$ of $f$ on $Ω$ .

Depends on

Used by

Dependency tree · two levels

45 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

L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §4.4 (standard reference, not scraped)
J. Lebl, Complex Analysis, Ch. 4 §4.3 (standard reference, not scraped)