ConeCellCollapse.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.ConeSkeleton.square_collapsedBoundary line 15
lemma OAI.HyperbolicObstruction.ConeSkeleton.six_collapsedBoundary line 20
theorem OAI.HyperbolicObstruction.ConeSkeleton.cell_collapse_filling line 27
Source documentation
Uniform factor 30 for every actual bounded normal-form cell. The fan paths, macro walk, exceptional loose edge and both decoration families have all been expanded literally into the finite simple-cycle presentation.
```
theorem cell_collapse_filling (a : Cell n w d) :
    ∃ k ≤ 30, WordPictures.Homotopy (SimpleWordRelator n w d)
      (collapsedBoundary n w d a) [] k := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Cell, OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.ConeSkeleton.collapsedBoundary
lemma OAI.HyperbolicObstruction.ConeSkeleton.collapse_letter_word line 48
theorem OAI.HyperbolicObstruction.ConeSkeleton.polygon_filling_to_simple line 56
Source documentation
Quantitative replacement of a literal polygon word derivation. This is an algebraic substitution theorem, not an assumed bound on disk production.
```
theorem polygon_filling_to_simple {z : List (Alphabet n)} {k : ℕ}
    (h : WordPictures.Homotopy (Set.range (boundary n w d).attachingWord)
      (z.map (letterDart n w)) [] k) :
    ∃ a ≤ 30*k, WordPictures.Homotopy (SimpleWordRelator n w d) z [] a := by
…
```
Mentions: OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.ConeSkeleton.boundary, OAI.HyperbolicObstruction.ConeSkeleton.letterDart
theorem OAI.HyperbolicObstruction.ConeSkeleton.nullWord_polygon_iff line 70
Source documentation
The cone-polygon comparison creates no new relations among original letters. Combined with the opposite implication, it is an exact null-word equivalence in the original marked presentation, not a surjection claim.
```
theorem nullWord_polygon_iff (z : List (Alphabet n)) :
    PresentedGroup.mk (FreeGroup.mk '' Set.range (boundary n w d).attachingWord)
      (FreeGroup.mk (z.map (letterDart n w))) = 1 ↔
    PresentedGroup.mk (Relator n w d) (FreeGroup.mk z) = 1 := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.boundary, OAI.HyperbolicObstruction.ConeSkeleton.letterDart