PolygonFilling.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.relator_boundary line 22
Source documentation
Both literal orientations of every included polygon are available as one relator face; indexed positions are retained even for repeated labels.
```
lemma relator_boundary {R : Set (Word A)} (c : C) (hc : B.attachingWord c ∈ R)
    (b : Bool) (i : Fin (B.size c)) :
    ∃ ys : List B.Side, IsBoundary B.next ys ∧ (⟨c,b,i⟩ : B.Side) ∈ ys ∧
      SymmetricRelator R (ys.map B.sideLabel) := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary
theorem OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.picture_filling line 60
Source documentation
A genuine mapped polygon disk gives a counted derivation over EXACTLY its original attaching words. The distinguished outside is excluded from the relator list, so this is not the tautological exterior-relator argument.
```
theorem picture_filling (xs : List P.Dart) (hx : IsBoundary P.pairing.face xs)
    (hw : xs.map ((B.outsideTarget ell hell word closed weight apex radial).edge ∘ P.index) =
      List.ofFn word)
    (ht : ∀ x, B.outsideTag ell hell word closed (P.index x) =
      if x ∈ xs then some true else none) :
    ∃ k, Homotopy (Set.range B.attachingWord) (List.ofFn word) [] k ∧
      k ≤ Fintype.card P.Dart / 2 ∧ (k : ℤ) ≤ cycles P.pairing.face := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary, OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.weight, OAI.HyperbolicObstruction.PictureSwitch.cycles