ResidualPaths.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Joining the endpoint clique to a path in the remaining component.

theorem OAI.CycleClique.Construction.endpoint_residual_order line 12

Source documentation

The pair consisting of the remaining-path endpoint and a vertex of the endpoint clique directly gives the needed combined order.

theorem endpoint_residual_order {V : Type*} [Fintype V] [DecidableEq V]
    {H : SimpleGraph V} {E R : Finset V} {u v w y z : V} {s : ℕ}
    (hu : u ∈ R) (hv : v ∈ R) (hw : w ∈ E)
    (hcoverv : ∀ a, H.Adj v a → a ∈ R ∨ a = y ∨ a = z)
    (hcoverw : ∀ a, H.Adj w a → a ∈ E ∨ a = u ∨ a = y ∨ a = z)
    (hexpand : 2 * s ≤ (closedNeighborhood H {v, w}).card) :
    2 * s - 2 ≤ E.card + R.card := by
…

Mentions: OAI.CycleClique.Construction.closedNeighborhood

theorem OAI.CycleClique.Construction.clique_join_remaining_path line 45

Source documentation

Traverse the whole endpoint clique first, entering the remaining path through one of two attachment neighbours.

theorem clique_join_remaining_path {V : Type*} [DecidableEq V]
    {H : SimpleGraph V} {E : Finset V} {u w : V}
    (hclique : H.IsClique (E : Set V)) (hw : w ∈ E)
    (hattach : ∃ a ∈ E, ∃ b ∈ E, a ≠ b ∧ H.Adj a u ∧ H.Adj b u)
    (R : List V) (hR : R.Nodup) (hRchain : R.IsChain H.Adj)
    (hRhead : R.head? = some u) (hRoutside : ∀ v ∈ R, v ∉ E) :
    ∃ L : List V, L.Nodup ∧ L.IsChain H.Adj ∧ L.head? = some w ∧
      L.length = E.card + R.length ∧ ∀ v ∈ L, v ∈ E ∨ v ∈ R := by
…

theorem OAI.CycleClique.Construction.no_colored_path_list_bound line 81