Foundation Singular Prism Is Iso Homology Map Of Homotopy Equiv

Homotopy invariance of homology

In algebraic topology, homology groups are algebraic invariants attached to a topological space. They count features like connected components, holes, and voids. A fundamental property is homotopy invariance: if one space can be continuously deformed into another, without tearing or gluing, then their homology groups are isomorphic. The declaration isIso_homology_map_of_homotopyEquiv in the framework's library proves exactly this, in a fully formal, machine-checked way.

The theorem states that if there is a homotopy equivalence between two spaces X and Y, meaning a pair of continuous maps that are inverses up to deformation, then the induced map on homology groups is an isomorphism. This is a standard result, known since the early development of algebraic topology in the 1940s, but here it is not taken as an axiom or assumed as a lemma. It is derived from first principles within the framework's formal system. The proof constructs explicit chain homotopies, which are algebraic analogues of continuous deformations, using a geometric construction called a prism operator.

This result is foundational for the framework's broader program. It shows that the algebraic invariants the framework computes are stable: they do not depend on the specific way a space is represented, but only on its homotopy type. This is a necessary step for connecting the framework's discrete, combinatorial structures to the continuous spaces of classical geometry and physics.

In Recognition Science, this theorem is part of the infrastructure, not the main result. The framework's own claims about the cost function and the forcing chain do not rely on this theorem. It is a piece of standard mathematics, formalized in the framework's language, that provides a reliable foundation for further work.

/-- The map on singular homology induced by (the forward map of) a homotopy
equivalence is an isomorphism. -/
theorem isIso_homology_map_of_homotopyEquiv
    (h : ContinuousMap.HomotopyEquiv X Y) (n : ℕ) :
    IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj
      (ModuleCat.of ℤ ℤ)).map (TopCat.ofHom h.toFun)) :=
  inferInstanceAs (IsIso ((homotopyEquiv_homology_iso h n).hom))

What this page does not claim

This theorem does not prove that the framework's cost function or any of its derived constants are correct. It does not claim that homotopy equivalence is the only way to establish isomorphism of homology groups. It does not provide a constructive method for finding the isomorphism, only its existence.

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