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.
A density integral on the Mobius band
Example
On the compact Möbius band the density descends to a smooth positive density , and .
Facts & Assumptions
Orientation-free density integration and its properties: Compactly supported smooth density integration is independent of charts and partition, linear, local, nonnegative on nonnegative densities and strictly positive for a nonzero nonnegative density. It is invariant under every diffeomorphism, without choosing an orientation. The finite-parametrization formula holds under the hypotheses of prop-integration-of-top-forms-by-finite-parametrizations, with orientation preservation omitted and absolute Jacobians used.
Pullback of densities by local diffeomorphisms: For a local diffeomorphism , pullback of smooth densities is smooth and in coordinates satisfies It is real-linear, obeys for smooth functions on , and for composable local diffeomorphisms.
Verification
Given: The objects and hypotheses in the statement above.
The quotient map is open because the inverse image of an image-open set is the union of its translates. A rectangle with s-width less than one is disjoint from all its nontrivial translates, so maps homeomorphically onto its image; at t=1 or t=-1 use a half-rectangle. For two inequivalent points only finitely many translates of a bounded neighborhood of one can approach a bounded neighborhood of the other; shrink to separate these finitely many translates. Their saturated neighborhoods are disjoint, proving Hausdorffness. Images of rational rectangles form a countable base. The transition maps are restrictions of , hence smooth, so these charts define a smooth manifold with boundary. It is compact as the image of .
The seam transition has determinant , with absolute value one, so the local densities glue and are positive. Equivalently by the pullback formula; the same holds for all integer powers.
Use the single finite parametrization from to the quotient. It is a diffeomorphism onto the open complement of seam and boundary, extends continuously from the closed rectangle, and is smooth up to each edge in target coordinates. Its image closure is B and its pulled-back density coefficient is one. The density parametrization formula therefore gives . Seam and boundary are covered by that formula’s null-boundary control.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
8 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 Proposition 16.37 and Exercise 16.44; Nicolaescu Definition 3.4.1 (standard reference, not scraped)