Pith. sign in
module module moderate

IndisputableMonolith.Foundation.SingularSphere

show as:
view Lean formalization →

Defines singular homology of a space X with integer coefficients, together with the constant-simplex and augmentation apparatus needed to compute H_n of spheres. Algebraic topologists and RS foundation authors cite it when reducing sphere homology to a single generator in degree n. The module assembles prism, pair, subdivision, and Mayer–Vietoris machinery into the standard singular chain complex and its homology groups.

claimFor a topological space $X$ and $n \in \mathbb{Z}$, the module introduces the singular homology group $H_n(X;\mathbb{Z})$, the constant singular simplex on a point, the augmentation map from $0$-chains to $\mathbb{Z}$, and the identification of a point with its constant $0$-simplex, as the algebraic substrate for computing $H_*(S^n)$.

background

Singular homology is built from the free abelian groups on continuous maps $\Delta^n \to X$. The module sits in the Foundation layer of Recognition Science, where topological invariants of spheres enter the forcing chain that fixes spatial dimension $D=3$ and the eight-tick octave.

Upstream imports supply the supporting calculus: prism operators for homotopies, relative pairs, barycentric subdivision for excision, and a Mayer–Vietoris sequence. Mathlib contributes contractibility of convex sets, path homotopies, and the manifold structure on spheres.

Local definitions include the homology group functor $H_n(-;\mathbb{Z})$, the constant simplex on a base point, the point-extraction map inverse to it on $0$-simplices, and the augmentation homomorphism that sends a $0$-chain to the sum of its coefficients. These are the standard ingredients that make $H_0$ of a path-connected space isomorphic to $\mathbb{Z}$ and prepare the inductive computation of sphere homology.

proof idea

This is primarily a definition-and-setup module rather than a single theorem. It wires Mathlib singular homology (single complexes, homology of single complexes) to the RS singular toolkit (prism, pair, subdivision, Mayer–Vietoris). Constant simplices and the augmentation are introduced by explicit maps and verified by elementary equalities (point-of-constant, constant-of-point, naturality under continuous maps). No deep computational proof lives here; the heavy lifting is deferred to the geometry module that consumes these definitions.

why it matters in Recognition Science

Sphere homology is the classical input that distinguishes $S^n$ from contractible spaces and underpins dimension-sensitive arguments in the RS foundation. The sole recorded consumer is Foundation.SingularSphereGeometry, which uses these groups and the augmentation to identify $H_n(S^n;\mathbb{Z})\cong\mathbb{Z}$ and vanishing in other degrees. That geometric layer in turn supports the forcing-chain step that locks spatial dimension at three (T8) and the eight-tick discrete period. Without a clean singular $H_*$ interface, later claims about topological obstruction and recognition on spheres would lack a formal carrier.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (55)