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.
Mod-two Thom class of the Möbius line bundle
Example
Assume AC for Thom existence. The Möbius line bundle is not -oriented, but it is canonically -oriented. It therefore has a normalized mod-two Thom class and isomorphisms
Facts & Assumptions
Given: The model .
R-oriented vector bundle and orientation local system defines orientation by the monodromy action on the top disk-pair cohomology and gives the canonical mod-two orientation.
Thom isomorphism for oriented vector bundles gives the normalized class and degree shift under AC.
The Axiom of Choice is used only through [F2].
Verification
The generator of is the pair connector of the endpoint class modulo diagonal constants. The Möbius clutching map is reflection , which swaps the endpoint coordinates. It sends to , and modulo the diagonal . Thus its integral orientation monodromy is .
A global integral generator would have to return to itself after the base loop, while step 1.1 returns its negative. Since a generator of the free module is nonzero, this is impossible. Modulo two, and the same transition fixes the unique nonzero generator, giving the canonical orientation of [F1].
Apply [F2] with rank one and . It produces a unique normalized degree-one Thom class and the displayed shift for every . The two fiber endpoints, the base-loop start/end, the zero vector, degree-zero unit and zero classes are explicit above. The base and fibers are nonempty, and the coefficient rings are fixed, so empty and zero-ring cases are inapplicable. The monodromy calculation is finite and choice-free; AC is used exactly through [A1] in [F2].
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
11 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
- May, A Concise Course in Algebraic Topology, Chapter 23 §5 (standard reference, not scraped)