support_abnd_asimplex
plain-language theorem explainer
Every generator in the support of the boundary of an affine simplex is one of its faces. Algebraic topologists and anyone tracking affine chain complexes or barycentric subdivision cite this. The proof rewrites the boundary via the alternating-sum formula, then unpacks Finsupp support of a finite sum of scaled singles.
Claim. Let $w : \mathrm{Fin}(n+2) \to \alpha$ be a vertex tuple and let $\sigma_w$ be the corresponding affine simplex generator. If $v$ lies in the support of $\partial_n(\sigma_w)$, then there exists $j \in \mathrm{Fin}(n+2)$ such that $v = w \circ j^{\widehat{}}$ (the $j$-th face of $w$).
background
The module SingularSubdivision builds an affine chain complex on a type $\alpha$ of vertices. An affine $n$-simplex generator is the Dirac mass $\sigma_w = \mathrm{single}(w,1)$ on a tuple $w : \mathrm{Fin}(n+1)\to\alpha$. Affine chains $\mathrm{AC},\alpha,n$ are finitely supported $\mathbb{Z}$-linear combinations of such generators.
The boundary $\partial_n : \mathrm{AC},\alpha,(n+1)\to\mathrm{AC},\alpha,n$ is the linear map sending each generator to the alternating sum of its faces: $\partial(\sigma_w)=\sum_i (-1)^i,\sigma_{w\circ i^{\widehat{}}}$. The companion lemma records exactly that identity on generators.
Support here is ordinary Finsupp support: the finite set of tuples with nonzero coefficient. The claim is that after taking $\partial$ of a pure generator, only face tuples can carry nonzero mass.
proof idea
Term-mode unpacking of Finsupp support. Rewrite the membership hypothesis by the generator boundary formula, so $v$ lies in the support of a finite sum $\sum_i (-1)^i,\sigma_{w\circ i^{\widehat{}}}$. Extract a summand index $j$ via Finsupp.mem_support_finset_sum. The scaled single $\sigma_{w\circ j^{\widehat{}}}$ has support contained in the singleton ${w\circ j^{\widehat{}}}$ (support_smul, support_single_subset), forcing $v$ equal to that face.
why it matters
Feeds the Stage 6 main estimate asub_support_bound: every piece of the barycentric subdivision of an affine simplex has vertices in the original hull, with pairwise distances contracted by $n/(n+1)$. That estimate needs control on which generators appear after boundary and subdivision operators; this lemma supplies the boundary half for pure generators.
In the Recognition foundation stack, affine singular chains and their subdivision operators underwrite discrete geometric comparisons (diameter contraction, hull membership) used later in gravity and ledger geometry. The result is local linear-algebra bookkeeping, not a forcing-chain step, but it is load-bearing for the subdivision diameter bound that those comparisons rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.