Alphabeta Math
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≥1, radial normalisation is a deformation retraction of Rn∖{0} onto Sn−1

Statement

Let n≥1, put P=Rn∖{0}, and let Sn−1⊆P be the unit sphere. Radial normalisation

r:P→Sn−1,r(x)=x∥x∥2,

is a retraction, and

H(x,t)=((1−t)+t∥x∥2)x

is a deformation retraction of P onto Sn−1.

Facts & Assumptions

Given: A natural n≥1, P=Rn∖{0} and Sn−1={x:∥x∥2=1}.

[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.1

If s∈Sn−1 then ∥s∥2=1, so r(s)=s. Thus the continuous map r of [L1] is a retraction.

L1algebra
1.2

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∈Sn−1 and t∈I.

L2
2.1

Steps 1.1 and 1.2 satisfy [A1], so (r,H) is a deformation retraction of P onto Sn−1.

step 1.1step 1.2A1∎

Depends on

Used by

Dependency tree · two levels

17 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