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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Initial longest-path obstruction in the coloured-path proof.

  1. theorem OAI.CycleClique.Construction.indexedPath_prefix line 9
  2. theorem OAI.CycleClique.Construction.indexedPath_cons line 16
  3. theorem OAI.CycleClique.Construction.colored_path_of_common_neighbor line 30

    Source documentation

    One of two differently coloured common neighbours can prefix any path avoiding them, producing different colours at its two ends.

    theorem colored_path_of_common_neighbor {V : Type*} {H : SimpleGraph V}
    {x y z : V} (hxy : H.Adj x y) (hxz : H.Adj x z)
    (χ : V → Fin 2) (hyz : χ y ≠ χ z) {q : ℕ}
    {f : Fin (q + 1) → V} (hf : IsIndexedPath H f) (hstart : f 0 = x)
    (havoid : ∀ i, f i ≠ y ∧ f i ≠ z) :
    ∃ g : Fin (q + 1 + 1) → V, IsIndexedPath H g ∧
      χ (g 0) ≠ χ (g (Fin.last (q + 1))) := by
…

    Mentions: OAI.CycleClique.Construction.IsIndexedPath

  4. theorem OAI.CycleClique.Construction.no_colored_path_start_bound line 53

    Source documentation

    Under failure of the desired exact-length coloured path, every path starting at the common neighbour in the deletion has smaller order.

    theorem no_colored_path_start_bound {V : Type*} {H : SimpleGraph V}
    {x y z : V} (hxy : H.Adj x y) (hxz : H.Adj x z)
    (χ : V → Fin 2) (hyz : χ y ≠ χ z) {ℓ : ℕ} (hℓ : 1 ≤ ℓ)
    (hno : ¬ ∃ g : Fin (ℓ + 1) → V, IsIndexedPath H g ∧
      χ (g 0) ≠ χ (g (Fin.last ℓ)))
    {q : ℕ} {f : Fin (q + 1) → V} (hf : IsIndexedPath H f) (hstart : f 0 = x)
    (havoid : ∀ i, f i ≠ y ∧ f i ≠ z) : q + 1 < ℓ := by
…

    Mentions: OAI.CycleClique.Construction.IsIndexedPath