dist_affineMap_le
plain-language theorem explainer
Any affine combination of the vertices of a simplex piece lies within the pairwise vertex diameter of the zeroth vertex. Diameter control under barycentric subdivision of singular simplices cites this bound. The argument is a one-line appeal to the convex-hull distance lemma once the image point and base vertex are known to sit in the hull.
Claim. Let $u_0,\ldots,u_m$ be points of the standard $d$-simplex whose pairwise distances are at most $D$. For every barycentric coordinate $x$ in the standard $m$-simplex, the affine image $\mathrm{aff}(u,x)$ satisfies $\mathrm{dist}(\mathrm{aff}(u,x),u_0)\le D$.
background
The module develops affine and singular subdivision of simplices, the combinatorial engine behind the small-simplices theorem in singular homology. An affine map sends a point of the standard $m$-simplex to the corresponding convex combination of $m+1$ labeled points in a standard $d$-simplex. The convex hull of those labeled points is the geometric support of the piece.
The key metric fact is that if every pair of generators is at most $D$ apart, then every point of the hull is at most $D$ from any fixed generator. That is exactly the content of the hull-distance lemma used here: membership of both the affine image and the zeroth vertex in the hull yields the bound.
Locally this sits inside Stage 7 of the subdivision pipeline, which iterates barycentric subdivision until every singular piece is small enough to land in one set of an open cover.
proof idea
One-line term proof. Apply the convex-hull distance lemma dist_le_of_mem_hullOf to the family of vertex distances hu, using that the affine image lies in the hull (affineMap_mem_hullOf) and that the zeroth vertex is a hull generator (coe_mem_hullOf). No further case analysis or induction.
why it matters
Feeds the Stage 7 small-simplices theorem exists_sdOpIter_small: after enough barycentric iterates, every support piece of a singular $n$-simplex has range inside one open set of a cover of $X$. Diameter control relative to a base vertex is the metric step that makes the Lebesgue-number argument close.
In the broader Recognition foundation this is pure singular-homology scaffolding (imports from Mathlib singular homology and the local SingularPrism layer). It does not itself invoke the forcing chain T0–T8, the J-cost, or the eight-tick octave; it supplies the geometric diameter estimate those later topological arguments rely on when they need subdivided chains to be cover-small.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.