Encyclopedia Foundation Foundation Linking Vanishing Low Dim Continuous Injective Circle Self Surjective

ARTICLE 3 claims 3 theorems

Foundation Linking Vanishing Low Dim Continuous Injective Circle Self Surjective

A continuous one-to-one map from a circle to itself must cover every point, a fact that anchors why linking can only be detected in higher dimensions.

Verify this page

The circle's self-map theorem

The circle, the set of points at a fixed distance from a center, has a property that seems too strong to be true: any continuous function from the circle to itself that never sends two different points to the same point must also hit every point of the circle. In mathematical language, a continuous injective self-map of the circle is surjective. The proof is short and visual. If such a map missed a point, you could use stereographic projection, the standard way of flattening a sphere onto a plane by projecting from a chosen point, to turn the map into a continuous one-to-one function from the circle into the real number line. But no such function exists: removing the preimage of a middle value would leave the circle connected, while the image would be split into two separated pieces, a contradiction.

This fact is classical and has been known in essence since the nineteenth century, when mathematicians like Camille Jordan and others formalized the behavior of continuous curves. It is a special case of the more general theorem that a continuous injective map from a compact space to a Hausdorff space is a homeomorphism onto its image, though the circle case carries extra force because the image must be the whole circle. The theorem also underlies why a circle cannot be embedded in a line, a fact that seems obvious but requires proof: the circle is connected in a way that the line is not.

In Recognition Science, the framework's machine-checked library of formal theorems restates this result as continuous_injective_circle_self_surjective, a theorem in its formal system. The framework uses the result to prove that its detector for nontrivial linking, a tool that measures whether a circle's complement has a certain algebraic structure, fails in dimension one. Because every embedded circle fills the entire one-dimensional sphere, its complement is empty, and the algebraic invariant vanishes. The same detector also fails in dimension zero, where the sphere is just two points. The formal library proves both failures, establishing that linking, in the framework's sense, can only be detected starting in dimension two.

What the theorem does not claim is broader. It does not say that all continuous self-maps of the circle are surjective; the map that sends every point to a single point is continuous and injective nowhere. It does not say that injective continuous maps between higher-dimensional spheres are surjective, and in fact they are not: a circle can be embedded in a two-dimensional sphere without filling it. The theorem is specifically about the one-dimensional sphere mapping to itself, and its role in the framework is to close off the low-dimensional cases of a linking detector, not to establish a general principle about spheres.

THEOREM continuous_injective_circle_self_surjective · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
continuous_injective_circle_self_surjective · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:178 
/-- A continuous injection of the metric circle into itself is surjective:
if it missed a point, composing with the stereographic projection from that
point would give a continuous injection of the circle into `ℝ¹`. -/
theorem continuous_injective_circle_self_surjective
    (f₀ : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) →
      ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1))
    (hc : Continuous f₀) (hinj : Function.Injective f₀) :
    Function.Surjective f₀ := by
  intro p
  by_contra hp
  push_neg at hp
  haveI fact2 : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 1 + 1) :=
    ⟨by norm_num [finrank_euclideanSpace_fin]⟩
  set φ := stereographic' (1 : ℕ) p with hφ
  have hmem : ∀ x, f₀ x ∈ φ.source := by
    intro x
    rw [hφ, stereographic'_source]
    exact Set.mem_compl_singleton_iff.mpr (hp x)
  have hφc : Continuous fun x => φ (f₀ x) :=
    φ.continuousOn.comp_continuous hc hmem
  set g : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) → ℝ :=
    fun x => (φ (f₀ x)) 0 with hg
  have hgc : Continuous g :=
    (EuclideanSpace.proj (0 : Fin 1)).continuous.comp hφc
  have hginj : Function.Injective g := by
    intro x y hxy
    apply hinj
    apply φ.injOn (hmem x) (hmem y)
    ext i
    obtain rfl : i = (0 : Fin 1) := Subsingleton.elim _ _
    exact hxy
  exact (no_continuous_injective_circle_to_real g hgc hginj).elim
THEOREM not_detects_one · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
not_detects_one · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:211 
/-- No embedded circle in the 1-sphere has homologically nontrivial
complement: the embedding is surjective, so the complement is empty, and
singular homology of the empty space vanishes in degree `1`. -/
theorem not_detects_one : ¬ DetectsNontrivialLinking 1 := by
  rintro ⟨f, hemb, hH⟩
  apply hH
  -- the underlying self-map of the metric circle
  set f₀ : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) →
      ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) :=
    fun x =>
      (show ULift.{0} ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) from
        f (show ↥(TopCat.sphere.{0} 1) from ULift.up x)).down with hf₀
  have hc : Continuous f₀ := by
    exact continuous_uliftDown.comp (f.continuous.comp continuous_uliftUp)
  have hinj : Function.Injective f₀ := by
    intro x y h
    have h2 : f (ULift.up x) = f (ULift.up y) := ULift.down_injective h
    have h3 := hemb.injective h2
    exact congrArg ULift.down h3
  have hsurj := continuous_injective_circle_self_surjective f₀ hc hinj
  haveI hE : IsEmpty {x : TopCat.sphere.{0} 1 // x ∉ Set.range f} := by
    constructor
    rintro ⟨x, hx⟩
    obtain ⟨y, hy⟩ := hsurj
      (show ULift.{0} ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) from x).down
    exact hx ⟨ULift.up y, ULift.down_injective hy⟩
  haveI hTD : TotallyDisconnectedSpace {x : TopCat.sphere.{0} 1 // x ∉ Set.range f} := by
    constructor
    intro t _ _ x hx
    exact (hE.false x).elim
  haveI : TotallyDisconnectedSpace
      ↥(TopCat.of {x : TopCat.sphere.{0} 1 // x ∉ Set.range f}) := hTD
  exact AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace
    (ModuleCat ℤ) 1 (ModuleCat.of ℤ ℤ)
    (TopCat.of {x : TopCat.sphere.{0} 1 // x ∉ Set.range f}) one_ne_zero
THEOREM not_detects_zero · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
not_detects_zero · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:75 
/-- No embedded circle in the 0-sphere has homologically nontrivial
complement: every subspace of the two-point space `S⁰` is totally
disconnected, so its first singular homology vanishes. -/
theorem not_detects_zero : ¬ DetectsNontrivialLinking 0 := by
  rintro ⟨f, -, hH⟩
  apply hH
  haveI hTD : TotallyDisconnectedSpace ↥(TopCat.sphere.{0} 0) := by
    show TotallyDisconnectedSpace
      (ULift.{0} ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1))
    infer_instance
  haveI : TotallyDisconnectedSpace
      ↥(TopCat.of {x : TopCat.sphere.{0} 0 // x ∉ Set.range f}) :=
    (inferInstance :
      TotallyDisconnectedSpace {x : TopCat.sphere.{0} 0 // x ∉ Set.range f})
  exact AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace
    (ModuleCat ℤ) 1 (ModuleCat.of ℤ ℤ)
    (TopCat.of {x : TopCat.sphere.{0} 0 // x ∉ Set.range f}) one_ne_zero

What this page does not claim

The theorem does not claim that all continuous self-maps of the circle are surjective. The theorem does not claim that injective continuous maps between higher-dimensional spheres are surjective. The theorem does not claim that the framework derives the physical existence of three-dimensional space from this result alone.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND