prism_comp_face_bot
plain-language theorem explainer
Bottom-face identity for the singular prism: the last prism map composed with the last face map is the height-zero inclusion $x\mapsto(x,0)$ of the standard simplex into the prism. Cited by the prism double-sum cancellation (Hatcher 2.10 style) that feeds homotopy invariance of singular homology. Proof is pointwise: the first factor recovers the identity via opposite face-index maps; the second factor is an empty filtered sum, hence zero.
Claim. For every $n$, the composition of the prism map at the last vertex of $\Delta^n$ with the face map at the last vertex of $\Delta^{n+1}$ equals the continuous map $x \mapsto (x, 0)$ from the standard $n$-simplex into $\Delta^n \times I$.
background
The module builds the singular prism operator used to prove that homotopic continuous maps induce the same map on singular homology (the classical Hatcher argument). A prism map takes an $n$-simplex and extrudes it along the unit interval, producing an $(n+1)$-chain whose faces encode the two ends of a homotopy together with lateral faces that cancel in pairs.
The face maps are the standard inclusions of codimension-one faces of the standard simplex, realized by the usual succAbove/predAbove index maps on barycentric coordinates. The second coordinate of a prism is a continuous height function on the simplex (nonnegative, at most one), built as a filtered sum of barycentric weights.
Locally one needs the three prism-face identities that make the alternating double sum for $\partial P - P\partial$ collapse. This declaration is the bottom-end case: last prism composed with last face lands on the floor of the prism.
proof idea
Pointwise equality of continuous maps into a product, via ContinuousMap.ext and Prod.ext.
First component: after composing the two simplex maps (pred-above at last $n$, then succ-above at last $n+1$), reduce by the standard map_map_eq_self criterion. On each barycentric index the two Fin maps cancel: case-split on the succAbove/predAbove thresholds and finish with omega on the underlying naturals.
Second component: rewrite the height function after succAbove by the dedicated simplification lemma, then show the resulting Finset sum is empty. Membership in the filter forces a strict inequality on Fin values that is impossible at the last index (again split_ifs plus omega). Hence the height is identically zero.
why it matters
This is one of the three prism-face identities required by the abstract cancellation lemma prism_sum_cancellation, which packages Hatcher's Theorem 2.10: the signed double sums for faces-of-prisms versus prisms-of-faces collapse to the difference of the two end maps of the homotopy. That cancellation is the algebraic engine behind homotopy invariance of singular homology in this development, and is consumed by isIso_homology_map_of_homotopyEquiv (the induced map on singular homology of a homotopy equivalence is an isomorphism).
In the Recognition Science foundation layer the result is pure classical algebraic topology scaffolding: it underwrites that continuous deformations do not change singular homology, so later RS constructions that quote homotopy-invariant functors sit on a proved base rather than an axiom. It does not itself touch the forcing chain (T0-T8), the J-cost, or the phi ladder; it is infrastructure those layers may later import.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.