OAI/Geometry/HyperbolicGroups/RelativeTopTurns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.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 (.inl (a,e))) :
       3 ≤ Fintype.card {y : P.Dart // P.pairing.face.SameCycle x y ∧
         isApex n w (start n w ((target n w d ell hell word c hc f).label (P.index y))) = true} := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.start, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.target

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

   Source documentation

   Source 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 ell hell word c hc f P select) ≤
         Fintype.card (TopTurnDart n w d ell hell word c hc f P select) := by
   …

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