OAI/Algebra/GroupRing/DegreeTwoSuppression.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.out line 14
  2. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.mem_out line 15
  3. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.unique_other line 18
  4. def OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.turn line 36
  5. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.turn_of_mark line 39
  6. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.turn_of_unmarked line 42
  7. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.turn_origin line 47
  8. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.turn_fixed_iff line 52
  9. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.turn_involutive line 59
  10. def OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.suppressed line 71

    Source documentation

    Darts of the actual suppressed multigraph: all outgoing darts at marked vertices. The return map pairs them by the unique maximal degree-two chain.

    def suppressed (Γ : PortGraph V D) (mark : V → Prop)
    (h2 : ∀ v, ¬mark v → (out Γ.origin v).card=2) :
    PortGraph V {d : D // turn Γ.origin mark h2 d=d} where
…

    Mentions: OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.out, OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.turn

  11. def OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.chainLength line 84

    Source documentation

    Positive integral lengths count exactly the original directed edges along the chains; the two orientations have the same length.

    def chainLength (Γ : PortGraph V D) (mark : V → Prop)
    (h2 : ∀ v, ¬mark v → (out Γ.origin v).card=2)
    (d : {d : D // turn Γ.origin mark h2 d=d}) : ℕ :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.out, OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.turn

  12. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.chainLength_pos line 90
  13. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.chainLength_reverse line 95
  14. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.chainLength_total line 101
  15. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.suppressed_degree line 106
  16. lemma OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.suppressed_min_degree line 124

    Source documentation

    Minimum degree two becomes minimum degree three whenever a component has some branching. Pure circle components give no darts and are treated separately.

    lemma suppressed_min_degree (Γ : PortGraph V D)
    (hmin : ∀ d, 2 ≤ (out Γ.origin (Γ.origin d)).card) :
    let mark := fun v => (out Γ.origin v).card≠2
…

    Mentions: OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.out

  17. def OAI.TorsionFreeZeroDivisors.SuppressedMoore.iterChain line 153
  18. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.head_iterChain line 158
  19. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.last_iterChain line 162
  20. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.iterChain_good line 170
  21. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.chain_good line 191
  22. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.chain_last line 197
  23. def OAI.TorsionFreeZeroDivisors.SuppressedMoore.chainWalk line 211

    Source documentation

    Literal expansion of one suppressed edge into the original graph. Its endpoints are the two marked ports, and every internal vertex is degree two.

    def chainWalk (d : B) : Γ.subdivision.Walk (.inr d.val) (.inr ((Γ').reverse d).val) :=
…
  24. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.chainWalk_reduced line 215
  25. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.cost_iterChain_one line 220
  26. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.chainWalk_weight line 230
  27. def OAI.TorsionFreeZeroDivisors.SuppressedMoore.join line 243
  28. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.join_head line 248
  29. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.join_last line 252
  30. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.join_cost line 259
  31. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.join_good line 268
  32. def OAI.TorsionFreeZeroDivisors.SuppressedMoore.outWord line 280
  33. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.outWord_injective line 285
  34. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.outWord_join line 293
  35. def OAI.TorsionFreeZeroDivisors.SuppressedMoore.pickEven line 300
  36. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.pickEven_portWord line 306
  37. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.iterChain_no_marks line 312
  38. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.chain_one_mark line 324
  39. def OAI.TorsionFreeZeroDivisors.SuppressedMoore.expand line 340

    Source documentation

    Expand every macro-edge, preserving the ordered path occurrence data.

    def expand : {k : ℕ} → Chain B k → (Σ l, Chain D l)
  | 0, d => ⟨len d-1,iterChain F (len d-1) d.val⟩
  | _+1, p => join (iterChain F (len p.1-1) p.1.val) (expand p.2)

    Mentions: OAI.TorsionFreeZeroDivisors.SuppressedMoore.iterChain, OAI.TorsionFreeZeroDivisors.SuppressedMoore.join

  40. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.expand_head line 344
  41. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.expand_last line 349
  42. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.expand_good line 355
  43. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.expand_cost line 365
  44. lemma OAI.TorsionFreeZeroDivisors.SuppressedMoore.expand_marks line 376
  45. theorem OAI.TorsionFreeZeroDivisors.SuppressedMoore.original_short_cycle line 387

    Source documentation

    The stationary Moore collision in the suppressed graph expands to a literal original cycle. Girth is imposed only on the original graph.

    theorem original_short_cycle [Nonempty B]
    (hdeg : ∀ d, 3 ≤ (PortWalk.out (Γ').origin ((Γ').origin d)).card) :
    let k := Nat.log 2 (Fintype.card B) + 2
…
  46. theorem OAI.TorsionFreeZeroDivisors.SuppressedMoore.original_dart_inequality line 445

    Source documentation

    Actual branch-port complexity from original edge count and original girth, without an a priori graph-rank or chain-count hypothesis.

    theorem original_dart_inequality [Nonempty B]
    (hdeg : ∀ d, 3 ≤ (PortWalk.out (Γ').origin ((Γ').origin d)).card)
    (L C : ℝ) (hL : 0 < L)
    (htotal : (Fintype.card D : ℝ) ≤ 2*C*L)
    (hgirth : ∀ a (c : Γ.subdivision.Walk a a), c.IsCycle →
      L ≤ WeightedCycles.weight (edgeWeight (fun _ : D => (1:ℝ))) c) :
    (Fintype.card B : ℝ) ≤ 8*C*(Nat.log 2 (Fintype.card B)+3:ℝ) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.WeightedCycles.weight

  47. theorem OAI.TorsionFreeZeroDivisors.SuppressedMoore.bounded_branch_ports line 465

    Source documentation

    Uniformly many branch ports in an actual finite graph of minimum degree two with O(L) edges and girth L. Pure circles contribute no branch ports.

    theorem bounded_branch_ports (C : ℝ) (hC : 0 ≤ C) :
    ∃ R : ℕ, ∀ {V D : Type} [Fintype D] (Γ : PortGraph V D)
      (_ : ∀ d, 2 ≤ (DegreeTwoSuppression.out Γ.origin (Γ.origin d)).card)
      (L : ℝ) (_ : 0 < L)
      (_ : (Fintype.card D : ℝ) ≤ 2*C*L)
      (_ : ∀ a (c : Γ.subdivision.Walk a a), c.IsCycle →
          L ≤ WeightedCycles.weight (edgeWeight (fun _ : D => (1:ℝ))) c),
      (Finset.univ.filter (fun d : D =>
        (DegreeTwoSuppression.out Γ.origin (Γ.origin d)).card≠2)).card ≤ R := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.DegreeTwoSuppression.out, OAI.TorsionFreeZeroDivisors.WeightedCycles.weight