OAI/Combinatorics/Ramsey/CycleClique/Construction/CECycleExtension.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.Construction.ce_cycle_to_indexed line 11
2. theorem OAI.CycleClique.Construction.ce_cycle_rotate line 20
3. theorem OAI.CycleClique.Construction.ce_consecutive_ear_cycle line 29

   Source documentation

   Replacing a cycle edge by an exterior path retains every cycle vertex.

   theorem ce_consecutive_ear_cycle {V : Type*} {H : SimpleGraph V} {r l : ℕ}
       (hl : 2 ≤ l) {c : Fin (r + 1) → V} (hc : Function.Injective c)
       (he : ∀ i, H.Adj (c i) (c (cycleNext i)))
       (a : Fin (r + 1)) {g : Fin (l + 1) → V} (hg : IsIndexedPath H g)
       (hg0 : g 0 = c a) (hgl : g (Fin.last l) = c (a + 1))
       (hdis : ∀ i : Fin (l + 1), 0 < i.val → i.val < l →
         ∀ j : Fin (r + 1), c j ≠ g i) : HasCycle H (r + l) := by
   …

   Mentions: OAI.CycleClique.Construction.cycleNext, OAI.CycleClique.Construction.IsIndexedPath, OAI.CycleClique.Construction.HasCycle

4. def OAI.CycleClique.Construction.ceChordIndex line 56
5. theorem OAI.CycleClique.Construction.ceChordIndex_injective line 60
6. theorem OAI.CycleClique.Construction.ce_cycle_step line 71
7. theorem OAI.CycleClique.Construction.ce_successor_chord_path line 81

   Source documentation

   The successor chord joins the two complementary portions of the old cycle.

   theorem ce_successor_chord_path {V : Type*} {H : SimpleGraph V} {r : ℕ}
       {c : Fin (r + 1) → V} (hc : Function.Injective c)
       (he : ∀ i, H.Adj (c i) (c (cycleNext i)))
       (j : Fin r) (hj : 0 < j.val)
       (hchord : H.Adj (c ⟨1, by omega⟩) (c j.succ)) :
       ∃ f : Fin (r + 1) → V, IsIndexedPath H f ∧
         f 0 = c j.castSucc ∧ f (Fin.last r) = c 0 ∧
         Set.range f = Set.range c := by
   …

   Mentions: OAI.CycleClique.Construction.cycleNext, OAI.CycleClique.Construction.IsIndexedPath

8. theorem OAI.CycleClique.Construction.ce_chord_ear_cycle line 138
9. theorem OAI.CycleClique.Construction.ce_indexedPath_tail line 152
10. theorem OAI.CycleClique.Construction.ce_reverse_tail_snoc line 161

    Source documentation

    Reverse the noninitial part of an ear and attach a new final vertex. Every internal vertex of the resulting path was internal to the original ear.

    theorem ce_reverse_tail_snoc {V : Type*} {H : SimpleGraph V} {l : ℕ}
        (hl : 2 ≤ l) {g : Fin (l + 1) → V} (hg : IsIndexedPath H g) (v : V)
        (hv : ∀ i : Fin (l + 1), 0 < i.val → g i ≠ v)
        (hadj : H.Adj (g ⟨1, by omega⟩) v) :
        ∃ h : Fin (l + 1) → V, IsIndexedPath H h ∧
          h 0 = g (Fin.last l) ∧ h (Fin.last l) = v ∧
          ∀ i : Fin (l + 1), 0 < i.val → i.val < l →
            ∃ j : Fin (l + 1), 0 < j.val ∧ j.val < l ∧ h i = g j := by
    …

    Mentions: OAI.CycleClique.Construction.IsIndexedPath

11. theorem OAI.CycleClique.Construction.ce_no_external_common_neighbor line 191
12. theorem OAI.CycleClique.Construction.ce_nonwrapping_ear_impossible line 229

    Source documentation

    In a graph with no independent triple, a longest cycle has no exterior ear whose second endpoint is not the predecessor of the first.

    theorem ce_nonwrapping_ear_impossible {V : Type*} {H : SimpleGraph V} {r l : ℕ}
        (hr : 2 ≤ r) (hl : 2 ≤ l) {c : Fin (r + 1) → V} (hc : Function.Injective c)
        (he : ∀ i, H.Adj (c i) (c (cycleNext i)))
        (hmax : ∀ q, HasCycle H q → q ≤ r + 1) (hα : ¬ HasIndependent H 3)
        (j : Fin r) (hj : 0 < j.val) {g : Fin (l + 1) → V} (hg : IsIndexedPath H g)
        (hg0 : g 0 = c 0) (hgl : g (Fin.last l) = c j.castSucc)
        (hdis : ∀ i : Fin (l + 1), 0 < i.val → i.val < l →
          ∀ k : Fin (r + 1), c k ≠ g i) : False := by
    …

    Mentions: OAI.CycleClique.Construction.cycleNext, OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.HasIndependent, OAI.CycleClique.Construction.IsIndexedPath

13. theorem OAI.CycleClique.Construction.ce_rooted_ear_impossible line 281
14. theorem OAI.CycleClique.Construction.ce_external_ear_impossible line 325

    Source documentation

    A longest cycle in an alpha-two graph cannot have an exterior ear.

    theorem ce_external_ear_impossible {V : Type*} {H : SimpleGraph V} {r l : ℕ}
        (hr : 2 ≤ r) (hl : 2 ≤ l) {c : Fin (r + 1) → V} (hc : Function.Injective c)
        (he : ∀ i, H.Adj (c i) (c (cycleNext i)))
        (hmax : ∀ q, HasCycle H q → q ≤ r + 1) (hα : ¬ HasIndependent H 3)
        {g : Fin (l + 1) → V} (hg : IsIndexedPath H g)
        (hg0 : g 0 ∈ Set.range c) (hgl : g (Fin.last l) ∈ Set.range c)
        (hdis : ∀ i : Fin (l + 1), 0 < i.val → i.val < l →
          ∀ k : Fin (r + 1), c k ≠ g i) : False := by
    …

    Mentions: OAI.CycleClique.Construction.cycleNext, OAI.CycleClique.Construction.HasCycle, OAI.CycleClique.Construction.HasIndependent, OAI.CycleClique.Construction.IsIndexedPath