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.

The diagonal in the two-sphere has self-intersection two

Example

Assume AC. Let $S^{2} \subseteq R^{3}$ carry its induced orientation and give $S^{2} \times S^{2}$ the product orientation. Then the diagonal $Δ \subseteq S^{2} \times S^{2}$ is a closed oriented embedded surface with $2 \dim Δ = \dim (S^{2} \times S^{2})$ and $Δ \cdot Δ = ⟨ e (T S^{2}), [S^{2}] ⟩ = 2.$ The value $2$ is computed from the explicit tangent field $X (p) = e_{3} - z p$ , whose zeros are the two poles with local index $+ 1$ each; it previews the Euler characteristic $χ (S^{2}) = 2$ of the later Euler/index pair (not used here).

Facts & Assumptions

Given: AC, the unit sphere $S^{2} \subseteq R^{3}$ with its induced orientation, the product $S^{2} \times S^{2}$ with the product orientation, its diagonal and the explicit field $X (p) = e_{3} - z p$ .

[F1]

The diagonal $Δ \subseteq S^{2} \times S^{2}$ is a closed embedded surface of dimension $2$ with $2 \cdot 2 = 4 = \dim (S^{2} \times S^{2})$ (The diagonal is an embedded submanifold, Products of smooth manifolds have a canonical product smooth structure).

[F2]

The normal bundle of the diagonal is canonically $T M$ , orientation-preservingly when $Δ_{M}$ carries the orientation transported from $M$ , with the tangent-first normal orientation (The normal bundle of the diagonal is canonically the tangent bundle, Product orientations, Canonical tangent and cotangent splittings for products).

[F3]

The self-intersection is $Δ \cdot Δ = ⟨ e (ν_{Δ}), [Δ] ⟩ = ⟨ e (T M), [M] ⟩$ (The self-intersection number is the Euler number of the normal bundle).

[F4]

$S^{2}$ is the unit sphere, the regular level $∣ p ∣^{2} = 1$ , with tangent space $T_{p} S^{2} = \ker (v \mapsto 2 p \cdot v) = p^{⊥}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ , A regular level set is an embedded submanifold, The tangent space of a regular level set is the kernel).

[F5]

The local sign of the push-off equals the local zero index of the section, so the signed zero count is the self-intersection number (Normal push-off zeros are the self-intersection points).

Verification

technique · identify the normal bundle and compute the two zero signs in pole charts

1.1F1F2F3given

$Δ$ is closed embedded of dimension $2$ with $2 \cdot 2 = 4 = \dim (S^{2} \times S^{2})$ [F1], so [F3] gives $Δ \cdot Δ = ⟨ e (ν_{Δ}), [Δ] ⟩$ . By [F2] the normal identification is the canonical one and is orientation-preserving with the orientation of $Δ$ transported from $S^{2}$ , so $Δ \cdot Δ = ⟨ e (T S^{2}), [S^{2}] ⟩$ .

2.1F3F4F5step 1.1algebra∎

In the projection charts of the two poles $(x, y) \mapsto (x, y, \pm \sqrt{1 - x^{2} - y^{2}})$ the given field $X (p) = e_{3} - z p$ , tangent because $(e_{3} - z p) \cdot p = z - z ∣ p ∣^{2} = 0$ by [F4], has exactly the two zeros $\pm e_{3}$ , with local components $(- z x, - z y)$ and derivatives $- I_{2}$ at the north pole and $I_{2}$ at the south pole. Both determinants are $+ 1$ , so each zero has index $+ 1$ and the signed zero count of $T S^{2}$ is $2$ ; [F5] and [F3] identify that count with $⟨ e (T S^{2}), [S^{2}] ⟩$ . Hence $Δ \cdot Δ = 2$ , which previews the Euler characteristic $χ (S^{2}) = 2$ of the later Euler/index pair (not used here).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

77 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

Ralph L. Cohen, Bundles, Manifolds, and Homotopy (author draft bookR4) (standard reference, not scraped)
Victor Guillemin and Alan Pollack, Differential Topology (Prentice-Hall, 1974; complete 236-page PDF) (standard reference, not scraped)
Eleny-Nicoleta Ionel (notes by Andrew Lin), Stanford Math 215B Differential Topology, Winter 2023 (complete 63-page lecture notes) (standard reference, not scraped)