eps_comp_abnd
plain-language theorem explainer
The augmentation on affine 0-chains annihilates every boundary from degree 1: ε ∘ ∂₀ = 0. Cited when checking that barycentric subdivision is a chain map in degree zero, and more generally whenever total mass of a 1-boundary must vanish. Proof evaluates on generators, expands the two-term alternating face sum, and cancels the unit coefficients by arithmetic.
Claim. For affine chains valued in a type $\alpha$, the composition of the augmentation $\varepsilon$ with the degree-$0$ affine boundary $\partial_0$ is the zero map: $\varepsilon \circ \partial_0 = 0$.
background
The module builds barycentric subdivision for affine singular chains. Generators are affine simplices (vertex tuples in a carrier $\alpha$); chains form the free module AC on those generators. The affine boundary abnd is the usual alternating sum of faces. The augmentation eps is the linear map on 0-chains that sends every vertex to the unit coefficient, so it records total mass.
Classically $\varepsilon\partial=0$: every 1-boundary has coefficient sum zero. That is the degree-zero shadow of $\partial^2=0$ after composing with augmentation, and it is the first compatibility needed before subdivision can be shown to intertwine with $\partial$. The surrounding Stage-3 development treats subdivision via an abstract apex (barycenter) function; the present identity is independent of that choice.
proof idea
Term-mode proof via free-module extensionality: AC.hom_ext reduces equality of chain maps to evaluation on generators. On a 1-simplex, abnd_asimplex expands the boundary as a two-term sum (Fin.sum_univ_two). After map_sum and map_smul, eps_asimplex turns each face into a signed unit; the signs are $1$ and $-1$ (pow_zero, pow_one). The resulting $1-1$ is discharged by omega, matching the zero map.
why it matters
Direct input to abnd_comp_asub, the chain-map identity $\partial\circ S=S\circ\partial$ for the barycentric subdivision operator on affine chains. That identity is the main Stage-3 goal of this module (subdivision defined by the cone recursion $S(\sigma)=b_\sigma\cdot S(\partial\sigma)$). Without $\varepsilon\partial=0$, the degree-zero case of the chain-map square does not close.
In the Recognition foundation layer this is infrastructure, not a forcing-chain step (T0–T8). It supplies the singular/affine chain toolkit used later for topological and dimensional arguments. The result is fully proved (no sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.