# A hyperbolic group without a geometric CAT(0) action

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

- [A hyperbolic group with no geometric $\mathrm{CAT}(0)$ action](../../preprints/A-hyperbolic-group-with-no-geometric-CAT0-action-September-25-2026/paper.pdf)

## Scope

The formalized result constructs a finite connected aspherical complex with a linear disk-filling bound whose fundamental group is word-hyperbolic but admits no geometric action on a nonempty proper complete $\mathrm{CAT}(0)$ space. It also excludes locally $\mathrm{CAT}(-1)$ geodesic metrics on every finite complex homotopy equivalent to the witness. The stronger claims that the witness is two-dimensional and that those models admit no locally $\mathrm{CAT}(0)$ metric are not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Hyperbolic group with no geometric CAT(0) action | [HyperbolicObstruction.lean](../ComparatorChallenges/HyperbolicObstruction.lean) |