Foundation Singular Sphere Is Zero H1

The zero homology of a point

In algebraic topology, the singular homology groups of a space measure its holes in each dimension. The zeroth homology group counts the path-connected components, so for a single point it is the integers, one copy for the one component. The higher homology groups, first and above, record higher-dimensional holes, and a point has none. The Recognition Science declaration isZero_h1 establishes exactly this: for a point, every homology group in dimension one or higher is the zero group, meaning it contains only the identity element and no nontrivial cycles.

The proof in the machine-checked library of formal theorems proceeds through a standard route. It first shows the space consisting of a single point is totally disconnected, meaning its only connected subsets are the point itself and the empty set. A theorem in the library then states that for any totally disconnected space, all positive-dimensional homology groups vanish. Applying this to the one-point space gives the result. The declaration isZero_h1 is a lemma, not a definition, and it is proved in the library's SingularSphere file.

This result is a basic structural fact. It confirms that the singular homology construction, as formalized in the library, behaves as expected on the simplest possible space. It also provides a foundation for later statements about the homology of spheres and other spaces. The zeroth homology of a point being the integers is also established separately, so the full homology of a point is known: integers in dimension zero, zero everywhere else.

In Recognition Science, this fact is part of the toolkit for building up the homology of more complex spaces, which in turn supports the framework's larger claims about the structure of recognition events. The declaration does not itself make any statement about the physical world, about recognition costs, or about the golden ratio. It is a purely topological lemma about a single point.

/-- **Stage A.** `H_m(pt) = 0` for `m ≠ 0`. -/
lemma hn_pt_isZero {m : ℕ} (hm : m ≠ 0) : IsZero (Hgrp (TopCat.of Unit) m) :=
  isZero_homology_of_totallyDisconnected (TopCat.of Unit) hm

/-- **Stage A.** `H₀(pt) ≅ ℤ`. -/
noncomputable def h0_pt_iso_int :
    Hgrp (TopCat.of Unit) 0 ≅ ModuleCat.of ℤ ℤ :=
  h0_iso_int (TopCat.of Unit)

What this page does not claim

This result does not claim anything about the physical world or about recognition events. It does not derive the golden ratio or any other constant of the framework. It does not state that the zeroth homology of any space is the integers, only for a path-connected space.

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: