Pith. sign in
module module moderate

IndisputableMonolith.Foundation.SingularPrism

show as:
view Lean formalization →

Defines prism maps on standard simplices for singular homology: the continuous map whose second coordinate sums barycentric weights strictly above a fixed index, plus face restrictions and elementary bounds. Algebraic topologists building chain homotopies cite it. The module is definitional scaffolding with continuity and interval-membership lemmas, not deep theorems.

claimOn the standard simplex, the $i$-th prism map has second coordinate equal to the sum of barycentric coordinates strictly above $i$; the module packages this map $\Delta^{n+1}\to\Delta^n\times I$, its face restrictions, and the elementary facts that the second coordinate lies in $[0,1]$ and is continuous.

background

Singular homology needs a prism operator to turn a homotopy of maps into a chain homotopy of singular chains. The standard construction sends an $(n+1)$-simplex to a prism in $X\times I$ by splitting barycentric coordinates at an index $i$: the first block maps into the base simplex, and the tail sum becomes the $I$-coordinate.

This module sits in the Foundation singular-homology stack and imports Mathlib singular homology, module-category colimits, and basic homotopy. It introduces prismSndFun (the tail-sum second coordinate), the full prism map, and face maps, with lemmas that the second coordinate is nonnegative, at most one, and continuous.

Downstream modules on Mayer-Vietoris, pairs, spheres, and subdivision import these maps as the geometric input to chain-level prism operators.

proof idea

Definition module with elementary supporting lemmas. The second coordinate is defined as an explicit sum of barycentric coordinates above $i$; nonnegativity, the bound $\le 1$, membership in the unit interval, and continuity are proved by direct estimates and continuity of finite sums. The prism and face maps are then assembled by pairing the projected simplex map with that second coordinate; apply lemmas record the two projections.

why it matters in Recognition Science

Supplies the geometric prism and face data required by the Foundation singular-homology layer. It is imported by SingularMayerVietoris, SingularPair, SingularSphere, and SingularSubdivision, which need prism operators for excision-style exact sequences, relative pairs, sphere homology computations, and subdivision chain homotopies. In the broader Recognition stack this is pure topological infrastructure: it does not touch the forcing chain T0-T8, J-cost, or phi-ladder, but underwrites any later argument that identifies topological invariants with recognition-derived discrete structure.

scope and limits

used by (4)

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

declarations in this module (49)