Alphabeta Math
CorollaryStatement: 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 the increment of a continuous argument divided by 2π

Statement

Let γ:[a,b]C be a closed complex contour, let pγ, let λ be a continuous logarithm of γp along γ and let θ=Imλ be the associated continuous argument (Continuous logarithms and continuous arguments along a contour). Then

Reλ(t)=logγ(t)p(atb),n(γ,p)=θ(b)θ(a)2π.

In particular θ(b)θ(a) is an integer multiple of 2π, and it is the same for every continuous argument of γp along γ.

Facts & Assumptions

Given: A closed complex contour γ:[a,b]C, a point pγ, a continuous logarithm λ of γp along γ, and θ=Imλ.

[L1]

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

[L2]

A continuous logarithm of γp along γ is a continuous λ with exp(λ(t))=γ(t)p for every t, its continuous argument is θ=Imλ, and any two continuous logarithms differ by a constant in 2πiZ (Continuous logarithms and continuous arguments along a contour, Every contour missing a point admits a continuous logarithm, unique up to a constant in 2πiZ).

[L4]

For a complex contour γ, pγ and a continuous logarithm λ of γp along γ, γdz/(zp)=λ(b)λ(a) (The integral of dz/(zp) along a contour is the increment of a continuous logarithm).

[L5]

For x>0, logx is the unique real y with expy=x (The natural logarithm as the inverse of the exponential function).

[L6]

For z=a+bi with a,b real, Rez=a and Imz=b (Real and imaginary parts, complex conjugation, and modulus).

[L7]

A complex contour is closed when γ(a)=γ(b) (Rectifiable complex contours, reversal, concatenation, closedness, and orientation).

[L8]

The integers form a commutative ring (The integers form a commutative ring).

Proof

technique · direct
1.1

Writing λ(t)=Reλ(t)+iθ(t) as in [L6], the identity exp(λ(t))=γ(t)p of [L2] and the modulus formula [L3] give γ(t)p=eReλ(t), so Reλ(t)=logγ(t)p by [L5].

givenL2L3L5L6
1.2

Since γ is closed, γ(b)=γ(a) by [L7], so γ(b)p=γ(a)p.

givenL7
2.1

Steps 1.1 and 1.2 give Reλ(b)=Reλ(a), hence λ(b)λ(a)=i(θ(b)θ(a)) by [L6].

step 1.1step 1.2L6
3.1

By [L1] and [L4], 2πin(γ,p)=λ(b)λ(a), which step 2.1 rewrites as i(θ(b)θ(a)); dividing by 2πi gives n(γ,p)=(θ(b)θ(a))/(2π).

step 2.1L1L4
4.1

Since n(γ,p) is an integer by [L1] and [L8], step 3.1 makes θ(b)θ(a)=2πn(γ,p) an integer multiple of 2π; and replacing λ by another continuous logarithm changes it by a constant of 2πiZ by [L2], which cancels in the increment, so the value is the same for every continuous argument.

step 3.1L1L2L8

Depends on

Used by

Dependency tree · two levels

62 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