Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedprecheck 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≥1, the map H(x,t)=((1−t)+t/∥x∥2)x is continuous on (Rn∖{0})×[0,1], starts at x, ends at radial normalisation, fixes the unit sphere, and never reaches 0

Statement

For n≥1, put P=Rn∖{0} and define

H:P×[0,1]→P,H(x,t)=((1−t)+t/∥x∥2)x.

Then H is continuous, H(x,0)=x, H(x,1)=x/∥x∥2, H(s,t)=s for s∈Sn−1, and H(x,t)≠0.

Facts & Assumptions

Given: x∈P and t∈[0,1].

[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↦1/u is continuous on R∖{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=R, numerator 1 and denominator the identity.

Proof

technique · direct
1.1

The scalar c(x,t):=(1−t)+t/∥x∥2 is positive, since 1−t≥0, t≥0, and ∥x∥2>0.

L3
1.2

The coordinate projections on P×[0,1] are continuous by [L2]. By [L3] the map x↦∥x∥2 is continuous on P and never 0 there, so composing it with u↦1/u gives a continuous x↦1/∥x∥2 by [L4]; hence c(x,t)=(1−t)+t/∥x∥2 is continuous, being built from continuous functions by sums, scalar multiples and products as in [L4], and each coordinate Hi(x,t)=c(x,t)xi is continuous. Componentwise continuity in [L4] makes H continuous as a map into Rn.

L1L2L3L4
1.3

Substituting t=0 and t=1 gives H(x,0)=x and H(x,1)=x/∥x∥2. If s∈Sn−1, then ∥s∥2=1 and H(s,t)=s.

L3
2.1

Since c(x,t)>0 and x≠0, H(x,t)≠0. Hence H takes values in P, and [L5] makes it continuous as a map P×[0,1]→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 · two levels

63 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