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.
False: every closed C1 field on a connected open set is exact
Statement
Every closed vector field on a connected open subset of is exact.
Facts & Assumptions
Given: The proposed implication, the punctured plane , and the vortex field
With coordinates indexed from , so that , closedness means , while exactness supplies a potential with gradient (Exact and closed C1 vector fields).
A gradient line integral is its potential's endpoint increment and is therefore zero on a closed path (The gradient theorem: the line integral of a gradient is the endpoint increment).
Vector line integrals integrate ; sine and cosine have derivatives and and satisfy (Scalar line integrals with respect to arc length and vector-field line integrals, The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).
A continuous real function on a closed interval takes every value between its endpoint values (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on takes every value between and ).
On a star-shaped open domain, closedness and exactness are equivalent for vector fields (On a star-shaped open domain, closed, exact, conservative, path-independent, and zero-loop are equivalent).
Refutation
Direct differentiation gives , so [L1] makes closed and on the open set . Radial segments at positive radius followed by a circular arc give a piecewise- path in between any two of its points.
For on , [L3] gives . Hence [L3] and [L4] give
If were a separation into disjoint nonempty relatively open sets, choose and and let be the path from step 1.1. The function equal to when and to when is locally constant, hence continuous, and has endpoint values and . By [L5] it would take the value , which is impossible. Thus is connected.
If were exact, [L1] and [L2] would make the integral in step 1.2 zero. Thus it is not exact, and the statement is false despite steps 1.1 and 2.1. The valid correction in [L6] replaces connectedness by the stronger star-shaped hypothesis.
Depends on
- Exact and closed C1 vector fields
- The gradient theorem: the line integral of a gradient is the endpoint increment
- Scalar line integrals with respect to arc length and vector-field line integrals
- The derivatives of sine and cosine are cosine and minus sine
- Parity and the Pythagorean identity for sine and cosine
- If $m \le f \le M$ on $[a,b]$ then $m(b-a) \le L(f,P) \le \underline{\int_a^b} f \le \overline{\int_a^b} f \le U(f,P) \le M(b-a)$ for every partition $P$; in particular every constant function is integrable, with $\int_a^b c = c(b-a)$
- Pi as twice the smallest positive zero of cosine
- Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$
- On a star-shaped open domain, closed, exact, conservative, path-independent, and zero-loop are equivalent
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 167 results over 27 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)