Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 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.

A continuous argument computed along a spiralling contour

Example

Let γ(t)=(1+t)exp⁡(2πit) for t∈[0,1] and let p=0. Then γ is a complex contour with 0∉γ∗, and

λ(t)=log⁡(1+t)+2πit

is a continuous logarithm of γ−0 along γ, with continuous argument θ(t)=2πt increasing by 2π. Consequently

∫γdzz=λ(1)−λ(0)=log⁡2+2πi.

The contour is not closed: γ(0)=1 and γ(1)=2. So no winding number is defined for it, and the increment log⁡2+2πi is not an element of 2πiZ. This is exactly the gap between the logarithm-increment identity, which holds for every contour missing p, and the integrality statement, which needs closedness.

Facts & Assumptions

Given: The contour γ(t)=(1+t)exp⁡(2πit) on [0,1] and the point p=0.

[L1]

A continuous logarithm of γ−p along γ is a continuous λ with exp⁡(λ(t))=γ(t)−p for every t, and its continuous argument is Im⁡λ (Continuous logarithms and continuous arguments along a contour, The complex exponential by its power series).

[L2]

For a complex contour γ and p∉γ∗ there is a continuous logarithm of γ−p along γ, and any two differ by a constant in 2πiZ (Every contour missing a point admits a continuous logarithm, unique up to a constant in 2πiZ).

[L3]

For a complex contour γ:[a,b]→C, a point p∉γ∗ and a continuous logarithm λ of γ−p along γ, ∫γdz/(z−p)=λ(b)−λ(a) (The integral of dz/(z−p) along a contour is the increment of a continuous logarithm).

[L4]

For x>0, log⁡x is the unique real y with exp⁡y=x (The natural logarithm as the inverse of the exponential function); the natural logarithm is continuous and strictly increasing on (0,∞), and log⁡1=0 (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L5]

A complex contour is a rectifiable path, and it is closed when its two endpoint values agree (Rectifiable complex contours, reversal, concatenation, closedness, and orientation); a continuous path differentiable with a continuous derivative on each piece of a partition is rectifiable (A continuous piecewise-C1 path is rectifiable and its length is the sum of the speed integrals over its pieces).

[L6]

exp⁡(z+w)=exp⁡zexp⁡w (exp⁡(z+w)=exp⁡z exp⁡w, and the complex exponential extends the real exponential), and for real x,y, exp⁡(x+iy)=ex(cos⁡y+isin⁡y) with ∣exp⁡(x+iy)∣=ex; in particular exp⁡(2πi)=1 (exp⁡(x+iy)=ex(cos⁡y+isin⁡y), ∣exp⁡(x+iy)∣=ex, and eiπ+1=0, Quarter-turn values and shifts by pi/2 and pi).

[L7]

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

[L8]

cos⁡ and sin⁡ are differentiable with cos⁡′=−sin⁡ and sin⁡′=cos⁡ (The derivatives of sine and cosine are cosine and minus sine).

Verification

technique · direct
1.1givenL5L6L8

Writing γ(t)=(1+t)cos⁡(2πt)+i(1+t)sin⁡(2πt) by [L6], the path is differentiable in t with a continuous derivative by [L8], hence rectifiable by [L5]; and ∣γ(t)∣=(1+t) ∣exp⁡(2πit)∣=1+t≥1 by [L6], so 0 does not lie on the trace.

1.2givenL1L4L6L7

The map λ(t)=log⁡(1+t)+2πit is continuous on [0,1], and by [L4] and [L6], exp⁡(λ(t))=elog⁡(1+t)exp⁡(2πit)=(1+t)exp⁡(2πit)=γ(t)−0; so λ is a continuous logarithm of γ−0 along γ in the sense of [L1], with continuous argument θ(t)=Im⁡λ(t)=2πt by [L7].

2.1step 1.1step 1.2L2L3L4

By [L3] and step 1.2, ∫γdz/z=λ(1)−λ(0)=(log⁡2+2πi)−(log⁡1+0)=log⁡2+2πi using [L4]; and θ(1)−θ(0)=2π. By [L2] the value does not depend on which continuous logarithm is taken.

3.1step 2.1L4L5L6∎

The endpoint values are γ(0)=1 and γ(1)=2exp⁡(2πi)=2 by [L6], so γ is not closed by [L5] and no winding number is defined for it; consistently, log⁡2+2πi is not an element of 2πiZ because log⁡2≠0 by [L4].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

71 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