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 Mobius band is nonorientable although its boundary circle is orientable
Example
The Möbius band is nonorientable, while its boundary circle is orientable independently.
Facts & Assumptions
Given: The standard smooth Möbius band , equivalently the quotient of by the deck transformation , with quotient map .
An orientation is a smooth choice of a ray in each determinant line (Oriented smooth manifolds and oriented charts).
A manifold is orientable exactly when it admits such an orientation (Orientable manifolds).
Verification
Suppose had an orientation. Pulling its determinant rays back by the local diffeomorphism would orient the connected strip . Relative to the standard ray of , this continuous choice has one constant sign on the strip.
Since , the pulled-back orientation would have to be invariant under . But has determinant and reverses every determinant ray, contradicting step 1.1. Hence is nonorientable by [L2].
The two boundary lines of the strip are exchanged by , so their quotient is one component. The map is a smooth bijection with smooth inverse in the quotient charts. It identifies with a circle, whose positive -direction supplies an orientation under [L1]. This orientation is chosen on the boundary itself and is not induced from the nonorientable band.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
5 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
- Ioan Mărcuț, Manifolds (2017 lecture notes), §§14.5, 15.1 (standard reference, not scraped)
- Will Merry, Differential Geometry (2021), Lecture 24 (standard reference, not scraped)