# Negative Kähler curvature without bounded holomorphic coordinates

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

- [A negatively pinched Kähler threefold without bounded holomorphic coordinates](../../preprints/A-negatively-pinched-Kahler-threefold-without-bounded-holomorphic-coordinates-September-25-2026/paper.pdf)

## Scope

The formalized result constructs a nonempty contractible complex threefold with a complete Kähler metric whose real sectional curvatures lie between two fixed negative constants. Nevertheless, it has no system of bounded holomorphic coordinates and is not biholomorphic to a bounded domain. The metric is obtained from an explicitly controlled potential. This is the negatively pinched construction; the different companion with only one-sided curvature control is separate.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Negatively pinched Kähler threefold without bounded coordinates | [PinchedKahler.lean](../ComparatorChallenges/PinchedKahler.lean) |