CellularFilling.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PictureSwitch.CellPicture.wordPicture line 22
Source documentation
Reverse bridge from a literal genus-zero target-cell diagram to an area-counted word picture. Every local premise is an actual attaching polygon membership, not a filling or diagram-existence assumption.
```
def wordPicture (xs : List P.Dart) (hx : IsBoundary P.pairing.face xs)
    (hw : xs.map (T.edge ∘ P.index) = w)
    (hr : ∀ x, x ∉ xs → ∃ ys : List S, IsBoundary T.next ys ∧
      P.index x ∈ ys ∧ SymmetricRelator R (ys.map T.edge)) : WordPicture R w where
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary

theorem OAI.HyperbolicObstruction.PictureSwitch.CellPicture.word_filling line 46

Source documentation

Quantitative extraction of a mapped genus-zero disk. Costs count real relator moves, including inverse orientations, in the original word alphabet.

theorem word_filling (xs : List P.Dart) (hx : IsBoundary P.pairing.face xs)
    (hw : xs.map (T.edge ∘ P.index) = w)
    (hr : ∀ x, x ∉ xs → ∃ ys : List S, IsBoundary T.next ys ∧
      P.index x ∈ ys ∧ SymmetricRelator R (ys.map T.edge)) :
    ∃ k, Homotopy R w [] k ∧ k ≤ Fintype.card P.Dart / 2 ∧
      (k : ℤ) ≤ cycles P.pairing.face :=
…

Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary, OAI.HyperbolicObstruction.PictureSwitch.cycles