eps
plain-language theorem explainer
The augmentation map sends an affine 0-chain to the sum of its integer coefficients. Algebraic topologists and anyone building the RS singular-chain complex cite it as the terminal face of the chain complex. It is defined directly as the Finsupp linear combination that evaluates every generator at 1.
Claim. For any type $\alpha$, the augmentation $\varepsilon:\mathrm{AC}(\alpha,0)\to\mathbb{Z}$ is the $\mathbb{Z}$-linear map on finitely supported 0-chains that sends each generator (a point of $\alpha$) to $1$, equivalently the sum of all coefficients of the chain.
background
In this module, affine $n$-chains $\mathrm{AC}(\alpha,n)$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. When $n=0$ the generators are simply points of $\alpha$, so a 0-chain is a finite formal sum $\sum_i c_i[p_i]$ with $c_i\in\mathbb{Z}$.
The classical augmentation of a simplicial (or singular) chain complex is the unique chain map from degree 0 to $\mathbb{Z}$ that sends every oriented point to $1$. It is the last nontrivial differential in the augmented complex and is used to define reduced homology. The module builds the affine singular apparatus (boundaries, cones, prism operators, subdivision) needed later for Recognition Science foundation arguments that pass through singular homology.
proof idea
One-line definition: apply Finsupp.linearCombination over $\mathbb{Z}$ with the constant weight function that assigns $1$ to every generator of type $\mathrm{Fin},1\to\alpha$. No further lemmas are invoked; the Finsupp API supplies $\mathbb{Z}$-linearity automatically.
why it matters
Augmentation is the standard terminal map of the affine chain complex assembled in SingularSubdivision. Sibling maps (affine boundary, cone, and the induced maps on simplices) compose with it in the usual way, so every later identity about reduced 0-homology or cone contractions routes through $\varepsilon$.
Downstream modules that import the subdivision stack (Hamiltonian emergence, J-cost Hessian certificates, primitive recognition calculus distance increments) sit on top of this chain-level infrastructure. Within the RS forcing chain the singular apparatus is scaffolding for continuum limits and local quadratic expansions of the J-cost $J(x)=(x+x^{-1})/2-1$, not a direct T0–T8 step, but it is the homology language those continuum arguments speak.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.