isEmbedding_toSphMap
plain-language theorem explainer
If a continuous map from the circle into the D-sphere is a topological embedding in the universe-lifted sphere model, the corresponding map in the unit-sphere model is also an embedding. Anyone transferring linking or complement-homology statements between the two sphere presentations cites this. The proof is a short composition of the given embedding with the ULift homeomorphism and its inverse.
Claim. For every natural number $D$ and every continuous map $f : S^1 \to S^D$ in the universe-lifted topological sphere model that is a topological embedding, the corresponding continuous map between the unit-sphere models of $S^1$ and $S^D$ is also a topological embedding.
background
The module works with two presentations of spheres: the universe-lifted topological sphere (built with ULift over the metric sphere) and the unit-sphere model used by the singular-sphere geometry layer. Linking and complement homology are stated most naturally on the unit-sphere side, while some embedding data arrives in the lifted model.
The conversion map strips the universe-lift wrappers coordinatewise. Given a continuous map $f$ from the lifted circle to the lifted $D$-sphere, it produces a continuous map between the corresponding unit spheres. A topological embedding is a map that is a homeomorphism onto its image with the subspace topology.
This sits in the high-dimensional linking-vanishing development. For $D \neq 3$, embedded circles should not detect nontrivial linking in the homology of the complement, which is the topological half of the forcing that spatial dimension equals three (T8; linking requires $D = 3$).
proof idea
Term-mode proof by composing three embeddings. Every homeomorphism is an embedding, so the universe-lift homeomorphism and its inverse are embeddings. Pre- and post-composing the given embedding $f$ with those two homeomorphisms yields an embedding of the unit-sphere models: lift-embedding composed with $f$, then composed with the inverse-lift embedding. No case analysis on $D$ is required.
why it matters
Feeds not_detects_of_arcAcyclic, which states that, granting arc-complement acyclicity, no embedded circle in $S^D$ for $D \ge 1$, $D \neq 3$ has a homologically nontrivial complement. That theorem applies high-dimensional vanishing of $H_1$ of the complement to the transported map, and needs this lemma to know the transported map remains an embedding.
In the Recognition Science chain this is infrastructure for dimensional forcing: nontrivial circle linking is special to $D = 3$ (T8 spatial dimension; AlphaDerivation records that linking requires $D = 3$). Without model-transfer of the embedding property, the vanishing argument cannot be stated uniformly on the unit-sphere side where the homology computation lives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.