ElementaryCover.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.ConeSkeleton.elementaryOffset line 25
Source documentation
Deck offset from the specified basepoint of each literal elementary cell. For a triangle, that basepoint is its top apex; for a frozen cell it is the initial vertex of the fixed boundary indexing.
```
def elementaryOffset (a : ElementaryCell n w d) (i : Fin (elementarySize n w d a)) : G :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryCell, OAI.HyperbolicObstruction.ConeSkeleton.elementarySize
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOffset_next line 29
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOffset_triangle_zero line 35
Source documentation
Apex coordinate of a triangle lift is exactly its independent chain index.
```
lemma elementaryOffset_triangle_zero (a : Top n w) (c : MacroCell) :
    elementaryOffset n w d v (.inl (a,c)) (0 : Fin 3) = 1 := rfl
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.MacroCell, OAI.HyperbolicObstruction.ConeSkeleton.elementaryOffset
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOffset_triangle_one line 38
lemma OAI.HyperbolicObstruction.ConeSkeleton.elementaryOffset_triangle_two line 46
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryLiftedBoundary line 57
Source documentation
Literal elementary boundary incidence in the voltage cover, at every deck translate, including the wraparound side. No covering-space or CW-realization assertion is made by this finite incidence construction.
```
def elementaryLiftedBoundary : PolygonTarget.Boundary
    (G × ElementaryCell n w d) (G × ElementaryDart n w) (G × ElementaryVertex n w) where
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.ElementaryCell, OAI.HyperbolicObstruction.ConeSkeleton.ElementaryDart, OAI.HyperbolicObstruction.ConeSkeleton.ElementaryVertex
def OAI.HyperbolicObstruction.ConeSkeleton.elementaryLetterLiftedBoundary line 76
Source documentation
The actual original quotient supplies every triangle and frozen-cell lift; no relator equations or nonvacuity properties are added as hypotheses.
```
def elementaryLetterLiftedBoundary :=
…
```