# The isoperimetric profile of the cubic three-torus

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The Isoperimetric Conjecture for the Cubic Flat Three-Torus](../../preprints/The-Isoperimetric-Conjecture-for-the-Cubic-Flat-Three-Torus-September-24-2026/article.pdf)

## Scope

The formalization determines the isoperimetric profile and all minimizers in the unit cubic flat three-torus. At every volume $0<V<1$, a minimizer exists, and the minimizers, up to null-set changes, are exactly balls, circular tubes about shortest closed geodesics, coordinate slabs, and their complements in the appropriate volume ranges.

The classification includes all equality cases at the transition volumes $4\pi/81$ and $1/\pi$, and every minimizer has the stated candidate-profile perimeter.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Isoperimetric profile and all minimizers in the cubic flat three-torus | [CubicTorus.lean](../ComparatorChallenges/CubicTorus.lean) |