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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Insert an outside detour into any step of an expanded chain. All old vertices and assigned-path endpoints are retained.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.exists_edge_detour line 14
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.no_edge_detour line 122

    Source documentation

    An outside detour that stays in the exact closing interval is excluded by the established optimality criterion.

    theorem IsOptimal.no_edge_detour {S : ExpandedPathSystem G Q} {k : ℕ}
    (hopt : S.IsOptimal k) (hk : 3 ≤ k) (hQk : Q.card ≤ k)
    (hQ : G.IsClique (Q : Set V)) (hcycle : ¬ HasCycle G (k + 1))
    {P R : List (List V)} {A B J : List V} {x y : V}
    (hsys : S.chains = P ++ (A ++ x :: y :: B) :: R)
    (hJQ : ∀ z ∈ J, z ∉ Q)
    (hJ : J.Nodup) (hdis : J.Disjoint S.chains.flatten)
    (hpath : (x :: (J ++ [y])).IsChain G.Adj) (hpos : J ≠ [])
    (hupper : S.amount + J.length + S.incident ≤ k + 1) : False := by
…

    Mentions: OAI.CycleClique.Construction.ExpandedPathSystem, OAI.CycleClique.Construction.HasCycle

  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.forbidden_edge_detour line 139
  4. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.forbidden_one_vertex_edge_detour line 161