exists_asubIter_small
plain-language theorem explainer
Iterated barycentric subdivision shrinks every affine simplex in the standard simplex to arbitrarily small diameter: for any ε>0 some iterate k makes all support pieces have pairwise vertex distance <ε. Algebraic topologists cite this as the Stage 6 diameter payoff before the small-simplices cover argument. The proof is a geometric-series bound: diameter contracts by the factor n/(n+1)<1 at each step.
Claim. Fix $n\in\mathbb{N}$ and an affine $n$-simplex whose vertices lie in the standard $d$-simplex. For every $\varepsilon>0$ there exists $k\in\mathbb{N}$ such that every simplex $u$ in the support of the $k$-fold barycentric subdivision of that affine simplex satisfies $\mathrm{dist}(u(i),u(j))<\varepsilon$ for all vertices $i,j$.
background
This lives in the Diameter section of the singular-subdivision foundation module, which builds an affine barycentric subdivision operator on chains of standard simplices and then lifts it to singular chains on a space $X$. An affine simplex is a tuple of points in $\Delta^d$; its support after subdivision is the finite set of smaller affine simplices produced by repeatedly inserting barycenters.
The key geometric fact is classical: each barycentric step multiplies diameters by at most $n/(n+1)<1$. The module packages that contraction as a support-wise bound on the iterated affine subdivision (with the barycenter map as the subdivision rule). Upstream, the iteration combinator is the ordinary $k$-fold function iterate; the ambient metric is the standard simplex metric, whose diameter is at most $1$.
Stage 6 is purely metric. Stage 7 will feed the same support into a Lebesgue-number argument for open covers of $X$.
proof idea
First record $n/(n+1)<1$ by positivity and a one-line linear arithmetic comparison. Invoke the standard real-analysis lemma that powers of a number strictly less than $1$ fall below any positive $\varepsilon$, obtaining $k$ with $(n/(n+1))^k<\varepsilon$.
For an arbitrary support simplex $u$ of the $k$-fold affine subdivision of the input, apply the pre-proved support diameter bound: pairwise distances are at most $(n/(n+1))^k$ times the original diameter bound $1$ (itself from the fact that any two points of a standard simplex are at distance $\le 1$). Cancel the factor $1$ and conclude the distance is $<\varepsilon$.
why it matters
This is the Stage 6 payoff named in the module doc: iterated barycentric pieces become uniformly small. The sole recorded consumer is the Stage 7 small-simplices theorem, which states that for an open cover $U\cup V=X$ and any singular $n$-simplex there is an iterate of the singular subdivision operator whose pieces land entirely in $U$ or entirely in $V$.
That Stage 7 result combines the present diameter decay with the Lebesgue number of the preimage cover on the compact metric $\Delta^n$, then identifies support pieces with the generators of the singular subdivision operator via the generator-compatibility lemma. The chain-homotopy relating the iterated subdivision to the identity is supplied separately, so together these steps give the classical subdivision argument underlying Mayer–Vietoris and excision in the Recognition singular-homology bridge.
Within the broader forcing chain this is infrastructure rather than a T0–T8 landmark: it equips the foundation layer with a fully formal small-simplices engine so later geometric and physical constructions can quote singular homology without metric gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.