ProtectedNormal.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Unopposed line 25
Source documentation
A protected indexed side has no oppositely indexed side anywhere in the input. A single oriented exterior polygon satisfies this condition literally.
```
def Unopposed (keep : S → Prop) : Prop :=
…
```
structure OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Preserves line 28
def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Preserves.trans line 32
lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.Survives.unopposed line 40
lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.cancel_frozen_protected line 49

theorem OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.normalize_protected line 110

Source documentation

Relative mixed normal form. Every protected frozen side, with its exact cyclic successor and index, survives. In particular the operation does not turn an exterior null-word into a fictitious target relator.

theorem normalize_protected (B : FrozenTarget T) (hm : P.FrozenMapped B)
    (keep : S → Prop) (hk : ∀ s, keep s → T.free (T.kind s) = false)
    (hu : P.Unopposed keep) (apex : V → Bool)
    (hr : ∀ s, apex (T.start (T.label s)) = true →
      apex (T.start (T.rev (T.label s))) = false) :
    ∃ Q : WalkPicture.{u} T, Nonempty (P.Preserves keep Q) ∧ Q.FrozenMapped B ∧
      Q.Simple ∧ Q.NoBigon ∧ Q.FullyReduced ∧ Q.RadialInjective apex ∧
      Q.chain = P.chain := by
…

Mentions: OAI.HyperbolicObstruction.PictureSwitch.FrozenTarget