TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-07-31

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.

For $n \geq 1$ , radial normalisation is a deformation retraction of $R^{n} ∖ {0}$ onto $S^{n - 1}$

Statement

Let $n \geq 1$ , put $P = R^{n} ∖ {0}$ , and let $S^{n - 1} \subseteq P$ be the unit sphere. Radial normalisation

$r : P \to S^{n - 1}, r (x) = \frac{x}{∥ x ∥_{2}},$

is a retraction, and

$H (x, t) = ((1 - t) + \frac{t}{∥ x ∥_{2}}) x$

is a deformation retraction of $P$ onto $S^{n - 1}$ .

Facts & Assumptions

Given: A natural $n \geq 1$ , $P = R^{n} ∖ {0}$ and $S^{n - 1} = {x : ∥ x ∥_{2} = 1}$ .

[L1]

Radial normalisation $r : P \to S^{n - 1}$ is continuous (Radial normalisation $x \mapsto x / ∥ x ∥_{2}$ is continuous on $R^{n} ∖ {0}$ , Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

[L2]

The displayed $H : P \times I \to P$ is continuous, begins at $x$ , ends at $r (x)$ , fixes every $s \in S^{n - 1}$ , and never reaches $0$ (For $n \geq 1$ , the map $H (x, t) = ((1 - t) + t / ∥ x ∥_{2}) x$ is continuous on $(R^{n} ∖ {0}) \times [0, 1]$ , starts at $x$ , ends at radial normalisation, fixes the unit sphere, and never reaches $0$ ).

[A1]

A deformation retraction onto $A$ is a retraction $r$ together with a homotopy from the identity to the inclusion followed by $r$ , fixed pointwise on $A$ (Retractions and deformation retracts, with a deformation retraction required to fix the retract pointwise).

Proof

technique · direct

1.1L1algebra

If $s \in S^{n - 1}$ then $∥ s ∥_{2} = 1$ , so $r (s) = s$ . Thus the continuous map $r$ of [L1] is a retraction.

1.2L2

By [L2], $H$ is a continuous homotopy in $P$ from ${id}_{P}$ to the inclusion followed by $r$ , and $H (s, t) = s$ for every $s \in S^{n - 1}$ and $t \in I$ .

2.1step 1.1step 1.2A1∎

Steps 1.1 and 1.2 satisfy [A1], so $(r, H)$ is a deformation retraction of $P$ onto $S^{n - 1}$ .

For $n \geq 1$ , radial normalisation is a deformation retraction of $R^{n} ∖ {0}$ onto $S^{n - 1}$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

For n≥1n≥1, radial normalisation is a deformation retraction of Rn∖{0}Rn∖{0} onto Sn−1Sn−1

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

For $n \geq 1$ , radial normalisation is a deformation retraction of $R^{n} ∖ {0}$ onto $S^{n - 1}$