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 angular period and the obstruction to bounding
Example
On let Its integral over the counterclockwise unit circle is . Therefore that circle cannot be the induced oriented boundary of a compact oriented embedded smooth surface contained in the punctured plane; the form is also not exact there.
Facts & Assumptions
A nonzero period obstructs exactness and bounding: Let be an oriented compact boundaryless embedded -submanifold, , and let be a closed smooth -form on . If , then is not exact on , and cannot be the induced oriented boundary of a compact embedded -submanifold of .
Computing form integrals by finite parametrizations: Let , let be oriented, and let . For let be bounded open Jordan domains and continuous and smooth up to the boundary in target coordinates: near each parameter point, a target coordinate representative extends smoothly to a Euclidean neighborhood. Suppose is an orientation-preserving diffeomorphism onto an open , the are pairwise disjoint, and . Then An empty family is allowed when the support is empty. No nonsingularity of on , and no -valued extension across a genuine target boundary, is assumed.
Verification
Given: The objects and hypotheses in the statement above.
Write and . Direct differentiation gives , hence on the punctured plane. The origin is excluded from its domain.
For , . The interval maps diffeomorphically to the circle minus one point and extends smoothly to its closure. The finite-parametrization formula gives .
The circle is compact, embedded, oriented, and boundaryless, with dimension one. Its nonzero period and the closedness calculation meet all hypotheses of the period obstruction, giving both nonexactness and the stated nonbounding conclusion.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
10 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
- Lee Example 16.16 and Corollary 16.15, p.415 (standard reference, not scraped)