Encyclopedia Foundation Foundation Linking Vanishing Low Dim Not Detects One

ARTICLE 3 claims 3 theorems

Foundation Linking Vanishing Low Dim Not Detects One

In low dimensions, a circle has no room to link around anything, and the framework's detector of linking proves this exactly.

Verify this page

A circle in a line

Linking is a topological idea: one closed loop is linked with another if it cannot be pulled free without cutting. The classic example is two interlocked rings. A circle in three-dimensional space can link with another circle. In lower dimensions, this becomes impossible, and the framework's library of machine-checked theorems proves exactly when the possibility vanishes.

The framework defines a detector for nontrivial linking. It looks at a circle embedded in a sphere of dimension D, removes the circle, and checks the first homology of what remains. Homology is an algebraic way to count holes: the first homology of a space is zero when the space has no one-dimensional holes. The detector succeeds when the complement has a nonzero first homology, meaning a hole remains after the circle is removed.

The theorem not_detects_one proves the detector fails in dimension one. The 1-sphere is itself a circle. A continuous injection of a circle into itself must be surjective: if it missed a point, stereographic projection would give a continuous injection of the circle into the real line, which is impossible because the circle is connected while the line minus a point is not. So the embedded circle fills the whole 1-sphere, its complement is empty, and the homology of the empty space vanishes. The detector finds no hole because there is no complement left to contain one.

The same failure happens in dimension zero. The 0-sphere is a two-point space, totally disconnected, so every subspace has vanishing first homology. The detector cannot detect linking in dimensions zero or one.

This result is a boundary condition for the framework's account of three-dimensional space. The framework proves that three spatial dimensions are forced by a chain of recognition events, and this theorem shows why lower dimensions cannot host the linking structure the framework requires. It is a negative result that clears the ground: the detector works only where there is enough room for a loop to encircle a hole, and that room appears only in dimension three and above.

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 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_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

This theorem does not claim that linking is impossible in dimension two, where the detector might behave differently. This result does not prove that three dimensions are the only ones where linking exists, only that dimensions zero and one fail. The theorem does not address what happens in dimensions greater than three.

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