PathEndpoints.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Possible endpoints on a fixed path vertex set

These are the endpoint-clique and rotation consequences in manuscript Lemma clq:coloured-path.

def OAI.CycleClique.Construction.IsSpanningPath line 14
def OAI.CycleClique.Construction.pathEnds line 20
theorem OAI.CycleClique.Construction.mem_pathEnds line 26
theorem OAI.CycleClique.Construction.pathEnds_subset line 33
theorem OAI.CycleClique.Construction.start_not_pathEnds line 41
theorem OAI.CycleClique.Construction.successor_mem_pathEnds line 52
Source documentation
The successor of any neighbour of the last vertex becomes an endpoint by the explicit fixed-end rotation.
```
theorem successor_mem_pathEnds {V : Type*} [Fintype V]
    {G : SimpleGraph V} {x : V} {W : Finset V} {r : ℕ}
    {f : Fin (r + 1) → V} (hf : IsSpanningPath G x W f)
    (i : Fin r) (hi : G.Adj (f (Fin.last r)) (f i.castSucc)) :
    f i.succ ∈ pathEnds G x W r := by
…
```
Mentions: OAI.CycleClique.Construction.IsSpanningPath, OAI.CycleClique.Construction.pathEnds

theorem OAI.CycleClique.Construction.clique_of_endpoint_neighbor_cover line 64

Source documentation

Independent-pair expansion makes a set of possible endpoints a clique when their neighbourhoods fit inside too few vertices.

theorem clique_of_endpoint_neighbor_cover {V : Type*} [Fintype V] [DecidableEq V]
    {G : SimpleGraph V} {E W Z : Finset V} {s : ℕ}
    (hEW : E ⊆ W)
    (hcover : ∀ e ∈ E, ∀ v, G.Adj e v → v ∈ W ∪ Z)
    (hsize : W.card + Z.card < 2 * s)
    (hexpand : ∀ a b, a ≠ b → ¬ G.Adj a b →
      2 * s ≤ (closedNeighborhood G {a, b}).card) : G.IsClique (E : Set V) := by
…

Mentions: OAI.CycleClique.Construction.closedNeighborhood

theorem OAI.CycleClique.Construction.endpoint_degree_le line 91

Source documentation

Each neighbour of an endpoint has a different successor endpoint, so its degree is at most the number of possible endpoints.

theorem endpoint_degree_le {V : Type*} [Fintype V]
    {G : SimpleGraph V} {x e : V} {W : Finset V} {r : ℕ}
    (he : e ∈ pathEnds G x W r)
    (hneighbors : ∀ v, G.Adj e v → v ∈ W) :
    (G.neighborSet e).ncard ≤ (pathEnds G x W r).card := by
…

Mentions: OAI.CycleClique.Construction.pathEnds

theorem OAI.CycleClique.Construction.pathEnds_successor_closed line 132

Source documentation

On any spanning path the endpoint clique is a final segment.

theorem pathEnds_successor_closed {V : Type*} [Fintype V]
    {G : SimpleGraph V} {x : V} {W : Finset V} {r : ℕ}
    {f : Fin (r + 1) → V} (hf : IsSpanningPath G x W f)
    (hclique : G.IsClique (pathEnds G x W r : Set V))
    {i : Fin r} (hi : f i.castSucc ∈ pathEnds G x W r) :
    f i.succ ∈ pathEnds G x W r := by
…

Mentions: OAI.CycleClique.Construction.IsSpanningPath, OAI.CycleClique.Construction.pathEnds