OAI/Algebra/GroupRing/MapEuler.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

The weighted centroid needed by planar dual-tree separator constructions. This is an actual theorem for finite Mathlib trees, not a separator assumption.

  1. lemma OAI.TorsionFreeZeroDivisors.MapEuler.component_card_one_of_connected line 15
  2. lemma OAI.TorsionFreeZeroDivisors.MapEuler.connected_of_component_card_one line 23
  3. lemma OAI.TorsionFreeZeroDivisors.MapEuler.connected_iff_component_card_one line 37

    Source documentation

    Literal connectedness can be read from the map's component quotient.

    lemma connected_iff_component_card_one :
    (graph σ α ha).Connected ↔ Nat.card (Component σ α)=1 :=
…

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

  4. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subpairing_commute line 51
  5. lemma OAI.TorsionFreeZeroDivisors.MapEuler.complement_involutive line 65
  6. lemma OAI.TorsionFreeZeroDivisors.MapEuler.complement_subpairing line 73
  7. lemma OAI.TorsionFreeZeroDivisors.MapEuler.complement_face line 81
  8. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subpairing_support_subset line 90
  9. lemma OAI.TorsionFreeZeroDivisors.MapEuler.complement_support line 98
  10. lemma OAI.TorsionFreeZeroDivisors.MapEuler.complement_support_card line 108
  11. theorem OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_complement_dual line 115

    Source documentation

    Deleting a chosen set of primal edges is actual complementary-pair deletion in the dual map, not an assumed planar-minor interface.

    theorem genusZero_complement_dual (hz : GenusZero σ α) : GenusZero (α*σ) (α*β) :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero

  12. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_subpairing line 127
  13. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_support_tree line 133
  14. theorem OAI.TorsionFreeZeroDivisors.MapEuler.tree_contour_card line 140

    Source documentation

    The literal contour permutation of a chosen spanning tree has one cycle.

    theorem tree_contour_card (hz : GenusZero σ α) (ht : T.IsTree) :
    Nat.card (Cycle (subgraphPair σ α ha T hT*σ))=1 := by
…

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

  15. lemma OAI.TorsionFreeZeroDivisors.MapEuler.cotree_support line 154

    Source documentation

    The complementary edge matching in the original dual rotation has exactly one fewer edge than dual vertices.

    lemma cotree_support (hz : GenusZero σ α) (ht : T.IsTree) :
    (α*subgraphPair σ α ha T hT).support.card+2=2*Nat.card (Cycle (α*σ)) := by
…

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

  16. theorem OAI.TorsionFreeZeroDivisors.MapEuler.spanning_cotree_isTree line 166

    Source documentation

    Tree--cotree duality proved from actual permutations and Euler equality. Loops and parallel edges in the original map are allowed. No embedding or planar-duality axiom is used.

    theorem spanning_cotree_isTree (hz : GenusZero σ α) (ht : T.IsTree) :
    (graph (α*σ) (α*subgraphPair σ α ha T hT)
      (complement_involutive α _ ha (subgraphPair_involutive σ α ha T hT)
        (subgraphPair_subpairing σ α ha T hT))).IsTree := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.MapEuler.graph, OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair, OAI.TorsionFreeZeroDivisors.MapEuler.complement_involutive, OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_involutive, OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_subpairing

  17. lemma OAI.TorsionFreeZeroDivisors.MapEuler.sameCycle_of_card_one line 194
  18. theorem OAI.TorsionFreeZeroDivisors.MapEuler.contour_interval_reachable line 202

    Source documentation

    In a cyclic contour with at most one exit from S, the labels of all members of S are connected using only steps internal to S. This finite orbit argument replaces a geometric assertion that tree-subtree corners form an interval.

    theorem contour_interval_reachable (θ : Equiv.Perm O)
    (hθ : ∀ x y,θ.SameCycle x y) (S : Set O) (p : O)
    (hout : ∀ x∈S,θ x∉S → x=p) (H : SimpleGraph V) (label : O → V)
    (hstep : ∀ x∈S,θ x∈S → H.Reachable (label x) (label (θ x)))
    (x : O) (hx : x∈S) : H.Reachable (label p) (label x) := by
…
  19. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pairFinset_adj line 235
  20. lemma OAI.TorsionFreeZeroDivisors.MapEuler.pairFinset_cycle_injective line 242
  21. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_nonfixed_mem line 254
  22. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_nonfixed_apply line 259
  23. lemma OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_adj line 263
  24. theorem OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair_dart_unique line 271

    Source documentation

    A realized simple subgraph has exactly one dart per directed adjacency.

    theorem subgraphPair_dart_unique {x y : O}
    (hx : subgraphPair σ α ha T hT x≠x) (hy : subgraphPair σ α ha T hT y≠y)
    (h₁ : cycle σ x=cycle σ y)
    (h₂ : cycle σ (subgraphPair σ α ha T hT x)=cycle σ (subgraphPair σ α ha T hT y)) : x=y := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.subgraphPair

  25. def OAI.TorsionFreeZeroDivisors.TreeCentroid.path line 295
  26. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.path_isPath line 296
  27. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.path_length line 298
  28. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.eq_path line 300
  29. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.path_dist line 303
  30. def OAI.TorsionFreeZeroDivisors.TreeCentroid.next line 306
  31. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.next_adj line 307
  32. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.next_ne line 309
  33. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.next_concat line 311
  34. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.next_adjacent line 317
  35. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.next_walk line 329
  36. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.dist_next line 338
  37. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.dist_not_next line 344
  38. def OAI.TorsionFreeZeroDivisors.TreeCentroid.branch line 355
  39. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.mem_branch line 356
  40. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.branch_adj line 358
  41. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.branch_closed line 361
  42. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.branch_disjoint line 365
  43. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.distance_step line 370
  44. def OAI.TorsionFreeZeroDivisors.TreeCentroid.potential line 386
  45. lemma OAI.TorsionFreeZeroDivisors.TreeCentroid.potential_step line 387
  46. theorem OAI.TorsionFreeZeroDivisors.TreeCentroid.exists_centroid line 402

    Source documentation

    A finite tree has a weighted centroid: every branch after its deletion has at most half of the total nonnegative integral weight. Zero weights allowed.

    theorem exists_centroid (w : V → ℕ) :
    ∃ c : V,∀ n : V,2*(∑ z∈(branch h) c n,w z)≤∑ z,w z := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.TreeCentroid.branch