OAI/Geometry/HyperbolicGroups/CycleDecomposition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConeWalks.chain line 14
2. lemma OAI.HyperbolicObstruction.ConeWalks.chain_nil line 15
3. lemma OAI.HyperbolicObstruction.ConeWalks.chain_cons line 16
4. lemma OAI.HyperbolicObstruction.ConeWalks.chain_append line 18
5. abbrev OAI.HyperbolicObstruction.ConeWalks.Circuit line 22

   Source documentation

   A simple loop with its actual base vertex and edge traversals.

   abbrev Circuit (G : SimpleGraph V) := Σ a : V, {p : G.Walk a a // p.IsCycle}

6. def OAI.HyperbolicObstruction.ConeWalks.perimeter line 23
7. def OAI.HyperbolicObstruction.ConeWalks.total line 24
8. lemma OAI.HyperbolicObstruction.ConeWalks.perimeter_nil line 25
9. lemma OAI.HyperbolicObstruction.ConeWalks.perimeter_cons line 26
10. lemma OAI.HyperbolicObstruction.ConeWalks.total_nil line 28
11. lemma OAI.HyperbolicObstruction.ConeWalks.total_cons line 29
12. lemma OAI.HyperbolicObstruction.ConeWalks.short_loop_chain line 32
13. theorem OAI.HyperbolicObstruction.ConeWalks.decompose_walk line 49

    Source documentation

    Loop erasure WITH the removed simple circuits retained, preserving the exact signed edge chain. This is stronger than existence of an elementary cycle and does not discard a nonzero cellular chain.

    theorem decompose_walk (c : G.Dart → A) (hc : ∀ d, c d.symm = -c d)
        {u v : V} (p : G.Walk u v) :
        ∃ (q : G.Walk u v) (cs : List (Circuit G)), q.IsPath ∧
          chain c p = chain c q + total c cs ∧ q.length + perimeter cs ≤ p.length := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeWalks.Circuit, OAI.HyperbolicObstruction.ConeWalks.chain, OAI.HyperbolicObstruction.ConeWalks.total, OAI.HyperbolicObstruction.ConeWalks.perimeter

14. theorem OAI.HyperbolicObstruction.ConeWalks.decompose_closed line 92

    Source documentation

    Every closed macro walk splits into simple cycles and cancelling backtracks, with exact signed cone chain and nonincreasing total perimeter.

    theorem decompose_closed (c : G.Dart → A) (hc : ∀ d, c d.symm = -c d)
        {u : V} (p : G.Walk u u) :
        ∃ cs : List (Circuit G), chain c p = total c cs ∧ perimeter cs ≤ p.length := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeWalks.Circuit, OAI.HyperbolicObstruction.ConeWalks.chain, OAI.HyperbolicObstruction.ConeWalks.total, OAI.HyperbolicObstruction.ConeWalks.perimeter