Hyperbolicity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Release075.MarkedLineData.presentation_cochainBound line 9
Source documentation
Honest linear filling estimate on all lazy Cayley loops, not just original edges.
```
theorem presentation_cochainBound : Discrete.CochainBound (d.presentation hr).cayleyMetric 114 := by
…
```
Mentions: OAI.Release075.Discrete.CochainBound
theorem OAI.Release075.MarkedLineData.presentation_wordHyperbolic line 18
Source documentation
The constructed finite presentation is word hyperbolic in the literal thin-triangle sense.
```
theorem presentation_wordHyperbolic : WordHyperbolic (d.presentation hr).GroupType := by
…
```
Mentions: OAI.Release075.WordHyperbolic