prismSndFun_map_succAbove
plain-language theorem explainer
When the second (height) coordinate of a prism map is evaluated on a face inclusion of a simplex, the filtered barycentric sum reindexes along the vertex skip map. Algebraic topologists building the prism operator for singular homology cite this to move face maps past the height functional. The proof is a one-line application of the filtered-sum reindexing lemma for stdSimplex.map.
Claim. For $c \in \mathrm{Fin}(n+1)$, $j \in \mathrm{Fin}(n+2)$, and $x$ a point of the standard $n$-simplex over $\mathbb{R}$, the prism height functional at $c$ on the image of $x$ under the face inclusion that skips vertex $j$ equals $\sum_{m:\, c^{\uparrow} < j^{\uparrow}(m)} x_m$, where $(\cdot)^{\uparrow}$ denotes the corresponding $\mathrm{succAbove}$ (resp. $\mathrm{castSucc}$) embedding.
background
The module builds the classical prism operator on singular chains: continuous maps $\Delta^{n+1} \to \Delta^n \times I$ that subdivide the product into $n+1$ simplices. The height coordinate of the $i$-th prism map is prismSndFun i, the sum of barycentric coordinates of a point of $\Delta^{n+1}$ strictly above index $i$. The topological face inclusion face j is the continuous realization of $\delta_j$, induced by Fin.succAbove j on vertices.
The upstream lemma sum_filter_map_apply states that a filtered coordinate sum of stdSimplex.map f x reindexes along $f$: $\sum_{k:, p(k)} (\mathrm{map}, f, x)k = \sum{m:, p(f(m))} x_m$. That identity is the only algebraic input here. The surrounding development sits in Mathlib's singular-homology and continuous-map infrastructure; the Recognition Science use is as foundation for chain-homotopy identities, not a direct physics claim.
proof idea
One-line term proof. Unfolding the definition of the height functional on the face-mapped simplex produces a filtered sum of stdSimplex.map j.succAbove x. Instantiate sum_filter_map_apply at $f = j.\mathrm{succAbove}$ and predicate $p(k) = (c.\mathrm{castSucc} < k)$ to reindex the sum onto the original barycentric coordinates of $x$. No case splits or continuity arguments appear.
why it matters
Feeds the five prism–face composition identities in the same module: top and bottom faces (prism_comp_face_top, prism_comp_face_bot), the adjacent-face cancellation used in $\partial P$ (prism_comp_face_cancel), and the high/low face commutation rules (prism_comp_face_of_gt, prism_comp_face_of_le) that match $(i,j)$ terms of $\partial P$ against $P\partial$. Those identities are the combinatorial heart of the prism operator, which supplies the chain homotopy proving homotopy invariance of singular homology.
In the Recognition Science mirror this is pure foundation scaffolding: it underwrites topological arguments (circle windings, singular chains) that later modules import, rather than a T0–T8 forcing step or a mass/alpha identity. Closing the prism calculus cleanly keeps downstream homology and homotopy lemmas free of sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.