FormalConjectures.WrittenOnTheWallII.GraphConjecture316

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Written on the Wall II - Conjecture 316

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

namespace WrittenOnTheWallII.GraphConjecture316open SimpleGraphvariable {α : Type*} [Fintype α] [DecidableEq α]

WOWII Conjecture 316

Let G be a simple connected graph and let P denote the set of pendant vertices (vertices of degree 1). If |P| ≥ deg_avg(Gᶜ), then G is well totally dominated, where deg_avg(Gᶜ) is the average degree of the complement of G.

Proof sketch. In the trivial cases (P = ∅, or at most 2 vertices) G is complete, and complete graphs are well totally dominated. Otherwise the set C of non-pendant vertices satisfies |C| ≤ 3 and is a clique of G, and a case split on the set Q ⊆ C of neighbours of pendant vertices shows that G is well totally dominated.

@[category research solved, AMS 5,
  formal_proof using lean4 at "https://github.com/KitaKen1/wowii-graph-conjecture-316-lean/blob/3335e07151bc43e86d5c104dd30fee3596f06410/GraphConjecture316.lean"]
theorem conjecture316 (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected)
    (h : (averageDegree Gᶜ : ℚ) ≤ (pendantVertices G).card) :
    IsWellTotallyDominated G := byα:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjhG:G.Connectedh:Gᶜ.averageDegree ≤ ↑G.pendantVertices.card⊢ G.IsWellTotallyDominated
  sorryAll goals completed! 🐙

-- Sanity checks

The average degree of the edgeless graph on 3 vertices is 0.

@[category test, AMS 5]
example : averageDegree (⊥ : SimpleGraph (Fin 3)) = 0 := byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq α⊢ ⊥.averageDegree = 0
  unfold averageDegreeα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq α⊢ (∑ v, ↑(⊥.degree v)) / ↑(Fintype.card (Fin 3)) = 0; simp [Fintype.card_fin]All goals completed! 🐙

In P₃ (path 0-1-2), the average degree is 4/3 and there are 2 pendant vertices.

@[category test, AMS 5]
example : averageDegree (SimpleGraph.fromEdgeSet {s(0,1), s(1,2)} : SimpleGraph (Fin 3)) = 4/3 := byα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq α⊢ (fromEdgeSet {s(0, 1), s(1, 2)}).averageDegree = 4 / 3
  unfold averageDegreeα:Type u_1inst✝¹:Fintype αinst✝:DecidableEq α⊢ (∑ v, ↑((fromEdgeSet {s(0, 1), s(1, 2)}).degree v)) / ↑(Fintype.card (Fin 3)) = 4 / 3; decide +nativeAll goals completed! 🐙

end WrittenOnTheWallII.GraphConjecture316