OAI/Algebra/GroupRing/BFSTree.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

A literal breadth-first spanning tree, with its distances and radius preserved. This is the rooted tree used in the sharp planar separator.

  1. def OAI.TorsionFreeZeroDivisors.ConedMap.oldVertex line 17
  2. def OAI.TorsionFreeZeroDivisors.ConedMap.centerVertex line 18
  3. lemma OAI.TorsionFreeZeroDivisors.ConedMap.oldVertex_injective line 19
  4. lemma OAI.TorsionFreeZeroDivisors.ConedMap.centerVertex_injective line 21
  5. lemma OAI.TorsionFreeZeroDivisors.ConedMap.old_ne_center line 23
  6. lemma OAI.TorsionFreeZeroDivisors.ConedMap.oldVertex_cycle line 28
  7. lemma OAI.TorsionFreeZeroDivisors.ConedMap.centerVertex_cycle line 29
  8. lemma OAI.TorsionFreeZeroDivisors.ConedMap.old_adj line 31
  9. lemma OAI.TorsionFreeZeroDivisors.ConedMap.radial_adj line 37
  10. def OAI.TorsionFreeZeroDivisors.ConedMap.oldHom line 43
  11. theorem OAI.TorsionFreeZeroDivisors.ConedMap.connected line 45
  12. lemma OAI.TorsionFreeZeroDivisors.ConedMap.old_distance_le line 50
  13. lemma OAI.TorsionFreeZeroDivisors.ConedMap.center_distance_le line 56
  14. def OAI.TorsionFreeZeroDivisors.ConedMap.oldEmbedding line 66
  15. def OAI.TorsionFreeZeroDivisors.ConedMap.liftSet line 67
  16. lemma OAI.TorsionFreeZeroDivisors.ConedMap.liftSet_card line 68
  17. lemma OAI.TorsionFreeZeroDivisors.ConedMap.old_mem_liftSet line 69
  18. lemma OAI.TorsionFreeZeroDivisors.ConedMap.center_not_liftSet line 71
  19. theorem OAI.TorsionFreeZeroDivisors.ConedMap.distance_cost line 79

    Source documentation

    Distances to zero-cost auxiliary centers incur one extra step, but all original vertices remain within the original radius.

    theorem distance_cost (hc : (G).Connected) (root : Cycle σ) (r : ℕ)
    (hr : ∀ v,(G).dist root v≤r) (v : Cycle ρ) :
    (G').dist (oldVertex σ α root) v + (if v∈liftSet σ α Finset.univ then 1 else 0)≤r+1 := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ConedMap.oldVertex, OAI.TorsionFreeZeroDivisors.ConedMap.liftSet

  20. lemma OAI.TorsionFreeZeroDivisors.BFSTree.exists_parent line 103
  21. def OAI.TorsionFreeZeroDivisors.BFSTree.parent line 116
  22. lemma OAI.TorsionFreeZeroDivisors.BFSTree.parent_adj line 117
  23. lemma OAI.TorsionFreeZeroDivisors.BFSTree.parent_dist line 120
  24. lemma OAI.TorsionFreeZeroDivisors.BFSTree.parent_ne line 124
  25. def OAI.TorsionFreeZeroDivisors.BFSTree.tree line 126
  26. lemma OAI.TorsionFreeZeroDivisors.BFSTree.tree_le line 132
  27. lemma OAI.TorsionFreeZeroDivisors.BFSTree.exists_tree_walk line 140
  28. lemma OAI.TorsionFreeZeroDivisors.BFSTree.connected line 154
  29. theorem OAI.TorsionFreeZeroDivisors.BFSTree.dist_root line 162

    Source documentation

    All root distances are unchanged, not merely bounded by an abstract height.

    theorem dist_root (v : V) : (tree G hc root).dist v root=G.dist v root := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.BFSTree.tree

  30. def OAI.TorsionFreeZeroDivisors.BFSTree.parentEdge line 169
  31. lemma OAI.TorsionFreeZeroDivisors.BFSTree.parentEdge_surjective line 171
  32. theorem OAI.TorsionFreeZeroDivisors.BFSTree.isTree line 185

    Source documentation

    The parent edges form an actual spanning tree of the original graph.

    theorem isTree : (tree G hc root).IsTree := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.BFSTree.tree

  33. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.rootPath_cost line 204
  34. theorem OAI.TorsionFreeZeroDivisors.TreeCentroid.two_root_paths_cost line 224

    Source documentation

    Zero-cost face centers may be introduced for triangulation without losing the sharp original-vertex bound. Only original vertices are charged.

    theorem two_root_paths_cost (budget : Finset V) (root v w : V) (r : ℕ)
    (hroot : root∈budget)
    (hv : T.dist root v+(if v∈budget then 1 else 0)≤r+1)
    (hw : T.dist root w+(if w∈budget then 1 else 0)≤r+1) :
    ((rootPath ht root v∪rootPath ht root w)∩budget).card≤2*r+1 := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.TreeCentroid.rootPath

  35. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.two_root_paths_cost_erase_root line 240
  36. theorem OAI.TorsionFreeZeroDivisors.MapEuler.radius_separator line 261

    Source documentation

    The exact bounded-radius separator on a genus-zero rotation map. The partition balances any chosen set of unit-weight vertices. In particular the root is charged once, so deleting a contracted root saves one unit.

    theorem radius_separator (σ α : Equiv.Perm O) (ha : Function.Involutive α)
    (hz : GenusZero σ α) (hc : (graph σ α ha).Connected)
    (root : Cycle σ) (r : ℕ) (hr : ∀ v,(graph σ α ha).dist root v≤r)
    (active : Finset (Cycle σ)) :
    ∃ cut side : Finset (Cycle σ), root∈cut ∧ cut.card≤2*r+1 ∧
      (cut.erase root).card≤2*r ∧
      3*(active.filter (fun v=>v∉cut ∧ v∈side)).card≤2*active.card ∧
      3*(active.filter (fun v=>v∉cut ∧ v∉side)).card≤2*active.card ∧
      ∀ v w,v∉cut→w∉cut→(graph σ α ha).Adj v w→(v∈side↔w∈side) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.MapEuler.graph

  37. def OAI.TorsionFreeZeroDivisors.MapRestrict.perm line 355
  38. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.perm_val line 357
  39. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.not_invariant line 360
  40. def OAI.TorsionFreeZeroDivisors.MapRestrict.cycleInclude line 364
  41. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.cycleInclude_cycle line 366
  42. def OAI.TorsionFreeZeroDivisors.MapRestrict.cycleRaw line 368
  43. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.cycleRaw_apply line 371
  44. def OAI.TorsionFreeZeroDivisors.MapRestrict.cycleEquiv line 378
  45. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.cycle_card line 397
  46. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.perm_involutive line 400
  47. def OAI.TorsionFreeZeroDivisors.MapRestrict.supportEquiv line 403
  48. lemma OAI.TorsionFreeZeroDivisors.MapRestrict.support_card line 418