Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedprecheck passaudited 2026-09-07
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.

Positive-dimensional real projective space is orientable exactly in odd dimension

Example

For n1, RPn is orientable exactly when n is odd; RP0 is a point and is orientable.

Facts & Assumptions

Given: An integer n1, the standard sphere orientation on Sn=Bn+1, the antipodal map a:SnSn, a(x)=x, and the quotient covering π:SnRPn=Sn/{1,a}.

[L1]

The orientation on the boundary of the standard oriented ball is outward-normal-first (Induced boundary orientation).

[L2]

Between manifolds equipped with chosen orientations, a local diffeomorphism has a well-defined pointwise orientation sign, constant on a nonempty connected source (Pointwise orientation sign of a local diffeomorphism).

[L3]

A zero-dimensional real vector space has two determinant-line orientation rays (Determinant-line orientations of finite-dimensional real vector spaces).

Verification

technique · direct
1.1

Fix xSn and a positive tangent basis (v1,,vn) at x. By [L1], (x,v1,,vn) is positive in Rn+1. Since dax(vi)=vi, the corresponding ambient tuple at x is (x,v1,,vn), whose sign relative to the original tuple is (1)n+1. Thus [L2] gives the antipodal map the constant orientation sign (1)n+1.

givenL1L2algebra
2.1

If a preserves orientation, define the orientation ray at [x] by pushing the ray at x forward with dπx. The other lift is a(x), and πa=π makes the resulting ray independent of that choice. Conversely, an orientation on RPn pulls back through the local diffeomorphism π to an orientation of Sn that a must preserve. By step 1.1 this occurs exactly when (1)n+1=1, namely when n is odd. Finally, RP0 is a point and is orientable by [L3].

givenL2L3step 1.1

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