Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

Holomorphic integrals agree on homologous cycles

Statement

Let Ω⊆C be open, let f:Ω→C be holomorphic, and let Γ0,Γ1 be complex chains which are cycles with traces in Ω and which are homologous in Ω (Null-homologous cycles and homologous cycles in an open set). Then

∫Γ0f(z) dz=∫Γ1f(z) dz.

Facts & Assumptions

Given: An open Ω, a holomorphic f:Ω→C, and cycles Γ0,Γ1 with traces in Ω, homologous in Ω.

[L1]

If Γ is a cycle with trace in an open Ω, null-homologous in Ω, and f is holomorphic on Ω, then ∫Γf dz=0 (Cauchy's theorem for a null-homologous cycle).

[L2]

Two cycles with traces in Ω are homologous in Ω when their difference is null-homologous in Ω (Null-homologous cycles and homologous cycles in an open set).

[L3]

(Γ1+Γ2)∗=Γ1∗∪Γ2∗ and (−Γ)∗=Γ∗; the sum of two cycles and the negative of a cycle are cycles; and for f continuous on the traces involved, ∫Γ1+Γ2f dz=∫Γ1f dz+∫Γ2f dz and ∫−Γf dz=−∫Γf dz (Chain integration and the index are additive in the chain, and reverse with it).

[L4]

∫Γf dz=∑k<r, mk≠0mk∫γkf dz (Integration over a complex chain and the index of a chain), a chain being a finite list of integer-weighted complex contours (Complex chains, their traces, and cycles).

[L5]

A complex differentiable function is continuous (Complex differentiability at a point implies continuity there).

Proof

technique · direct
1.1givenL3L4L5

By [L3] the chain Γ0−Γ1 is a cycle and its trace is Γ0∗∪Γ1∗, which lies in Ω; and f is continuous on that trace by [L5].

1.2givenL2

By [L2] the chain Γ0−Γ1 is null-homologous in Ω, since Γ0 and Γ1 are homologous there.

2.1step 1.1step 1.2L1

Steps 1.1 and 1.2 put Γ0−Γ1 under the hypotheses of [L1], so ∫Γ0−Γ1f dz=0.

3.1step 2.1L3∎

By [L3] the left-hand side of step 2.1 equals ∫Γ0f dz−∫Γ1f dz, so the two integrals agree.

Depends on

Used by

Dependency tree · two levels

38 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