WalkRadial.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.RadialInjective line 24
lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.makeSimpleRadial line 28
theorem OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.normalize_radial line 58
Source documentation
Simultaneous macro simplicity, top-side cancellation, and radial-label injectivity. Cross-pairing radial sides may create new cancellable macro adjacencies; the induction re-tests and removes them rather than silently assuming old reducedness survives a switch.
```
theorem normalize_radial (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.Retains Q) ∧ Q.Simple ∧ Q.NoBigon ∧
      Q.Reduced ∧ Q.RadialInjective apex ∧ Q.chain = P.chain := by
…
```