CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated

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 tangent bundle of RP² is not Spin

Statement refuted

A Spin structure can be supplied to every tangent bundle. In particular, the tangent bundle of ${R P}^{2}$ would admit one.

Facts & Assumptions

Given: AC and the tangent bundle of ${R P}^{2}$ .

[F1]

In $H^{*} ({R P}^{m}; F_{2}) = F_{2} [a] / (a^{m + 1})$ the class $a$ is nonzero and $w (T {R P}^{m}) = (1 + a)^{m + 1}$ (Stiefel-Whitney classes of the tangent bundle of real projective space), using the exact convention of Stiefel–Whitney classes from the projective-bundle relation.

[F2]

Under AC, $w_{1} (E) = 0$ exactly when the real bundle is orientable (The first Stiefel–Whitney class classifies orientability).

[F3]

A given Spin structure is a lift of the oriented orthonormal frame bundle, and therefore requires an orientation (Given Spin and Spin-c structures and their spinor bundles).

Counterexample

1.1F1algebra

Put $m = 2$ in [F1]. Modulo two and $a^{3} = 0$ , $(1 + a)^{3} = 1 + 3 a + 3 a^{2} + a^{3} = 1 + a + a^{2}$ . Its degree-one part is $w_{1} (T {R P}^{2}) = a \neq 0$ . The exact SW definition supplier is the existing item with the in its ID; no nonexistent substitute is used.

2.1F2F3step 1.1∎

By [F2] the tangent bundle is not orientable. A Spin lift would supply the orientation required by [F3], a contradiction. Thus $T {R P}^{2}$ has no Spin structure, refuting the asserted universal existence and exhibiting the intended first-class obstruction. AC is carried from the characteristic-class and orientability suppliers.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 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

Milnor and Stasheff, Characteristic Classes, §2 (standard reference, not scraped)
M. F. Atiyah, R. Bott, and A. Shapiro, Clifford Modules, Topology 3, Supplement 1 (1964) (standard reference, not scraped)