Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge 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.

Integration over a complex chain and the index of a chain

Definition

Let Γ=∑k<rmkγk be a complex chain (Complex chains, their traces, and cycles) with trace Γ∗, and let f be continuous on Γ∗. The integral of f over Γ is

∫Γf(z) dz:=∑k<rmk≠0mk∫γkf(z) dz,

a finite sum (A finite sum in a commutative monoid indexed by an arbitrary finite set) of the complex line integrals of The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral. Each summand exists: for k with mk≠0 the trace γk∗ is contained in Γ∗, so f is continuous on it, and γk is rectifiable, so Continuous integrands have complex and absolute line integrals along every rectifiable path applies. Terms with mk=0 are omitted, so no integral of f over a contour outside the trace is required. The empty chain, and any chain all of whose coefficients vanish, give ∫Γf dz=0.

For p∈C∖Γ∗, the index of Γ about p is

n(Γ,p):=12πi∫Γdzz−p.

This is defined: z↦1/(z−p) is complex differentiable, hence continuous, on C∖{p}⊇Γ∗ by Linearity, product, reciprocal, and quotient rules for complex derivatives and Complex differentiability at a point implies continuity there.

Remarks

The notation is consistent with the single-contour case. If r=1, m0=1 and γ0 is closed, then Γ∗=γ0∗, the sum has the one term ∫γ0f dz, and n(Γ,p) is the winding number n(γ0,p) of The winding number of a closed contour about a point off its trace for every p∉γ0∗. So writing n for both costs no ambiguity.

Linearity in the integrand is inherited termwise from Complex line integrals are linear in the integrand, finite sums in the additive commutative monoid of C (A finite sum in a commutative monoid indexed by an arbitrary finite set), and distributivity in the complex field (C=R[x]/(x2+1) is a field, every element is uniquely a+bi, and every nonzero element has inverse (a−bi)/(a2+b2)): for f,g continuous on Γ∗ and α,β∈C, ∫Γ(αf+βg) dz=α∫Γf dz+β∫Γg dz.

The index is not defined on the trace. For p∈Γ∗ the integrand is undefined at z=p, and no value is assigned; every statement about n(Γ,⋅) below carries the hypothesis p∉Γ∗.

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