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.
The closed angular form on the punctured plane is not exact
Statement refuted
Every closed smooth one-form on the punctured plane is exact.
Facts & Assumptions
Given: The witness on .
Closed and exact differential forms: For the complex def-de-rham-cochain-complex, put and . A form is closed if it belongs to and exact if it belongs to . If , then by thm-the-exterior-derivative-squares-to-zero, so . In particular , since . The zero form is both closed and exact in every degree.
The local coordinate formula for the exterior derivative: Let be a smooth chart on a smooth manifold and a smooth -form on , with . Summing over increasing -tuples , and writing , if , then
Newton–Leibniz needs only continuity on , differentiability on , and a Riemann-integrable extension of the interior derivative: Let . Suppose is continuous on and differentiable on . If is Riemann integrable and then No derivative of at either endpoint is assumed, and the two endpoint values assigned to the integrable extension do not enter the conclusion.
Counterexample
The denominator is positive. Writing its coefficients as and gives . Hence .
On , and its integral is . If , then the chain rule and the fundamental theorem would make this integral . Thus the closed witness is not exact.
Source locator
Lee, angular form (17.1), p.441; the zero derivative and nonzero loop period are calculated above by Newton–Leibniz.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
17 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
- John M. Lee, Introduction to Smooth Manifolds, second edition (standard reference, not scraped)