Alphabeta Math
LemmaStatement: 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.

Normalized clutching data for bundles over X×S²

Statement

Assume AC and let X be compact Hausdorff. Every complex vector bundle on X×S2 is represented, after adding a trivial bundle if necessary, by data [E,f]: two copies of prXE on X×D2 glued along X×S1 by a bundle automorphism f, normalized by f(x,1)=idEx. For a fixed bundle, different choices of normalized hemisphere trivializations give homotopic normalized clutching maps. Homotopies through normalized automorphisms give isomorphic stabilized bundles.

Facts & Assumptions

Given: AC, a compact Hausdorff space X, and a finite-rank complex bundle V on X×S2.

[F1]

Under AC, bundle pullback is invariant under homotopy (Homotopy invariance of vector-bundle pullback).

[F2]

The fixed clutching definition supplies the upper-to-lower convention (Clutching construction for bundles over a suspension). Applying the transition-cocycle construction in local charts of E, also with an interval parameter, glues two copies of prXE by an equatorial bundle automorphism and turns a homotopy of such automorphisms into a bundle over the parameter cylinder (Vector bundles are glued from transition cocycles).

[F3]

Under AC, finite complements and common trivial stabilization are available (Finite-rank complement theorem over compact Hausdorff bases, Equality in K⁰ is stable isomorphism over compact bases).

[A1]

AC is used through [F1] and [F3].

Proof

technique · direct
1.1

Let D+2 and D2 be the closed hemispheres. Each inclusion X×{0}X×D±2 is a homotopy inverse to projection. By [F1], there are bundles E± on X and isomorphisms VX×D±2prXE±. In these trivializations, V is obtained by an equatorial isomorphism f(x,z):(E+)x(E)x.

F1F2A1
2.1

At z=1, f(x,1) is an isomorphism E+E. Identify E with E=E+ by f(x,1)1. In the fixed coefficient convention the transition becomes f(x,1)1f(x,z), which equals the identity at z=1. Thus V=[E,f] with normalized f.

F2step 1.1algebra
3.1

If h± and h± are two normalized hemisphere trivializations of the same bundle, their ratios are maps g±:X×D±2Aut(E) with g±(x,1)=I. The straight contraction of each disk to 1 fixes 1, so composing g± with it gives homotopies to the identity through maps still equal to I at 1. Applying these changing gauges to the equatorial transition gives a homotopy between the two normalized clutching maps.

F2step 2.1construct
4.1

For a virtual class, [F3] complements its negative bundle into a finite trivial bundle and then applies steps 1.1–3.1 to the resulting actual bundle; this is the optional stabilization in the statement.

F3A1step 1.1step 2.1step 3.1
5.1

A normalized homotopy ft glues, by [F2], a bundle on X×S2×I. Its endpoint restrictions are isomorphic by [F1]. The normalization keeps the chosen common bundle and basepoint frame fixed, and adding trivial summands before the homotopy gives the same conclusion for stabilized data.

F1F2A1step 2.1step 4.1

Depends on

Used by

Dependency tree · two levels

17 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