TheoremStatement: Literature-sourcedProof: 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.

The fundamental inequality: the modulus of the integral is at most the absolute line integral for rectifiable contours

Statement

For a continuous $f$ on the trace of a rectifiable contour $γ$ , $∣ \int_{γ} f (z) d z ∣ \leq \int_{γ} ∣ f (z) ∣ ∣ d z ∣ .$

Facts & Assumptions

Given: A rectifiable contour $γ$ and a continuous integrand $f$ .

[L1]

Both the complex and absolute line integrals exist (Continuous integrands have complex and absolute line integrals along every rectifiable path).

[L2]

Complex modulus satisfies $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ and $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[L3]

Every chord of a rectifiable path is at most the length of the corresponding subpath (Every endpoint chord is no longer than the arc: $∥ γ (b) - γ (a) ∥_{2} \leq L (γ)$ ).

Proof

technique · direct

1.1

For a tagged partition $P$ , the complex polygonal sum $S_{P} = \sum f (γ (ξ_{j})) (γ (t_{j + 1}) - γ (t_{j}))$ satisfies $∣ S_{P} ∣ \leq \sum ∣ f (γ (ξ_{j})) ∣ ∣ γ (t_{j + 1}) - γ (t_{j}) ∣$ by [L2].

2.1

By [L3], each chord in step 1.1 is at most $s_{γ} (t_{j + 1}) - s_{γ} (t_{j})$ . The resulting tagged arc-length sums converge to the existing absolute line integral from [L1].

step 1.1L1L3

3.1

Letting the mesh tend to $0$ , [L1] identifies the limit of $S_{P}$ with the complex line integral and step 2.1 identifies the majorant limit with the absolute integral, proving the inequality with sharp constant $1$ . The same argument includes a constant contour: every chord and arc-length increment is $0$ , so both sides vanish.

step 1.1step 2.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 52 results over 14 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

L. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 (standard reference, not scraped)