TheoremStatement: 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.

Poincare's lemma on a star-shaped domain: every closed C1 field is exact

Statement

Let $U \subseteq R^{n}$ be open and star-shaped with respect to $a \in U$ . Every closed $C^{1}$ field $F : U \to R^{n}$ is exact. A $C^{2}$ potential is

$ϕ (x) : = \int_{0}^{1} ⟨ F (a + t (x - a)), x - a ⟩ d t .$

Facts & Assumptions

Given: The star-shaped domain, centre, and closed $C^{1}$ field in the Statement.

[L1]

Star-shapedness gives $a + t (x - a) \in U$ for every $x \in U$ and $0 \leq t \leq 1$ (Star-shaped open subsets of Euclidean space).

[L2]

Closedness is the system $\partial_{j} F_{i} = \partial_{i} F_{j}$ , and exactness requires a $C^{2}$ function with gradient $F$ (Exact and closed C1 vector fields).

[L3]

On a compact rectangle, a continuous parameter derivative may be passed through the integral when it is represented by a continuous function (Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral).

[L4]

If a continuous function has an integrable interior derivative on a compact interval, the integral of that derivative is the endpoint increment (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

[L5]

Continuous partial derivatives imply total differentiability, with derivative matrix equal to the Jacobian (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative).

Proof

technique · direct

1.1

By [L1], the integrand defining $ϕ (x)$ is defined for every $t \in [0, 1]$ ; it is continuous, so the integral exists. Fix $x \in U$ and a coordinate $j$ . Openness and [L1] provide a small closed coordinate interval about $x$ whose radial segments from $a$ remain in $U$ .

givenL1

2.1

On that interval, [L3] differentiates the defining integral with respect to $x_{j}$ and gives $\partial_{j} ϕ (x) = \int_{0}^{1} (F_{j} (z_{t}) + t \sum_{i} \partial_{j} F_{i} (z_{t}) (x_{i} - a_{i})) d t,$ where $z_{t} = a + t (x - a)$ . The integrand and its parameter derivative are continuous because $F$ is $C^{1}$ .

step 1.1L3algebra

3.1

By closedness in [L2], $\partial_{j} F_{i} = \partial_{i} F_{j}$ . Thus the integrand in step 2.1 is $F_{j} (z_{t}) + t \sum_{i} \partial_{i} F_{j} (z_{t}) (x_{i} - a_{i}) = \frac{d}{d t} (t F_{j} (z_{t})) .$

givenstep 2.1L2algebra

4.1

Apply [L4] to step 3.1. The endpoint at $t = 0$ is $0 \cdot F_{j} (a) = 0$ , and the endpoint at $t = 1$ is $F_{j} (x)$ , so $\partial_{j} ϕ (x) = F_{j} (x)$ .

step 2.1step 3.1L4algebra

5.1

Since this holds for every $x$ and $j$ , the partial derivatives of $ϕ$ are the $C^{1}$ functions $F_{j}$ . In particular they are continuous, so [L5] gives $\nabla ϕ = F$ , and their first partials are continuous; hence $ϕ$ is $C^{2}$ .

step 4.1L5given

6.1

By the definition in [L2], step 5.1 makes $F$ exact with the displayed potential.

step 5.1L2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 120 results over 22 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.-B. Campesato, Poincare Lemma, section 2 (standard reference, not scraped)