OAI/Geometry/HyperbolicGroups/ConeSkeleton.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.FanRow line 20
2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.Fan line 25

   Source documentation

   Fan occurrences are the actual included rows, counted once even if several top occurrences use them. Positions are NOT identified by generator labels.

   abbrev Fan := {b : FanRow n // w ⟨.inl b.1,b.2⟩ = true}

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.FanRow

3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.Vertex line 27
4. abbrev OAI.HyperbolicObstruction.ConeSkeleton.Edge line 28
5. abbrev OAI.HyperbolicObstruction.ConeSkeleton.Dart line 29
6. def OAI.HyperbolicObstruction.ConeSkeleton.start line 31
7. def OAI.HyperbolicObstruction.ConeSkeleton.rev line 36
8. def OAI.HyperbolicObstruction.ConeSkeleton.isApex line 37
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.radial line 41
10. abbrev OAI.HyperbolicObstruction.ConeSkeleton.Outgoing line 45
11. def OAI.HyperbolicObstruction.ConeSkeleton.radialLabel line 47
12. lemma OAI.HyperbolicObstruction.ConeSkeleton.radialLabel_bijective line 50
13. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 66) line 66
14. lemma OAI.HyperbolicObstruction.ConeSkeleton.card_outgoing line 69
15. theorem OAI.HyperbolicObstruction.ConeSkeleton.normalize line 78

    Source documentation

    The source's reduced target one-skeleton, after top cone neighborhoods have been assembled into macro polygons. Every created apex-link now has at most five steps. The genus-zero side pairing is PRODUCED, not a hypothesis about some already-normalized picture. Its face permutation is unchanged.

    theorem normalize {D : Type*} [DecidableEq D] [Fintype D]
        (M : PictureSwitch.PictureMap D) (label : D → Dart n w)
        (hM : M.Respects label (start n w) (rev n w)) (hG : M.GenusZero) :
        ∃ N : PictureSwitch.PictureMap D,
          N.face = M.face ∧ N.Respects label (start n w) (rev n w) ∧ N.GenusZero ∧
          (∀ a b, isApex n w (start n w (label a)) = true →
            N.vertex.SameCycle a b → label a = label b → a = b) ∧
          ∀ a f, start n w (label a) = .inr f →
            Fintype.card {x : D // N.vertex.SameCycle a x} ≤ 5 := by
    …

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap, OAI.HyperbolicObstruction.ConeSkeleton.Dart, OAI.HyperbolicObstruction.ConeSkeleton.start, OAI.HyperbolicObstruction.ConeSkeleton.rev, OAI.HyperbolicObstruction.ConeSkeleton.isApex