LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

A degree-zero sphere map extends over the ball without zeros

Statement

Assume countable choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $m \geq 1$ and let $u : S^{m} \to S^{m}$ be a continuous map of degree $0$ (Degree of a map between oriented closed manifolds). Then $u$ is homotopic to a constant map, and there is a continuous nowhere-zero map $F : D^{m + 1} \to R^{m + 1} ∖ {0}$ with $D^{m + 1} = {\overline{B}}_{2} (0, 1)$ and $F ∣_{S^{m}} = u$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ). If $u$ is smooth, $F$ can be chosen smooth with $F (x) = u (x / ∣ x ∣)$ for every $x$ with $∣ x ∣ \geq \frac{2}{3}$ ; in particular $F$ restricts to $u$ on $S^{m}$ .

Facts & Assumptions

Given: $m \geq 1$ , a continuous map $u : S^{m} \to S^{m}$ of degree $0$ , and ${A C}_{ω}$ for the smooth clause.

[A1]

Countable choice is The Axiom of Countable Choice ( ${A C}_{ω}$ ); it is used only in [F3].

[F1]

For $m \geq 1$ and a continuous self-map $f$ of $S^{m}$ , the sphere degree of Degree of a self map of an oriented sphere reads the multiplier $f_{*} [S^{m}] = \deg (f) [S^{m}]$ on the integral top generator of $H_{m} (S^{m}; Z) ≅ Z$ given by Homology of spheres, while the degree of Degree of a map between oriented closed manifolds reads the multiplier of the fundamental classes of the two standard orientations; for $S^{m}$ these are the same integer. Homotopic maps have equal degree and $\deg (g \circ f) = \deg (g) \deg (f)$ ; every homotopy equivalence $S^{m} \to S^{m}$ has degree $1$ or $- 1$ ; the identity has degree $1$ and constant maps have degree $0$ (Degree is homotopy invariant and multiplicative under composition, Degree of identity constant reflection and antipodal sphere maps, Homotopic maps induce the same map on singular homology).

[F2]

For every $r \geq 1$ the degree is an isomorphism $π_{r} (S^{r}, b) \to Z$ ; hence two based self-maps of $S^{r}$ are homotopic through based maps if and only if their degrees agree, and the constant map represents the zero element (Based sphere maps are classified by degree).

[F3]

If two smooth maps between smooth manifolds are continuously homotopic, then they are smoothly homotopic (Continuously homotopic smooth maps are smoothly homotopic).

[F4]

The standard smooth step function $σ : R \to [0, 1]$ is smooth with $σ (t) = 0$ for $t \leq 0$ and $σ (t) = 1$ for $t \geq 1$ (The standard smooth step function).

[F5]

$S^{m} = {\overline{B}}_{2} (0, 1) ∖ B_{2} (0, 1) = \partial D^{m + 1}$ is the unit sphere in $R^{m + 1}$ and is contained in $R^{m + 1} ∖ {0}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

Proof

1.1F1F5algebra

Fix $b \in S^{m}$ . If $u (b) = b$ put $R : = id$ ; otherwise put $R (x) : = x - 2 ⟨ x, w ⟩ w / ∣ w ∣^{2}$ with $w : = u (b) - b \neq 0$ . A direct computation gives $∣ R (x) ∣ = ∣ x ∣$ , $R^{2} = id$ and $R (w) = - w$ , hence $R (u (b)) = R (b) + R (w) = u (b) - (u (b) - b) = b$ ; thus $R$ restricts to a self-map of $S^{m}$ and is its own continuous inverse, so $g : = R \circ u$ is a based self-map of $S^{m}$ at $b$ with $\deg g = \deg R \cdot \deg u = 0$ .

2.1F1F2step 1.1

By [F2] the degree is an isomorphism $π_{m} (S^{m}, b) \to Z$ , so $g$ , having degree $0$ , is based-homotopic to the constant map at $b$ ; applying the continuous map $R$ to that based homotopy exhibits a homotopy from $u = R^{- 1} \circ g$ to the constant map at $R (b)$ , proving that $u$ is homotopic to a constant.

3.1F2F5step 2.1algebra

Let $H : S^{m} \times [0, 1] \to S^{m}$ be a homotopy with $H_{0} = u$ and $H_{1} \equiv c$ , and define $F (0) : = c$ and $F (x) : = H (x / ∣ x ∣, 1 - ∣ x ∣)$ for $x \in D^{m + 1} ∖ {0}$ . Then $F$ is continuous away from $0$ as a composite of continuous maps, and for $x \to 0$ continuity at every point of $S^{m} \times {1}$ and a finite subcover of the compact sphere give $H (v, t) \to c$ uniformly in $v$ as $t \to 1$ , so $F (x) \to c$ ; on $S^{m}$ we have $1 - ∣ x ∣ = 0$ and $F (x) = H (x, 0) = u (x)$ ; and $F$ takes values in $S^{m} \subseteq R^{m + 1} ∖ {0}$ , so $F$ is nowhere zero.

4.1A1F3F4F5step 3.1constructalgebra∎

Suppose now that $u$ is smooth. By [F3] the continuously homotopic smooth maps $u$ and the constant $c$ are smoothly homotopic; let $H^{'}$ be a smooth homotopy from $u$ to $c$ and put $φ (t) : = σ (3 t - 1)$ , so that $φ$ is smooth with $φ (t) = 0$ for $t \leq 1 / 3$ and $φ (t) = 1$ for $t \geq 2 / 3$ by [F4]. Then $H^{''} (x, t) : = H^{'} (x, φ (t))$ is a smooth homotopy from $u$ to $c$ with $H^{''} (x, t) = u (x)$ for $t \leq 1 / 3$ , and we redefine $F (0) : = c$ , $F (x) : = H^{''} (x / ∣ x ∣, 1 - ∣ x ∣)$ for $x \neq 0$ . This $F$ is smooth on ${0 < ∣ x ∣ < 1}$ and equals $c$ for $0 < ∣ x ∣ \leq 1 / 3$ (where $1 - ∣ x ∣ \geq 2 / 3$ ), so it is smooth at $0$ as well; on the collar ${∣ x ∣ \geq 2 / 3}$ it equals $H^{''} (x / ∣ x ∣, 1 - ∣ x ∣) = u (x / ∣ x ∣)$ , a smooth function of $x$ on that collar because $∣ x ∣ \geq 2 / 3 > 0$ , and at the boundary points $∣ x ∣ = 1$ it equals $u (x)$ , where $x / ∣ x ∣ = x$ ; so $F$ is smooth on $D^{m + 1}$ with $F (x) = u (x / ∣ x ∣)$ for $∣ x ∣ \geq 2 / 3$ , and it takes values in $S^{m}$ , hence is nowhere zero.

Depends on

Used by

Opposite-index nondegenerate zeros cancel in a ball Lemma

Dependency tree · two levels

46 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)
Joel W. Robbin and Dietmar A. Salamon, Introduction to Differential Topology (web draft 2018, complete PDF) (standard reference, not scraped)