affineMap_vertex
plain-language theorem explainer
The affine map determined by a vertex tuple on the standard simplex sends each standard basis vertex to the corresponding prescribed point. Singular-homology and subdivision arguments cite this as the vertex-evaluation identity for affine maps Δⁿ → Δᵐ. The proof is a coordinatewise single-term sum: vertices are Kronecker deltas, so only one summand survives.
Claim. Let $v$ assign to each index $i\in\{0,\ldots,n\}$ a point of the standard simplex $\Delta^m$. Write $A_v:\Delta^n\to\Delta^m$ for the continuous affine map with $A_v(x)_j=\sum_i x_i\,v(i)_j$. Then for every vertex $e_i$ of $\Delta^n$ one has $A_v(e_i)=v(i)$.
background
The ambient module builds continuous affine maps between standard simplices as the geometric engine for singular subdivision (barycentric and prism operators feeding singular homology). The standard simplex $\Delta^k\subset\mathbb{R}^{k+1}$ consists of nonnegative coordinates summing to one; its vertices are the standard basis vectors $e_i=\mathrm{Pi.single},i,1$.
Given a tuple $v:\mathrm{Fin}(n+1)\to\Delta^m$, the map $A_v$ is defined pointwise by the barycentric combination $A_v(x)_j=\sum_i x_i,v(i)_j$. The companion lemma affineMap_apply_coe records exactly that coordinate formula. The present statement is the special case $x=e_i$: the combination collapses to the single prescribed vertex $v(i)$.
Arithmetic facts used are the ordinary identities $1\cdot a=a$ and $0\cdot a=0$ (appearing here on real coordinates via the Mathlib instances, with parallel forms in the RS arithmetic layers).
proof idea
Extend equality of simplex points by comparing all coordinates (stdSimplex.ext), then funext on the target index $j$. Rewrite the $j$-th coordinate via the barycentric formula. Apply Finset.sum_eq_single at the vertex index $i$: the matching term is $1\cdot v(i)_j=v(i)_j$ by Pi.single_eq_same and one_mul; every off-diagonal term is $0\cdot v(b)_j=0$ by Pi.single_eq_of_ne and zero_mul; the missing-index side condition is absurd because $i$ lies in the universe. No further topology is needed.
why it matters
This is the vertex-evaluation axiom for affine maps of simplices. Downstream it discharges the identity-tuple composition: $A_v\circ\mathrm{idTuple}=v$ is literally funext of this lemma, and it feeds the face-restriction identity that $A_v\circ\mathrm{face}j=A{v\circ\mathrm{succAbove},j}$. Those two facts are the elementary naturality steps needed before prism and cone operators can be shown to act correctly on singular chains.
In the Recognition foundation stack this sits under singular subdivision infrastructure imported from Mathlib's singular homology, not under the T0–T8 forcing chain itself. It is pure geometric algebra supporting later continuum and homology constructions rather than a direct physics claim (no J-cost, phi-ladder, or dimension forcing appears here).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.