Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 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.

The integral of dz/(z−p) along a contour is the increment of a continuous logarithm

Statement

Let γ:[a,b]→C be a complex contour, let p∈C with p∉γ∗, and let λ be a continuous logarithm of γ−p along γ (Continuous logarithms and continuous arguments along a contour). Then

∫γdzz−p=λ(b)−λ(a).

The contour need not be closed, and the right-hand side is the same for every continuous logarithm of γ−p along γ.

Facts & Assumptions

Given: A complex contour γ:[a,b]→C, a point p∉γ∗, and a continuous logarithm λ of γ−p along γ.

[L1]

A continuous logarithm of γ−p along γ is a continuous λ:[a,b]→C with exp⁡(λ(t))=γ(t)−p for every t (Continuous logarithms and continuous arguments along a contour).

[L2]

For a complex contour γ and p∉γ∗ there is a continuous logarithm of γ−p along γ, and any two of them differ by a constant lying in 2πiZ (Every contour missing a point admits a continuous logarithm, unique up to a constant in 2πiZ).

[L3]

For a complex contour γ and p∉γ∗, the distance d=inf⁡{∣w−p∣:w∈γ∗} is positive and some partition a=t0<⋯<tr=b satisfies γ([ti,ti+1])⊆D(γ(ti),d) and p∉D(γ(ti),d) for every i<r (A contour missing a point subdivides into arcs lying in discs that miss it).

[L4]

If D(c,ρ) is an open disc with ρ>0 and p∉D(c,ρ), there is a holomorphic L on D(c,ρ) with exp⁡(L(z))=z−p there, and every such L satisfies L′(z)=1/(z−p) (A disc missing p carries a holomorphic logarithm of z−p).

[L5]

If F is a primitive of a continuous f on an open set containing the trace of a rectifiable contour γ:[a,b]→C and F′=f is continuous, then ∫γf(z) dz=F(γ(b))−F(γ(a)) (The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path, A primitive of a complex function on an open set).

[L6]

If ϕ:[c,d]→[a,b] is a strictly increasing continuous bijection and f is continuous on the trace of the rectifiable γ, then ∫γ∘ϕf dz=∫γf dz (Complex and absolute line integrals are invariant under increasing continuous reparametrization).

[L7]

For composable rectifiable contours α,β, ∫α∗βf dz=∫αf dz+∫βf dz (Complex line integrals change sign under reversal and add under concatenation); concatenation of α,β:[0,1]→C with α(1)=β(0) is (α∗β)(s)=α(2s) for s≤12 and β(2s−1) for s≥12 (Rectifiable complex contours, reversal, concatenation, closedness, and orientation, Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations).

[L8]

For a rectifiable γ and f continuous on its trace, ∫γf dz exists (Continuous integrands have complex and absolute line integrals along every rectifiable path).

[L9]

Arc length is additive across a split of the parameter interval, and γ is rectifiable exactly when both restrictions are (Arc length is additive across every subdivision point and decreases under restriction).

[L10]

ker⁡(exp⁡)=2πiZ, and exp⁡z=exp⁡w exactly when z−w∈2πiZ (ker⁡(exp⁡)=2πiZ, and exp⁡z=exp⁡w exactly when z−w∈2πiZ).

[L12]

If a property holds at 0 and passes from n to n+1, it holds for every natural number (The principle of mathematical induction).

[L14]
[L15]

For z=a+bi with a,b real, Im⁡z=b and ∣z∣=a2+b2 (Real and imaginary parts, complex conjugation, and modulus).

[L16]

The integers form an ordered commutative ring, and their canonical image in R is discrete; hence if m<n then m+12 lies strictly between them and is not an integer (The integers form a commutative ring, The integers form a totally ordered ring, Integer part: for every real x there is exactly one integer m with m≤x<m+1).

[L17]

Nonvanishing quotients of functions complex differentiable at a point are complex differentiable there (Linearity, product, reciprocal, and quotient rules for complex derivatives).

Proof

technique · direct
1.1givenL8L14L17

The function z↦1/(z−p) is defined and continuous on γ∗ by [L14] and [L17], since p∉γ∗, so the integral ∫γdz/(z−p) exists by [L8].

1.2L2

By [L2] any two continuous logarithms of γ−p along γ differ by a constant, so the increment λ(b)−λ(a) is the same for all of them.

1.3givenL3L4L9

Assume a<b. By [L3] fix d>0 and a partition a=t0<⋯<tr=b with γ([ti,ti+1])⊆Di:=D(γ(ti),d) and p∉Di for i<r, and by [L4] fix a holomorphic Li on Di with exp⁡(Li(z))=z−p and Li′(z)=1/(z−p) there. By [L9] each restriction γi:=γ∣[ti,ti+1] is rectifiable.

2.1givenstep 1.3L1L10L11L14L15L16

Fix i<r. For t∈[ti,ti+1] both exp⁡(λ(t)) and exp⁡(Li(γ(t))) equal γ(t)−p, so λ(t)−Li(γ(t))∈2πiZ by [L10]; that difference is continuous by [L14], its scaled imaginary part is a continuous integer-valued real function by [L15], and [L11] with [L16] forces it to be constant on the interval. Hence λ(ti+1)−λ(ti)=Li(γ(ti+1))−Li(γ(ti)).

2.2step 1.3L4L5L14L17

Fix i<r. The trace of γi lies in the open disc Di, on which Li is a primitive of the continuous function 1/(z−p), so [L5] gives ∫γidz/(z−p)=Li(γ(ti+1))−Li(γ(ti)).

2.3step 1.1step 1.3L6L7L12

For a≤u<v<w≤b the increasing affine reparametrisations α(s)=γ(u+s(v−u)) and β(s)=γ(v+s(w−v)) of [0,1] satisfy α(1)=β(0) and α∗β=γ∣[u,w]∘ϕ for the strictly increasing continuous bijection ϕ:[0,1]→[u,w] that is affine on [0,12] and on [12,1] with ϕ(12)=v, so [L6] and [L7] split the integral at v; applying this at t1, then to γ∣[t1,b] at t2, and so on, an induction on the number of partition points ([L12]) gives ∫γdz/(z−p)=∑i<r∫γidz/(z−p).

3.1step 2.1step 2.2step 2.3algebra

Substituting step 2.2 into step 2.3 and then step 2.1, the integral equals ∑i<r(λ(ti+1)−λ(ti)). Expanding this finite sum, every intermediate value λ(ti) with 0<i<r appears once with sign + and once with sign −, so the sum telescopes to λ(tr)−λ(t0)=λ(b)−λ(a).

4.1step 1.2L4L5∎

If instead a=b, choose ρ>0 with p∉D(γ(a),ρ); [L4] gives a holomorphic L on that disc with L′(z)=1/(z−p). The trace of the constant contour γ lies in that disc, so [L5] gives ∫γdz/(z−p)=L(γ(a))−L(γ(a))=0, while λ(b)−λ(a)=0. Thus the identity also holds when a=b; and by step 1.2 the value asserted is independent of which continuous logarithm is used.

Depends on

Used by

Dependency tree · two levels

129 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