Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Uniqueness of Stiefel–Whitney classes from normalization, naturality, and sum

Statement

Assume AC. Let w′ be a rule assigning to every isomorphism class of numerable real vector bundles E→B over an admissible base a total class w′(E)∈H∗(B;F2) such that

  1. the degree-zero part of w′(E) is 1 and w′(E) has finite degree bounded by the rank of E;
  2. w′ is natural: w′(f∗E)=f∗w′(E) for every map f of admissible bases;
  3. w′ is multiplicative: w′(E⊕F)=w′(E)w′(F) for bundles over one base;
  4. w′(γ1)=1+a for the tautological line γ1→RP∞, where a generates H1(RP∞;F2).

Then w′=w: the rule agrees with the total Stiefel–Whitney class of Stiefel–Whitney classes from the projective-bundle relation on every numerable real bundle over an admissible base, and wi′(E)=0 for i greater than the rank of E.

Facts & Assumptions

Given: AC, a rule w′ satisfying the four clauses of the statement, and a numerable real bundle E→B of rank n≥0 over an admissible base.

[F1]

The universal line γ1→RP∞ has H∗(RP∞;F2)=F2[a] with ∣a∣=1, and the Stiefel–Whitney classes of a line bundle L are w0(L)=1, w1(L)=xL and wi(L)=0 for i≥2, where xL is computed from a classifying map of L (Mod-two cohomology ring of infinite real projective space, Stiefel–Whitney classes from the projective-bundle relation).

[F2]

By naturality, a line bundle L over an admissible base with classifying map c (a map with c∗γ1≅L, available from the numeration) satisfies w1(L)=c∗a and w′(L)=c∗w′(γ1) (Tautological degree-one class on a real projective bundle, Naturality of Stiefel–Whitney classes).

[F3]

The flag bundle q:Fl⁡(E)→B is an admissible base with q∗E≅L1⊕⋯⊕Ln and q∗ injective on F2-cohomology (Real flag bundle and Stiefel–Whitney roots, Real splitting principle with mod-two injective pullback).

[F4]

The Stiefel–Whitney class satisfies naturality, the Whitney product formula and w(γ1)=1+a (Whitney sum formula for Stiefel–Whitney classes, Naturality of Stiefel–Whitney classes, Stiefel–Whitney classes from the projective-bundle relation).

[A1]

AC is the Axiom of Choice in the form fixed by The Axiom of Choice.

Proof

1.1F1F2

The rule is determined on line bundles. Let L→B be a numerable real line bundle with classifying map c, so c∗γ1≅L. Then naturality of w′ and the normalization w′(γ1)=1+a give w′(L)=w′(c∗γ1)=c∗w′(γ1)=c∗(1+a)=1+c∗a=1+w1(L), where the last equality is [F2]. Hence w′(L)=w(L) for every line bundle, including the trivial line, for which c is nullhomotopic and w1=0.

2.1F1F3F4step 1.1

The rule is determined on every bundle. Let E→B have rank n≥0 and let q:Fl⁡(E)→B be its flag bundle, with q∗E≅L1⊕⋯⊕Ln and q∗ injective. Iterating multiplicativity of w′ over the successive summands gives w′(q∗E)=∏j=1nw′(Lj), where the empty product for n=0 is 1; by step 1.1 and [F1] this is ∏j=1n(1+w1(Lj))=w(L1⊕⋯⊕Ln)=w(q∗E), the last equality by the Whitney formula and [F1]. On the other hand naturality of both rules gives w′(q∗E)=q∗w′(E) and w(q∗E)=q∗w(E), so q∗w′(E)=q∗w(E); injectivity of q∗ gives w′(E)=w(E). For n=0 the bundle is the zero bundle, Fl⁡(E)=B, and both rules give 1 by their degree-zero normalization, so the identity is literal.

3.1F1F3step 2.1

The rank bound. Since w′=w by step 2.1 and the classes wi(E) vanish for i>n by the rank convention of their definition, also wi′(E)=0 for i>n. Combined with clause 1 of the statement this shows the rule is exactly the total class computed from the projective-bundle relation, whose coefficients are the classes wi.

4.1F1F2F3A1step 1.1step 2.1∎

Boundary cases. For rank n=1 the flag bundle is B up to the identification P(L)≅B, the splitting is q∗L≅L1 with L1≅L, and step 2.1 reduces to step 1.1. For the empty base all groups vanish and both rules give the zero class with degree-zero part the zero-ring unit. The normalization clause 4 is exactly the universal case of step 1.1 over RP∞, and the tautological line is the line bundle with classifying map the identity. AC is used through the splitting principle of [F3], as recorded.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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