NormalFaceFilling.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.ConeSkeleton.exterior_same_top line 24

theorem OAI.HyperbolicObstruction.ConeSkeleton.exterior_top_filling line 43

Source documentation

Local source03 cost for an ACTUAL free face in a protected normal disk. Simplicity is read in the template, never in the random bouquet labels.

theorem exterior_top_filling (hs : P.Simple) (hb : P.NoBigon)
    (x : P.Dart) (a : Top n w) (e : MacroGraph.graph.Dart)
    (hx : P.index x = .inl (.inl (a,e))) :
    ∃ ys : List P.Dart, IsBoundary P.pairing.face ys ∧ x ∈ ys ∧
      ∃ k ≤ 30, WordPictures.Homotopy (SimpleWordRelator n w d)
        ((ys.map ((exteriorWalkTarget n w d ell hell word closed c hc f).label ∘ P.index)).flatMap
          (collapse n w)) [] k := by
…

Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkTarget, OAI.HyperbolicObstruction.ConeSkeleton.collapse

theorem OAI.HyperbolicObstruction.ConeSkeleton.exterior_frozen_filling line 91
Source documentation
Frozen triangles and decorations retain the complete indexed attaching polygon. Pulling that literal boundary back preserves its true local cost.
```
theorem exterior_frozen_filling
    (hm : P.FrozenMapped (exteriorWalkFrozen n w d ell hell word closed c hc f))
    (x : P.Dart) (s : (frozenBoundary n w d).Side)
    (hx : P.index x = .inl (.inr s)) :
    ∃ ys : List P.Dart, IsBoundary P.pairing.face ys ∧ x ∈ ys ∧
      ∃ k ≤ 30, WordPictures.Homotopy (SimpleWordRelator n w d)
        ((ys.map ((exteriorWalkTarget n w d ell hell word closed c hc f).label ∘ P.index)).flatMap
          (collapse n w)) [] k := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkFrozen, OAI.HyperbolicObstruction.ConeSkeleton.frozenBoundary, OAI.HyperbolicObstruction.WordPictures.Homotopy, OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkTarget, OAI.HyperbolicObstruction.ConeSkeleton.collapse