Taut fillings
Peter Doyle, Matthew Ellison, Zili Wang
math.GT
May 14, 2025 · v3
math.CO
TL;DR
AI tools were used to formalize and prove in Lean the splitting theorem for taut fillings and the cleanness, shellability, and flagness results.
Abstract
Let $σ$ 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 $σ$ 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.
Problem
For a simplicial triangulation of the 2-sphere, the question is what structure taut fillings have, meaning integral 3-chains of minimal L1-norm whose boundary is the associated 2-cycle. The interest comes from the Sleator–Tarjan–Thurston bounds on tetrahedral volume.
Approach
The authors prove that taut fillings of n-cycles split under almost disjoint unions when n is at least 2. In an almost disjoint union, the supports overlap in at most n+1 vertices. They use this splitting with an edge-flip and eligible-tetrahedron argument to analyze fillings of sphere triangulations. The splitting theorem and the cleanness, shellability, and flagness consequences were formalized in Lean with AI assistance, and the formal claims are those checked by the Lean kernel in the accompanying source.
Results
Any taut filling of a sphere triangulation is clean: it has no repeated tetrahedra. Its support complex is a simplicial triangulation of the 3-ball that is freely shellable and flag. Taut rational fillings also split under almost disjoint union.
