OAI/Algebra/GroupRing/ShortClosure.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.ShortClosure.simpleGraph line 14

    Source documentation

    Forgetting loops and multiplicities, only for measuring component distances.

    def simpleGraph : SimpleGraph V where
…
  2. def OAI.TorsionFreeZeroDivisors.ShortClosure.edgeDart line 21
  3. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.edgeDart_start line 22
  4. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.edgeDart_end line 24
  5. def OAI.TorsionFreeZeroDivisors.ShortClosure.liftWalk line 27
  6. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.liftWalk_length line 31
  7. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.liftWalk_start line 36
  8. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.liftWalk_head_target line 46
  9. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.liftWalk_finish line 57
  10. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.liftWalk_reduced line 67
  11. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.dart_reachable line 82
  12. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath.reachable line 89

    Source documentation

    A literal reduced segment stays in one connected component, including when loops or parallel darts were present in the original port graph.

    lemma ReducedPath.reachable {a b : V} {l : List D} (hp : ReducedPath Γ a b l) :
    (simpleGraph Γ).Reachable a b := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath, OAI.TorsionFreeZeroDivisors.ShortClosure.simpleGraph

  13. lemma OAI.TorsionFreeZeroDivisors.ShortClosure.reduced_return line 108

    Source documentation

    Geodesics of the simple shadow lift without backtracking to the actual multigraph. Thus the previously proved component diameter is the needed one.

    lemma reduced_return {a b : V} {p : List D} (hp : ReducedPath Γ a b p) :
    ∃ q : List D,ReducedPath Γ b a q ∧ q.length=(simpleGraph Γ).dist b a := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath, OAI.TorsionFreeZeroDivisors.ShortClosure.simpleGraph

  14. theorem OAI.TorsionFreeZeroDivisors.ShortClosure.short_closure line 116

    Source documentation

    The entire deterministic closure lemma, with an explicit logarithmic additive loss. No graph embedding theorem or cyclic cancellation is assumed.

    theorem short_closure (B : ℕ)
    (hdiam : ∀ a b,(simpleGraph Γ).Reachable a b → (simpleGraph Γ).dist a b≤B)
    (hdeg : ∀ v,7≤(Finset.univ.filter (fun x : D => Γ.origin x=v)).card)
    {a b : V} {p : List D} (hp : ReducedPath Γ a b p) (hpn : p≠[]) :
    ∃ t : List D,t.length≤B+4*(Nat.log 2 (Fintype.card V)+1) ∧
      ReducedPath Γ a a (p++t) ∧
      ∀ᵉ (x∈(p++t).getLast?) (y∈(p++t).head?),PortWalk.step Γ.origin Γ.reverse x y := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ShortClosure.simpleGraph, OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath

  15. lemma OAI.TorsionFreeZeroDivisors.SumPort.simple_eq line 134
  16. lemma OAI.TorsionFreeZeroDivisors.SumPort.degree_left line 140
  17. lemma OAI.TorsionFreeZeroDivisors.SumPort.degree_right line 146
  18. lemma OAI.TorsionFreeZeroDivisors.SumPort.typed_degree line 152
  19. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.simple_eq line 161
  20. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.degreeA line 164
  21. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.degreeB line 173
  22. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.degree line 182
  23. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.diameter line 187
  24. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.card_vertices line 192
  25. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.closure_log_bound line 196
  26. theorem OAI.TorsionFreeZeroDivisors.SampleGraph.short_closure line 205

    Source documentation

    The short-closure conclusion on the actual sampled two-side graph, with one uniform fixed constant independent of the segment and n.

    theorem short_closure (hL : 1≤L (size rep)) (hd : GraphSample.Diameters rep r)
    {a b : VA rep⊕VB rep} {p : List (DA rep⊕DB rep)}
    (hp : ShortClosure.ReducedPath (graph rep r) a b p) (hpn : p≠[]) :
    ∃ t : List (DA rep⊕DB rep),t.length≤(TypedDiameter.D₀+1608)*L (size rep) ∧
      ShortClosure.ReducedPath (graph rep r) a a (p++t) ∧
      ∀ᵉ (x∈(p++t).getLast?) (y∈(p++t).head?),
        WeightedMoore.PortWalk.step (graph rep r).origin (graph rep r).reverse x y := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.GraphSample.Diameters, OAI.TorsionFreeZeroDivisors.SampleGraph.VA, OAI.TorsionFreeZeroDivisors.SampleGraph.VB, OAI.TorsionFreeZeroDivisors.SampleGraph.DA, OAI.TorsionFreeZeroDivisors.SampleGraph.DB, OAI.TorsionFreeZeroDivisors.ShortClosure.ReducedPath, OAI.TorsionFreeZeroDivisors.SampleGraph.graph, OAI.TorsionFreeZeroDivisors.TypedDiameter.D₀, OAI.TorsionFreeZeroDivisors.WeightedMoore.PortWalk.step

  27. abbrev OAI.TorsionFreeZeroDivisors.RestrictComparisons.Length line 225
  28. def OAI.TorsionFreeZeroDivisors.RestrictComparisons.embed line 227
  29. def OAI.TorsionFreeZeroDivisors.RestrictComparisons.liftPosition line 228
  30. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.embed_local line 229
  31. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.local_embed line 230
  32. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.embed_injective line 231
  33. abbrev OAI.TorsionFreeZeroDivisors.RestrictComparisons.Active line 236
  34. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.active_flip line 237
  35. def OAI.TorsionFreeZeroDivisors.RestrictComparisons.flip line 239
  36. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.flip_inv line 241
  37. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.flip_ne line 245
  38. def OAI.TorsionFreeZeroDivisors.RestrictComparisons.partner line 249
  39. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.partner_image_yes line 252
  40. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.partner_no line 256
  41. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.partner_inv line 259
  42. def OAI.TorsionFreeZeroDivisors.RestrictComparisons.side line 270

    Source documentation

    Drop comparisons exactly when either whole path has been deleted.

    def side (x : Position (Length keep (len:=len))) : Option {e // Active C keep e} :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.RestrictComparisons.Length, OAI.TorsionFreeZeroDivisors.RestrictComparisons.Active

  43. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.side_some line 274
  44. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.partner_image_of_side line 284
  45. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.side_none line 289
  46. def OAI.TorsionFreeZeroDivisors.RestrictComparisons.comparisons line 318
  47. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.fixed_iff line 353

    Source documentation

    A new fixed position was either already fixed or points to a deleted path. This is an exact dichotomy of literal occurrence indices.

    lemma fixed_iff (x : Position (Length keep (len:=len))) :
…

    Mentions: OAI.TorsionFreeZeroDivisors.RestrictComparisons.Length

  48. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.deleted_partner_card line 371
  49. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.old_fixed_card line 382
  50. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.fixed_card line 391
  51. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.deleted_nonfixed_partner_card line 403
  52. lemma OAI.TorsionFreeZeroDivisors.RestrictComparisons.fixed_card_sharp line 419