FullWalkNormal.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.FullyReduced line 24
Source documentation
No adjacent sides are oppositely indexed pieces of the same target cell, including both the free top occurrences and all genuine frozen cells.
```
def FullyReduced : Prop := ∀ a, P.index (P.pairing.edge a) ≠ T.opposite (P.index a)
```
theorem OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.normalize_full line 30
Source documentation
Simultaneous normal form for mixed macro walks and literal frozen cells. Frozen dipoles may be exposed by top surgery or radial switches. The induction therefore retests all these conditions, and preserves the full elementary chain, rather than separately asserting that the operations commute.
```
theorem normalize_full (B : FrozenTarget T) (hm : P.FrozenMapped B)
    (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.Survives Q) ∧ Q.FrozenMapped B ∧
      Q.Simple ∧ Q.NoBigon ∧ Q.FullyReduced ∧ Q.RadialInjective apex ∧
      Q.chain = P.chain := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.FrozenTarget