LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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 Type I boundary identity for the P dx term

Statement

Let

$D = {(x, y) : a \leq x \leq b, α (x) \leq y \leq β (x)}$

be a Type I region, and let $P$ be $C^{1}$ on an open neighbourhood of $D$ . With the positive boundary orientation,

$\int_{\partial D} P d x = - \iint_{D} \partial_{y} P d A .$

Facts & Assumptions

Given: The region, function, and orientation in the Statement.

[L1]

The positive Type I boundary traverses the lower graph from left to right, the right endpoint arc upward, the upper graph from right to left, and the left endpoint arc downward, omitting zero-length arcs (Positive orientation of elementary-region boundaries).

[L2]

The line integral $\int P d x$ is the vector line integral of $(P, 0)$ , computed piece by piece; reversal negates it and concatenation adds it (Scalar line integrals with respect to arc length and vector-field line integrals, Line integrals under reversal and concatenation).

[L3]

For continuous $H$ on a graph-bounded region, $\iint_{D} H d A = \int_{a}^{b} \int_{α (x)}^{β (x)} H (x, y) d y d x$ (A region between two continuous graphs is Jordan measurable, and a continuous integrand extending to its closure integrates by vertical sections).

[L4]

A continuous function whose interior derivative admits an integrable extension satisfies Newton-Leibniz: that extension integrates to the endpoint increment (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

Proof

technique · direct

1.1

The endpoint arcs in [L1] have constant $x$ , so their contributions to $\int P d x$ are zero. The lower graph contributes $\int_{a}^{b} P (x, α (x)) d x$ , while [L2] makes the reversed upper graph contribute $- \int_{a}^{b} P (x, β (x)) d x$ .

givenL1L2algebra

1.2

For each fixed $x$ with $α (x) < β (x)$ , [L4] applied in the $y$ variable gives $P (x, β (x)) - P (x, α (x)) = \int_{α (x)}^{β (x)} \partial_{y} P (x, y) d y .$ Since $α < β$ on $(a, b)$ , this covers every interior $x$ . At $x = a$ and $x = b$ the region definition requires only $α (x) \leq β (x)$ , so both cases occur: where $α (x) < β (x)$ , as for a rectangle, the same application of [L4] applies verbatim, and where $α (x) = β (x)$ both sides are zero. Hence the displayed identity holds for every $x \in [a, b]$ .

givenL4

2.1

Therefore $\int_{\partial D} P d x = - \int_{a}^{b} (P (x, β (x)) - P (x, α (x))) d x .$

step 1.1algebra

3.1

Substitute step 1.2 into step 2.1 and apply [L3] to obtain the asserted identity.

step 2.1step 1.2L3

4.1

If an endpoint arc has zero length, [L1] omits it and its would-be contribution is already zero. Piecewise- $C^{1}$ breakpoints merely subdivide the graph integrals, so [L2] keeps the calculation unchanged.

L1L2step 1.1∎

Depends on

Used by

Green's theorem for finite unions of elementary regions Theorem

Dependency tree · next 3 levels

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

J. Lebl, Basic Analysis II, section 10.6 (standard reference, not scraped)