# Sharp Cartan–Hadamard isoperimetry and rigidity

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

- [Sharp integral fillings in $\mathrm{CAT}(0)$ spaces](../../preprints/Sharp-integral-fillings-in-CAT(0)-spaces-September-23-2026/paper.pdf)

## Scope

The formalization proves the sharp Euclidean filling inequality for every compactly supported integral $n$-cycle in a proper $\mathrm{CAT}(0)$ space, for $n\ge2$. It constructs a compactly supported integral filling whose mass is at most $C_n$ times the boundary mass to the power $(n+1)/n$, where $C_n$ is the Euclidean isoperimetric coefficient. Integer multiplicities and the ambient dimension are unrestricted.

A second statement proves that this coefficient is optimal by giving, in Euclidean space, a cycle for which every compactly supported integral filling has at least that mass. This yields the selected integral-current form of the Cartan–Hadamard isoperimetric conjecture.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Optimality of the Euclidean filling coefficient | [FillingCoefficient.lean](../ComparatorChallenges/FillingCoefficient.lean) |
| Sharp integral fillings in proper $\mathrm{CAT}(0)$ spaces | [SharpCAT0Filling.lean](../ComparatorChallenges/SharpCAT0Filling.lean) |