ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

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

Example

First, $\int_{0}^{1} (t - i)^{3} d t = - 5 / 4$ . Next let $σ (t) = t$ and $ρ (t) = t + i t (1 - t)$ for $0 \leq t \leq 1$ . Both go from $0$ to $1$ , and $\int_{σ} z d z = \int_{ρ} z d z = \frac{1}{2} .$

Facts & Assumptions

Given: The paths and polynomial integrands in the Example.

[L1]

Complex polynomials are entire with the usual derivative formula (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).

[L2]

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

[L3]

Piecewise- $C^{1}$ contour integrals agree with their parametric formulas (For piecewise-C1 contours the Riemann–Stieltjes integral agrees with the parametric complex integral and the published real line integrals).

Verification

technique · direct

1.1

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

L1L2algebra

1.2

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

L1L2

2.1

Direct substitution into [L3] gives $\int_{0}^{1} σ (t) σ^{'} (t) d t$ and $\int_{0}^{1} ρ (t) ρ^{'} (t) d t$ ; each is the endpoint difference of $γ (t)^{2} / 2$ , confirming the same values with both orientations explicit.

step 1.2L3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 130 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

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