support_acone
plain-language theorem explainer
Every generator in the support of an affine cone chain is the original support generator with the apex prepended. Support-tracking arguments in barycentric subdivision cite this when pushing diameter bounds through the cone operator. The proof is a short unpack of Finsupp.mapDomain support: the cone is lmapDomain of Fin.cons, so support lands in the image of that map.
Claim. Let $c$ be an affine $n$-chain on a type $\alpha$ (a finitely supported $\mathbb{Z}$-combination of maps $\mathrm{Fin}(n+1)\to\alpha$), and let $b\in\alpha$. Write $\mathrm{cone}_b(c)$ for the image of $c$ under the linear map that prepends $b$ to every vertex tuple. Then for every $u$ in the support of $\mathrm{cone}_b(c)$ there exists $v$ in the support of $c$ with $u=\mathrm{Fin.cons}\,b\,v$.
background
The module works with affine chains on a vertex type $\alpha$: an affine $n$-chain is a finitely supported integer combination of ordered $(n+1)$-tuples $\mathrm{Fin}(n+1)\to\alpha$. Generators are the obvious Dirac masses on those tuples.
The cone operator with apex $b$ is the $\mathbb{Z}$-linear map $\mathrm{AC},\alpha,n\to\mathrm{AC},\alpha,(n+1)$ induced by prepending $b$ on the domain of each tuple (implemented as Finsupp.lmapDomain of Fin.cons b). Support of a Finsupp is the finite set of domain points with nonzero coefficient.
This lemma sits in the SupportTracking section of SingularSubdivision, which records how supports move under the elementary affine operators used to build barycentric subdivision. Upstream, the cone is defined exactly as that domain map; the claim is the corresponding support-image statement.
proof idea
Classical reasoning, then introduce $u$ in the support of the cone. Unfold the cone definition and Finsupp.lmapDomain_apply, so membership becomes membership in the support of a mapDomain along Fin.cons b. Apply Finsupp.mapDomain_support and Finset.mem_image to extract a preimage $v$ already in the support of $c$ with image equal to $u$. Symmetry of that equality finishes the existential.
why it matters
Barycentric subdivision is built by iterated coning and face operators on affine chains. Diameter and hull control for subdivided pieces require knowing that every surviving generator is a cone over an earlier generator, not an arbitrary new tuple. Downstream, asub_support_bound (Stage 6 main estimate) uses this: every piece of the barycentric subdivision of an affine simplex has vertices in the original hull and pairwise distances contracted by $n/(n+1)$. That estimate is the geometric engine for mesh refinement in the singular-homology side of the foundation stack. Within Recognition Science this is pure scaffolding for the topological forcing apparatus (singular chains, subdivision, homology), not a direct T0–T8 identity, but it is required infrastructure before continuum or continuum-limit arguments can sit on a formal chain complex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.