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

The winding number is constant on each connected component of the complement of the trace

Statement

Let γ be a closed complex contour with trace γ and length L(γ). Then Cγ is open, and the index function pn(γ,p) satisfies the quantitative estimate

n(γ,p)n(γ,p0)  L(γ)pp0πd2whenever p0γ, d=infwγwp0, pp0<d2.

In particular n(γ,) is continuous on Cγ; it is constant on every connected component of that set; and since those components are open, it is locally constant.

Facts & Assumptions

Given: A closed complex contour γ:[a,b]C; the plane carries the Euclidean metric of C=R[x]/(x2+1) as the Euclidean plane and as a normed real algebra: what the identification preserves.

[L1]

For a closed complex contour γ and pγ, n(γ,p)=(2πi)1γdz/(zp) (The winding number of a closed contour about a point off its trace).

[L2]

The winding number of a closed complex contour about a point off its trace is an integer (The winding number of a closed contour is an integer).

[L3]

For a complex contour γ and p0γ, the distance d=inf{wp0:wγ} exists and is positive (A contour missing a point subdivides into arcs lying in discs that miss it).

[L4]

If f(z)M on the trace of a rectifiable contour γ, with M0, then γf(z)dzML(γ) (ML estimate: a contour integral is bounded by a supremum bound times path length).

[L5]

For continuous f,g on the trace of a rectifiable contour γ and α,βC, γ(αf+βg)dz=αγfdz+βγgdz (Complex line integrals are linear in the integrand).

[L6]

The connected component C(x) is the union of all connected subsets containing x, hence the largest connected subset containing x (Connected components, quasicomponents, and totally disconnected spaces).

[L7]

Every connected component of an open subset URn is open in Rn and polygonally connected (Every connected component of an open subset of Rn is open and polygonally connected).

[L11]

zw=zw and z+wz+w for complex z,w (Conjugation is an involutive real-field automorphism, zz=z2, and modulus is definite, multiplicative, and subadditive).

[L12]

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 mx<m+1).

Proof

technique · direct
1.1

The trace γ is the continuous image of a compact interval, hence compact and closed by [L9], so its complement Cγ is open by [L10].

givenL9L10
1.2

Fix p0γ and put d=inf{wp0:wγ}, which is positive by [L3]; let p satisfy pp0<d/2. For zγ one has zp0d and, by [L11], zpzp0pp0>dd2=d2>0, so pγ as well.

givenL3L11
2.1

For zγ, elementary algebra gives 1zp1zp0=pp0(zp)(zp0), whose modulus is at most pp0/(d2d)=2pp0/d2 by step 1.2 and [L11].

step 1.2L11algebra
3.1

By [L1] and [L5] the difference n(γ,p)n(γ,p0) is (2πi)1γ(1zp1zp0)dz, and [L4] with the bound of step 2.1 makes its modulus at most (2π)12pp0L(γ)/d2=L(γ)pp0/(πd2).

step 2.1L1L4L5
4.1

Step 3.1 shows n(γ,) is continuous at every p0γ, since the bound tends to 0 with pp0.

step 3.1L10
5.1

Let C be a connected component of Cγ. By [L2] the function n(γ,) is integer-valued, and by step 4.1 it is continuous, so by [L6] and [L8] its image on C is an order-convex subset of R contained in Z; by [L12] such a set has at most one element, so n(γ,) is constant on C. By [L7] applied to the open set of step 1.1, C is open, so the index is locally constant on Cγ.

step 1.1step 4.1L2L6L7L8L12

Depends on

Used by

Dependency tree · two levels

127 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