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

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+bt) 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αβ

αβdzzp=αdzzp+βdzzp.

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/(zp) (The winding number of a closed contour about a point off its trace).

[L2]

For a rectifiable contour γ, γfdz=γfdz; for composable rectifiable contours α,β, αβfdz=αfdz+βfdz (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+bt); and for α,β:[0,1]C with α(1)=β(0) the concatenation is (αβ)(s)=α(2s) for s12 and β(2s1) for s12 (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.1

The map ta+bt 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].

givenL3L4
1.2

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.

givenL3L4L5
1.3

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

givenL3
2.1

With pγ the function z1/(zp) 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].

step 1.1L1L2L6
2.2

With pαβ the function z1/(zp) 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].

step 1.2L2L6
3.1

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.

step 1.3step 2.1step 2.2L1L7

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