OAI/Geometry/HyperbolicGroups/SeparatorRecursion.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.HyperbolicObstruction.PlanarRecursion.CutPartition line 18

    Source documentation

    A finite partition with a recorded set of removed separator vertices. Edges between distinct labels must meet that set. This is only the recursive combinatorial stage; no planar separator is supplied by this definition.

    structure CutPartition (G : SimpleGraph V) (U : Finset V) (K : ℕ) where
…
  2. def OAI.HyperbolicObstruction.PlanarRecursion.CutPartition.trivial line 28
  3. def OAI.HyperbolicObstruction.PlanarRecursion.region line 37
  4. lemma OAI.HyperbolicObstruction.PlanarRecursion.mem_region line 40
  5. def OAI.HyperbolicObstruction.PlanarRecursion.vertexNumber line 43
  6. lemma OAI.HyperbolicObstruction.PlanarRecursion.vertexNumber_injective line 46
  7. def OAI.HyperbolicObstruction.PlanarRecursion.coloredLabel line 49
  8. lemma OAI.HyperbolicObstruction.PlanarRecursion.coloredLabel_mod line 53
  9. lemma OAI.HyperbolicObstruction.PlanarRecursion.coloredLabel_tag line 62
  10. lemma OAI.HyperbolicObstruction.PlanarRecursion.coloredLabel_zero line 68
  11. lemma OAI.HyperbolicObstruction.PlanarRecursion.coloredLabel_one line 75
  12. lemma OAI.HyperbolicObstruction.PlanarRecursion.coloredLabel_two line 82
  13. lemma OAI.HyperbolicObstruction.PlanarRecursion.region_card line 92

    Source documentation

    The three literal regions partition the carrier.

    lemma region_card (U : Finset V) (t : V → Fin 3) :
    (region U t 0).card + (region U t 1).card + (region U t 2).card = U.card := by
…

    Mentions: OAI.HyperbolicObstruction.PlanarRecursion.region

  14. lemma OAI.HyperbolicObstruction.PlanarRecursion.tag_cases line 98
  15. lemma OAI.HyperbolicObstruction.PlanarRecursion.CutPartition.merge_small line 106
  16. def OAI.HyperbolicObstruction.PlanarRecursion.CutPartition.merge line 137

    Source documentation

    One literal recursive step: every separator vertex becomes a singleton, while the two nonadjacent sides retain their recursively constructed parts.

    def merge (hK : 0 < K)
    (hsep : ∀ x ∈ region U t 1, ∀ y ∈ region U t 2, ¬ G.Adj x y) :
    CutPartition G U K where
…

    Mentions: OAI.HyperbolicObstruction.PlanarRecursion.region, OAI.HyperbolicObstruction.PlanarRecursion.CutPartition

  17. lemma OAI.HyperbolicObstruction.PlanarRecursion.CutPartition.merge_removed_card line 169