PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

An odd sphere admits a nowhere zero tangent vector field

Statement

For $n = 2 m - 1 \geq 1$ , identify $R^{2 m}$ with $C^{m}$ . The map $v : S^{n} \to R^{2 m}$ given by $v (x) = i x$ is a continuous unit tangent vector field.

Facts & Assumptions

Given: The objects and hypotheses in the statement above.

Proof

1.1

In real coordinates, $v (x_{1}, x_{2}, \dots, x_{2 m}) = (- x_{2}, x_{1}, \dots, - x_{2 m}, x_{2 m - 1})$ . This linear map is continuous and $⟨ v (x), x ⟩ = \sum_{j = 1}^{m} (- x_{2 j} x_{2 j - 1} + x_{2 j - 1} x_{2 j}) = 0$ .

givenalgebra

2.1

Moreover $∣ v (x) ∣^{2} = \sum_{j = 1}^{2 m} x_{j}^{2} = 1$ on the sphere, so the field never vanishes. For $m = 1$ this is the usual quarter-turn field on the circle.

step 1.1algebra∎

Used by

A sphere has a nowhere zero tangent vector field iff its dimension is odd Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Hatcher, Algebraic Topology, Theorem 2.28, positive direction p.135 (standard reference, not scraped)