Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

Euler class of zero and trivial positive-rank bundles

Example

Assume AC. For every base B in the general Thom scope and every commutative ring R:

  1. the zero bundle of rank zero with its standard unit orientation has e(0B,1)=1H0(B;R);
  2. every trivial bundle εBn of positive rank n1, with its standard product R-orientation, has e(εBn)=0Hn(B;R).

Facts & Assumptions

Given: AC, a base B in the general Thom scope, a commutative ring R and an integer n1.

[F1]

The Euler class is e(ξ)=sj(uξ); in rank zero the maps j and s are identities and e(0B,o)=o for the supplied orientation o, so the standard unit orientation gives e(0B,1)=1 (Euler class by zero-section pullback of the Thom class).

[F2]

Under AC, an R-oriented numerable real bundle of positive rank over a base in the general Thom scope has zero Euler class if it admits a nowhere-zero section; no converse is asserted (A nowhere-zero section forces the Euler class to vanish).

[F3]

Give εBn=B×Rn its product Euclidean metric. The global product chart identifies every fiber disk pair with (Dn,Sn1) and every stalk of its R-orientation local system with Hn(Dn,Sn1;R)R. The constant fiber class corresponding to 1R generates every stalk and is compatible in the single global chart, so it is an R-orientation by R-oriented vector bundle and orientation local system. For R=Z it is the coefficient orientation induced by the standard ordinary orientation of Rn in Oriented real bundles and oriented frame bundles. The formula b(b,e1) is a continuous section by the product topology and is nowhere zero because e10.

[A1]

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

Verification

1.1

The rank-zero value. Give 0B the standard unit orientation. Its disk bundle is B, its sphere bundle is empty, and the zero section and relative-to-absolute map are identities; fiber normalization makes the Thom class the unit 1 in degree zero. Hence e(0B,1)=sj(1)=1H0(B;R) by [F1]. For another supplied rank-zero orientation o, the same calculation instead gives e(0B,o)=o.

F1
1.2

The trivial bundle of positive rank. For n1 the constant section b(b,e1) of εBn is nowhere zero and continuous. Its global product chart, together with the constant partition of unity 1, makes the bundle numerable, while [F3] supplies its standard product R-orientation. The standing hypothesis places B in the general Thom scope. Thus every hypothesis of [F2] holds, and e(εBn)=0Hn(B;R).

F2F3
2.1

Boundary cases. For the empty base the unique cohomology class in every degree is zero, and the standard rank-zero convention reads e(0,1)=1=0 in the zero ring; the two displayed identities remain consistent. For a point base, ε0 with unit orientation contributes e=1H0(;R)=R and εn with n1 contributes e=0Hn(;R)=0. For the zero ring both classes coincide with the unique element, so the identities hold. The section of step 1.2 is a specified function and no choice is made in it; AC is used only through the Thom suppliers that give the Euler class its value.

F1F2F3A1step 1.1step 1.2

Depends on

Used by

Nothing in the library uses this result yet.

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