ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Self-intersection of the zero section in an oriented plane bundle

Example

Assume AC. Let $S^{2} \subseteq R^{3}$ be the unit sphere with its induced orientation and let $E$ be a smooth oriented rank-2 real bundle over $S^{2}$ ; write $Z \subseteq E$ for the zero section, a compact closed oriented surface embedded in the boundaryless $4$ -manifold $E$ , oriented by base tangent first and fibre second. Then $Z \cdot Z = ⟨ e (E), [S^{2}] ⟩ \in Z$ . Two cases are computed. (a) For the trivial bundle $E = S^{2} \times R^{2}$ the constant section $x \mapsto (x, (1, 0))$ is nowhere zero, so $Z$ pushes off itself disjointly and $Z \cdot Z = 0$ . (b) For the tangent bundle $E = T S^{2}$ , the explicit field $X (p) = e_{3} - z p$ on $p = (x, y, z) \in S^{2}$ (the tangential projection of the constant field $e_{3}$ , i.e. the gradient of the height function for the induced Euclidean metric) is a smooth section vanishing exactly at the two poles $\pm e_{3}$ ; in the projection charts $(x, y) \mapsto (x, y, \pm \sqrt{1 - x^{2} - y^{2}})$ at the two poles its linearization is $- (x \partial_{x} + y \partial_{y}) + O (∣ (x, y) ∣^{2})$ at $e_{3}$ and $+ (x \partial_{x} + y \partial_{y}) + O (∣ (x, y) ∣^{2})$ at $- e_{3}$ , both with determinant $+ 1$ in dimension two, so both zeros are nondegenerate of index $+ 1$ and the signed zero count is $2$ ; hence $Z \cdot Z = 2$ . The trivial bundle realizes $0$ and the tangent bundle realizes $2$ ; no general clutching classification is asserted here.

Facts & Assumptions

Given: AC, the unit sphere $S^{2} \subseteq R^{3}$ with its induced orientation, an oriented rank-two real bundle $E \to S^{2}$ , its zero section $Z$ (a closed oriented surface in the boundaryless oriented four-manifold $E$ ) and the two bundles of the statement.

[F1]

For a closed oriented $A$ with $2 \dim A = \dim M$ the self-intersection satisfies $A \cdot A = ⟨ e (ν_{A}), [A] ⟩$ (The self-intersection number is the Euler number of the normal bundle).

[F2]

If an oriented bundle admits a nowhere-zero section then its Euler class vanishes, and the geometric consequences include $e (E) \cap [M] = 0$ and, when rank equals dimension, $⟨ e (E), [M] ⟩ = 0$ and vanishing integral self-intersections for nowhere-zero normal fields when the ambient manifold and embedded submanifold are integrally oriented and the normal orientation is their induced tangent-first orientation (A nowhere-zero section forces the Euler data to vanish).

[F3]

The local oriented intersection sign of the push-off equals the local zero index of the section, $ε = sign \det \partial_{ν} s_{x}$ (Normal push-off zeros are the self-intersection points).

[F4]

$S^{2}$ is the unit sphere in $R^{3}$ , and it is a regular level set of a smooth function, hence an embedded submanifold with $T_{p} S^{2} = 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 tangent bundle is the disjoint union of the tangent spaces and a smooth section assigns compatibly smooth vectors, so $X (p) = e_{3} - z p$ defines a smooth section of $T S^{2}$ (The tangent bundle as a disjoint union, Smooth sections, local sections, and support, Smoothness of a section is equivalent to smooth local components).

Verification

technique · apply the self-intersection/Euler-number theorem and compute the signed zero count of an explicit section

1.1F1F5given

By The zero section is a smooth embedding the zero section is embedded, and in bundle charts the splitting along it is $T E ∣_{Z} = T S^{2} \oplus E$ , so its quotient normal bundle is $E$ with the specified fibre orientation, and $Z$ is compact, so [F1] gives $Z \cdot Z = ⟨ e (ν_{Z}), [Z] ⟩ = ⟨ e (E), [S^{2}] ⟩$ .

2.1F2step 1.1

Case (a): the constant unit section $x \mapsto (x, (1, 0))$ is smooth and nowhere zero, so by [F2] both the Euler number and the self-intersection vanish: $⟨ e (E), [S^{2}] ⟩ = 0 = Z \cdot Z$ for the trivial bundle.

3.1F1F3F4F5step 1.1algebra∎

Case (b): $S^{2}$ is the regular level set $∣ p ∣^{2} = 1$ of a smooth function [F4] with $T_{p} S^{2} = p^{⊥}$ , so $X (p) = e_{3} - z p$ satisfies $X (p) \cdot p = z - z ∣ p ∣^{2} = 0$ and is a smooth section of $T S^{2}$ by [F5]. It vanishes iff $e_{3} = z p$ , i.e. iff $p = \pm e_{3}$ . In the projection charts $(x, y) \mapsto (x, y, \pm \sqrt{1 - x^{2} - y^{2}})$ near the poles the linearizations are $- (x \partial_{x} + y \partial_{y}) + O (∣ (x, y) ∣^{2})$ at $e_{3}$ and $+ (x \partial_{x} + y \partial_{y}) + O (∣ (x, y) ∣^{2})$ at $- e_{3}$ , whose Jacobians $- I$ and $+ I$ both have determinant $+ 1$ in dimension two, and the chart-orientation sign cancels between source and target in the local index [F3]. Hence both zeros are nondegenerate of index $+ 1$ and the signed zero count is $2$ ; [F1] and [F3] identify it with $Z \cdot Z$ and with $⟨ e (T S^{2}), [S^{2}] ⟩$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

83 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)
Eleny-Nicoleta Ionel (notes by Andrew Lin), Stanford Math 215B Differential Topology, Winter 2023 (complete 63-page lecture notes) (standard reference, not scraped)
John W. Milnor and James D. Stasheff, Characteristic Classes (Princeton University Press, 1974; complete PDF) (standard reference, not scraped)