NormalDiskArea.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.ConeSkeleton.BoundedConeRelator line 18
Source documentation
Only locally PROVED fillings are admitted to this auxiliary relator set. It is used for derivation substitution, not to alter either presentation.
```
def BoundedConeRelator : Set (List (Dart n w)) :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Dart
def OAI.HyperbolicObstruction.ConeSkeleton.normalWordPicture line 36
Source documentation
A normalized actual cone disk defines a word picture whose every interior face has a proved cost30 replacement. The protected exterior is EXCLUDED.
```
def normalWordPicture : WordPicture (BoundedConeRelator n w d) (List.ofFn word) where
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.BoundedConeRelator
theorem OAI.HyperbolicObstruction.ConeSkeleton.normal_disk_area line 66
Source documentation
The genuine normalized cone disk costs at most THIRTY times its number of INTERIOR cells in the finite simple presentation. No bound on the number of diagram cells is assumed or claimed here.
```
theorem normal_disk_area :
    ∃ a, Homotopy (SimpleWordRelator n w d) ((List.ofFn word).flatMap (collapse n w)) [] a ∧
      (a : ℤ) ≤ 30 * (cycles P.pairing.face - 1) := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.collapse