coe_sbary
plain-language theorem explainer
The barycenter of an (m+1)-tuple of points in the standard d-simplex, read in ambient R^{d+1}, equals the equal-weight average of those points. Cited by anyone moving between the simplex subtype and convex-hull arguments in singular subdivision. The proof is a short pointwise calculation: extensionality, sum_apply, and factoring the common scalar.
Claim. For $m \in \mathbb{N}$ and any map $w$ from an $(m+1)$-point index set into the standard $d$-simplex in $\mathbb{R}^{d+1}$, the ambient coordinate vector of the barycenter of $w$ equals $\sum_i \frac{1}{m+1}\, w(i)$.
background
The ambient space is $\mathbb{R}^{d+1}$ with the standard $d$-simplex as the set of nonnegative coordinates summing to 1. A vertex tuple $w$ is an $(m+1)$-indexed family of points in that simplex. The barycenter construction packages the equal-weight average back into the simplex subtype: each coordinate is $((m:\mathbb{R})+1)^{-1}$ times the sum of the corresponding coordinates of the $w_i$.
This module develops singular subdivision (barycentric and prism-style) for chains valued in standard simplices, importing Mathlib singular homology and the local SingularPrism layer. The present lemma is the ambient-space reading of that barycenter: it forgets the subtype and writes the average as an explicit $\mathbb{R}$-linear combination of the coersions of the vertices.
Upstream, the barycenter definition already builds the point as that scaled sum inside the subtype; the lemma only exposes the equality after coercion.
proof idea
Term-mode, pointwise. Apply function extensionality on the ambient index $j$. Rewrite the sum of functions by Finset.sum_apply, then simplify scalar multiplication on coordinates (Pi.smul_apply, smul_eq_mul). Pull the common factor $((m:\mathbb{R})+1)^{-1}$ out of the finite sum via Finset.mul_sum, and finish by reflexivity against the coordinate formula in the barycenter definition.
why it matters
Immediate parent is the membership lemma that places the barycenter in the convex hull of the vertex tuple: that argument rewrites by this equality, then invokes convexity of the convex hull and positivity of the equal weights. Without the ambient average form, the hull membership step cannot fire.
In the broader Foundation stack this is infrastructure for singular subdivision of simplices (and the prism operators imported alongside). Subdivision supplies the chain-level moves used when comparing singular chains, cones, and boundaries; the barycenter is the geometric center of those moves. The lemma itself is pure convex geometry and does not encode Recognition-specific constants, but it is part of the topological scaffolding those later arguments sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.