coe_mem_hullOf
plain-language theorem explainer
Each vertex of a finite tuple of points in the standard simplex lies, as an ambient coordinate vector, in the convex hull of that tuple. Subdivision and affine-map estimates cite it whenever they need vertex membership in the original hull. The proof is a one-line application of the general fact that a set sits inside its convex hull.
Claim. Fix $m\in\mathbb{N}$ and a tuple $w$ of $m+1$ points of the standard $d$-simplex in $\mathbb{R}^{d+1}$. For every index $i$, the coordinate vector of the $i$-th point $w_i$ belongs to the convex hull of $\{w_0,\ldots,w_m\}$.
background
The ambient object is the standard simplex $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(d+1))$: nonnegative coordinate vectors in $\mathbb{R}^{d+1}$ summing to $1$. A finite tuple $w$ of such points is treated as the vertex set of an affine simplex.
The local helper hullOf is the convex hull, taken in the ambient coordinate space $\mathrm{Fin}(d+1)\to\mathbb{R}$, of the range of that tuple. The module builds barycentric subdivision of affine simplices (singular chains), so hull membership is the basic containment that keeps subdivided vertices inside the original geometric simplex.
Upstream, the definition of the hull is exactly $\mathrm{convexHull},\mathbb{R}$ of the set of coordinate vectors of the $w_i$; no deeper Recognition forcing is used here.
proof idea
One-line term proof. The $i$-th coordinate vector is definitionally an element of the range of $w$, witnessed by $\langle i,\mathrm{rfl}\rangle$. Mathlib's subset_convexHull then places every point of a set inside its convex hull over $\mathbb{R}$. No case split or induction.
why it matters
This is the seed membership fact for the whole hull calculus in SingularSubdivision. Downstream, the barycenter of $w$ is shown to lie in the hull by writing it as a convex combination and invoking this lemma at each summand. The Stage 6 main estimate (barycentric subdivision support bound) and its iterated form both conclude that every vertex of every subdivided piece remains in the original hull, with pairwise distances contracted by $n/(n+1)$ (resp. its $k$-th power). Affine-map hull membership and the distance-to-vertex bound for points of an affine piece also route through it.
In the Recognition foundation stack this is pure geometric scaffolding for singular homology and prism/subdivision arguments, not a forcing-chain step (T5–T8). It closes no open physics hypothesis; it keeps subdivided supports geometrically honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.