prismSndFun_nonneg
plain-language theorem explainer
The second coordinate of each prism map is nonnegative: it equals a partial sum of barycentric coordinates of a point in the standard simplex. Algebraic topologists assembling prism operators for singular homology cite this bound. The proof is a one-line appeal to nonnegativity of finite sums of nonnegative reals.
Claim. For every index $i \in \{0,\ldots,n\}$ and every point $x$ of the standard $(n+1)$-simplex over $\mathbb{R}$, the sum of the barycentric coordinates of $x$ strictly above $i$ is nonnegative: $0 \le \sum_{k > i} x_k$.
background
The module builds prism maps on standard simplices, the classical tool that produces chain homotopies in singular homology. A point $x$ of the standard simplex $\Delta^{n+1}$ is a tuple of barycentric coordinates $x_k \ge 0$ summing to $1$.
The second coordinate of the $i$-th prism map is defined as the partial sum of those coordinates strictly above $i$: $\mathrm{prismSndFun}(i,x) = \sum_{k > i} x_k$. That quantity is the height parameter along the prism direction. Establishing it lies in the unit interval is the first arithmetic step before continuity and face relations can be stated.
proof idea
One-line term proof. Apply Finset.sum_nonneg to the finite sum defining the second prism coordinate. Each summand is a barycentric coordinate of $x$, hence nonnegative by the definition of the standard simplex (the second component of the subtype carries the pointwise nonnegativity witness). No further arithmetic is required.
why it matters
Feeds directly into the sibling lemma that places the second prism coordinate in the closed unit interval $I = [0,1]$, via the pair of bounds nonnegativity and $\le 1$. That membership is required to treat the prism map as a continuous map into $\Delta^{n} \times I$, the geometric prism used for singular chain homotopies.
In the Recognition Science foundation stack this sits inside the singular-prism scaffolding that underwrites topological forcing arguments (homology of recognition complexes). It is pure classical simplex arithmetic, not an RS-specific identity, but it is a necessary gate before prism face operators and homotopy identities can be formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.