sbary
plain-language theorem explainer
Defines the barycenter of an (m+1)-tuple of points in the standard d-simplex as their coordinatewise average, returning a point still in that simplex. Algebraic topologists and anyone building barycentric subdivision operators cite it as the apex map. Membership in the simplex is discharged by nonnegativity of the average and the fact that the coordinates sum to one.
Claim. Given $m\in\mathbb{N}$ and a map $w:\mathrm{Fin}(m+1)\to\Delta^d$ into the standard $d$-simplex over $\mathbb{R}$, the barycenter is the point of $\Delta^d$ whose $j$-th barycentric coordinate is $\bigl((m+1)\bigr)^{-1}\sum_i w(i)_j$.
background
The ambient object is the standard simplex $\Delta^d=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(d+1))$: nonnegative real $(d+1)$-tuples summing to $1$. A vertex tuple $w$ is an ordered list of $m+1$ such points. The barycenter is the equal-weight convex combination of those points, taken coordinatewise in the ambient $\mathbb{R}^{d+1}$.
This module develops singular subdivision for Recognition Science foundations, importing Mathlib singular homology and the local prism/cone apparatus (SingularPrism). The barycenter is the concrete apex function that later stages feed into abstract subdivision operators (asub, atee) and their equivariance lemmas.
Upstream arithmetic facts used only at the margin are the usual mul_one and nonnegativity lemmas that let the sum-to-one identity close after casting cardinalities.
proof idea
The definition packages the coordinate formula together with a two-part membership proof for stdSimplex.
Nonnegativity: each coordinate is $((m+1)^{-1})$ times a sum of nonnegative simplex coordinates, so mul_nonneg and Finset.sum_nonneg (via stdSimplex.zero_le) apply.
Sum-to-one: pull the scalar out (Finset.mul_sum), swap sums, replace each inner sum by $1$ (stdSimplex.sum_eq_one), then evaluate $\sum_{i},1=m+1$ by sum_const and card_fin. Cancel by inv_mul_cancel₀ (positivity of $m+1$).
why it matters
This is the concrete barycentric apex on $\Delta^d$. Downstream, baryFn is literally fun w => sbary w, and baryFn_apply is definitional equality. The coe lemma coe_sbary rewrites it as an ambient convex combination; dist_sbary_le gives the key metric bound (barycenter of an $m$-tuple of diameter $\le D$ lies within $\frac{m}{m+1}D$ of the hull), which drives mesh-refinement arguments for singular subdivision.
Affine equivariance sbary_affineMap supplies the intertwining hypothesis needed by stage-5a lemmas such as amap_comp_atee ("a map intertwining the apex functions intertwines atee"). In the Recognition foundation stack this is infrastructure for controlled singular chains, not a physics forcing step (T0–T8), but it is the geometric engine behind subdivision homotopies used later in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.