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 de rham cohomology class of a form is defined without closedness
Statement
False claim: every smooth differential form represents a de Rham cohomology class.
Facts & Assumptions
Given: The smooth one-form 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.
De rham cohomology: The real de Rham cohomology is , with as in def-closed-and-exact-differential-forms. This is def-cohomology-object-of-a-cochain-complex in real vector spaces. Only a closed form represents a class . For closed forms , equality means precisely for some -form . Addition and real scalar multiplication are induced by those of forms. All groups on the empty manifold are zero.
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
Refutation
The coordinate formula gives , whose value on is . Thus .
A class in must be represented by an element of . The displayed smooth form is outside that numerator, so is not a de Rham class.
Source locator
Lee, p.441, definition of the cycle quotient; the witness is calculated locally.
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
- John M. Lee, Introduction to Smooth Manifolds, second edition (standard reference, not scraped)