ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Stiefel-Whitney numbers of real projective space

Example

Assume AC (The Axiom of Choice), inherited from the Stiefel-Whitney class construction and the field-duality supplier. Let $n \geq 0$ . For $n \geq 1$ let $x \in H^{1} ({R P}^{n}; F_{2})$ be the nonzero generator, and for $n = 0$ set $x = 0$ . Then $H^{*} ({R P}^{n}; F_{2}) = F_{2} [x] / (x^{n + 1})$ and $⟨ x^{n}, [{R P}^{n}] ⟩ = 1$ . Then the total Stiefel-Whitney class of the tangent bundle is $w (T {R P}^{n}) = (1 + x)^{n + 1},$ so for a partition $I = (i_{1}, \dots, i_{r})$ of $n$ the Stiefel-Whitney number is the product of binomial coefficients $w^{I} [{R P}^{n}] = (\binom{n + 1}{i_{1}}) \dots (\binom{n + 1}{i_{r}}) m o d 2,$ and the top number is $w_{n} [{R P}^{n}] = n + 1 m o d 2$ : it is $1$ for $n$ even and $0$ for $n$ odd. In particular ${R P}^{2 k}$ is not null-cobordant, extending the known surface case to all even dimensions; and for $n = 2^{s} - 1$ with $s \geq 1$ the total class is $(1 + x)^{2^{s}} = 1 + x^{2^{s}} = 1 + x^{n + 1} = 1$ in $F_{2} [x] / (x^{n + 1})$ , so all Stiefel-Whitney numbers of ${R P}^{2^{s} - 1}$ vanish, consistent with these manifolds being boundaries in the cases $1 \leq s \leq 3$ . Explicit witnesses are the disk bundles of $γ^{\otimes 2}$ over ${C P}^{k}$ for $k = 0, 1, 3$ , where $γ$ is the tautological complex line; their boundaries are ${R P}^{2 k + 1}$ .

Facts & Assumptions

Given: An integer $n \geq 0$ , the real projective space ${R P}^{n}$ with its smooth structure and tautological line bundle $γ$ , all cohomology with $F_{2}$ coefficients unless stated, and the inward/outward normal line data below; AC is inherited from the Stiefel-Whitney class construction as recorded in [F2].

[F1]

Mod-two cohomology ring of infinite real projective space: $H^{*} ({R P}^{\infty}; F_{2}) = F_{2} [a]$ with $∣ a ∣ = 1$ , and restriction along the skeletal inclusion is an isomorphism in degrees at most $n$ , sending $a$ to the unique nonzero degree-one class of ${R P}^{n}$ for $n \geq 1$ ; Real projective space cellular homology and the pinch map gives the finite CW structure with one cell in each dimension and the mod-two homology $F_{2}$ in every degree $0 \leq j \leq n$ .

[F2]

Stiefel–Whitney classes from the projective-bundle relation defines the Stiefel-Whitney classes over admissible bases and gives $w_{1} (L) = x_{L}$ , $w (L) = 1 + w_{1} (L)$ for a real line $L$ ; Naturality of Stiefel–Whitney classes gives naturality and isomorphism invariance; Whitney sum formula for Stiefel–Whitney classes gives $w (E \oplus F) = w (E) w (F)$ and $w (E \oplus ε^{r}) = w (E)$ ; The first Stiefel–Whitney class classifies orientability identifies $w_{1}$ as the classifying class of line bundles. The Axiom of Choice is assumed exactly as declared by these suppliers.

[F3]

For a real line $ℓ \subset R^{n + 1}$ , graph coordinates identify $T_{ℓ} {R P}^{n}$ with $Hom (ℓ, ℓ^{⊥})$ : the derivative of a moving spanning vector is taken modulo $ℓ$ , independently of its rescaling. These identifications vary smoothly in graph charts. The metric identifies $ℓ^{*} ≅ ℓ$ , while $Hom (ℓ, ℓ)$ is the trivial scalar line. Splitting $R^{n + 1} = ℓ \oplus ℓ^{⊥}$ therefore gives $ε^{1} \oplus T {R P}^{n} ≅ Hom (γ, {\underline{R}}^{n + 1}) ≅ (n + 1) γ$ . This proves the tangent splitting directly, including $n = 0$ . For $n \geq 1$ the tautological line is nonorientable: along the loop $t \mapsto [\cos (π t) e_{1} + \sin (π t) e_{2}]$ a continuous spanning vector returns with the opposite sign. Thus [F2] gives $w_{1} (γ) \neq 0$ , identifying it with the unique nonzero degree-one class $x$ of [F1]; for $n = 0$ both are zero.

[F4]

Stiefel-Whitney numbers of a closed manifold defines $w^{I} [M] = ⟨ w^{I} (T M), [M] ⟩$ for monomials of total degree $n$ , with the canonical mod-two fundamental class and the componentwise convention; Fundamental class of a compact oriented manifold characterizes the canonical mod-two fundamental class $[{R P}^{n}]$ by its local generators; Kronecker evaluation pairing is evaluation of cocycles on cycles; Cohomology over a field is dual to homology over that field makes evaluation $H^{n} (X; F_{2}) \to {Hom}_{F_{2}} (H_{n} (X; F_{2}), F_{2})$ an isomorphism under AC.

[F5]

Boundaries have zero Stiefel-Whitney numbers: every Stiefel-Whitney number of a closed manifold that is the boundary of a compact manifold vanishes, so a closed manifold with a nonzero number is not null-cobordant (Null-cobordant closed manifolds).

[F6]

Complex projective bundle and tautological complex line supplies the complex tautological line; Whitney sum, tensor, dual, Hom, and exterior-power bundles supplies its tensor square used in the explicit boundary construction.

Verification

1.1F1F4

For $n \geq 1$ , [F1] makes $H^{j} ({R P}^{n}; F_{2}) ≅ F_{2}$ for $0 \leq j \leq n$ and zero above, generated by the powers of $x$ , and $x^{n + 1} = 0$ ; for $n = 0$ the space is a point and $x = 0$ in $H^{1}$ , with the ring $F_{2}$ . By [F4] and field duality, the evaluation pairing $H^{n} ({R P}^{n}; F_{2}) \times H_{n} ({R P}^{n}; F_{2}) \to F_{2}$ is a nondegenerate pairing of one-dimensional spaces, so the nonzero classes $x^{n}$ and $[{R P}^{n}]$ pair to $1$ , as asserted.

1.2F2F3

The line bundle computation [F2] gives $w (γ) = 1 + x$ by the last calculation in [F3], and [F3] gives $T {R P}^{n} \oplus ε^{1} ≅ (n + 1) γ$ . Applying the Whitney formula and the trivial-summand stability [F2] to this isomorphism yields $w (T {R P}^{n}) = w (T {R P}^{n} \oplus ε^{1}) = w (γ)^{n + 1} = (1 + x)^{n + 1}$ , and naturality makes the identification independent of the chosen isomorphism because isomorphic bundles have equal classes. Expanding in $F_{2} [x] / (x^{n + 1})$ gives $w_{i} (T {R P}^{n}) = (\binom{n + 1}{i}) x^{i}$ for $0 \leq i \leq n$ .

2.1F4step 1.1step 1.2

Let $I = (i_{1}, \dots, i_{r})$ be a partition of $n$ and $w^{I} = w_{i_{1}} \dots w_{i_{r}}$ . By step 1.2,[F4] $w^{I} [{R P}^{n}] = ⟨ \prod_{j} (\binom{n + 1}{i_{j}}) x^{i_{j}}, [{R P}^{n}] ⟩ = (\prod_{j} (\binom{n + 1}{i_{j}})) ⟨ x^{n}, [{R P}^{n}] ⟩ = \prod_{j} (\binom{n + 1}{i_{j}}) m o d 2,$ using step 1.1 for the top evaluation; for the monomial of total degree $n$ with $r = 1$ and $i_{1} = n$ this gives the top number $w_{n} [{R P}^{n}] = (\binom{n + 1}{n}) = n + 1 m o d 2$ , which is $1$ for even $n$ and $0$ for odd $n$ .

3.1F3F5F6step 1.1step 2.1construct

For even $n = 2 k$ the top number is $1$ , so [F5] obstructs null-cobordism. If $n = 2^{s} - 1$ with $s \geq 1$ , characteristic two gives $(1 + x)^{2^{s}} = 1 + x^{2^{s}} = 1$ in the truncated ring; all positive-degree characteristic numbers vanish. For the stated boundary witnesses put $L = γ^{\otimes 2} \to {C P}^{k}$ , with its tensor metric. Its unit disk bundle is a compact smooth manifold with boundary its unit circle bundle: local smooth unitary frames give charts $U \times D^{2}$ , with boundary $U \times S^{1}$ , and finitely many compact trivializing neighbourhoods cover the compact base. The smooth map $S^{2 k + 1} \to S (L)$ , $v \mapsto ([v], v \otimes v)$ , is surjective and identifies precisely $v$ and $- v$ . In a local unitary frame it is the circle map $z \mapsto z^{2}$ , so the induced bijection ${R P}^{2 k + 1} \to S (L)$ and its local inverses are smooth. Taking $k = 0, 1, 3$ gives the three claimed boundaries.

4.1F2F4F5step 1.1step 3.1∎

For $n = 0$ the empty characteristic monomial is $1$ and evaluates to $1$ on the point, so this case is nonbounding; it is excluded from the $s \geq 1$ vanishing assertion. For $n = 1$ the above witness is the disk over a point. The empty manifold is allowed by the library conventions and has zero numbers, though it is not a member of the projective-space family. The calculation and explicit witnesses use no choice beyond the declared characteristic-class and duality suppliers.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

79 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

John Milnor and James Stasheff, Characteristic Classes (original pagination; chapters 16-18 of the re-typeset scan) (standard reference, not scraped)
Daniel S. Freed, Bordism: Old and New (lecture notes, UT Austin, Fall 2012) (standard reference, not scraped)
Tom Weston, An Introduction to Cobordism Theory (standard reference, not scraped)