Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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.

Cauchy's integral formula on a circle compactly contained in a disc of holomorphy

Statement

Let a∈C, let R>0, and let f be holomorphic on the disc

D(a,R)={ζ∈C:∣ζ−a∣<R}.

If 0<r<R, ∣z−a∣<r, and γ(t)=a+rexp⁡(it) for 0≤t≤2π, then

f(z)=12πi∫γf(ζ)ζ−z dζ.

Facts & Assumptions

Given: A function f holomorphic on D(a,R), a radius 0<r<R, an interior point z with ∣z−a∣<r, and the positively oriented circle γ of radius r about a.

[L1]

The filled difference quotient is continuous on the disc and holomorphic away from its filled point (The filled difference quotient is continuous at its exceptional point and holomorphic away from it).

[L2]

A continuous function holomorphic away from one point on a star-shaped open set has zero integral around every closed rectifiable contour there (A continuous function holomorphic away from one point on a star-shaped domain has a primitive and zero closed-contour integrals).

[L3]

Complex line integrals are linear in the integrand (Complex line integrals are linear in the integrand).

[L4]

On the positively oriented circle about a, the integral of (ζ−a)m is 2πi for m=−1 and zero for every other integer m (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).

[L5]

Uniform convergence on a fixed rectifiable contour permits passage of the limit through the complex line integral (A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral).

Proof

technique · direct
1.1L1

Define g(ζ)=(f(ζ)−f(z))/(ζ−z) for ζ≠z and g(z)=f′(z). By [L1], g is continuous on D(a,R) and holomorphic away from z.

1.2givenL4algebra

If z=a, [L4] gives ∫γ1/(ζ−z) dζ=2πi. If z≠a, the finite identity 1/(ζ−z)=∑k=0N(z−a)k/(ζ−a)k+1+(z−a)N+1/((ζ−a)N+1(ζ−z)) holds on γ, and its remainder has modulus at most (∣z−a∣/r)N+1/(r−∣z−a∣) there.

2.1givenstep 1.1L2

The disc is star-shaped with respect to a, since ∣(1−t)a+tζ−a∣=t∣ζ−a∣<R. The circle lies in the disc and is closed and rectifiable, so [L2] gives ∫γg(ζ) dζ=0.

2.2step 1.2L4L5L6

In the second case, [L6] makes the remainder tend uniformly to zero; [L5] and [L4] then give ∫γ1/(ζ−z) dζ=2πi, because only the k=0 term has exponent −1. Thus the same kernel integral value holds also in the first case.

3.1step 2.1L3algebra

Since ζ≠z on γ, [L3] expands step 2.1 as ∫γf(ζ)/(ζ−z) dζ=f(z)∫γ1/(ζ−z) dζ.

4.1step 3.1step 2.2algebra∎

Substitute step 2.2 into step 3.1 and divide by the nonzero number 2πi to obtain the formula.

Depends on

Used by

Dependency tree · two levels

43 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