EndpointAttachment.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The degree calculations forcing a second attachment and a common neighbour.

theorem OAI.CycleClique.Construction.degree_le_of_neighbor_cover line 8
theorem OAI.CycleClique.Construction.degree_cover_forces_neighbor line 17
theorem OAI.CycleClique.Construction.clique_extension_size line 30
theorem OAI.CycleClique.Construction.erased_pair_cover_card line 40

theorem OAI.CycleClique.Construction.endpoint_second_attachment line 50

Source documentation

The attachment vertex has a second neighbour in the endpoint clique; this is the two-case degree calculation in the manuscript.

theorem endpoint_second_attachment {V : Type*} [Fintype V] [DecidableEq V]
    {H : SimpleGraph V} {E : Finset V} {u w₀ y z : V} {s : ℕ}
    (hs : 4 ≤ s) (hsize : s - 2 ≤ E.card ∧ E.card ≤ s - 1)
    (hclique : H.IsClique (E : Set V)) (hno : H.cliqueNum < s)
    (hy : y ∉ E) (hz : z ∉ E) (hw₀ : w₀ ∈ E)
    (hdegree : ∀ w ∈ E, s ≤ (H.neighborSet w).ncard)
    (hpartial : ∀ w ∈ E, w ≠ w₀ → ∀ v, H.Adj w v →
      v ∈ (E.erase w) ∪ {u, y, z})
    (hzero : ¬ H.Adj w₀ y → ¬ H.Adj w₀ z → (H.neighborSet w₀).ncard ≤ E.card) :
    ∃ w ∈ E, w ≠ w₀ ∧ H.Adj u w := by
…

theorem OAI.CycleClique.Construction.endpoint_common_deleted_neighbor line 115

Source documentation

Once all endpoints attach only through u, one endpoint sees both deleted vertices.

theorem endpoint_common_deleted_neighbor {V : Type*} [Fintype V] [DecidableEq V]
    {H : SimpleGraph V} {E : Finset V} {u y z : V} {s : ℕ}
    (hs : 4 ≤ s) (hsize : s - 2 ≤ E.card ∧ E.card ≤ s - 1)
    (hclique : H.IsClique (E : Set V)) (hno : H.cliqueNum < s) (hu : u ∉ E)
    (hdegree : ∀ w ∈ E, s ≤ (H.neighborSet w).ncard)
    (hcover : ∀ w ∈ E, ∀ v, H.Adj w v → v ∈ (E.erase w) ∪ {u, y, z}) :
    ∃ w ∈ E, H.Adj w y ∧ H.Adj w z := by
…