Foundation Circle H1 Computation Homology One Nonempty Iso Int Of Quasi Iso At S

The algebraic core

In algebraic topology, the first homology group of a circle is the integers. This is a foundational fact, often written H₁(S¹; ℤ) ≅ ℤ. It says that loops on a circle can be wound any integer number of times, and that these winding numbers capture all the essential structure. The declaration homologyOneNonemptyIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex is a machine-checked proof of a precise algebraic version of this statement, working not with the topological circle itself but with a simpler algebraic stand-in.

The stand-in is a chain complex, a sequence of abelian groups connected by maps called boundaries, which encodes the shape of a space algebraically. The specific complex used, singleDegreeOneIntComplex, is the simplest possible model: it has the integers in degree one, and zero everywhere else. The theorem states that if any chain complex is quasi-isomorphic to this simple model, meaning it has the same homology, then its first homology group is also the integers. The proof is constructive, providing an explicit isomorphism, and it is verified by the machine-checked library of formal theorems.

The theorem is deliberately narrow. It does not claim that this algebraic model is the actual topological circle, nor that the homology of the true singular chain complex of the sphere has been computed. That computation, connecting this algebraic core to the genuine topological object, remains an open target. The declaration is a stepping stone, a proved atom that later work can build upon.

/-- Global quasi-isomorphism transport, for the common case where the finite
circle chain model is proved quasi-isomorphic to the single-supported reduced
model in every degree. -/
def homologyOneIsoIntOfQuasiIsoSingleDegreeOneIntComplex
    {K : HomologicalComplex (ModuleCat ℤ) (ComplexShape.down ℕ)}
    (f : K ⟶ singleDegreeOneIntComplex)
    [∀ i, K.HasHomology i] [QuasiIso f] :
    K.homology 1 ≅ ModuleCat.of ℤ ℤ :=
  homologyOneIsoIntOfQuasiIsoAtSingleDegreeOneIntComplex f

What this page does not claim

The theorem does not prove that the algebraic model is the topological circle. The theorem does not compute the homology of the singular chain complex of the sphere. The theorem does not rely on any Recognition Science-specific axioms beyond the standard ones.

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