TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-06 (claude-sonnet-5)

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\ge1$ , the map $H(x,t)=((1-t)+t/\lVert x\rVert_2)x$ is continuous on $(\mathbb{R}^n\setminus\{0\})\times[0,1]$ , starts at $x$ , ends at radial normalisation, fixes the unit sphere, and never reaches $0$

Statement

For $n\ge1$ , put $P=\mathbb R^n\setminus\{0\}$ and define

$H:P\times[0,1]\to P,\qquad H(x,t)=\bigl((1-t)+t/\lVert x\rVert_2\bigr)x.$

Then $H$ is continuous, $H(x,0)=x$ , $H(x,1)=x/\lVert x\rVert_2$ , $H(s,t)=s$ for $s\in S^{n-1}$ , and $H(x,t)\ne0$ .

Facts & Assumptions

Given: $x\in P$ and $t\in[0,1]$ .

[L1]

Radial normalisation is continuous on $P$ (Radial normalisation $x\mapsto x/\lVert x\rVert_2$ is continuous on $\mathbb{R}^n\setminus\{0\}$ ).

[L2]

Coordinate projections and the map into a product are continuous as stated by the product universal property (A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice, The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space).

[L3]

The Euclidean norm is continuous for the Euclidean metric and is positive away from $0$ , and the unit sphere consists of its norm-one points (The finite and reverse triangle inequalities for a norm; and for $n \ge 1$ every norm $N$ on $\mathbb{R}^n$ satisfies $N(x) \le C\lVert x\rVert_1$ and is Lipschitz, hence continuous, for $d_2$ , Euclidean spheres and closed balls as subspaces of $\mathbb{R}^n$ ).

[L4]

For maps on a subset of a metric space, sums, scalar multiples and pointwise products of continuous real-valued functions are continuous, and a vector-valued map is continuous exactly when its coordinate functions are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions, clauses 1 and 3, the product being the case $m = 1$ of the inner product); composites of continuous maps are continuous (Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous); and $u \mapsto 1/u$ is continuous on $\mathbb{R} \setminus \{0\}$ , this being clause 4 of (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function) with $A = \mathbb{R}$ , numerator $1$ and denominator the identity.

[L5]

A map into a subspace is continuous exactly when its composite with the ambient inclusion is continuous (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

Proof

technique · direct

1.1

The scalar $c(x,t):=(1-t)+t/\lVert x\rVert_2$ is positive, since $1-t\ge0$ , $t\ge0$ , and $\lVert x\rVert_2>0$ .

1.2

The coordinate projections on $P\times[0,1]$ are continuous by [L2]. By [L3] the map $x\mapsto\lVert x\rVert_2$ is continuous on $P$ and never $0$ there, so composing it with $u\mapsto 1/u$ gives a continuous $x\mapsto 1/\lVert x\rVert_2$ by [L4]; hence $c(x,t)=(1-t)+t/\lVert x\rVert_2$ is continuous, being built from continuous functions by sums, scalar multiples and products as in [L4], and each coordinate $H_i(x,t)=c(x,t)x_i$ is continuous. Componentwise continuity in [L4] makes $H$ continuous as a map into $\mathbb R^n$ .

L1L2L3L4

1.3

Substituting $t=0$ and $t=1$ gives $H(x,0)=x$ and $H(x,1)=x/\lVert x\rVert_2$ . If $s\in S^{n-1}$ , then $\lVert s\rVert_2=1$ and $H(s,t)=s$ .

2.1

Since $c(x,t)>0$ and $x\ne0$ , $H(x,t)\ne0$ . Hence $H$ takes values in $P$ , and [L5] makes it continuous as a map $P\times[0,1]\to P$ .

step 1.1step 1.2L5

3.1

These identities and step 2.1 prove the statement.

step 2.1step 1.3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 161 results over 28 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Deformation retract (standard reference, not scraped)