abnd_asimplex
plain-language theorem explainer
On an affine generator simplex with vertex tuple w, the boundary operator returns the alternating sum of its face simplices. Anyone proving chain-complex identities (∂∂ = 0, cone formulas, subdivision chain maps) cites this evaluation. The proof is a one-line application of the linearCombination-on-generator lemma.
Claim. For any vertex tuple $w : \mathrm{Fin}(n+2) \to \alpha$, the affine boundary of the generator simplex on $w$ equals $\sum_{i \in \mathrm{Fin}(n+2)} (-1)^i \, [w \circ i^{\uparrow}]$, where $i^{\uparrow}$ is the face map omitting the $i$-th vertex.
background
The module builds the affine chain complex used for singular subdivision. Affine $n$-chains $\mathrm{AC},\alpha,n$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. The generator $\mathrm{asimplex}(w)$ is the Dirac chain at tuple $w$.
The boundary $\partial : \mathrm{AC},\alpha,(n+1)\to\mathrm{AC},\alpha,n$ is defined by linear extension of the classical alternating face sum: on a tuple $w$, sum $(-1)^i$ times the face that drops coordinate $i$ via $\mathrm{Fin.succAbove}$. Upstream, $\mathrm{lift_asimplex}$ records that any map built by $\mathrm{Finsupp.linearCombination}$ evaluates on a generator by reading the coefficient function at that tuple.
Local setting is pure algebraic topology scaffolding (Mathlib singular homology imports plus the in-module prism/cone apparatus), not yet the RS forcing chain.
proof idea
One-line term proof: apply $\mathrm{lift_asimplex}$ to the coefficient function that defines $\mathrm{abnd},n$. Because $\mathrm{abnd}$ is exactly $\mathrm{Finsupp.linearCombination}$ of the alternating face sum, evaluation on $\mathrm{asimplex}(w)$ returns that sum at $w$. No further rewriting is needed.
why it matters
This is the generator-level face formula that every subsequent boundary identity reduces to via $\mathrm{AC.hom_ext}$. Downstream parents include $\partial\partial=0$ ($\mathrm{abnd_comp_abnd}$), the cone identities $\partial(b\cdot c)=c-b\cdot\partial c$ in positive degree and the degree-zero augmentation form, naturality of pushforward past $\partial$, $\varepsilon\circ\partial=0$, support control on boundaries, and ultimately that the singular subdivision operator is a chain map ($\partial\circ S=S\circ\partial$).
In the Recognition framework this sits in Foundation singular-subdivision infrastructure: it supplies the algebraic $\partial$ needed before geometric subdivision, prism operators, and gluing arguments can talk about chains. It does not itself touch T0–T8, RCL, or constants; it is the classical chain-complex hinge those later constructions rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.