ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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.

Constructing a potential on a rectangle by coordinate-segment integrals

Example

On an open rectangle $U$ containing $(a, b)$ , let

$F (x, y) = (2 x y + y^{2}, x^{2} + 2 x y) .$

The coordinate-segment construction

$ϕ (x, y) : = \int_{a}^{x} F_{0} (t, b) d t + \int_{b}^{y} F_{1} (x, t) d t$

gives the normalized potential

$ϕ (x, y) = x^{2} y + x y^{2} - a^{2} b - a b^{2} .$

Facts & Assumptions

Given: The rectangle, basepoint, and field in the Example.

[L1]

With coordinates indexed from $0$ , so that $F = (F_{0}, F_{1})$ , a $C^{1}$ field is closed when $\partial_{y} F_{0} = \partial_{x} F_{1}$ , and it is exact when it is the gradient of a $C^{2}$ potential (Exact and closed C1 vector fields).

[L2]

A closed $C^{1}$ field on a star-shaped open domain has the radial potential based at a star centre (Poincare's lemma on a star-shaped domain: every closed C1 field is exact).

[L3]

Two potentials of one field differ by a constant on a piecewise- $C^{1}$ path component (Two potentials of the same field differ by a constant on each piecewise-C1 path component).

[L4]

For a continuous function whose interior derivative admits an integrable extension, Newton-Leibniz evaluates the integral of that extension by the endpoint increment (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

Verification

technique · direct

1.1

Direct differentiation gives $\partial_{y} F_{0} = 2 x + 2 y = \partial_{x} F_{1},$ so $F$ is closed by [L1].

givenL1algebra

1.2

Evaluating the two polynomial integrals using [L4] gives $ϕ (x, y) = b (x^{2} - a^{2}) + b^{2} (x - a) + x^{2} (y - b) + x (y^{2} - b^{2}) = x^{2} y + x y^{2} - a^{2} b - a b^{2} .$

givenL4algebra

2.1

Differentiating step 1.2 yields $\partial_{x} ϕ = 2 x y + y^{2} = F_{0}$ and $\partial_{y} ϕ = x^{2} + 2 x y = F_{1}$ . Thus [L1] makes $ϕ$ a potential, and substitution gives $ϕ (a, b) = 0$ .

step 1.2L1algebra

3.1

An open rectangle is convex and hence star-shaped with respect to $(a, b)$ , so [L2] also supplies a radial potential normalized to zero there. By [L3] and the common normalization, that radial potential agrees with $ϕ$ .

givenstep 2.1L2L3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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.-B. Campesato, Poincare Lemma, sections 1 and 2 (standard reference, not scraped)