asub_asimplex
plain-language theorem explainer
On generators, barycentric subdivision in degree n+1 is exactly the cone on the barycenter of the subdivided boundary. Algebraic topologists cite this when verifying that the subdivision operator is a chain map or a chain homotopy factor. The proof is a one-line evaluation of the linearCombination definition on a single simplex.
Claim. For any apex rule $\mathrm{bary}$ and any vertex tuple $w:\mathrm{Fin}(n+2)\to\alpha$, the barycentric subdivision of the affine generator $\sigma_w$ in degree $n+1$ equals the cone with apex $\mathrm{bary}(w)$ applied to the subdivision of $\partial\sigma_w$: $S_{n+1}(\sigma_w)=C_{\mathrm{bary}(w)}\bigl(S_n(\partial\sigma_w)\bigr)$.
background
The module builds affine singular chains $AC,\alpha,n$ as finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. Generators are the Dirac simplices $\sigma_w$. The boundary $\partial:AC,\alpha,(n+1)\to AC,\alpha,n$ is the alternating sum of face restrictions $w\circ i.succAbove$. The cone $C_b$ prepends a fixed apex $b$ to every tuple, raising degree by one.
Barycentric subdivision $S$ is defined recursively on generators by the classical cone formula: $S_0=\mathrm{id}$ and $S_{n+1}(\sigma_w)=C_{\mathrm{bary}(w)}(S_n(\partial\sigma_w))$. The apex rule $\mathrm{bary}$ is an arbitrary family of maps choosing a point in each simplex (later specialized to the geometric barycenter). The evaluation lemma for linear combinations on generators reduces any identity of maps built by $Finsupp.linearCombination$ to a check on single tuples.
proof idea
One-line term proof. By definition, $S_{n+1}$ is the linear combination whose value on a generator tuple $w$ is exactly $C_{\mathrm{bary}(w)}(S_n(\partial\sigma_w))$. The lemma $lift_asimplex$ states that a $Finsupp.linearCombination$ map applied to $\sigma_w$ returns the coefficient function at $w$. Instantiating that evaluation finishes the proof.
why it matters
This generator identity is the computational engine for the chain-map theorem $\partial\circ S=S\circ\partial$ (abnd_comp_asub), which opens the inductive argument in degree zero by rewriting $S(\sigma_w)$ via the cone formula. The same rewrite feeds the chain-homotopy identity $\partial T+T\partial=\mathrm{id}-S$ in positive degrees (abnd_comp_atee, Hatcher's Prop. 2.21) and the equivariance of $S$ under maps that intertwine apex rules (amap_comp_asub).
Downstream, the Stage 6 diameter estimate (asub_support_bound) relies on the recursive cone structure to prove that every piece of a subdivided affine simplex stays in the original hull and contracts pairwise distances by $n/(n+1)$. In the Recognition Science foundation this supplies the mesh-refinement step that makes singular chains compatible with the discrete recognition calculus, without yet invoking the forcing chain T0–T8 or the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.