prismSndFun_le_one
plain-language theorem explainer
On the standard simplex, the partial sum of barycentric coordinates strictly above a fixed index is at most 1. Anyone building prism operators for singular chains or checking that prism coordinates land in [0,1] cites this bound. The proof compares that filtered sum to the full barycentric sum via a nonnegativity subset argument, then uses that the full sum equals 1.
Claim. For every index $i \in \{0,\ldots,n\}$ and every point $x$ of the standard $(n+1)$-simplex in $\mathbb{R}^{n+2}$, the sum of the barycentric coordinates of $x$ over indices strictly larger than $i$ is at most $1$.
background
The ambient object is the standard simplex $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin},(n+2))$: nonnegative barycentric coordinates on $n+2$ vertices that sum to 1. Prism maps for singular homology send an $(n+1)$-simplex times an interval into an $(n+2)$-simplex; their second coordinate is the partial sum of those barycentrics lying strictly above a chosen face index.
That second coordinate is defined as $\sum_{k:,i.castSucc < k} x_k$. Nonnegativity of each $x_k$ is part of the simplex structure, and the full sum $\sum_k x_k = 1$ is the remaining simplex axiom. The present bound is the upper half of the claim that this partial sum lies in the unit interval $[0,1]$.
proof idea
Term-mode calc with two steps. First, the filtered sum over ${k \mid i.castSucc < k}$ is at most the unrestricted sum $\sum_k x_k$, by Finset.sum_le_sum_of_subset_of_nonneg applied to the filter-subset inclusion and the pointwise nonnegativity of the barycentric coordinates. Second, the unrestricted sum equals 1 by the simplex normalization axiom. No other lemmas are required.
why it matters
This is the upper bound half of the unit-interval membership for the prism second coordinate. The immediate parent is prismSndFun_mem_unitInterval, which packages nonnegativity with this inequality into $x \mapsto \mathrm{prismSndFun},i,x \in I = [0,1]$. That membership is needed so the prism map lands in a product of a simplex with the unit interval, the standard domain for prism operators in singular homology.
In the Recognition Science foundation layer the singular-prism apparatus supports chain-level constructions (homotopies, subdivisions) that underwrite discrete-to-continuous comparison arguments. The lemma itself is pure convex geometry; its place in the stack is as a short, fully discharged inequality feeding the continuous prism map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.