WordPictureFold.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.WordPictures.WordPicture.foldAt line 21
Source documentation
Free boundary cancellation lands in a new actual genus-zero diagram, retaining every interior relator face, with all repeated side indices intact.
```
def foldAt {l r : List P.Dart} {a b : P.Dart} (he : P.outside = l++a::b::r)
    (hc : P.label a = invLetter (P.label b)) : WordPicture R ((l++r).map P.label) := by
…
```
Mentions: OAI.HyperbolicObstruction.WordPictures.invLetter, OAI.HyperbolicObstruction.WordPictures.WordPicture
lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.of_step line 71
lemma OAI.HyperbolicObstruction.WordPictures.WordPicture.of_red line 83
theorem OAI.HyperbolicObstruction.WordPictures.reduced_picture_existence line 94
Source documentation
Source disk producer with a freely reduced exterior: a null word admits an actual finite genus-zero relator diagram whose literal boundary is a reduction of that word, hence has no greater boundary length. No diagram or planarity hypothesis is assumed.
```
theorem reduced_picture_existence {R : Set (Word A)} (w : Word A)
    (h : PresentedGroup.mk (FreeGroup.mk '' R) (FreeGroup.mk w) = 1) :
    ∃ z, FreeGroup.Red w z ∧ Nonempty (WordPicture R z) := by
…
```
Mentions: OAI.HyperbolicObstruction.WordPictures.Word, OAI.HyperbolicObstruction.WordPictures.WordPicture