baryFn
plain-language theorem explainer
Barycentric apex map on the standard n-simplex: given any finite vertex tuple in Δⁿ it returns the barycenter of those vertices. Affine subdivision and the prism homotopy take this map as a parameter. The body is a thin wrapper that freezes the ambient dimension and delegates to the existing barycenter construction.
Claim. For each ambient dimension $n$, there is a map sending any finite tuple of points $w_0,\ldots,w_m \in \Delta^n$ to their barycenter $\frac{1}{m+1}\sum_{i=0}^{m} w_i \in \Delta^n$. This is the apex function expected by the affine subdivision and prism operators.
background
Singular subdivision in this module works with affine simplices whose vertices live in a standard simplex $\Delta^n = \mathrm{stdSimplex},\mathbb{R},(\mathrm{Fin}(n+1))$. The barycenter of a vertex tuple $w : \mathrm{Fin}(m+1) \to \Delta^n$ is the convex combination with equal weights $1/(m+1)$.
That barycenter is already implemented as sbary: it returns the point whose $j$-th barycentric coordinate is $((m:\mathbb{R})+1)^{-1}\sum_i w_i(j)$, with nonnegativity and sum-to-one proved in the subtype. Subdivision operators such as asub and the prism operator need an apex function of a fixed ambient dimension $n$, polymorphic in the number of input vertices $m$.
The local setting is Stage 6 of the singular-homology foundation: barycentric subdivision must contract diameters by the factor $n/(n+1)$ while keeping all new vertices in the convex hull of the original tuple, so that iterated subdivision produces arbitrarily small pieces.
proof idea
One-line definitional wrapper. The ambient dimension $n$ is fixed by the outer parameter; the inner argument is an $m$-tuple of points in $\Delta^n$. The body ignores the explicit $m$ binder and applies sbary to the tuple, which already computes the equal-weight barycenter in $\Delta^n$. No extra proof obligations: the subtype certificates come from sbary.
why it matters
This is the apex parameter threaded through the entire barycentric subdivision pipeline. Downstream, asub_support_bound (Stage 6 main estimate) and asubIter_support_bound use it to prove that every piece of the subdivided affine simplex has vertices in the original hull and pairwise distances contracted by $n/(n+1)$ (resp. its $k$-th power). The payoff theorem exists_asubIter_small then obtains uniformly small mesh after enough iterations.
The same map feeds the singular subdivision operator and the prism homotopy: sdOp_mem_smallSpan and tOp_mem_smallSpan in SingularMayerVietoris rely on generator compositions built from it, so that subdivision preserves the small-span submodule used in Mayer–Vietoris arguments. In the Recognition foundation this is pure algebraic topology scaffolding (singular chains, not the T0–T8 forcing chain), but it is required before singular homology can support later geometric claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.