asubIter_support_bound
plain-language theorem explainer
k-fold barycentric subdivision of an affine n-simplex contracts every pairwise vertex distance by the factor (n/(n+1))^k, while keeping all new vertices inside the original convex hull. Anyone proving mesh-refinement or diameter-control for singular chains cites this bound. The argument is induction on k, feeding the one-step support bound through a support-transport lemma.
Claim. For every $k\in\mathbb{N}$, every $n$, every vertex tuple $w:\mathrm{Fin}(n+1)\to\Delta^d$, and every $D\ge 0$ with $\mathrm{dist}(w_i,w_j)\le D$ for all $i,j$: if $u$ lies in the support of the $k$-fold iterated barycentric subdivision of the affine simplex on $w$, then $\mathrm{dist}(u_i,u_j)\le\bigl(\frac{n}{n+1}\bigr)^k D$ for all $i,j$, and each $u_i$ lies in the convex hull of $w$.
background
The module develops affine singular subdivision on the standard simplex $\Delta^d\subset\mathbb{R}^{d+1}$. An affine $n$-simplex is a vertex map $w:\mathrm{Fin}(n+1)\to\Delta^d$; its formal chain is written $\mathrm{asimplex},w$. The one-step operator $\mathrm{asub}(\mathrm{baryFn},d),n$ replaces each such simplex by the formal sum of its barycentric children. Iteration $\mathrm{asubIter},k$ is the $k$-fold composite of that operator.
The geometric content is diameter control: each barycentric child has pairwise distances scaled by at most $n/(n+1)<1$ relative to its parent, and all new vertices remain in the convex hull of the original tuple (denoted $\mathrm{hullOf},w$). The one-step statement of that fact is the sibling bound on the support of a single subdivision; the present theorem lifts it to arbitrary iteration depth.
Spatial dimension $d$ is the ambient simplex dimension used throughout the singular-homology setup (forced to $3$ elsewhere in the foundation chain, but treated as a fixed parameter here).
proof idea
Induction on the iteration depth $k$.
Base $k=0$: $\mathrm{asubIter}$ is the identity, so the support is the singleton ${\mathrm{asimplex},w}$. The distance claim reduces to the hypothesis via $\mathrm{pow_zero}$ and $\mathrm{one_mul}$; hull membership is the tautology that each vertex of $w$ lies in $\mathrm{hullOf},w$.
Successor: rewrite by $\mathrm{asubIter_succ}$ and $\mathrm{LinearMap.comp_apply}$, then apply the support-transport lemma with predicates $P$ (the inductive diameter/hull bound at depth $k$) and $Q$ (the same bound at depth $k+1$). The inductive hypothesis supplies $P$ on the intermediate support. For each intermediate vertex $v$ satisfying $P$, the one-step support bound $\mathrm{asub_support_bound}$ yields the extra factor $n/(n+1)$ on distances and hull membership for children; multiplying powers and using $\mathrm{hullOf_subset}$ closes $Q$.
why it matters
This is the quantitative engine behind Stage 6 of the singular-subdivision development. The sole downstream consumer is $\mathrm{exists_asubIter_small}$, whose doc-comment calls it the "Stage 6 payoff": for any $\varepsilon>0$ there exists $k$ such that every simplex in the $k$-fold subdivided support has diameter $<\varepsilon$. That existence is immediate once the geometric ratio $(n/(n+1))^k\to 0$ is in hand.
In the broader Recognition foundation, controlled mesh refinement of singular chains is the bridge from combinatorial eight-tick / $D=3$ structure (T7–T8) to continuous singular homology. Without a uniform diameter bound on iterated barycentric pieces, one cannot pass from discrete recognition events to continuum limits or homology comparisons. The theorem itself is pure convex geometry; its place in the chain is as the diameter lemma that makes the Stage 6 smallness statement unconditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.