Encyclopedia Foundation Foundation Linking Vanishing Low Dim Not Detects Zero

ARTICLE 4 claims 4 theorems

Foundation Linking Vanishing Low Dim Not Detects Zero

In dimensions zero and one, a proposed detector for linked loops provably finds nothing, a boundary case that shapes the framework's account of three-dimensional space.

Verify this page

The low-dimensional limit

In topology, linking asks whether two loops are tangled together, like two rings of a chain that cannot be separated without breaking one. A standard way to detect linking is to look at the complement: if you remove one loop from the space, the other loop may leave a trace in the homology of what remains. The Recognition Science framework formalizes this idea as a detector, a property that a space of dimension D holds (that is, satisfies) when an embedded circle has a complement whose first homology is nonzero.

The framework's machine-checked library of formal theorems proves that this detector fails in the two lowest dimensions. In dimension 0, the unit sphere is just two points. Every subspace of a two-point space is totally disconnected, and the first singular homology of any totally disconnected space vanishes, so no embedded circle can have a homologically nontrivial complement. The theorem not_detects_zero states exactly this: the detector does not hold for dimension 0. In dimension 1, the argument is different but the conclusion matches: a continuous injection from a circle into itself must be surjective, so the complement of an embedded circle is empty, and the homology of the empty space is zero. The theorem not_detects_one records that the detector also fails in dimension 1.

These results are boundary cases, not failures of the framework's main path. The framework uses linking to argue that three spatial dimensions are forced, and it proves that the detector works in dimension 3. The low-dimensional theorems are the necessary bookkeeping that shows the detector is not vacuous: it genuinely distinguishes dimension 3 from the degenerate cases below it. Without not_detects_zero and not_detects_one, the claim that the detector is meaningful in dimension 3 would lack its contrast class.

What these theorems do not claim is broader than what they prove. They say nothing about whether linking is detectable in dimensions above 1, and they do not address the physical question of whether the mathematical linking detector corresponds to anything observable in space. The framework's bridge from recognition to physical linking remains open, and these low-dimensional results are purely topological facts, not statements about the physical world.

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
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 sphere_fin_one_finite · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean
sphere_fin_one_finite · IndisputableMonolith/Foundation/LinkingVanishingLowDim.lean:49 
/-- The unit sphere in `ℝ¹` is contained in the two-point set `{e, -e}`. -/
lemma sphere_fin_one_finite :
    (Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1).Finite := by
  have hsub : Metric.sphere (0 : EuclideanSpace ℝ (Fin 1)) 1 ⊆
      {EuclideanSpace.single (0 : Fin 1) (1 : ℝ),
        EuclideanSpace.single (0 : Fin 1) (-1 : ℝ)} := by
    intro x hx
    rw [EuclideanSpace.sphere_zero_eq _ zero_le_one, Set.mem_setOf_eq,
      Fin.sum_univ_one] at hx
    have h0 : (x 0 - 1) * (x 0 + 1) = 0 := by nlinarith
    rcases mul_eq_zero.mp h0 with h | h
    · left
      ext i
      obtain rfl : i = (0 : Fin 1) := Subsingleton.elim _ _
      rw [EuclideanSpace.single_apply, if_pos rfl]
      linarith
    · right
      ext i
      obtain rfl : i = (0 : Fin 1) := Subsingleton.elim _ _
      rw [EuclideanSpace.single_apply, if_pos rfl]
      linarith
  exact ((Set.finite_singleton _).insert _).subset hsub
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

What this page does not claim

The detector works in any dimension above 1. The mathematical linking detector corresponds to anything physically observable. The framework's recognition-to-linking bridge is established.

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