Encyclopedia Foundation Foundation Linking Vanishing Low Dim No Continuous Injective Circle To Real

ARTICLE 4 claims 4 theorems

Foundation Linking Vanishing Low Dim No Continuous Injective Circle To Real

A continuous, one-to-one map from a circle to a line is impossible; the proof is a compact fact of topology with a consequence for a framework's linking detector.

Verify this page

The circle cannot enter the line

A circle and a line are different in a way you can feel: a circle loops back on itself, a line runs off forever. Topology makes that difference precise. One classic result is that there is no continuous, one-to-one function from a circle into the real number line. The theorem no_continuous_injective_circle_to_real in the framework's machine-checked library of formal theorems proves exactly this: for any continuous and injective map from the metric circle into the real numbers, a contradiction follows.

The proof runs through a middle-value argument. If such a map existed, its image would be a connected set on the line. Removing the preimage of a value strictly between two attained values would disconnect the image interval, but the circle minus a point stays connected. That contradiction is the whole argument. The result is a standard fact of topology, restated and verified in the framework's library.

In Recognition Science, this fact serves a specific purpose. The framework defines a linking detector, a test that asks whether an embedded circle leaves behind a homologically nontrivial complement. The theorem shows the detector fails in dimension one: an embedded circle fills the whole one-dimensional sphere, so its complement is empty and the homology test returns zero. The same detector also fails in dimension zero, where the sphere is just two points and every subspace is totally disconnected.

What the declaration does not claim is broader. It says nothing about circles in higher dimensions, where linking is a rich and real phenomenon. It does not claim that the framework's linking detector is the only way to detect linking, nor that the failure in low dimensions is surprising. The theorem is a narrow, precise tool: it rules out one specific map, and that ruling is what the framework uses to close off low-dimensional linking.

THEOREM no_continuous_injective_circle_to_real · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
no_continuous_injective_circle_to_real · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:95 
/-- There is no continuous injection from the metric circle into `ℝ`:
removing the preimage of a strictly-middle value leaves the circle connected
(stereographic projection identifies it with `ℝ¹`), while the image must be
an order-connected set that omits a middle point between two attained
values. -/
theorem no_continuous_injective_circle_to_real
    (g : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) → ℝ)
    (hgc : Continuous g) (hginj : Function.Injective g) : False := by
  -- three distinct points on the circle
  have mem1 : EuclideanSpace.single (0 : Fin 2) (1 : ℝ) ∈
      Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
    rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single]; norm_num
  have mem2 : EuclideanSpace.single (1 : Fin 2) (1 : ℝ) ∈
      Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
    rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single]; norm_num
  have mem3 : EuclideanSpace.single (0 : Fin 2) (-1 : ℝ) ∈
      Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
    rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single]; norm_num
  set a : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) := ⟨_, mem1⟩ with ha
  set b : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) := ⟨_, mem2⟩ with hb
  set c : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) := ⟨_, mem3⟩ with hc
  have hab : a ≠ b := by
    intro h
    have h0 := congrArg (fun v : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) =>
      (v : EuclideanSpace ℝ (Fin 2)) 0) h
    simp only [ha, hb, EuclideanSpace.single_apply] at h0
    norm_num at h0
  have hac : a ≠ c := by
    intro h
    have h0 := congrArg (fun v : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) =>
      (v : EuclideanSpace ℝ (Fin 2)) 0) h
    simp only [ha, hc, EuclideanSpace.single_apply] at h0
    norm_num at h0
  have hbc : b ≠ c := by
    intro h
    have h0 := congrArg (fun v : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) =>
      (v : EuclideanSpace ℝ (Fin 2)) 0) h
    simp only [hb, hc, EuclideanSpace.single_apply] at h0
    norm_num at h0
  -- among the three (distinct) values pick the strictly-middle one
  have hgab : g a ≠ g b := fun h => hab (hginj h)
  have hgac : g a ≠ g c := fun h => hac (hginj h)
  have hgbc : g b ≠ g c := fun h => hbc (hginj h)
  obtain ⟨x0, y1, y2, hy1, hy2, hlt1, hlt2⟩ :
      ∃ x0 y1 y2 : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1),
        y1 ≠ x0 ∧ y2 ≠ x0 ∧ g y1 < g x0 ∧ g x0 < g y2 := by
    rcases hgab.lt_or_gt with h1 | h1
    · rcases hgbc.lt_or_gt with h2 | h2
      · exact ⟨b, a, c, hab, hbc.symm, h1, h2⟩
      · rcases hgac.lt_or_gt with h3 | h3
        · exact ⟨c, a, b, hac, hbc, h3, h2⟩
        · exact ⟨a, c, b, hac.symm, hab.symm, h3, h1⟩
    · rcases hgac.lt_or_gt with h3 | h3
      · exact ⟨a, b, c, hab.symm, hac.symm, h1, h3⟩
      · rcases hgbc.lt_or_gt with h2 | h2
        · exact ⟨c, b, a, hbc, hac, h2, h3⟩
        · exact ⟨b, c, a, hbc.symm, hab, h2, h1⟩
  -- the circle minus the middle point is connected (stereographic projection)
  haveI fact2 : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 1 + 1) :=
    ⟨by norm_num [finrank_euclideanSpace_fin]⟩
  have hconn :
      IsConnected ({x0}ᶜ : Set ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) := by
    haveI hct : ConnectedSpace ((stereographic' (1 : ℕ) x0).target) := by
      rw [stereographic'_target]
      exact (Homeomorph.Set.univ (EuclideanSpace ℝ (Fin 1))).symm.surjective.connectedSpace
        (Homeomorph.Set.univ (EuclideanSpace ℝ (Fin 1))).symm.continuous
    haveI hcs : ConnectedSpace ((stereographic' (1 : ℕ) x0).source) :=
      (stereographic' (1 : ℕ) x0).toHomeomorphSourceTarget.symm.surjective.connectedSpace
        (stereographic' (1 : ℕ) x0).toHomeomorphSourceTarget.symm.continuous
    rw [← stereographic'_source (n := 1) x0]
    exact isConnected_iff_connectedSpace.mpr hcs
  -- its image omits the middle value, contradicting order-connectedness
  have hy1m : y1 ∈ ({x0}ᶜ : Set ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) :=
    Set.mem_compl_singleton_iff.mpr hy1
  have hy2m : y2 ∈ ({x0}ᶜ : Set ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) :=
    Set.mem_compl_singleton_iff.mpr hy2
  have himg : IsPreconnected (g '' ({x0}ᶜ)) :=
    hconn.isPreconnected.image g hgc.continuousOn
  have hmid : g x0 ∈ g '' ({x0}ᶜ) :=
    himg.Icc_subset ⟨y1, hy1m, rfl⟩ ⟨y2, hy2m, rfl⟩ ⟨hlt1.le, hlt2.le⟩
  obtain ⟨z, hz, hzeq⟩ := hmid
  exact Set.mem_compl_singleton_iff.mp hz (hginj hzeq)
THEOREM no_continuous_injective_circle_to_real · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
no_continuous_injective_circle_to_real · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:95 
/-- There is no continuous injection from the metric circle into `ℝ`:
removing the preimage of a strictly-middle value leaves the circle connected
(stereographic projection identifies it with `ℝ¹`), while the image must be
an order-connected set that omits a middle point between two attained
values. -/
theorem no_continuous_injective_circle_to_real
    (g : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) → ℝ)
    (hgc : Continuous g) (hginj : Function.Injective g) : False := by
  -- three distinct points on the circle
  have mem1 : EuclideanSpace.single (0 : Fin 2) (1 : ℝ) ∈
      Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
    rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single]; norm_num
  have mem2 : EuclideanSpace.single (1 : Fin 2) (1 : ℝ) ∈
      Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
    rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single]; norm_num
  have mem3 : EuclideanSpace.single (0 : Fin 2) (-1 : ℝ) ∈
      Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 := by
    rw [mem_sphere_zero_iff_norm, EuclideanSpace.norm_single]; norm_num
  set a : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) := ⟨_, mem1⟩ with ha
  set b : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) := ⟨_, mem2⟩ with hb
  set c : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) := ⟨_, mem3⟩ with hc
  have hab : a ≠ b := by
    intro h
    have h0 := congrArg (fun v : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) =>
      (v : EuclideanSpace ℝ (Fin 2)) 0) h
    simp only [ha, hb, EuclideanSpace.single_apply] at h0
    norm_num at h0
  have hac : a ≠ c := by
    intro h
    have h0 := congrArg (fun v : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) =>
      (v : EuclideanSpace ℝ (Fin 2)) 0) h
    simp only [ha, hc, EuclideanSpace.single_apply] at h0
    norm_num at h0
  have hbc : b ≠ c := by
    intro h
    have h0 := congrArg (fun v : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) =>
      (v : EuclideanSpace ℝ (Fin 2)) 0) h
    simp only [hb, hc, EuclideanSpace.single_apply] at h0
    norm_num at h0
  -- among the three (distinct) values pick the strictly-middle one
  have hgab : g a ≠ g b := fun h => hab (hginj h)
  have hgac : g a ≠ g c := fun h => hac (hginj h)
  have hgbc : g b ≠ g c := fun h => hbc (hginj h)
  obtain ⟨x0, y1, y2, hy1, hy2, hlt1, hlt2⟩ :
      ∃ x0 y1 y2 : ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1),
        y1 ≠ x0 ∧ y2 ≠ x0 ∧ g y1 < g x0 ∧ g x0 < g y2 := by
    rcases hgab.lt_or_gt with h1 | h1
    · rcases hgbc.lt_or_gt with h2 | h2
      · exact ⟨b, a, c, hab, hbc.symm, h1, h2⟩
      · rcases hgac.lt_or_gt with h3 | h3
        · exact ⟨c, a, b, hac, hbc, h3, h2⟩
        · exact ⟨a, c, b, hac.symm, hab.symm, h3, h1⟩
    · rcases hgac.lt_or_gt with h3 | h3
      · exact ⟨a, b, c, hab.symm, hac.symm, h1, h3⟩
      · rcases hgbc.lt_or_gt with h2 | h2
        · exact ⟨c, b, a, hbc, hac, h2, h3⟩
        · exact ⟨b, c, a, hbc.symm, hab, h2, h1⟩
  -- the circle minus the middle point is connected (stereographic projection)
  haveI fact2 : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 1 + 1) :=
    ⟨by norm_num [finrank_euclideanSpace_fin]⟩
  have hconn :
      IsConnected ({x0}ᶜ : Set ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) := by
    haveI hct : ConnectedSpace ((stereographic' (1 : ℕ) x0).target) := by
      rw [stereographic'_target]
      exact (Homeomorph.Set.univ (EuclideanSpace ℝ (Fin 1))).symm.surjective.connectedSpace
        (Homeomorph.Set.univ (EuclideanSpace ℝ (Fin 1))).symm.continuous
    haveI hcs : ConnectedSpace ((stereographic' (1 : ℕ) x0).source) :=
      (stereographic' (1 : ℕ) x0).toHomeomorphSourceTarget.symm.surjective.connectedSpace
        (stereographic' (1 : ℕ) x0).toHomeomorphSourceTarget.symm.continuous
    rw [← stereographic'_source (n := 1) x0]
    exact isConnected_iff_connectedSpace.mpr hcs
  -- its image omits the middle value, contradicting order-connectedness
  have hy1m : y1 ∈ ({x0}ᶜ : Set ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) :=
    Set.mem_compl_singleton_iff.mpr hy1
  have hy2m : y2 ∈ ({x0}ᶜ : Set ↥(Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1)) :=
    Set.mem_compl_singleton_iff.mpr hy2
  have himg : IsPreconnected (g '' ({x0}ᶜ)) :=
    hconn.isPreconnected.image g hgc.continuousOn
  have hmid : g x0 ∈ g '' ({x0}ᶜ) :=
    himg.Icc_subset ⟨y1, hy1m, rfl⟩ ⟨y2, hy2m, rfl⟩ ⟨hlt1.le, hlt2.le⟩
  obtain ⟨z, hz, hzeq⟩ := hmid
  exact Set.mem_compl_singleton_iff.mp hz (hginj hzeq)
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 anything about circles embedded in spaces of dimension two or higher. It does not claim that the linking detector is the only possible detector of linking. It does not claim that the failure in low dimensions is unexpected or paradoxical.

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