Encyclopedia Foundation Foundation Singular Prism

ARTICLE 2 claims 2 theorems

Foundation Singular Prism

A machine-checked library proves that two continuously deformable shapes have identical internal structure, a key idea for how Recognition Science models change.

Verify this page

The singular prism

The singular prism is a standard construction in algebraic topology. It takes a continuous deformation between two shapes and turns it into a chain of algebraic data connecting their internal structures. The classical idea, due to Eilenberg and Steenrod in the 1950s, is that a homotopy between maps should induce a chain homotopy between the corresponding chain maps. This is the prism operator, and it is the technical heart of why homology groups are homotopy invariants.

In this framework, the module SingularPrism.lean formalizes that prism operator and proves its key property. The central theorem, isIso_homology_map_of_homotopyEquiv, states that if two spaces are homotopy equivalent, then the induced map on their singular homology groups is an isomorphism. In plainer terms: if one shape can be continuously squashed and stretched into another, then the algebraic record of holes and loops in both shapes is identical. The proof builds the prism map, verifies the chain homotopy equations, and concludes the homology isomorphism.

The framework uses this result as a foundational building block. Recognition Science models physical change as a ledger of discrete recognition events, and a continuous deformation between two configurations must preserve the algebraic structure that records those events. The singular prism theorem guarantees that such a deformation does not create or destroy the invariants the framework cares about. This is a theorem in the machine-checked library, meaning its proof has been verified by a computer, with no gaps and no unstated assumptions.

What this establishes in plain language is a conservation principle: the deep structure of a space is unchanged by continuous motion. A sphere and a cube have the same homology, because one can be deformed into the other. A sphere and a torus do not, because the torus has a hole the sphere lacks. The prism operator is the tool that makes this precise, and the framework's formalization makes it a reliable foundation for further work.

THEOREM isIso_homology_map_of_homotopyEquiv · IndisputableMonolith/Foundation/SingularPrism.lean
isIso_homology_map_of_homotopyEquiv · IndisputableMonolith/Foundation/SingularPrism.lean:912 
/-- 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))
THEOREM prism_chain_homotopy_succ · IndisputableMonolith/Foundation/SingularPrism.lean
prism_chain_homotopy_succ · IndisputableMonolith/Foundation/SingularPrism.lean:758 
/-- The chain homotopy identity in positive degrees:
`∂ ∘ P + P ∘ ∂ = (F₁)♯ − (F₀)♯` on the degree-`(n+1)` chain group. -/
lemma prism_chain_homotopy_succ (Ho : ContinuousMap.Homotopy F₀.hom F₁.hom) (n : ℕ) :
    bnd X n ≫ prismOp Ho.toContinuousMap n prism +
        prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1) =
      chainMap F₁ (n + 1) - chainMap F₀ (n + 1) := by
  apply Sigma.hom_ext
  intro s
  have hL1 : gen X (n + 1) s ≫ (bnd X n ≫ prismOp Ho.toContinuousMap n prism) =
      ∑ k : Fin (n + 2), ∑ i' : Fin (n + 1), (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) •
        gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
          ((TopCat.toSSet.obj X).δ k s)) := by
    rw [← Category.assoc, gen_d, Preadditive.sum_comp]
    refine Finset.sum_congr rfl fun k _ => ?_
    rw [Preadditive.zsmul_comp, gen_prismOp, Pgen, Finset.smul_sum]
    refine Finset.sum_congr rfl fun i' _ => ?_
    rw [smul_smul, ← pow_add]
  have hL2 : gen X (n + 1) s ≫ (prismOp Ho.toContinuousMap (n + 1) prism ≫ bnd Y (n + 1)) =
      ∑ i : Fin (n + 2), ∑ j : Fin (n + 3), (-1 : ℤ) ^ ((i : ℕ) + (j : ℕ)) •
        gen Y (n + 1) ((TopCat.toSSet.obj Y).δ j
          (prismSimplex Ho.toContinuousMap (n + 1) (prism i) s)) := by
    rw [← Category.assoc, gen_prismOp, Pgen, Preadditive.sum_comp]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [Preadditive.zsmul_comp, gen_d, Finset.smul_sum]
    refine Finset.sum_congr rfl fun j _ => ?_
    rw [smul_smul, ← pow_add]
  rw [Preadditive.comp_add, hL1, hL2, Preadditive.comp_sub, gen_map, gen_map,
    add_comm (∑ k : Fin (n + 2), ∑ i' : Fin (n + 1), (-1 : ℤ) ^ ((k : ℕ) + (i' : ℕ)) •
      gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
        ((TopCat.toSSet.obj X).δ k s)))]
  refine Eq.trans (prism_sum_cancellation n
    (fun i j => gen Y (n + 1) ((TopCat.toSSet.obj Y).δ j
      (prismSimplex Ho.toContinuousMap (n + 1) (prism i) s)))
    (fun k i' => gen Y (n + 1) (prismSimplex Ho.toContinuousMap n (prism i')
      ((TopCat.toSSet.obj X).δ k s)))
    (fun i j hij => congrArg (gen Y (n + 1)) (δ_prismSimplex_of_face
      Ho.toContinuousMap (prism i.succ) (prism i)
      (prism_comp_face_of_le (Fin.le_def.mpr (by simpa using hij))) s))
    (fun i j hij => congrArg (gen Y (n + 1)) (δ_prismSimplex_of_face
      Ho.toContinuousMap (prism i.castSucc) (prism i)
      (prism_comp_face_of_gt (Fin.lt_def.mpr (by simpa using hij))) s))
    (fun i => congrArg (gen Y (n + 1)) (δ_prismSimplex_congr
      Ho.toContinuousMap (prism i.castSucc) (prism i.succ)
      (prism_comp_face_cancel i) s))) ?_
  congr 1
  · exact congrArg (gen Y (n + 1)) (δ_prismSimplex_top Ho (n + 1) s)
  · exact congrArg (gen Y (n + 1)) (δ_prismSimplex_bot Ho (n + 1) s)

What this page does not claim

This module does not itself derive any physical constants or empirical predictions. The theorem does not state that all shapes with the same homology are deformable into each other, only that deformation preserves homology.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND