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

Pontryagin numbers of the complex projective plane

Example

Assume AC (The Axiom of Choice), inherited from the tangent-bundle and Pontryagin-number suppliers. For ${C P}^{2}$ with its complex orientation, $H^{*} ({C P}^{2}; Z) = Z [x] / (x^{3})$ with $x = c_{1} (γ^{*})$ and $⟨ x^{2}, [{C P}^{2}] ⟩ = 1$ . Its total Pontryagin class is $(1 + x^{2})^{3} = 1 + 3 x^{2}$ in this truncated ring. Its unique degree-four Pontryagin number is therefore $p_{1} [{C P}^{2}] = 3$ . Consequently it is not an oriented boundary and represents a nonzero class of $Ω_{4}^{S O}$ . This supplies the degree-four numerical normalization for later signature computations without assuming that the test manifold is already known to generate integral bordism.

Facts & Assumptions

Given: The complex projective plane ${C P}^{2}$ with its complex orientation and the tautological complex line $γ$ with dual $γ^{*}$ , and $x = c_{1} (γ^{*})$ .

[F1]

The tangent bundle of complex projective space and its Pontryagin classes gives the Euler sequence, the splitting, and the computations $H^{*} ({C P}^{2}; Z) = Z [x] / (x^{3})$ , $⟨ x^{2}, [{C P}^{2}] ⟩ = 1$ , $c (T {C P}^{2}) = (1 + x)^{3}$ and $p (T {C P}^{2}) = (1 + x^{2})^{3}$ , hence $p_{1} (T {C P}^{2}) = 3 x^{2}$ and $p_{k} (T {C P}^{2}) = (\binom{3}{k}) x^{2 k}$ .

[F2]

Pontryagin numbers of a closed oriented manifold defines $p_{J} [{C P}^{2}] = ⟨ p_{j_{1}} \dots p_{j_{r}}, [{C P}^{2}] ⟩$ for a partition $J$ of the dimension divided by four, here the single partition $(1)$ of $1$ , with the Kronecker pairing of Kronecker evaluation pairing.

[F3]

Oriented boundaries have zero Pontryagin numbers: a closed oriented $4 k$ -manifold with a nonzero Pontryagin number is not an oriented boundary, and Null-cobordant closed manifolds, Unoriented and oriented bordism groups identify the oriented boundary classes with the zero class of $Ω_{4}^{S O}$ .

[F4]

Zero-dimensional bordism groups identifies $Ω_{0}^{S O} ≅ Z$ through the signed count and its positive point generator; no assertion about $Ω_{4}^{S O}$ is part of that result.

Verification

1.1F1

By [F1] the truncated ring is $Z [x] / (x^{3})$ , so $x^{3} = 0$ and $x^{2} \neq 0$ with $⟨ x^{2}, [{C P}^{2}] ⟩ = 1$ . The total Pontryagin class is $p (T {C P}^{2}) = (1 + x^{2})^{3} = 1 + 3 x^{2} + 3 x^{4} + x^{6}$ , and all powers of $x$ with exponent at least three vanish in the truncated ring, so $p (T {C P}^{2}) = 1 + 3 x^{2}$ . Thus $p_{1} = 3 x^{2}$ and $p_{2} = 0$ , the latter by the cohomological dimension, not the rank cutoff: the real tangent rank is $4$ and $2 \cdot 2 = 4$ does not exceed it.

1.2F2step 1.1

The only partition of $1$ is $(1)$ , so by [F2] the unique degree-four Pontryagin number is $p_{1} [{C P}^{2}] = ⟨ 3 x^{2}, [{C P}^{2}] ⟩ = 3 ⟨ x^{2}, [{C P}^{2}] ⟩ = 3,$ where the evaluation uses the normalization of step 1.1 and the linearity of the Kronecker pairing on classes [F2]. No other partition contributes, and classes of the wrong degree evaluate to zero by the conventions of [F2].

2.1F3step 1.2

Since $p_{1} [{C P}^{2}] = 3 \neq 0$ , the manifold is not an oriented boundary by [F3], so its class in $Ω_{4}^{S O}$ is nonzero: a boundary class has all Pontryagin numbers zero, and here $p_{1}$ does not vanish. The empty manifold and the zero class are excluded by [F3]; in particular $[{C P}^{2}] \neq 0$ without any appeal to a classification of $Ω_{4}^{S O}$ .

3.1F1F2F4step 1.1step 2.1∎

Normalization and boundary cases. The degree-zero oriented bordism group is $Ω_{0}^{S O} ≅ Z$ generated by the positively oriented point [F4], whose only number is $p_{\emptyset} = ⟨ 1, [p t] ⟩ = 1$ ; this identifies the degree-zero normalization but makes no claim about $Ω_{4}^{S O}$ , and in particular no generator or rank statement for degree four is asserted here. For dimension zero the example reduces to that point computation, and the empty manifold has value $0$ . The formulas of step 1.1 include the degenerate case $x^{3} = 0$ through the truncation, and the cited suppliers carry their own choice declarations, so the verification adds no choice.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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)