CorollaryStatement: AI-adaptedProof: 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.

On a star-shaped open domain, closed, exact, conservative, path-independent, and zero-loop are equivalent

Statement

Let $U \subseteq R^{n}$ be open and star-shaped, and let $F : U \to R^{n}$ be $C^{1}$ . The following are equivalent:

$F$ is closed;
$F$ is exact;
$F$ is conservative;
$F$ is path-independent;
every closed piecewise- $C^{1}$ path $γ$ in $U$ satisfies $\int_{γ} F \cdot d r = 0$ .

Facts & Assumptions

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

[L1]

A star-shaped open set is nonempty and contains every segment from a star centre to a point of the set (Star-shaped open subsets of Euclidean space).

[L2]

Exactness uses a $C^{2}$ potential, whereas conservativity uses a $C^{1}$ potential (Exact and closed C1 vector fields, Piecewise-C1 path-connected domains, potential functions, conservative fields, and path independence).

[L3]

Every exact $C^{1}$ field is closed, and every closed $C^{1}$ field on a star-shaped domain is exact (Every exact C1 vector field is closed, Poincare's lemma on a star-shaped domain: every closed C1 field is exact).

[L4]

For a continuous field on a nonempty open piecewise- $C^{1}$ path-connected domain, conservativity, path independence, and the zero-loop condition are equivalent (Conservative, path-independent, and zero-closed-loop conditions are equivalent).

Proof

technique · direct

1.1

If $a$ is a star centre, any $x, y \in U$ are joined by the segment from $x$ to $a$ followed by the segment from $a$ to $y$ . By [L1] these segments lie in $U$ , so $U$ is piecewise- $C^{1}$ path-connected.

givenL1

1.2

Conditions 1 and 2 are equivalent by the two implications in [L3].

givenL3

1.3

Condition 2 implies condition 3 by [L2]. Conversely, if $F = \nabla ϕ$ with $ϕ$ merely $C^{1}$ , then the first partials of $ϕ$ are the components of the $C^{1}$ field $F$ ; hence $ϕ$ is $C^{2}$ , and condition 2 holds.

givenL2algebra

2.1

By step 1.1, all hypotheses of [L4] hold, so conditions 3, 4, and 5 are equivalent.

step 1.1L4

3.1

Combining steps 1.2, 1.3, and 2.1 proves the five-way equivalence.

step 1.2step 1.3step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 57 results over 18 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, sections 1 and 2 (standard reference, not scraped)