CorollaryStatement: Literature-sourcedProof: 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.

Conservative fields are path-independent and have zero integral around every closed path

Statement

Let $U \subseteq R^{n}$ be open and let $F : U \to R^{n}$ be conservative. Then $F$ is path-independent. Moreover,

$\int_{γ} F \cdot d r = 0$

for every closed piecewise- $C^{1}$ path $γ$ in $U$ .

Facts & Assumptions

Given: The open set and conservative field in the Statement.

[L1]

Conservativity means that $F = \nabla ϕ$ for some $C^{1}$ potential $ϕ$ , and path independence compares any two piecewise- $C^{1}$ paths having the same endpoints (Piecewise-C1 path-connected domains, potential functions, conservative fields, and path independence).

[L2]

For every piecewise- $C^{1}$ path $γ$ , $\int_{γ} \nabla ϕ \cdot d r = ϕ (γ (b)) - ϕ (γ (a))$ (The gradient theorem: the line integral of a gradient is the endpoint increment).

Proof

technique · direct

1.1

Choose a potential $ϕ$ as in [L1]. If $α$ and $β$ have the same initial point $x$ and terminal point $y$ , then [L2] gives $\int_{α} F \cdot d r = ϕ (y) - ϕ (x) = \int_{β} F \cdot d r .$

givenL1L2

1.2

If $γ$ is closed, then its two endpoint values agree, and [L2] gives $\int_{γ} F \cdot d r = 0$ .

givenL2algebra

2.1

Hence $F$ is path-independent by [L1].

step 1.1L1

3.1

The closed-loop conclusion does not require connectedness: it is an endpoint calculation for each path that exists.

step 1.2∎

Depends on

Used by

Dependency tree · two levels

6 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. Lebl, Basic Analysis II, Corollary 9.3.2 (standard reference, not scraped)