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.

Fixed-endpoint homotopic paths give the same analytic continuation

Statement

Let $Ω \subseteq C$ be a complex domain, let $a_{0} \in Ω$ , and let $ξ_{0}$ be a holomorphic germ at $a_{0}$ . Assume that $ξ_{0}$ admits analytic continuation along every path in $Ω$ starting at $a_{0}$ .

If $α, β : [0, 1] \to Ω$ satisfy $α (0) = β (0) = a_{0}$ , have the same terminal point, and are path homotopic relative to the endpoints, then the continuation of $ξ_{0}$ along $α$ and along $β$ has the same terminal germ.

Facts & Assumptions

Given: A complex domain $Ω$ , a base point $a_{0} \in Ω$ , a germ $ξ_{0}$ at $a_{0}$ , paths $α, β$ starting at $a_{0}$ , and an endpoint-fixed path homotopy $H : [0, 1] \times [0, 1] \to Ω$ from $α$ to $β$ .

[L1]

For a fixed path, the terminal germ of continuation is independent of the chosen admissible chain, hence unique (The terminal germ of a continuation along a fixed path is chain-independent, Analytic continuation along a fixed path is unique whenever it exists).

[L2]

A path homotopy relative to the endpoints is a continuous map $H : [0, 1] \times [0, 1] \to Ω$ whose slices $α_{t} (s) : = H (s, t)$ all start at $a_{0}$ and all end at the common endpoint (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

Proof

technique · direct

1.1

For $t \in [0, 1]$ , write $α_{t} (s) : = H (s, t)$ . By [L2], each $α_{t}$ is a path from $a_{0}$ to the common endpoint, so continuation of $ξ_{0}$ along $α_{t}$ exists by hypothesis.

givenL2

1.2

Fix $t_{0} \in [0, 1]$ and choose an admissible continuation chain $(f_{j}, U_{j})$ over a subdivision $0 = s_{0} < \dots < s_{m} = 1$ for $α_{t_{0}}$ . For each $j < m$ , the compact set $α_{t_{0}} ([s_{j}, s_{j + 1}])$ lies in the open set $U_{j}$ . Continuity of $H$ therefore gives $ε_{j} > 0$ such that

$H ([s_{j}, s_{j + 1}] \times ((t_{0} - ε_{j}, t_{0} + ε_{j}) \cap [0, 1])) \subseteq U_{j} .$

For each $j < m - 1$ , admissibility gives equality of the germs of $f_{j}$ and $f_{j + 1}$ at $α_{t_{0}} (s_{j + 1})$ , so there is an open neighbourhood $W_{j} \subseteq U_{j} \cap U_{j + 1}$ of that point on which $f_{j} = f_{j + 1}$ . Continuity of $H$ at $(s_{j + 1}, t_{0})$ therefore gives $η_{j} > 0$ such that $H ({s_{j + 1}} \times ((t_{0} - η_{j}, t_{0} + η_{j}) \cap [0, 1])) \subseteq W_{j} .$ Taking the minimum of the finitely many $ε_{j}$ and $η_{j}$ produces $ε > 0$ with all of these properties. [step 1.1, choose]

2.1

For every $t$ with $∣ t - t_{0} ∣ < ε$ , step 1.2 keeps the subpath $α_{t} ([s_{j}, s_{j + 1}])$ inside $U_{j}$ for every $j < m$ . It also keeps each joining point $α_{t} (s_{j + 1})$ inside $W_{j}$ , where $f_{j} = f_{j + 1}$ . So the same function elements $(f_{j}, U_{j})$ and the same subdivision form an admissible continuation chain for $α_{t}$ . By [L1], the terminal germ of continuation along $α_{t}$ is therefore the terminal germ of this fixed chain, so it is independent of $t$ on that neighbourhood of $t_{0}$ .

L1step 1.2

3.1

Step 2.1 shows that the terminal germ depends locally constantly on $t \in [0, 1]$ . Since $[0, 1]$ is connected, this terminal germ is constant on the whole interval. In particular the terminal germs at $t = 0$ and $t = 1$ , namely the continuations along $α$ and $β$ , are equal.

step 2.1given∎

Depends on

Used by

Dependency tree · two levels

29 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

Lars V. Ahlfors, Complex Analysis, 3rd ed., Ch. 8 §§1.5-1.6 (standard reference, not scraped)
Henry Wilton, Riemann Surfaces lecture notes, §9.2 (standard reference, not scraped)