Alphabeta Math
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 Ω⊆C be a complex domain, let a0∈Ω, and let ξ0 be a holomorphic germ at a0. Assume that ξ0 admits analytic continuation along every path in Ω starting at a0.

If α,β:[0,1]→Ω satisfy α(0)=β(0)=a0, 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 a0∈Ω, a germ ξ0 at a0, paths α,β starting at a0, and an endpoint-fixed path homotopy H:[0,1]×[0,1]→Ω 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]×[0,1]→Ω whose slices αt(s):=H(s,t) all start at a0 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.1givenL2

For t∈[0,1], write αt(s):=H(s,t). By [L2], each αt is a path from a0 to the common endpoint, so continuation of ξ0 along αt exists by hypothesis.

1.2

Fix t0∈[0,1] and choose an admissible continuation chain (fj,Uj) over a subdivision 0=s0<⋯<sm=1 for αt0. For each j<m, the compact set αt0([sj,sj+1]) lies in the open set Uj. Continuity of H therefore gives εj>0 such that

H([sj,sj+1]×((t0−εj,t0+εj)∩[0,1]))⊆Uj.

For each j<m−1, admissibility gives equality of the germs of fj and fj+1 at αt0(sj+1), so there is an open neighbourhood Wj⊆Uj∩Uj+1 of that point on which fj=fj+1. Continuity of H at (sj+1,t0) therefore gives ηj>0 such that H({sj+1}×((t0−ηj,t0+ηj)∩[0,1]))⊆Wj. Taking the minimum of the finitely many εj and ηj produces ε>0 with all of these properties. [step 1.1, choose]

2.1L1step 1.2

For every t with ∣t−t0∣<ε, step 1.2 keeps the subpath αt([sj,sj+1]) inside Uj for every j<m. It also keeps each joining point αt(sj+1) inside Wj, where fj=fj+1. So the same function elements (fj,Uj) 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 t0.

3.1step 2.1given∎

Step 2.1 shows that the terminal germ depends locally constantly on t∈[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.

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