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

Path independence is equivalent to zero integral around every closed piecewise-C1 path

Statement

Let U⊆Rn be open and piecewise-C1 path-connected, and let F:U→Rn be continuous. The following are equivalent:

  1. F is path-independent;
  2. every closed piecewise-C1 path γ in U satisfies ∫γF⋅dr=0.

Facts & Assumptions

Given: The domain and field in the Statement.

[L1]

Path independence means equality of vector line integrals along any two piecewise-C1 paths with the same endpoints (Piecewise-C1 path-connected domains, potential functions, conservative fields, and path independence).

[L2]

Under concatenation vector line integrals add, and reversal negates a vector line integral (Line integrals under reversal and concatenation).

[L3]

A constant path has zero vector line integral because its velocity is zero (Scalar line integrals with respect to arc length and vector-field line integrals).

[L4]

An orientation-preserving oriented piecewise-C1 reparametrization leaves a vector line integral unchanged (Scalar line integrals are parametrization-independent; vector line integrals retain orientation and change sign when it reverses).

Proof

technique · direct
1.1givenL1L3

Assume condition 1, and let γ be closed at x. The path γ and the constant path at x have the same endpoints, so [L1] and [L3] give ∫γF⋅dr=0. Thus condition 2 holds.

1.2givenL2L4

Conversely, assume condition 2. Let α and β be paths from x to y. The increasing affine bijection of [0,1] onto a path's domain is an orientation-preserving oriented reparametrization, so by [L4] we may replace each path by its reparametrization on [0,1] without changing either integral. With both domains [0,1], the concatenation in [L2] is defined and α∗β− is closed.

2.1givenstep 1.2L2algebra

By condition 2 and [L2], 0=∫α∗β−F⋅dr=∫αF⋅dr−∫βF⋅dr.

3.1step 2.1L1algebra

Hence the two integrals agree, and [L1] gives path independence.

4.1step 1.1step 1.2step 2.1step 3.1L1∎

Step 1.1 proves the forward direction, and steps 1.2, 2.1, and 3.1 prove the reverse direction. Piecewise-C1 path-connectedness guarantees that the comparison paths relevant to condition 1 exist between any two points of U.

Depends on

Dependency tree · 2 levels

Sources