ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

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

Example

On the upper semicircle $∣ z ∣ = 2$ , $∣ \int d z / (z - 3) ∣ \leq 2 π$ . On the segment from $2$ to $2 + i$ , $∣ \int \frac{d z}{z^{2} + 1} ∣ \leq \frac{1}{2 \sqrt{5}} .$

Facts & Assumptions

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

[L1]

If $∣ f ∣ \leq M$ on a rectifiable contour, then $∣ \int f d z ∣ \leq M L (γ)$ (ML estimate: a contour integral is bounded by a supremum bound times path length).

[L2]

A piecewise- $C^{1}$ path has length equal to the sum of its speed integrals (A continuous piecewise- $C^{1}$ path is rectifiable and its length is the sum of the speed integrals over its pieces).

[L3]

Complex modulus is multiplicative and obeys the triangle inequality (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

Verification

technique · direct

1.1L1L2L3

On $∣ z ∣ = 2$ , the reverse triangle inequality from [L3] gives $∣ z - 3 ∣ \geq 1$ , so $∣ 1 / (z - 3) ∣ \leq 1$ ; [L2] gives semicircle length $2 π$ , and [L1] gives the first bound.

1.2L3algebra

On $z = 2 + i t$ , $0 \leq t \leq 1$ , one has $∣ z - i ∣ \geq 2$ and $∣ z + i ∣ \geq \sqrt{5}$ , so [L3] gives $∣ 1 / (z^{2} + 1) ∣ \leq 1 / (2 \sqrt{5})$ .

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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.2 (standard reference, not scraped)