Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Oriented clutching classifies oriented bundles over spheres

Statement

For n1 and k1, orientation-preserving isomorphism classes of oriented rank-n real bundles over Sk are classified by

[Sk1,GLn+(R)][Sk1,SO(n)].

Reversing the chosen fiber orientation acts on a clutching map by conjugation with an orientation-reversing matrix.

Facts & Assumptions

Given: n1, k1, and an oriented rank-n bundle over Sk.

[F1]

Unoriented clutching is controlled by hemisphere trivializations, homotopies, and disk-extending gauge maps (Clutching classifies vector bundles over spheres in the stable range).

[F2]

Positive frames and orientation-preserving maps have transition matrices in GLn+(R) (Oriented real bundles and oriented frame bundles).

[F3]

With a metric, positive orthonormal frames are the corresponding SO(n) reduction (Orientation is equivalent to an SO(n)-reduction).

Proof

technique · direct
1.1

Each hemisphere disk is connected and the restriction of the oriented bundle is trivial by the finite argument in [F1]. If a chosen trivialization reverses orientation, compose it with one fixed reflection; hence both hemisphere trivializations may be chosen orientation-preserving. Their equatorial transition then lies in GLn+(R) by [F2].

F1F2construct
2.1

Repeat the equivalence calculation of [F1] using only orientation-preserving hemisphere gauges. Such gauges take values in GLn+, which is path connected, and their disk restrictions are nullhomotopic. Thus two positive clutching maps give orientation-preservingly isomorphic bundles exactly when they are homotopic, proving the first classification. This includes k=1: every map from S0 to the path-connected group has the single unbased homotopy class.

F1F2step 1.1
3.1

Polar normalization preserves determinant sign and deformation retracts GLn+(R) onto SO(n). Equivalently, it orthonormalizes the positive frames in [F3]. It therefore induces the second displayed bijection on homotopy classes.

F3step 2.1algebra
4.1

Fix a reflection rGLn(R). After reversing the chosen orientation of every fiber, the old oriented hemisphere trivializations become orientation-reversing; postcomposing both with r makes them oriented again. If their old transition was g, the new one is rgr1. A different reflection differs from r by positive matrices and gives the same action on the classified homotopy classes. The argument is finite and uses no choice principle.

F1F2step 2.1step 3.1algebra

Depends on

Used by

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