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

✓ 12 results · all verified · 5 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Contour Integration — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-16Open item page →

An exponential contour integral approximated by Riemann sums and evaluated by parametrization and a primitive

Example

Let w=2+iπ/4 and γ(t)=tw for 0≤t≤1. Then ∫γexp⁡z dz=exp⁡(2+iπ/4)−1. The integral is obtained both as the limit of midpoint sums and from parametrization or a primitive.

Facts & Assumptions

Given: The segment γ(t)=tw and the integrand exp⁡z.

[L1]

The rectifiable complex integral is defined by componentwise Riemann–Stieltjes integrals (The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral).

[L2]

On a piecewise-C1 contour it agrees with the parametric integral ∫f(γ(t))γ′(t) dt (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).

[L3]

The complex exponential is entire and has derivative itself (The complex exponential is entire and its complex derivative is itself).

[L4]

Let F be a primitive of a continuous function f on an open set containing the trace of a rectifiable contour γ:[a,b]→C. If F′=f is continuous, then ∫γf(z) dz=F(γ(b))−F(γ(a)) (The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path).

Verification

technique · direct
1.1L1

The midpoint sum for the uniform N-partition is SN=∑j=0N−1exp⁡((j+1/2)w/N) w/N; by [L1] these sums converge componentwise to the contour integral.

1.2L2L3algebra

By [L2], the same limit is ∫01exp⁡(tw)w dt. Since (exp⁡(tw))′=wexp⁡(tw) by [L3], this equals exp⁡w−1.

2.1step 1.2L3L4∎

Alternatively, [L3] makes exp⁡ its own primitive on all of C, and since that derivative is exp⁡ itself it is continuous, so [L4] applies and gives the same endpoint increment exp⁡w−exp⁡0 directly.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Integrating a complex polynomial along a segment and a parabola by a primitive and by parametrization

Example

First, ∫01(t−i)3 dt=−5/4. Next let σ(t)=t and ρ(t)=t+it(1−t) for 0≤t≤1. Both go from 0 to 1, and ∫σz dz=∫ρz dz=12.

Facts & Assumptions

Given: The paths and polynomial integrands in the Example.

[L2]

Let F be a primitive of a continuous function f on an open set containing the trace of a rectifiable contour γ:[a,b]→C. If F′=f is continuous, then ∫γf(z) dz=F(γ(b))−F(γ(a)) (The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path).

Verification

technique · direct
1.1L1L2algebra

By [L1] the polynomial (z−i)3 is entire, hence continuous, and (z−i)4/4 is a primitive of it whose derivative is that same continuous polynomial; so the hypotheses of [L2] hold and [L2] gives ((1−i)4−(−i)4)/4=(−4−1)/4=−5/4.

1.2L1L2

By [L1] the polynomial z is entire with continuous derivative and has primitive z2/2, again meeting the hypotheses of [L2]; both σ and ρ have endpoints 0,1, so [L2] gives 1/2 on each.

2.1step 1.2L3algebra∎

Direct substitution into [L3] gives ∫01σ(t)σ′(t)dt and ∫01ρ(t)ρ′(t)dt; each is the endpoint difference of γ(t)2/2, confirming the same values with both orientations explicit.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

The integral of complex conjugation from -1 to 1 differs along a semicircle and a polygonal path

Example

Let γ(t)=ei(π−t) for 0≤t≤π, the upper semicircle from −1 to 1, and let η be the polygonal path −1→2i→1. Then ∫γz‾ dz=−πi,∫ηz‾ dz=−4i.

Facts & Assumptions

Given: The two oriented paths from −1 to 1.

[L2]

Complex line integrals add under concatenation and change sign under reversal (Complex line integrals change sign under reversal and add under concatenation).

Verification

technique · direct
1.1L1algebra

Along γ, γ(t)‾γ′(t)=e−i(π−t)(−i)ei(π−t)=−i, so [L1] integrated from 0 to π gives −πi.

1.2L1algebra

On a segment z(t)=z0+td with 0≤t≤1, direct integration gives ∫z‾ dz=z0‾d+∣d∣2/2. For −1→2i we have z0=−1 and d=1+2i, so ∣d∣2=5 and the value is (−1)(1+2i)+5/2=3/2−2i; for 2i→1 we have z0=2i and d=1−2i, so ∣d∣2=5 and the value is (−2i)(1−2i)+5/2=−3/2−2i.

2.1step 1.1step 1.2L2∎

Add the two segment values by [L2]: (3/2−2i)+(−3/2−2i)=−4i. Since −πi≠−4i, the unequal results prove path dependence.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

ML bounds for rational integrands on a semicircular arc and a line segment

Example

On the upper semicircle ∣z∣=2, ∣∫dz/(z−3)∣≤2π. On the segment from 2 to 2+i, ∣∫dzz2+1∣≤125.

Facts & Assumptions

Given: The two oriented contours and rational integrands in the Example.

[L1]

If ∣f∣≤M on a rectifiable contour, then ∣∫f dz∣≤ML(γ) (ML estimate: a contour integral is bounded by a supremum bound times path length).

[L2]

A piecewise-C1 path has length equal to the sum of its speed integrals (A continuous piecewise-C1 path is rectifiable and its length is the sum of the speed integrals over its pieces).

Verification

technique · direct
1.1L1L2L3

On ∣z∣=2, the reverse triangle inequality from [L3] gives ∣z−3∣≥1, so ∣1/(z−3)∣≤1; [L2] gives semicircle length 2π, and [L1] gives the first bound.

1.2L3algebra

On z=2+it, 0≤t≤1, one has ∣z−i∣≥2 and ∣z+i∣≥5, so [L3] gives ∣1/(z2+1)∣≤1/(25).

2.1step 1.2L1L2∎

The segment length is 1 by [L2], so [L1] gives the second bound. Both contours stay a positive distance from their poles.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-16Open item page →

Direct computation of the integral of 1/(z-a) around a semicircle and a full circle centred at a

Example

For r>0 and γ(t)=a+reit, ∫0≤t≤πdzz−a=iπ,∫0≤t≤2πdzz−a=2πi. Reversing either orientation negates its value.

Facts & Assumptions

Given: The positively oriented semicircle and circle centred at a.

[L1]

The integer-monomial circle theorem gives the full-circle value 2πi for exponent −1 (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).

Verification

technique · direct
1.1algebra

Since dz=ireitdt and z−a=reit, their quotient is the constant i; integration over [0,π] and [0,2π] gives iπ and 2πi.

2.1step 1.1L1L2

The full-circle value agrees with [L1], and [L2] gives the negative values on reversed paths.

3.1given∎

The positive-radius hypothesis ensures that the denominator never vanishes.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-16Open item page →

The unit-circle integral of exp(z)/z is 2 pi i by uniform termwise integration

Example

On the positively oriented unit circle γ, ∫γexp⁡zz dz=2πi.

Facts & Assumptions

Given: The positively oriented unit circle.

[L1]

The complex exponential is the series exp⁡z=∑n≥0zn/n! (The complex exponential by its power series), and this series converges absolutely for every complex z (The complex exponential series converges absolutely for every complex argument).

[L2]

Complex line integrals are linear in the integrand (Complex line integrals are linear in the integrand).

[L3]

Uniform convergence on a fixed contour permits passage of the limit through the line integral (A uniformly convergent sequence of continuous integrands on a fixed contour permits passage of the limit through the complex line integral).

[L4]

On a positive circle, the integral of (z−a)m is 0 for integer m≠−1 and 2πi for m=−1 (On a positively oriented circle about a, the integral of (z-a)^m is zero for every integer m except -1, and is 2 pi i for m=-1).

Verification

technique · direct
1.1L1

On ∣z∣=1, the exponential tail is bounded by the convergent numerical series ∑1/n!, so the partial sums converge uniformly; division by z preserves the bound because ∣z∣=1.

1.2L2L4

By [L2] and [L4], integrating the finite sum ∑n=0Nzn−1/n! gives 2πi from the n=0 term and 0 from every n≥1 term.

2.1step 1.1step 1.2L3∎

Apply [L3] to the uniform convergence in step 1.1 and pass to the limit in step 1.2. The circle excludes z=0, so division is defined.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-16Open item page →

Assembling a keyhole contour from two radial segments and two circular arcs

Example

Let 0<r<R. A keyhole contour about the positive real axis is the concatenation of the upper radial segment r→R, the outer circle once counterclockwise, the lower radial segment R→r, and the inner circle clockwise. For every continuous integrand on the trace, its integral is the signed sum of the four piece integrals.

Facts & Assumptions

Given: Radii 0<r<R and four oriented pieces with matching endpoints.

[L1]

Concatenation and reversal of rectifiable complex contours are defined in Rectifiable complex contours, reversal, concatenation, closedness, and orientation.

[L2]

Complex line integrals add under concatenation and change sign under reversal (Complex line integrals change sign under reversal and add under concatenation).

[L3]

Verification

technique · direct
1.1L1construct

On [0,1], parametrize the pieces by r+(R−r)t, Re2πit, R−(R−r)t, and re2πi(1−t), respectively. Their endpoints match in this order, so [L1] defines a closed concatenation.

2.1step 1.1L2

Repeated application of [L2] gives the total integral as the sum of the four oriented integrals, with the reversed radial and inner-circle orientations carrying their signs.

3.1step 1.1L3∎

By [L3], the piece lengths are R−r, 2πR, R−r, and 2πr. This verifies rectifiability and bookkeeping without evaluating the integral by Cauchy's theorem or choosing a logarithm branch.

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-16Open item page →

The rectifiable Riemann–Stieltjes definition on an explicit polygonal contour with corners

Example

Let γ follow the three segments 0→1→1+i→i, and let f(z)=z. Then the componentwise Riemann–Stieltjes definition gives ∫γz dz=−12, the same value as the piecewise-C1 parametric formula. The corners require no matching derivatives.

Facts & Assumptions

Given: The polygonal contour and affine integrand in the Example.

[L1]

The complex integral is the combination of four real Riemann–Stieltjes integrals (The complex line integral over a rectifiable path as a componentwise Riemann–Stieltjes integral).

Verification

technique · direct
1.1L1algebra

On each affine segment, the four Stieltjes components in [L1] reduce to ordinary integrals against constant coordinate derivatives. Recombination gives ∫01γj(t)γj′(t)dt on that segment.

2.1step 1.1L3algebra

Each segment integral is (z12−z02)/2. Adding the three endpoint increments by [L3] telescopes to (i2−02)/2=−1/2.

3.1step 1.1step 2.1L2∎

Formula [L2] gives the same three parametric integrals. The one-sided derivatives at the two corners need not agree.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

Reversing orientation does not preserve a complex contour integral

Statement refuted

Reversing a contour's orientation preserves every complex contour integral.

Facts & Assumptions

Given: The segment γ from 0 to 1, its reversal, and the constant integrand 1.

[L1]

The integral of a constant c is c times the endpoint displacement (The contour integral of a constant c is c times the endpoint displacement).

[L2]

Reversal negates the complex line integral while preserving the absolute line integral (Complex line integrals change sign under reversal and add under concatenation).

Counterexample

technique · direct
1.1L1algebra

By [L1], ∫γ1 dz=1(1−0)=1, whereas ∫γ−1 dz=1(0−1)=−1.

2.1step 1.1L2∎

The values differ, in agreement with [L2], so reversal does not preserve the oriented complex integral even though it preserves the absolute integral.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-16Open item page →

FALSE: the modulus of a contour integral always equals the absolute line integral

Statement

False claim. For every continuous f and rectifiable contour γ, ∣∫γf(z) dz∣=∫γ∣f(z)∣ ∣dz∣.

Facts & Assumptions

Given: The constant function 1 on a positively oriented circle γ of radius r>0.

[L1]

A constant contour integral is the constant times the endpoint displacement (The contour integral of a constant c is c times the endpoint displacement).

[L2]

The absolute integral of 1 is the contour length (The absolute line integral of the constant function 1 is the length of the path).

[L3]

The correct general relation is the fundamental inequality ∣∫f dz∣≤∫∣f∣ ∣dz∣ (The fundamental inequality: the modulus of the integral is at most the absolute line integral for rectifiable contours).

Refutation

technique · direct
1.1L1

Since the circle is closed, [L1] gives ∫γ1 dz=0.

1.2L2algebra

By [L2], its absolute integral is its positive length 2πr.

2.1step 1.1step 1.2L3∎

Thus equality fails: 0<2πr. The values still satisfy the inequality in [L3].

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

FALSE: contour length depends only on the trace and ignores multiplicity

Statement

False claim. Two contours with the same trace always have the same length.

Facts & Assumptions

Given: A radius r>0, the paths γ(t)=reit and η(t)=re2it for 0≤t≤2π.

[L1]
[L2]

Length is invariant under continuous surjective monotone reparametrization; bijective reparametrization does not add multiple coverings (Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal).

Refutation

technique · direct
1.1algebra

Both traces are the same circle of radius r, but their speeds are r and 2r.

2.1step 1.1L1

By [L1], L(γ)=2πr and L(η)=4πr.

3.1step 2.1L2∎

Since r>0, the lengths differ. This does not contradict [L2], because the double covering is not a bijective reparametrization of the single traversal.

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16Open item page →

FALSE: parametrization independence makes orientation reversal leave every contour integral unchanged

Statement

False claim. Parametrization independence implies that reversing a contour leaves every complex line integral unchanged.

Facts & Assumptions

Given: The segment from 0 to 1, its reversal, and the constant integrand 1.

[L1]

Complex and absolute line integrals are invariant under a strictly increasing continuous reparametrization; decreasing reversal is not in that hypothesis (Complex and absolute line integrals are invariant under increasing continuous reparametrization).

[L2]

The integral of a constant is the constant times the endpoint displacement (The contour integral of a constant c is c times the endpoint displacement).

Refutation

technique · direct
1.1L2algebra

By [L2], the forward segment has integral 1 and the reversed segment has integral −1.

2.1step 1.1L1∎

The values differ. This is consistent with [L1], whose exact hypothesis is increasing reparametrization and therefore does not include orientation reversal.

Sources