Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck 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)=log2+2πi.

The contour is not closed: γ(0)=1 and γ(1)=2. So no winding number is defined for it, and the increment log2+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/(zp)=λ(b)λ(a) (The integral of dz/(zp) along a contour is the increment of a continuous logarithm).

[L4]

For x>0, logx is the unique real y with expy=x (The natural logarithm as the inverse of the exponential function); the natural logarithm is continuous and strictly increasing on (0,), and log1=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)=expzexpw (exp(z+w)=expzexpw, and the complex exponential extends the real exponential), and for real x,y, exp(x+iy)=ex(cosy+isiny) with exp(x+iy)=ex; in particular exp(2πi)=1 (exp(x+iy)=ex(cosy+isiny), 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, Imz=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.1

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+t1 by [L6], so 0 does not lie on the trace.

givenL5L6L8
1.2

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

givenL1L4L6L7
2.1

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

step 1.1step 1.2L2L3L4
3.1

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, log2+2πi is not an element of 2πiZ because log20 by [L4].

step 2.1L4L5L6

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