hullOf_subset
plain-language theorem explainer
If every vertex of one finite tuple in the standard simplex lies in the convex hull of another tuple, the first hull is contained in the second. Subdivision support estimates cite this to keep barycentric pieces inside the original simplex. The argument is a one-line appeal to the universal property of convex hulls: the new vertex range already sits in a convex set containing the old vertices.
Claim. Let $w$ and $v$ be finite tuples of points in the standard simplex $\Delta^d \subset \mathbb{R}^{d+1}$. If every coordinate of $v$ (viewed in ambient $\mathbb{R}^{d+1}$) lies in the convex hull of the coordinates of $w$, then $\mathrm{conv}(\mathrm{range}\, v) \subseteq \mathrm{conv}(\mathrm{range}\, w)$.
background
In SingularSubdivision, affine simplices are vertex maps into the standard simplex $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(d+1))$. The ambient convex hull of such a tuple is the set of all real convex combinations of the embedded coordinates.
That hull is defined by taking the range of the vertex map in $\mathbb{R}^{d+1}$ and forming its convex hull over $\mathbb{R}$. Barycentric subdivision and its iterates produce new vertex tuples; geometric support must remain inside the original hull. Monotonicity under coordinatewise membership is the set-theoretic step that closes those inclusions.
The local setting is the continuum side of the singular-chain bridge: subdivided singular data stay inside the original geometric carrier before distance-contraction estimates are applied.
proof idea
Term-mode proof via Mathlib's convexHull_min. The first argument shows every point of the range of $v$ already lies in the hull of $w$: unpack the witness index $i$ and apply the membership hypothesis. The second argument records that the hull of $w$ is convex (as any convex hull is). Minimality of the convex hull then yields the inclusion of sets.
why it matters
Feeds the Stage 6 main estimate on barycentric subdivision support and its iterated form. Those results assert that every piece of the subdivision of an affine simplex has vertices in the hull of the original tuple, with pairwise distances contracted by $n/(n+1)$ (and $(n/(n+1))^k$ after $k$ iterations). The membership half of both bounds relies on this monotonicity.
In the Recognition foundation stack this keeps subdivided singular chains geometrically inside the original continuum carrier, which is the geometric side of the ledger-to-continuum identification used later in the forcing and gravity layers. It is pure convex geometry, not a physics claim, but it is load-bearing for the support control that makes the continuum bridge well-defined under refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.