hullOf
plain-language theorem explainer
Defines the ambient convex hull of an (m+1)-tuple of points in the standard d-simplex, as a subset of coordinate space ℝ^{d+1}. Subdivision and metric lemmas cite it to keep barycentric pieces inside the original simplex and to bound pairwise distances. The body is a one-line Mathlib convexHull of the range of the coe'd vertices.
Claim. For $m \in \mathbb{N}$ and a vertex tuple $w : \mathrm{Fin}(m+1) \to \Delta^d(\mathbb{R})$, write $\mathrm{hullOf}(w)$ for the convex hull in ambient coordinates $\mathbb{R}^{d+1}$ of the set $\{ w(i) : i \in \mathrm{Fin}(m+1) \}$.
background
This module develops affine singular subdivision for Recognition Science foundations: barycentric subdivision of affine simplices, support bounds, and diameter contraction. Vertices live in the standard simplex $\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(d+1))$, i.e. nonnegative coordinates summing to 1 in $\mathbb{R}^{d+1}$.
The ambient space is the full coordinate module $\mathrm{Fin}(d+1)\to\mathbb{R}$. Coercion from the standard simplex forgets the simplex constraints and yields ordinary vectors, so convex combinations and Euclidean distance are available via Mathlib.
hullOf packages the convex hull of those coe'd vertices. Downstream lemmas use it as the invariant set that subdivision vertices must remain inside, and as the domain for maximum-principle distance estimates.
proof idea
Pure definition: set equal to Mathlib convexHull ℝ of the range of the map sending each index $i$ to the ambient vector of $w(i)$. No proof obligations.
why it matters
Local glue for Stage 6 subdivision estimates. asub_support_bound ("every piece of the barycentric subdivision has vertices in the hull of the original tuple, pairwise distances contracted by $n/(n+1)$") and its iterate asubIter_support_bound both quantify membership in this hull. Metric lemmas dist_le_of_mem_hullOf (diameter of the hull equals diameter of the vertices) and dist_sbary_le (barycenter is within $m/(m+1)\cdot D$ of every hull point) are stated in terms of it, as are affineMap_mem_hullOf, coe_mem_hullOf, sbary_mem_hullOf, and hullOf_subset.
In the broader RS chain this is pure geometric scaffolding for singular homology / prism arguments that underwrite continuum limits and dimensional forcing, not a physics claim by itself. It does not touch T5–T8 or the RCL directly; it keeps subdivided chains inside the original simplex so diameter goes to zero under iteration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.