OAI/Geometry/HyperbolicGroups/WalkTopTurns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.top_face_apex_card_ge line 24

   Source documentation

   Actual source-face cardinal bound, not an assumed macro polygon.

   lemma top_face_apex_card_ge (hs : P.Simple) (hb : P.NoBigon)
       (x : P.Dart) (a : Top n w) (e : MacroGraph.graph.Dart) (hx : P.index x = .inl (a,e)) :
       3 ≤ Fintype.card {y : P.Dart // P.pairing.face.SameCycle x y ∧
         isApex n w (start n w (walkLabel n w d (P.index y))) = true} := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.start, OAI.HyperbolicObstruction.ConeSkeleton.walkLabel

2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.TopTurnDart line 64
3. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 67) line 67
4. abbrev OAI.HyperbolicObstruction.ConeSkeleton.FaceApexDart line 69
5. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 71) line 71
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.face_apex_card_ge line 74
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.selected_top_turns_ge line 97

   Source documentation

   The bound sum d_z >= 3 T at the actual selected top faces. The following apex transport identifies these darts with the indexed fan-turn counts.

   lemma selected_top_turns_ge (hs : P.Simple) (hb : P.NoBigon) :
       3 * Fintype.card (SelectedTopFace n w d c hc f P select) ≤
         Fintype.card (TopTurnDart n w d c hc f P select) := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.SelectedTopFace, OAI.HyperbolicObstruction.ConeSkeleton.TopTurnDart