Alphabeta Math
PropositionStatement: 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.

Reversal negates and concatenation adds winding numbers

Statement

Reversal. Let γ:[a,b]→C be a closed complex contour and let p∉γ∗. Then the reversal γ−(t)=γ(a+b−t) is a closed complex contour with the same trace, and

n(γ−,p)=−n(γ,p).

Concatenation. Let α,β:[0,1]→C be complex contours with α(1)=β(0). Then α∗β is a complex contour with trace α∗∪β∗, and for every p∉α∗∪β∗

∫α∗βdzz−p=∫αdzz−p+∫βdzz−p.

If moreover α and β are themselves closed, then α∗β is closed and

n(α∗β,p)=n(α,p)+n(β,p).

The hypothesis α(1)=β(0) is what makes the concatenation a contour, and closedness of α∗β is what makes its index defined; the integral identity needs neither α nor β to be closed.

Facts & Assumptions

Given: Closed complex contours where an index is asserted, composable complex contours where a concatenation is asserted, and a point off the traces involved.

[L1]

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

[L2]

For a rectifiable contour γ, ∫γ−f dz=−∫γf dz; for composable rectifiable contours α,β, ∫α∗βf dz=∫αf dz+∫βf dz (Complex line integrals change sign under reversal and add under concatenation).

[L3]

A complex contour is a rectifiable path γ:[a,b]→C; it is closed when γ(a)=γ(b); its reversal is γ−(t)=γ(a+b−t); and for α,β:[0,1]→C with α(1)=β(0) the concatenation is (α∗β)(s)=α(2s) for s≤12 and β(2s−1) for s≥12 (Rectifiable complex contours, reversal, concatenation, closedness, and orientation, Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations).

[L5]

Arc length is additive across a split of the parameter interval, and a path is rectifiable exactly when both restrictions are (Arc length is additive across every subdivision point and decreases under restriction).

[L6]

For a rectifiable contour and a continuous integrand on its trace, the complex line integral exists (Continuous integrands have complex and absolute line integrals along every rectifiable path).

[L7]

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).

Proof

technique · direct
1.1givenL3L4

The map t↦a+b−t is a decreasing continuous bijection of [a,b] onto itself, so by [L3] and [L4] the reversal γ− is a path of the same length as γ, hence rectifiable, and its trace is γ([a,b])=γ∗; it is closed because γ−(a)=γ(b)=γ(a)=γ−(b) by [L3].

1.2givenL3L4L5

By [L3] the concatenation α∗β is continuous on [0,1], its restrictions to [0,12] and [12,1] are monotone reparametrizations of α and β, so both are rectifiable by [L4] and α∗β is rectifiable by [L5]; its trace is α∗∪β∗ by the two-piece formula.

1.3givenL3

If α and β are closed then (α∗β)(0)=α(0)=α(1)=β(0)=β(1)=(α∗β)(1) by [L3], so α∗β is closed.

2.1step 1.1L1L2L6

With p∉γ∗ the function z↦1/(z−p) is continuous on γ∗=(γ−)∗, so all the integrals below exist by [L6]; applying the reversal identity of [L2] to it and dividing by 2πi gives n(γ−,p)=−n(γ,p) through [L1].

2.2step 1.2L2L6

With p∉α∗∪β∗ the function z↦1/(z−p) is continuous on that union, so the concatenation identity of [L2] applies to it and gives the displayed additive formula, all three integrals existing by [L6].

3.1step 1.3step 2.1step 2.2L1L7∎

If α and β are closed, step 1.3 makes α∗β closed, so [L1] turns step 2.2 into n(α∗β,p)=n(α,p)+n(β,p); all three values are integers by [L7], consistently with the identity.

Depends on

Used by

Dependency tree · two levels

30 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