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.
An exact one-form has zero period on every closed piecewise-C¹ curve
Statement
On any smooth manifold , if a smooth one-form is exact, so for a globally defined smooth scalar , then for every closed piecewise- curve in .
Statement references
Facts & Assumptions
Given: A smooth exact one-form on a smooth manifold and a closed piecewise- curve with an admissible finite subdivision.
Period of a smooth one-form along a closed curve: on a smooth manifold, for a smooth one-form and a closed continuous piecewise- curve with finitely many chartwise pieces and one-sided endpoint derivatives, the period is the sum of the integrals of over those pieces.
Closed and exact differential forms: exactness means for a globally defined smooth scalar .
The chain rule for total derivatives: : in local coordinates, the total derivative of a composition is the composition of the total derivatives.
A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion: each continuous derivative on a closed subinterval is integrable there.
The second fundamental theorem: if is differentiable on with and is integrable, then : if is differentiable on a closed interval and is integrable, then the integral of equals the endpoint increment of .
Proof
Fix the finite subdivision from [F1]. On each chartwise piece choose a chart containing its image, and put and . By [F2] the coordinate coefficients of are ; applying [F3] to gives in the piece interior. The same formula holds with one-sided derivatives at the endpoints: the differentiability expansion of composed with the one-sided expansion of gives . These derivatives are continuous on the closed piece by [F1] and smoothness of , so they are integrable by [F4].
Apply [F5] on each subdivision interval to . By [F1] the period is the sum of those integrals, so it equals the sum of the increments . The internal endpoint terms cancel, and the remaining increment is because is closed. Thus the period is zero.