ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 planar divergence theorem on a rectangle, checked against a direct boundary computation

Example

Let $D = [0, 1]^{2}$ and let $F (x, y) = (x^{2}, x y)$ . Then the flux form of Green's theorem gives $\int_{\partial D} (- F_{y}) d x + F_{x} d y = \iint_{D} (\partial_{x} F_{x} + \partial_{y} F_{y}) d A = \frac{3}{2},$ and the boundary integral can be checked directly edge by edge. On the same field, the circulation form gives $\int_{\partial D} F \cdot d r = \frac{1}{2} .$

Facts & Assumptions

Given: The unit square $D = [0, 1]^{2}$ with its positive boundary chain and the field $F (x, y) = (x^{2}, x y)$ .

[L1]

For a positively oriented finite elementary Green region and a $C^{1}$ planar field on an open neighbourhood of it, the flux form of Green's theorem is $\int_{\partial D} (- F_{y}) d x + F_{x} d y = \iint_{D} (\partial_{x} F_{x} + \partial_{y} F_{y}) d A$ (The planar divergence theorem: the flux form of Green's theorem).

[L2]

The circulation form of Green's theorem identifies $\int_{\partial D} F \cdot d r$ with the area integral of the third coordinate of the curl of the lifted field (Green's theorem is the curl statement for a planar field lifted to $R^{3}$ ).

[F1]

The unit square is an elementary Green region (Type I, Type II, and elementary regions for Green's theorem).

[F2]

Its positive boundary traverses the lower edge left to right, the right edge upward, the upper edge right to left, and the left edge downward (Positive orientation of elementary-region boundaries).

[F3]

Vector line integrals are computed from $⟨ F (γ (t)), γ^{'} (t) ⟩$ (Scalar line integrals with respect to arc length and vector-field line integrals).

[F4]

The planar divergence is $\partial_{x} F_{x} + \partial_{y} F_{y}$ (Divergence and curl of a $C^{1}$ vector field).

[L3]

Jordan Fubini computes a multiple integral by iterated section integrals (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

[L4]

If $a < b$ , $G$ is differentiable on $[a, b]$ , and $G^{'} = f$ is integrable there, then $\int_{a}^{b} f = G (b) - G (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[F5]

$⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Verification

technique · direct

1.1

The square $D$ is an elementary Green region by [F1], [F2] fixes the four directed edges of its positive boundary chain, and the polynomial field $F$ is $C^{1}$ on the open neighbourhood $R^{2}$ of $D$ .

F1F2given

2.1

Here $\partial_{x} F_{x} = 2 x$ and $\partial_{y} F_{y} = x$ , so [F4], [L3], and [L4] give $\iint_{D} (\partial_{x} F_{x} + \partial_{y} F_{y}) d A = \int_{0}^{1} \int_{0}^{1} 3 x d y d x = 3 / 2$ .

step 1.1F4L3L4

2.2

On the bottom edge $γ_{1} (t) = (t, 0)$ , $0 \leq t \leq 1$ , one has $d x = d t$ , $d y = 0$ , and $- F_{y} (γ_{1} (t)) = 0$ , so the flux-form integrand vanishes and this edge contributes $0$ .

step 1.1F2F3F5

2.3

On the right edge $γ_{2} (t) = (1, t)$ , $0 \leq t \leq 1$ , one has $d x = 0$ , $d y = d t$ , and $F_{x} (γ_{2} (t)) = 1$ , so the contribution is $1$ .

step 1.1F2F3F5

2.4

On the top edge $γ_{3} (t) = (1 - t, 1)$ , $0 \leq t \leq 1$ , one has $d x = - d t$ , $d y = 0$ , and $- F_{y} (γ_{3} (t)) = - (1 - t)$ , so the contribution is $\int_{0}^{1} (1 - t) d t = 1 / 2$ by [L4].

step 1.1F2F3F5L4

2.5

On the left edge $γ_{4} (t) = (0, 1 - t)$ , $0 \leq t \leq 1$ , one has $d x = 0$ , $d y = - d t$ , and $F_{x} (γ_{4} (t)) = 0$ , so the contribution is $0$ .

step 1.1F2F3F5

2.6

For the circulation form, $\int_{\partial D} F \cdot d r$ has edge contributions $1 / 3$ , $1 / 2$ , $- 1 / 3$ , and $0$ , so it equals $1 / 2$ ; the lifted field has curl third coordinate $y$ , and [L3], [L4], and [L2] give $\iint_{D} y d A = 1 / 2$ as well.

step 1.1L2F3L3L4

3.1

Steps 2.1, 2.2, 2.3, 2.4, and 2.5 give $0 + 1 + 1 / 2 + 0 = 3 / 2$ , agreeing with [L1].

step 2.1step 2.2step 2.3step 2.4step 2.5L1

4.1

On each directed edge, rotating the unit tangent clockwise gives the outward unit normal of the square, by the positive-orientation convention of [F2].

step 3.1F2F5∎

Remarks

The two zero edge contributions in steps 2.2 and 2.5 are computed, not inferred from symmetry. They vanish for two different reasons: $F_{y} = 0$ on the bottom edge and $F_{x} = 0$ on the left edge.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

47 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

J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus, Example 4.3.4 (standard reference, not scraped)