ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

A closed field on a star-shaped domain with its radial primitive computed

Example

On $U = R^{2}$ , which is star-shaped about the origin (Star-shaped open subsets of Euclidean space), consider the $C^{1}$ field $F (x, y) : = (2 x y, x^{2})$ (Exact and closed C1 vector fields). Its potential

$ϕ (x, y) : = x^{2} y$

has gradient $\nabla ϕ = (2 x y, x^{2}) = F$ , so $F$ is exact with potential $ϕ$ . The closed field condition $\partial_{1} F_{0} = \partial_{0} F_{1}$ holds as well, and the radial formula of the published Poincare lemma returns exactly $ϕ$ :

$\int_{0}^{1} ⟨ F (t (x, y)), (x, y) ⟩_{2} d t = \int_{0}^{1} 3 x^{2} y t^{2} d t = x^{2} y .$

Facts & Assumptions

Given: The open set $U = R^{2}$ with centre $0$ , the field $F (x, y) = (2 x y, x^{2})$ and the function $ϕ (x, y) = x^{2} y$ .

[L1]

$R^{2}$ is open and star-shaped with respect to $0$ : for every $x \in R^{2}$ and $0 \leq t \leq 1$ the point $t x$ lies in $R^{2}$ (Star-shaped open subsets of Euclidean space).

[L2]

A $C^{1}$ field $F = (F_{0}, F_{1})$ on an open subset of $R^{2}$ is closed when $\partial_{1} F_{0} = \partial_{0} F_{1}$ , and exact when there is a $C^{2}$ function $ϕ$ with $\nabla ϕ = F$ (Exact and closed C1 vector fields).

[L3]

Poincare's lemma: on a star-shaped open domain $U$ with centre $a$ , every closed $C^{1}$ field is exact, and a $C^{2}$ potential is $ϕ (x) = \int_{0}^{1} ⟨ F (a + t (x - a)), x - a ⟩_{2} d t$ (Poincare's lemma on a star-shaped domain: every closed C1 field is exact).

[L4]

If $f$ is Riemann integrable and $G$ is continuous on $[0, 1]$ and differentiable on $(0, 1)$ with $G^{'} = f$ there, then $\int_{0}^{1} f = G (1) - G (0)$ ; and the derivative of $t \mapsto t^{3}$ is $3 t^{2}$ (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative, For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term). A continuous real function on the nondegenerate rectangle $[0, 1]$ is Riemann integrable (Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable).

Verification

technique · direct; compute the partial derivatives and evaluate the radial integral

1.1givenL2algebra

The component functions $F_{0} (x, y) = 2 x y$ and $F_{1} (x, y) = x^{2}$ are $C^{1}$ , with $\partial_{1} F_{0} = 2 x = \partial_{0} F_{1}$ ; hence $F$ is closed by [L2].

2.1step 1.1L2algebra

The function $ϕ (x, y) = x^{2} y$ is $C^{2}$ with $\partial_{0} ϕ = 2 x y = F_{0}$ and $\partial_{1} ϕ = x^{2} = F_{1}$ , so $\nabla ϕ = F$ and $F$ is exact with potential $ϕ$ by [L2].

3.1step 2.1L1L3L4algebra∎

For $a = 0$ the radial formula of [L3] reads $ϕ_{r a d} (x, y) = \int_{0}^{1} ⟨ F (t x, t y), (x, y) ⟩_{2} d t = \int_{0}^{1} (2 t^{2} x^{2} y + t^{2} x^{2} y) d t = \int_{0}^{1} 3 x^{2} y t^{2} d t$ . The integrand is a continuous polynomial on $[0, 1]$ , hence Riemann integrable by [L4]. By [L4] applied to $G (t) : = x^{2} y t^{3}$ , whose derivative is $3 x^{2} y t^{2}$ , the integral equals $G (1) - G (0) = x^{2} y$ , so $ϕ_{r a d} = ϕ$ .

Remarks

The example exercises the exactness side of Poincare's lemma on the whole plane. Exactness is not a consequence of closedness on domains with holes: the standard angular field on $R^{2} ∖ {0}$ is closed but has no global primitive, a result established separately in the published counterexample cex-the-closed-angular-form-on-the-punctured-plane-is-not-exact, which is not used as a premise here.
Both displays agree on the potential because the radial formula is an explicit construction, not an independent existence argument; the differentiation check of step 2.1 is what identifies $ϕ$ as a potential.

A closed field on a star-shaped domain with its radial primitive computed

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources