dist_sbary_le
plain-language theorem explainer
The barycenter of an m-point tuple with pairwise distances at most D lies within distance (m/(m+1))D of every point of the tuple's convex hull. Anyone tracking metric contraction under barycentric subdivision of affine simplices cites this bound. The proof reduces to a nearest-vertex comparison, rewrites barycenter-minus-vertex as an average of differences, and applies the triangle inequality after dropping the zero self-term.
Claim. Let $w_0,\ldots,w_m$ be points of the standard simplex in $\mathbb{R}^{d+1}$ with pairwise distances at most $D$. If $x$ lies in the convex hull of $\{w_0,\ldots,w_m\}$, then $\mathrm{dist}(\bar w, x) \le \frac{m}{m+1} D$, where $\bar w = \frac{1}{m+1}\sum_{i=0}^{m} w_i$ is the barycenter of the tuple.
background
The module builds affine singular chains and their barycentric subdivision in the ambient standard simplex of $\mathbb{R}^{d+1}$. An $m$-tuple $w$ is a map from $\mathrm{Fin}(m+1)$ into that simplex; its hull is the convex hull of the image points, and its barycenter is the equal-weight average of those points.
The estimate is purely metric: only pairwise distances among the vertices and membership of the test point in the hull are used. Ambient dimension $d$ is a parameter of the simplex (elsewhere fixed to the RS spatial value $3$ by the forcing chain), but the contraction factor $m/(m+1)$ depends only on the number of vertices.
Downstream, the same factor appears as the uniform pairwise-distance contraction for every piece of the barycentric subdivision of an affine simplex.
proof idea
Pick a vertex $w_j$ of the hull that realises the maximum distance from the barycenter to any hull point (via the convex-hull distance lemma); it is enough to bound $\mathrm{dist}(w_j,\bar w)$.
Rewrite $\bar w - w_j$ as the average $\sum_i (m+1)^{-1}\cdot(w_i - w_j)$. Pass the norm through the sum by the triangle inequality, factor out the positive scalar $(m+1)^{-1}$, and drop the $i=j$ term (which is zero). The remaining $m$ summands are each at most $(m+1)^{-1}D$ by the pairwise hypothesis, so the total is at most $m/(m+1),D$.
why it matters
This is the elementary metric engine behind Stage 6 of the singular-subdivision development. The sole recorded consumer is the support bound for barycentric subdivision of an affine simplex: every subdivided piece has vertices still in the original hull, and all pairwise distances shrink by the factor $n/(n+1)$.
That contraction is what makes iterated subdivision Cauchy in the mesh, so singular chains can be refined while controlling support diameter. In the broader Recognition foundation it sits under the affine/singular apparatus that realises continuous geometry on top of the discrete forcing chain (T7 eight-tick octave, T8 spatial $D=3$), without itself invoking the J-cost or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.