TheoremStatement: Literature-sourcedProof: AI-adapted

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 star-shaped domain has a primitive

Let $U \subseteq C$ be open and star-shaped with respect to $a \in U$ . Every holomorphic function $f : U \to C$ has the primitive

$F (z) = \int_{ℓ_{a z}} f (ζ) d ζ .$

Given: A set $U$ open for $d_{C}$ and star-shaped with respect to $a \in U$ , meaning that $Φ [U]$ is open and star-shaped at $Φ (a)$ in Star-shaped open subsets of Euclidean space. This is equivalent to containment of every segment from $a$ to a point of $U$ , by The complex coordinate isometry transports topology and affine segments. We have and a holomorphic $f : U \to C$ .

[L1]

[L2]

[L3]

Vanishing triangle integrals construct the displayed primitive for a continuous function on a star-shaped domain (Vanishing integrals around triangles construct a primitive for a continuous function on a star-shaped domain).

technique · direct

1.1L1L2

By [L1], $f$ is continuous, and by [L2] its integral around every filled triangle contained in $U$ is zero.

2.1step 1.1L3∎

The hypotheses of [L3] now hold, so the displayed function is holomorphic on $U$ and has derivative $f$ .

Depends on