Taut fillings

Abstract

Let $\ddot{I}ƒ$ be a simplicial triangulation of the 2-sphere, $X$ the associated integral 2-cycle. A filling of $X$ is an integral 3-chain $M$ with $\partial M=X$; a taut filling is one with minimal $L_1$-norm. We show that any taut filling arises from an extension of $\ddot{I}ƒ$ to a simplicial complex homeomorphic to the 3-ball. The filling is clean: it has no repeated tetrahedron, and its support complex is a clean simplicial complex. This support complex is shellable and flag: every clique in its 1-skeleton occurs as a simplex. The key to the proof is the general fact that any taut filling of an $n$-cycle splits under disjoint union, connected sum, and more generally what we call almost disjoint union, where summands are supported on sets that overlap in at most $n+1$ vertices. We used AI to formalize and prove in Lean the splitting theorem and the resulting cleanness, shellability, and flagness results.

Using AI, all results have now been cleaned up,formalized, and verified in Lean 4