exists_sdOpIter_small
plain-language theorem explainer
Any singular n-simplex on a space covered by two opens U and V can be barycentrically subdivided until every subsimplex lands entirely in U or entirely in V. Algebraic topologists building Mayer–Vietoris for singular chains cite this as the geometric small-simplices step. The proof is Lebesgue-number plus diameter control on iterated affine subdivision of the standard simplex.
Claim. Let $X$ be a topological space and $U,V\subseteq X$ open with $U\cup V=X$. For every singular $n$-simplex $s:\Delta^n\to X$ there exists $k\in\mathbb{N}$ such that every affine piece $u$ appearing in the $k$-fold barycentric subdivision of the identity simplex satisfies $\mathrm{range}(s\circ u)\subseteq U$ or $\mathrm{range}(s\circ u)\subseteq V$.
background
The module develops singular subdivision for Recognition Science foundations: barycentric subdivision operators on singular chains, so that Mayer–Vietoris and excision become available in the singular setting.
A singular $n$-simplex is a continuous map from the standard simplex $\Delta^n=\mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(n+1))$ into $X$. The identity tuple generates the standard simplex; iterated affine subdivision asubIter of the barycentric map produces a finite support of affine maps $u:\Delta^n\to\Delta^n$. Pushing those pieces forward along $s$ yields the geometric subdivision of $s$.
The covering hypothesis $U\cup V=X$ with both sets open pulls back under $s$ to an open cover of the compact standard simplex. Compactness supplies a Lebesgue number: any set of diameter less than that number sits inside one member of the cover. An upstream diameter lemma (exists_asubIter_small) guarantees that some iterate makes every affine piece smaller than half that Lebesgue number.
proof idea
Identify $\sigma$ with the continuous map underlying $s$. Compactness of $\Delta^n$ is recorded once. The preimages $\sigma^{-1}(U)$ and $\sigma^{-1}(V)$ form an open cover of $\Delta^n$ (via $U\cup V=X$). Lebesgue’s number lemma in the metric topology yields $\delta>0$ such that every $\delta$-ball sits in one preimage.
Call exists_asubIter_small on half of $\delta$ to obtain an iterate $k$ making every support piece $u$ of diameter $<\delta/2$. For each such $u$, the image of the affine map through $u$ lies in the $\delta$-ball about $u(0)$ (by the diameter bound dist_affineMap_le), hence in one preimage. Transporting back via simplexEquiv_pushSimplex puts the pushed range inside $U$ or $V$.
why it matters
This is Stage 7 of the singular-subdivision development: the geometric small-simplices theorem that lets chains be refined until they respect a two-set open cover. Downstream, exists_sdOpIter_mem_smallSpan lifts the statement from generators to arbitrary singular chains by free induction, placing every chain in the small span after enough subdivision iterates.
That uniform smallness is the geometric engine of the singular Mayer–Vietoris sequence in SingularMayerVietoris. Within Recognition Science the construction sits in the Foundation layer that supplies the topological scaffolding for later forcing and continuum arguments; it does not itself invoke the J-cost, $\varphi$-ladder, or T0–T8 chain, but it is part of the singular-homology toolkit those layers may call.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.