dist_le_of_mem_hullOf
plain-language theorem explainer
Any two points in the convex hull of a finite vertex tuple with pairwise distances at most D remain at most D apart. Metric control lemmas for singular subdivision and affine maps on standard simplices cite this maximum principle. The argument applies the convex-hull distance maximizer twice and reduces to a vertex pair via the given diameter bound.
Claim. Let $w$ be an $(m+1)$-tuple of points in the standard simplex $\Delta^d\subset\mathbb{R}^{d+1}$. If $\mathrm{dist}(w_i,w_j)\le D$ for all indices $i,j$, and if $x,y$ both lie in the convex hull of the image of $w$, then $\mathrm{dist}(x,y)\le D$.
background
The ambient setting is singular subdivision of standard simplices in Recognition Science foundation code. Points live in the standard simplex $\Delta^d\subset\mathbb{R}^{d+1}$ (barycentric coordinates summing to 1 and nonnegative). The helper hullOf w is the ordinary convex hull, in ambient Euclidean space, of the finite set of vertices ${w_0,\ldots,w_m}$ viewed as vectors in $\mathbb{R}^{d+1}$.
The quantity $D$ here is a real diameter bound on the vertex tuple, not the spatial dimension constant from the forcing chain (though that constant is also named $D$ elsewhere and equals 3 by T8). The lemma is a pure convex-geometry fact: Euclidean distance on a convex set attains its maximum on extreme points, so the diameter of a hull equals the diameter of its generating set.
Upstream, Mathlib supplies convexHull_exists_dist_ge, which produces a vertex at least as far from a fixed query point as any hull point is.
proof idea
Term-style calc after two obtains. First apply convexHull_exists_dist_ge at $x$ relative to $y$ to get a vertex $w_i$ with $\mathrm{dist}(x,y)\le\mathrm{dist}(w_i,y)$. Then apply the same lemma at $y$ relative to $w_i$ to get a vertex $w_j$ with $\mathrm{dist}(y,w_i)\le\mathrm{dist}(w_j,w_i)$. Commute the middle distance, drop the subtype coercion via Subtype.dist_eq, and finish with the hypothesis $\mathrm{dist}(w_j,w_i)\le D$.
why it matters
Immediate parent is dist_affineMap_le: every point of an affine piece lies within the piece's vertex spread of its zeroth vertex, proved by feeding this lemma the membership facts affineMap_mem_hullOf and coe_mem_hullOf. That estimate is the metric engine for Stage 7 (the small-simplices theorem) in the singular-subdivision pipeline: open covers of simplicial data must control diameters under barycentric subdivision and prism operators.
In the broader Recognition framework this is infrastructure rather than a forcing-chain step. It keeps geometric diameters under control when singular chains, cones, and prisms act on standard simplices, which is prerequisite for any later comparison of recognition cost or ledger postings on subdivided complexes. No open scaffold is closed here; the lemma is fully proved and purely metric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.