ConeCover.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.ConeSkeleton.frozenOffset line 23
Source documentation
Cell lift coordinate at a frozen side, measured from its indexed first vertex. Reversing orientation changes the initial point but not the cell lift.
```
def frozenOffset (s : (frozenBoundary n w d).Side) : G :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.frozenBoundary
lemma OAI.HyperbolicObstruction.ConeSkeleton.frozenOffset_opposite line 28
def OAI.HyperbolicObstruction.ConeSkeleton.coverOffset line 39
lemma OAI.HyperbolicObstruction.ConeSkeleton.coverOffset_opposite line 44
def OAI.HyperbolicObstruction.ConeSkeleton.actualCellCover line 55
Source documentation
The actual regular covering target, constructed from ordinary group edge values satisfying the ORIGINAL cell equations. No lifted-chain conclusion is assumed. In particular it applies to quotient group values, not only to the bouquet auxiliary group.
```
def actualCellCover : WalkCellCover (indexingTarget n w d) G where
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.indexingTarget
def OAI.HyperbolicObstruction.ConeSkeleton.polygonGroupCover line 71
Source documentation
Canonical cover data for this presentation, with actual prefix-product coordinates and the proved cone potentials.
```
def polygonGroupCover : WalkCellCover (indexingTarget n w d) (PolygonGroup n w d) :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.indexingTarget, OAI.HyperbolicObstruction.ConeSkeleton.PolygonGroup