# A three-manifold without conjugate points or nonpositive curvature

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

- [A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric](../../preprints/A-Three-Manifold-Without-Conjugate-Points-and-Without-a-Nonpositively-Curved-Metric-September-24-2026/paper.pdf)

## Scope

The formalized result separates absence of conjugate points from nonpositive sectional curvature. It constructs a closed connected orientable smooth three-manifold with a smooth Riemannian metric having no conjugate points, while the same manifold admits no smooth metric of everywhere nonpositive sectional curvature. The no-conjugate-points assertion ranges over all geodesics and tangent-bundle Jacobi fields, including constant geodesics and unbounded time intervals. The separate no-focal-points and CAT(0) consequences are not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| No conjugate points without a nonpositively curved metric | [ConjugatePoints.lean](../ComparatorChallenges/ConjugatePoints.lean) |