NormalCell.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.HyperbolicObstruction.PictureSwitch.CellTarget line 22
Source documentation
Oriented, individually indexed polygon boundaries in a target cell complex. In a lifted target, S includes the lift of the cell. Opposite orientations have disjoint side cycles; the same indexed side is retained when reversing. These data contain no diagram or normal-form assertion.
```
structure CellTarget (S : Type v) (L : Type w) (V : Type z) (A : Type k)
    [AddCommMonoid A] where
…
```
structure OAI.HyperbolicObstruction.PictureSwitch.CellPicture line 45
Source documentation
A finite genus-zero side pairing with actual indexed cellular face maps. This describes a raw picture, without any reducedness or link bounds.
```
structure CellPicture (T : CellTarget S L V A) where
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.CellTarget
def OAI.HyperbolicObstruction.PictureSwitch.CellPicture.chain line 60
def OAI.HyperbolicObstruction.PictureSwitch.CellPicture.Reduced line 63
def OAI.HyperbolicObstruction.PictureSwitch.CellPicture.RadialInjective line 65
structure OAI.HyperbolicObstruction.PictureSwitch.CellPicture.Retains line 71
Source documentation
Retention maps leave every retained face and its individual side indices unchanged. They may discard whole faces; switches only change side pairings.
```
structure Retains (Q : CellPicture.{u} T) where
…
```
theorem OAI.HyperbolicObstruction.PictureSwitch.CellPicture.normalize line 82
Source documentation
Finite normalization producing BOTH forbidden-adjacency cancellation and radial-label injectivity, while preserving the EXACT signed cellular chain. After every cancellation there are fewer darts, so re-normalizing radial links cannot cause an infinite cancel/switch loop. No minimal-picture conclusion is assumed. The initial picture existence/realization theorem is separate.
```
theorem normalize : ∃ Q : CellPicture.{u} T,
    Nonempty (P.Retains Q) ∧ Q.Reduced ∧ Q.RadialInjective ∧ Q.chain = P.chain := by
…
```