Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Cauchy's theorem for a null-homologous cycle

Statement

Let ΩC be open, let f:ΩC be holomorphic, and let Γ be a complex chain which is a cycle, with trace in Ω and null-homologous in Ω. Then

Γf(z)dz=0.

Facts & Assumptions

Given: An open Ω, a holomorphic f:ΩC, and a cycle Γ with ΓΩ which is null-homologous in Ω; the plane is read as R2 through C=R[x]/(x2+1) as the Euclidean plane and as a normed real algebra: what the identification preserves.

[L1]

Under the hypotheses above, n(Γ,z)f(z)=(2πi)1Γf(ζ)(ζz)1dζ for every zΩΓ (Cauchy's integral formula for a null-homologous cycle).

[L2]

Products of functions complex differentiable at a point are complex differentiable there, and constants have derivative 0 (Linearity, product, reciprocal, and quotient rules for complex derivatives); a complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

[L3]

Γfdz=k<r,mk0mkγkfdz, and n(Γ,z)=(2πi)1Γdζ/(ζz) for zΓ (Integration over a complex chain and the index of a chain); a chain is a finite list of integer-weighted complex contours and its trace is the union of the γk with mk0 (Complex chains, their traces, and cycles).

[L4]

A cycle Γ with trace in Ω is null-homologous in Ω when n(Γ,p)=0 for every pCΩ (Null-homologous cycles and homologous cycles in an open set).

[L5]

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

[L8]

For n1, Rn is polygonally connected and connected (Rn is polygonally connected, connected, locally path-connected and locally connected).

Proof

technique · direct
1.1

If Ω= then Γ=, so by [L3] every mk is zero or the list is empty and Γfdz=0; assume from now on that Ω.

givenL3
1.2

The trace Γ is a finite union of continuous images of compact intervals by [L3], hence compact by [L6], and therefore closed and bounded by [L6].

givenL3L6
2.1

There is a point zΩΓ. Indeed ΓΩ, so ΩΓ= would force Ω=Γ; by step 1.2 that set is closed, and Ω is open, so Ω would be a nonempty clopen subset of C which is bounded by step 1.2 and [L9], hence different from C. That contradicts [L7] and [L8], since C is connected and its only clopen subsets are and C. The trace is not asserted to have empty interior anywhere in this argument.

step 1.1step 1.2L7L8L9
3.1

Fix such a z and put F(ζ)=(ζz)f(ζ) for ζΩ, which is holomorphic on Ω by [L2] and satisfies F(z)=0. Since Γ is null-homologous in Ω by the hypothesis and [L4], [L1] applies to F at the point z and gives 0=n(Γ,z)F(z)=(2πi)1ΓF(ζ)(ζz)1dζ.

step 2.1L1L2L4
4.1

On the trace ζz, so F(ζ)(ζz)1=f(ζ) there, and the integrand of step 3.1 is f itself; hence Γf(ζ)dζ=0 by [L3] and [L5].

step 3.1L3L5

Depends on

Used by

Dependency tree · two levels

94 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