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.
De rham homotopy formula on a product
Statement
For endpoint inclusions , on smooth forms of every degree.
Facts & Assumptions
Given: Write with tangential families.
The interval homotopy operator is coordinate independent: The interval operator is coordinate independent and maps smooth forms to smooth forms.
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.
Integration along the unit interval for a differential form: For smooth up to the endpoints, in positive degree, while in degree zero and on zero terms.
Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral: On a compact rectangle, a continuous parameter derivative may be passed through the integral when represented by a continuous function.
Proof
The coordinate differential gives : the minus sign follows from moving past . Consequently the definition F4 gives .
The fundamental theorem on each coefficient gives the first integral as . By F4, ; coefficientwise F5 permits each -coordinate derivative through this compact parameter integral, so F2 gives . Since , rearrangement proves the formula. In degree zero, and this is just the fundamental theorem; in top or out-of-range degrees the vanishing terms satisfy the same identity.
Source locator
Lee, Introduction to Smooth Manifolds, 2nd ed., Lemma 17.9 and Proposition 17.10, pp.444–445; the proof here computes the product differential directly.
Depends on
- Integration along the unit interval for a differential form
- The interval homotopy operator is coordinate independent
- The local coordinate formula for the exterior derivative
- Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral
- Newton–Leibniz needs only continuity on $[a,b]$, differentiability on $(a,b)$, and a Riemann-integrable extension of the interior derivative
Used by
Dependency tree · two levels
20 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)