sbary_mem_hullOf
plain-language theorem explainer
The barycenter of any finite tuple of points in the standard simplex lies in their convex hull in ambient coordinates. Subdivision and diameter-contraction arguments cite this to keep barycentric vertices inside the original support. The proof rewrites the barycenter as the equal-weight convex combination and applies convexity of the hull with unit total mass.
Claim. For any $m\in\mathbb{N}$ and any map $w:\{0,\ldots,m\}\to\Delta^{d}$ into the standard $d$-simplex, the barycenter of $w$, viewed as a point of $\mathbb{R}^{d+1}$, lies in the convex hull of the image of $w$.
background
The module develops affine singular subdivision for chains valued in the standard simplex $\Delta^{d}\subset\mathbb{R}^{d+1}$. Here $d$ is the ambient spatial dimension used throughout the foundation stack (forced to $3$ by the T8 step of the forcing chain). An affine $m$-simplex is a tuple $w$ of $m+1$ vertices in $\Delta^{d}$.
The hull of $w$ is the convex hull in ambient Euclidean space of the coersions of those vertices. The barycenter of $w$ is the equal-weight average of the vertices. Upstream, the coersion of each vertex already sits in the hull (by the generating inclusion into a convex hull), and the barycenter expands explicitly as $\sum_i (m+1)^{-1}\cdot w_i$ in ambient coordinates.
Locally this is pure convex geometry: once the barycenter is written as a convex combination with nonnegative weights summing to one, membership in the hull is immediate from convexity.
proof idea
Term-mode proof. Rewrite the ambient barycenter via the explicit average formula (equal weights $(m+1)^{-1}$). Apply the sum-membership rule for a convex set: the convex hull is convex, each weight is positive, and each vertex coersion lies in the hull by the vertex-membership lemma. It remains only to check that the weights sum to $1$: the sum is a constant sum over a finite index of cardinality $m+1$, which reduces to $(m+1)\cdot(m+1)^{-1}=1$ after casting and cancelling the nonzero scalar.
why it matters
Feeds the Stage 6 main estimate on barycentric subdivision: every piece of the subdivided affine simplex has vertices in the original hull, with pairwise distances contracted by the factor $n/(n+1)$. That estimate needs barycenters (and iterated cone/barycenter constructions) to remain inside the support hull; this lemma is the base membership fact.
In the Recognition foundation stack, controlled subdivision of singular simplices underwrites the chain-level geometry behind the eight-tick and dimensional forcing arguments. Without hull membership of barycenters, the diameter-contraction induction for affine subdivision would not close. The result is elementary convex analysis, but it is the precise hinge between the combinatorial subdivision operator and the metric support bound used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.