sbary_apply
plain-language theorem explainer
Coordinate-wise, the barycenter of an (m+1)-tuple of points in the standard d-simplex is the average of those points' coordinates. Anyone working the singular-subdivision metric estimates or affine equivariance lemmas cites this as the simp unfolding of the barycenter. The proof is pure definitional equality (rfl).
Claim. For $m \in \mathbb{N}$, a map $w : \mathrm{Fin}(m+1) \to \Delta^d(\mathbb{R})$, and a coordinate index $j \in \mathrm{Fin}(d+1)$, the $j$-th barycentric coordinate of the barycenter of $w$ equals $\bigl((m:\mathbb{R})+1\bigr)^{-1} \sum_i w(i)_j$.
background
The ambient object is the standard geometric $d$-simplex $\Delta^d(\mathbb{R}) = \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(d+1))$, the set of nonnegative real $(d+1)$-tuples summing to 1. Singular subdivision works with finite tuples of such points and needs a canonical interior point of their convex hull.
That point is the barycenter sbary: given $w : \mathrm{Fin}(m+1) \to \Delta^d$, one averages the $m+1$ vertices coordinatewise, $$(\mathrm{sbary},w)_j = \frac{1}{m+1}\sum_i w(i)_j,$$ and packages the result back into the simplex (nonnegativity and sum-to-one are checked in the definition). The present lemma is exactly the coordinate projection of that definition.
The module sits in the Foundation layer that builds singular-homology subdivision operators (prism, cone, barycentric subdivision) used later for equivariance and metric control of chains.
proof idea
One-line term proof by rfl. The definition of the barycenter already sets the underlying function to the averaged coordinates, so projecting to the $j$-th coordinate is definitionally the displayed average. Marked @[simp] so later lemmas can rewrite barycenter coordinates without unfolding by hand.
why it matters
Feeds two immediate parents in the same module. First, the key metric bound: if all pairwise distances among the $m+1$ vertices are at most $D$, then the barycenter lies within $\frac{m}{m+1}D$ of every point of the hull; the proof extracts the averaged coordinates via this simp lemma. Second, the intertwining property that affine maps send barycenters to barycenters (required by the stage-5a equivariance lemmas): after stdSimplex.ext and funext, both sides reduce to the same averaged sum once coordinates are unfolded.
In the broader Recognition foundation stack this is pure geometric scaffolding for singular subdivision, not a physics forcing step (T0–T8). It keeps the barycentric calculus definitionally transparent so metric and affine arguments stay short.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.