ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-16

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.

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

Example

Let $w = 2 + i π / 4$ and $γ (t) = t w$ for $0 \leq t \leq 1$ . Then $\int_{γ} \exp z d z = \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) = t w$ 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- $C^{1}$ contour it agrees with the parametric integral $\int f (γ (t)) γ^{'} (t) d t$ (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] \to C$ . If $F^{'} = f$ is continuous, then $\int_{γ} f (z) d z = 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 $S_{N} = \sum_{j = 0}^{N - 1} \exp ((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 $\int_{0}^{1} \exp (t w) w d t$ . Since $(\exp (t w))^{'} = w \exp (t w)$ 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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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

R. Howell and J. Mathews, Complex Analysis, §§6.1–6.2 (standard reference, not scraped)