prismSndFun_mem_unitInterval
plain-language theorem explainer
The second barycentric coordinate of each prism map lands in the closed unit interval. Anyone constructing continuous prism operators Δ^{n+1} → Δ^n × I needs this membership fact to package the height coordinate as an element of I. The proof is a one-line wrapper: nonnegativity and the upper bound ≤ 1 are paired via the closed-interval membership criterion.
Claim. For every index $i \in \mathrm{Fin}(n+1)$ and every point $x$ of the standard simplex $\Delta^{n+1}$ over $\mathbb{R}$, the second prism coordinate $s_i(x) := \sum_{k > i} x_k$ satisfies $s_i(x) \in [0,1]$.
background
The module builds affine prism maps used in singular homology: continuous maps $\Delta^{n+1} \to \Delta^n \times I$ that subdivide the prism $\Delta^n \times I$ into $n+1$ simplices. The second coordinate of the $i$-th such map is the partial sum of barycentric coordinates of $x \in \Delta^{n+1}$ strictly above index $i$.
A point of the standard simplex has nonnegative barycentric coordinates summing to 1. Consequently any subsum is nonnegative and at most the full sum 1. The closed unit interval $I = [0,1]$ is the codomain needed so that the height coordinate can be paired with a point of $\Delta^n$ inside the product space.
Upstream, nonnegativity of the partial sum and the bound $\le 1$ are already recorded as separate lemmas; the present statement only packages them as interval membership.
proof idea
One-line wrapper applying Set.mem_Icc.mpr. The two conjuncts are exactly the upstream lemmas: nonnegativity of the filtered barycentric sum, and the comparison of that sum against the full sum (which equals 1 on the simplex). No further arithmetic is required.
why it matters
The continuous prism map is defined by sending $x$ to the pair (face projection via predAbove, height coordinate). The height must inhabit $I$, not bare $\mathbb{R}$; this lemma supplies the proof term that constructs the subtype element. Without it the prism definition cannot typecheck.
In the broader foundation layer this is pure scaffolding for singular-homology prism operators (homotopies and subdivision), not a Recognition-forcing step (T0–T8). It sits upstream of any later use of prism operators in chain-level arguments, but does not itself touch J-cost, $\varphi$, or dimensional forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.