affineMapFun_mem
plain-language theorem explainer
The barycentric combination of simplex vertices stays inside the target standard simplex: if each vertex of an n-simplex is mapped to a point of Δ^m and x is a barycentric coordinate vector on Δ^n, then ∑_i x_i · v_i lies in Δ^m. Anyone building continuous affine maps Δ^n → Δ^m (singular chains, prism operators, subdivision) cites this membership lemma. The proof is a short two-goal tactic argument: nonnegativity of the double sum, then sum-to-one after commuting the sums.
Claim. Let $v : \mathrm{Fin}(n+1) \to \Delta^m$ be a tuple of points in the standard $m$-simplex and let $x \in \Delta^n$. Write $y_j = \sum_i x_i \, v_i(j)$ for each coordinate $j$. Then $y \in \Delta^m$: each $y_j \ge 0$ and $\sum_j y_j = 1$.
background
The ambient setting is singular subdivision in the Foundation layer: continuous maps between standard simplices, used to build chain-level operators (boundaries, cones, prisms, subdivisions) over $\mathbb{R}$.
The standard simplex $\Delta^k \subset \mathbb{R}^{k+1}$ consists of nonnegative coordinate vectors summing to $1$. The underlying function affineMapFun sends $x \in \Delta^n$ to the barycentric combination $\sum_i x_i \cdot v_i$ of a prescribed vertex tuple $v$, written coordinatewise as $j \mapsto \sum_i x_i , v_i(j)$.
Membership in $\Delta^m$ is exactly the pair of conditions (nonnegativity of each coordinate, total mass one). The lemma discharges that pair so the combination can be packaged as a point of the subtype stdSimplex.
proof idea
Tactic proof with two constructor goals for the simplex subtype.
Nonnegativity: for each target coordinate $j$, the sum $\sum_i x_i v_i(j)$ is a sum of products of nonnegative reals (stdSimplex.zero_le on $x$ and on each $v_i$), hence nonnegative by Finset.sum_nonneg and mul_nonneg.
Mass one: rewrite $\sum_j \sum_i x_i v_i(j)$ by commuting the finite sums, factor $x_i$ out of the inner sum, and apply stdSimplex.sum_eq_one on each $v_i$ to obtain $\sum_i x_i \cdot 1$. Then mul_one and stdSimplex.sum_eq_one on $x$ finish the calculation.
why it matters
This is the pure set-theoretic half of the continuous affine map $\Delta^n \to \Delta^m$ determined by a vertex tuple. Downstream, affineMap packages the function with this membership proof and a continuity proof into a C(Δ^n, Δ^m) morphism used throughout singular subdivision.
In the Recognition Science foundation stack, singular simplices and their subdivisions underwrite the combinatorial geometry behind the eight-tick octave and the discrete recognition calculus (T7 and the singular-homology imports). Without closed membership, the affine maps that implement face, cone, and prism operators cannot even be typed as maps of simplices.
The lemma is fully proved (no sorry); it closes a small but mandatory gap between the raw barycentric formula and the continuous map object the rest of the module consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.