abnd_comp_abnd
plain-language theorem explainer
The affine boundary squares to zero: ∂∘∂ = 0 as a map of affine chains AC α (n+2) → AC α n. Anyone building singular homology, barycentric subdivision, or chain homotopies on affine chains cites this. The proof is the classical face-commutation cancellation: expand the double sum, split by index order, and pair terms that differ by a sign via δ_i δ_j = δ_j δ_{i−1}.
Claim. For every $n \in \mathbb{N}$, the composition of affine boundary operators vanishes: $\partial_n \circ \partial_{n+1} = 0$ as a $\mathbb{Z}$-linear map from affine $(n+2)$-chains to affine $n$-chains on the vertex set $\alpha$.
background
Affine $n$-chains $AC,\alpha,n$ are finitely supported $\mathbb{Z}$-linear combinations of vertex tuples $\mathrm{Fin}(n+1)\to\alpha$. Generators are the affine simplices attached to such tuples. The affine boundary $\partial_n$ (written abnd n in the development) sends a generator to the alternating sum of its face restrictions, exactly as in the singular chain complex.
The module sits in the Foundation singular-subdivision stack: affine chains, cones, prisms, and barycentric subdivision operators are built so that classical Hatcher identities (chain maps, prism operators, $\partial\partial=0$) hold before any Recognition-specific forcing is applied. Upstream face-map facts (including coe_succAbove from SingularPrism) supply the combinatorial identity $\delta_i\delta_j=\delta_j\delta_{i-1}$ for $j<i$ used in the cancellation.
proof idea
Extend by linearity to a single generator $w$. Apply $\partial_n\circ\partial_{n+1}$ and expand: the double face sum becomes a sum over pairs $(i,j)\in\mathrm{Fin}(n+3)\times\mathrm{Fin}(n+2)$ of signed simplices $w\circ i.\mathrm{succAbove}\circ j.\mathrm{succAbove}$.
Rewrite as a product sum, then split the index set into $j<i$ and its complement. Construct an explicit bijection on the filtered Finsets that swaps the two index roles (sending $(i,j)$ with $j<i$ to $(j,i-1)$). Face commutation identifies the underlying simplices; the exponent of $(-1)$ increases by one, so paired terms cancel. The two halves therefore sum to negatives of each other and the total is zero.
why it matters
Nilpotency of the boundary is the first structural axiom of any chain complex. Downstream it is consumed by abnd_comp_asub (the chain-map identity $\partial\circ S=S\circ\partial$ for barycentric subdivision) and by abnd_comp_atee (the prism/chain-homotopy relation $\partial T+T\partial=\mathrm{id}-S$ in positive degrees, Hatcher Prop. 2.21).
In the Recognition foundation this clears the classical singular-homology substrate on which later forcing (eight-tick octave, dimensional constraints, cost algebra) can sit without re-proving $\partial\partial=0$. It is pure algebraic topology scaffolding, not a Recognition forcing step (T0–T8), but every subsequent subdivision or homology argument in the module depends on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.