prism_apply_snd
plain-language theorem explainer
The second factor of the i-th prism map on the standard (n+1)-simplex is definitionally the sum of barycentric weights strictly above i. Anyone simplifying expressions involving prism operators in singular homology cites this. The proof is pure reflexivity from the definition of the prism map.
Claim. For $i \in \{0,\ldots,n\}$ and $x$ in the standard simplex $\Delta^{n+1}$, the second component of the prism map $\mathrm{prism}_i(x) \in \Delta^n \times I$, read as a real, equals $\sum_{k: i < k} x_k$.
background
The module builds continuous prism operators used in singular homology: maps $\Delta^{n+1} \to \Delta^n \times I$ that subdivide the product of a simplex with the unit interval. The standard simplex $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},(n+2))$ is the set of nonnegative barycentric coordinates summing to 1 on $n+2$ vertices.
The auxiliary function $\mathrm{prismSndFun},i,x$ is exactly that second coordinate: the sum of the barycentric coordinates of $x$ on vertices strictly above index $i$. The prism map itself sends $x$ to the pair $(\mathrm{stdSimplex.map},i.\mathrm{predAbove},x,,\langle\mathrm{prismSndFun},i,x,\ldots\rangle)$, so the second factor is packaged as an element of the unit interval $I$.
Upstream, the face inclusions $\Delta^n \to \Delta^{n+1}$ are the topological realizations of $\mathrm{SimplexCategory}.\delta,j$ via $\mathrm{Fin.succAbove}$. Together, faces and prisms supply the combinatorial skeleton for prism operators and homotopy identities in singular chains.
proof idea
One-line term proof by rfl. Unfolding prism shows that its second component is definitionally ⟨prismSndFun i x, prismSndFun_mem_unitInterval i x⟩; coercing that subtype element to $\mathbb{R}$ recovers prismSndFun i x by construction. No lemmas are applied beyond the definitional equality.
why it matters
This simp lemma is the second-coordinate companion to the first-coordinate unpacking of the prism map. It lets downstream rewrites treat the $I$-factor of a prism as an ordinary real sum of barycentric weights, which is the form needed when checking boundary identities, homotopy operators, or continuity of prism constructions.
In the Recognition Science foundation layer, singular prisms sit under the topological infrastructure that supports circle-winding and higher simplicial arguments (cf. the face maps used in the circle-winding chain). The lemma itself is local bookkeeping: it does not invoke the forcing chain (T0–T8), the Recognition Composition Law, or the mass ladder, but it keeps the geometric side of those arguments machine-checkable.
No downstream consumers are recorded yet; the declaration is infrastructure for any proof that must open the second factor of prism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.