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.

Multiplicativity of the signature on products of projective spaces

Example

Assume AC, inherited from the signature-product theorem. Give ${C P}^{2} \times {C P}^{2}$ the product orientation and the product smooth structure. Then $σ ({C P}^{2} \times {C P}^{2}) = σ ({C P}^{2}) σ ({C P}^{2}) = 1 \cdot 1 = 1,$ and the L-genus of the product is also $1$ . Since $[{C P}^{2}]$ is the first of the polynomial generators of $Ω_{*}^{S O} \otimes Q$ , this verifies multiplicativity of the signature on the square of the degree-four generator of the graded ring $Ω_{*}^{S O} \otimes Q$ , whose square lies in degree eight.

Facts & Assumptions

Given: AC; the closed oriented smooth $4$ -manifold ${C P}^{2}$ with the complex orientation; the product ${C P}^{2} \times {C P}^{2}$ with the product orientation and product smooth structure.

[F1]

For closed oriented smooth manifolds $M^{4 a}$ and $N^{4 b}$ with the product orientation, $σ (M \times N) = σ (M) σ (N)$ (The signature is multiplicative under Cartesian products).

[F2]

The complex projective plane satisfies $σ ({C P}^{2}) = 1$ (The signature and the L-genus agree on complex projective space).

[F3]

For $P = {C P}^{2 k_{1}} \times \dots \times {C P}^{2 k_{r}}$ with the product orientation, $k_{i} \geq 1$ , one has $σ (P) = 1 = L [P]$ (The signature and the L-genus agree on products of complex projective spaces).

[F4]

The products ${C P}^{2 j_{1}} \times \dots \times {C P}^{2 j_{r}}$ over partitions form a $Q$ -basis of $Ω_{4 k}^{S O} \otimes Q$ ; equivalently $Ω_{*}^{S O} \otimes Q$ is the polynomial algebra on the classes $[{C P}^{2}], [{C P}^{4}], [{C P}^{6}], \dots$ (Products of complex projective spaces span rational oriented bordism).

[F5]

Products of closed oriented smooth manifolds carry the product orientation and the canonical product smooth structure, hence are again closed oriented smooth (Product orientations, Products of smooth manifolds have a canonical product smooth structure).

Verification

technique · direct; instantiate multiplicativity on the product and compare with the L-genus value

1.1givenF2

By The signature and the L-genus agree on complex projective space, $σ ({C P}^{2}) = 1$ .

1.2givenF1F5

By [F5], ${C P}^{2} \times {C P}^{2}$ is a closed oriented smooth $8$ -manifold with the product orientation, so [F1] with $M = N = {C P}^{2}$ gives $σ ({C P}^{2} \times {C P}^{2}) = σ ({C P}^{2}) σ ({C P}^{2})$ .

2.1step 1.2F2

By [F2], $σ ({C P}^{2}) = 1$ , so step 1.2 gives $σ ({C P}^{2} \times {C P}^{2}) = 1 \cdot 1 = 1$ .

3.1givenF3

By [F3] with $k_{1} = k_{2} = 1$ , the L-genus of the product is $L [{C P}^{2} \times {C P}^{2}] = 1$ , agreeing with the signature value of step 2.1.

4.1step 2.1step 3.1F4∎

By [F4] the class $[{C P}^{2}]$ is the first polynomial generator of $Ω_{*}^{S O} \otimes Q$ , so ${C P}^{2} \times {C P}^{2}$ represents its square in degree eight; steps 2.1 and 3.1 exhibit multiplicativity there, the signature of the product being the product of the factor signatures and the L-genus agreeing.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

87 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

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