prismSndFun
plain-language theorem explainer
Second coordinate of the i-th geometric prism map on the standard simplex: the sum of barycentric weights on vertices strictly above i. Anyone assembling Δ^{n+1} → Δ^n × I (homotopy of singular chains) cites this. The body is a single filtered sum over simplex coordinates.
Claim. For each index $i \in \{0,\ldots,n\}$ and each point $x$ of the standard $(n+1)$-simplex in barycentric coordinates, let $\mathrm{snd}_i(x)$ be the sum of the coordinates of $x$ at vertices strictly larger than $i$. This is the height coordinate of the $i$-th prism map into $\Delta^n \times I$.
background
The standard simplex $\Delta^{m}$ is the set of nonnegative real $(m+1)$-tuples summing to 1 (barycentric coordinates). Face inclusions skip a vertex; prism maps thicken a simplex into a product with the unit interval $I=[0,1]$.
In the classical prism operator of singular homology, one decomposes $\Delta^n \times I$ into $n+1$ simplices. The $i$-th piece is the affine map sending vertices of $\Delta^{n+1}$ to the bottom-then-top sequence $v_0,\ldots,v_i,w_i,\ldots,w_n$, where $v_j=(e_j,0)$ and $w_j=(e_j,1)$.
This definition isolates the second (interval) factor of that map: the cumulative mass of barycentric coordinates strictly above the cut index $i$. The first factor is handled separately by predAbove on the vertex set.
proof idea
Pure definition, not a proof. The value is the Finset sum of the coordinate functions $x_k$ over those $k$ with $i.\mathrm{castSucc}<k$. No lemmas are invoked; nonnegativity, the bound by 1, membership in $I$, and continuity are proved in sibling lemmas from this formula.
why it matters
Local scaffolding for the geometric prism in Foundation.SingularPrism. Downstream, prism packages this sum (with a unit-interval subtype proof) as the second component of the continuous map $\Delta^{n+1}\to\Delta^n\times I$; prism_apply_snd is the corresponding simp lemma, and continuous_prismSndFun discharges continuity of the height.
The face-commutation theorems that encode $\partial P=P\partial$ all read this coordinate: bottom face gives height 0 (prism_comp_face_bot), adjacent prisms agree on the shared face (prism_comp_face_cancel), and high/low faces factor through a lower-dimensional prism (prism_comp_face_of_gt, prism_comp_face_of_le, prism_comp_face_top). In the broader RS foundation stack this is ordinary singular-homology infrastructure (homotopy invariance of singular chains), not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.