ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated

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 hairy-ball theorem for even spheres

Example

Assume the Axiom of Choice (The Axiom of Choice) for the applications of Poincare-Hopf below.

Let $m \geq 1$ and $M = S^{2 m} \subseteq R^{2 m + 1}$ . Then $χ (S^{2 m}) = 1 + 1 = 2$ (Euler characteristic of a compact manifold), so by A nowhere-zero vector field forces zero Euler characteristic no smooth vector field on $S^{2 m}$ can be nowhere zero (A smooth vector field is a smooth section of the tangent bundle): every smooth field on an even-dimensional sphere has at least one zero. This recovers the classical hairy-ball theorem by the Euler-characteristic route rather than by the degree of the antipodal map.

Facts & Assumptions

Given: The even-dimensional sphere $S^{2 m} \subseteq R^{2 m + 1}$ , $m \geq 1$ .

[F1]

$H_{0} (S^{2 m}; Q) ≅ Q$ , $H_{2 m} (S^{2 m}; Q) ≅ Q$ and all other rational homology groups vanish (Homology of spheres).

[F2]

A closed manifold admitting a nowhere-zero smooth vector field has $χ = 0$ (A nowhere-zero vector field forces zero Euler characteristic, Euler characteristic of a compact manifold).

Verification

1.1F1algebra

By [F1] the only nonzero rational Betti numbers of $S^{2 m}$ are in degrees $0$ and $2 m$ , both equal to $1$ , so the alternating sum of the definition gives $χ (S^{2 m}) = (- 1)^{0} \cdot 1 + (- 1)^{2 m} \cdot 1 = 2 \neq 0$ .

2.1F2step 1.1algebra∎

If a smooth field on $S^{2 m}$ were nowhere zero, [F2] would force $χ (S^{2 m}) = 0$ , contradicting step 1.1; hence every smooth vector field on an even-dimensional sphere has at least one zero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Victor Guillemin and Alan Pollack, Differential Topology (Prentice-Hall 1974; complete PDF) (standard reference, not scraped)
Allen Hatcher, Algebraic Topology, Section 2.2 (standard reference, not scraped)