Foundation Singular Sphere

The point and its sphere

In algebraic topology, the singular homology of a space measures its holes by probing it with simplices: points, line segments, triangles, and their higher-dimensional cousins. The 0-dimensional homology, written H₀, counts the connected pieces of the space. For a path-connected space, H₀ is isomorphic to the integers ℤ, meaning every point is connected to every other by a path, and the space has exactly one connected component.

The foundation singular sphere is a machine-checked construction in the Recognition Science framework's library that builds this classical fact from a different starting point. Instead of beginning with a space and then computing its homology, it begins with a single point and shows that the point itself generates the entire 0-dimensional homology. The construction assigns to each point a generator, a basic building block, and then proves that these generators satisfy exactly the relations that define H₀.

The central theorem, isIso_homologyMap_augTo, states that for any path-connected space, the map from the point's homology to the full homology is an isomorphism. This means the homology of the whole space is completely determined by the homology of a single point. A second theorem, mono_mvPair_zero, shows that the map from the intersection of two clopen sets to their union is injective, a technical condition that ensures the construction is well-behaved.

In Recognition Science, this result provides the ledger, a discrete record of events, with a local foundation. The framework models physical structure as a discrete record, and this construction establishes that a single point in that record carries enough information to reconstruct the global topology. The point is not an isolated atom; it is a seed that contains the shape of the whole.

The practical consequence is that the framework's foundational claims about space do not require a pre-existing continuum. The topology of a space, at least at the level of connected components, can be derived from a single point and the relations it generates. This is a step toward showing that the framework's discrete starting point can reproduce the continuous structures of classical physics.

/-- **`H₀` of a path-connected space.** The augmentation induces an
isomorphism `H₀(X) ≅ ℤ` on homology. -/
theorem isIso_homologyMap_augTo (X : TopCat.{0}) [PathConnectedSpace X] :
    IsIso (HomologicalComplex.homologyMap
      (augTo X Set.univ isClopen_univ) 0) := by
  obtain ⟨x₀⟩ : Nonempty ↥X := PathConnectedSpace.nonempty
  apply isIso_homologyMap_chain_zero
  · intro y
    refine ⟨gen X 0 (constSimplex X x₀) (show ℤ from y), 0, ?_⟩
    rw [Zsingle_d_one_zero, zeroApp, add_zero, augTo_f_zero_apply,
      ← ModuleCat.comp_apply, gen_augFun, if_pos (Set.mem_univ _)]
    exact ModuleCat.id_apply _ _
  · intro z hz
    obtain ⟨w, hw⟩ := hz
    have hz0 : augFun X Set.univ z = 0 := by
      rw [augTo_f_zero_apply, Zsingle_d_one_zero, zeroApp] at hw
      exact hw
    obtain ⟨v, hv⟩ := exists_bnd_of_pathConnected x₀ z
    rw [hz0, map_zero, sub_zero] at hv
    exact ⟨v, hv.symm⟩

/-- The Mayer-Vietoris pair map is mono in degree `0` when `U ∩ V` is path
connected (its first component is split by the augmentation). -/
theorem mono_mvPair_zero (U V : Set X)
    [PathConnectedSpace ↥(U ∩ V : Set X)] :
    Mono (mvPair U V 0) := by
  haveI : IsIso (augH (TopCat.of (U ∩ V : Set X)) Set.univ isClopen_univ) :=
    isIso_augH_of_pathConnected _
  haveI hm1 : Mono (HomologicalComplex.homologyMap
      (sChainMap (mvInclU U V)) 0 ≫
        augH (TopCat.of U) Set.univ isClopen_univ) := by
    rw [homologyMap_augH]
    infer_instance
  haveI hm2 : Mono (HomologicalComplex.homologyMap
      (sChainMap (mvInclU U V)) 0) :=
    mono_of_mono _ (augH (TopCat.of U) Set.univ isClopen_univ)
  have hfac : mvPair U V 0 ≫
      (biprod.fst : _ ⟶ Hgrp (TopCat.of U) 0) =
      HomologicalComplex.homologyMap (sChainMap (mvInclU U V)) 0 :=
    biprod.lift_fst _ _
  haveI : Mono (mvPair U V 0 ≫
      (biprod.fst : _ ⟶ Hgrp (TopCat.of U) 0)) := by
    rw [hfac]
    exact hm2
  exact mono_of_mono (mvPair U V 0) biprod.fst

/-- **Stage A/B.** `H₀(X) ≅ ℤ` for a path-connected space, via the
augmentation. -/
noncomputable def h0_iso_int (X : TopCat.{0}) [PathConnectedSpace X] :
    Hgrp X 0 ≅ ModuleCat.of ℤ ℤ :=
  haveI := isIso_augH_of_pathConnected X
  asIso (augH X Set.univ isClopen_univ)

What this page does not claim

This module does not prove that all of space is a single point. It does not establish the full singular homology of a space, only the 0-dimensional case. It does not provide a physical model of space; it provides a mathematical foundation within the framework.

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/SingularSphere.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: