Foundation Circle H1 Computation Ordinary Cellular Circle Chain Model H1 Nonempt

The circle's first homology

In algebraic topology, the first homology group of a circle, written H₁(S¹; ℤ), counts the essentially different loops on the circle, and it is one of the most basic computations in the subject: it is the group of integers ℤ. A loop that winds once around is 1, twice is 2, and a loop that cancels its own winding is 0. This page concerns a machine-checked library of formal theorems and a specific result inside it about two algebraic models of the circle.

The declaration ordinaryCellularCircleChainModelH1NonemptyIsoReducedCellularH1 proves that the first homology of the ordinary cellular circle chain model is isomorphic to the first homology of the reduced cellular circle chain model. In plainer terms, it shows that two different algebraic ways of encoding the circle's one-dimensional structure give the same answer for H₁: both are ℤ. The proof constructs an explicit isomorphism between the two homology groups, so it is not merely a statement that both are ℤ; it gives the specific correspondence between them.

The result is a theorem in the framework's machine-checked library of formal theorems, meaning it has been verified by a computer proof checker. It is part of a larger workbench that aims to compute H₁(S¹; ℤ) ≅ ℤ. The declaration is a stepping stone: it shows that the two cellular models agree with each other, and separately each is known to have first homology ℤ. What it does not do is connect these cellular models to the standard singular homology of the topological circle, the object called TopCat.sphere 1 in the library. That connection is a separate, unproved bridge.

The missing bridge is named in the library as circleH1GeometricBridge, a formal statement that the singular chain complex of the topological circle is homotopy equivalent to the ordinary cellular model. Until that bridge is proved, the cellular computation is an algebraic core that does not feed the strict T8 bridge, which concerns three-dimensional space. The current result is therefore a precise algebraic fact with a clear boundary: it establishes agreement between two models, and it leaves the topological transport as an open target.

For the reader, the consequence is a concrete and verified piece of the circle's homology story. The two cellular models are not just both ℤ; they are isomorphic in a way that the proof makes explicit. The page's not-claimed list keeps the boundary sharp: the result does not prove the standard H₁(S¹; ℤ) ≅ ℤ computation, and it does not establish any link to the physical three-dimensional space result. Those remain open.

/-- Proposition-facing form of
`ordinaryCellularCircleChainModelH1IsoReducedCellularH1`. -/
theorem ordinaryCellularCircleChainModelH1NonemptyIsoReducedCellularH1 :
    Nonempty
      (ordinaryCellularCircleChainModel.homology 1 ≅
        reducedCellularCircleChainModel.homology 1) :=
  ⟨ordinaryCellularCircleChainModelH1IsoReducedCellularH1⟩

/-- Proposition-facing form of
`ordinaryCellularCircleChainModelH1IsoReducedCellularH1`. -/
theorem ordinaryCellularCircleChainModelH1NonemptyIsoReducedCellularH1 :
    Nonempty
      (ordinaryCellularCircleChainModel.homology 1 ≅
        reducedCellularCircleChainModel.homology 1) :=
  ⟨ordinaryCellularCircleChainModelH1IsoReducedCellularH1⟩

/-- The remaining geometric chain-level bridge for the strict T8 circle-H1
closure: Mathlib's singular chain complex for `TopCat.sphere 1` is chain
homotopy equivalent to the ordinary two-cell cellular circle model. -/
def circleH1GeometricBridge : Prop :=
  Nonempty
    (HomotopyEquiv sphereOneSingularIntChainComplex ordinaryCellularCircleChainModel)

What this page does not claim

The result does not prove the standard H₁(S¹; ℤ) ≅ ℤ computation for the topological circle. The result does not establish any link to the physical three-dimensional space result. The result does not state that the two cellular models are the same chain complex, only that their first homology groups are isomorphic.

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: