ExteriorTarget.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.exteriorBoundary line 26
Source documentation
The outside word is an arbitrary closed edge path, not an attaching word of a cell of the target. Its second orientation is solely bookkeeping.
```
def exteriorBoundary : PolygonTarget.Boundary Unit L V where
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary
abbrev OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.ExteriorSide line 35
def OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.withExterior line 40
Source documentation
Enlarge the indexing types by one protected exterior polygon. Only the original target's free cone-walk cells may be split. All added side weights are zero, so the chain is exactly the interior cellular chain.
```
def withExterior : WalkCellTarget (S ⊕ T.ExteriorSide ell hell word closed)
    (C ⊕ Unit) (W ⊕ V) L V A where
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget
def OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.exteriorFrozen line 88
def OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.isExterior line 122
Source documentation
Protect precisely the added exterior sides.
```
def isExterior : S ⊕ T.ExteriorSide ell hell word closed → Prop := Sum.elim (fun _ => False) (fun _ => True)
```
lemma OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.exterior_frozen line 124
lemma OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.exterior_unopposed line 130

theorem OAI.HyperbolicObstruction.PictureSwitch.WalkCellTarget.normalize_exterior line 146

Source documentation

Normalization with the literal outside word preserved side-for-side.

theorem normalize_exterior (P : WalkPicture.{u} (T.withExterior ell hell word closed))
    (hm : P.FrozenMapped (T.exteriorFrozen ell hell word closed B))
    (hp : ∀ x s, P.index x = .inr s → s.2.1 = true)
    (apex : V → Bool)
    (hr : ∀ l, apex (T.start l) = true → apex (T.start (T.rev l)) = false) :
    ∃ Q : WalkPicture.{u} (T.withExterior ell hell word closed),
      Nonempty (P.Preserves (T.isExterior ell hell word closed) Q) ∧
      Q.FrozenMapped (T.exteriorFrozen ell hell word closed B) ∧
      Q.Simple ∧ Q.NoBigon ∧ Q.FullyReduced ∧ Q.RadialInjective apex ∧
      Q.chain = P.chain := by
…