FormalConjectures.WrittenOnTheWallII.GraphConjecture3

/-
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 3

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

universe unamespace WrittenOnTheWallII.GraphConjecture3open SimpleGraphvariable {α : Type u} [Fintype α] [DecidableEq α]

WOWII Conjecture 3

For a connected simple graph G, the number of leaves in a maximum spanning tree satisfies Ls(G) ≥ G.indepDominationNumber * MaxTemp(G), where G.indepDominationNumber is the independent domination number and MaxTemp(G) is max_v deg(v)/(n(G) - deg(v)).

@[category research solved, AMS 5]
theorem conjecture3 {G : SimpleGraph α} [DecidableRel G.Adj] [Nontrivial α] (h_conn : G.Connected) :
    G.indepDominationNumber * MaxTemp G ≤ Ls G := byα:Type uinst✝³:Fintype αinst✝²:DecidableEq αG:SimpleGraph αinst✝¹:DecidableRel G.Adjinst✝:Nontrivial αh_conn:G.Connected⊢ ↑G.indepDominationNumber * G.MaxTemp ≤ G.Ls
  sorryAll goals completed! 🐙

-- Sanity checks

The number of vertices of the two-vertex graph K₂ is 2.

@[category test, AMS 5]
example : Fintype.card (Fin 2) = 2 := rfl



/-- In `K₂`, the temperature of vertex 0 is `deg(0) / (n - deg(0)) = 1 / 1 = 1`. -/
@[category test, AMS 5]
example : temp_v (⊤ : SimpleGraph (Fin 2)) ⟨0, byα:Type uinst✝¹:Fintype αinst✝:DecidableEq α⊢ 0 < 2 omegaAll goals completed! 🐙⟩ = 1 := byα:Type uinst✝¹:Fintype αinst✝:DecidableEq α⊢ ⊤.temp_v ⟨0, ⋯⟩ = 1
  unfold temp_vα:Type uinst✝¹:Fintype αinst✝:DecidableEq α⊢ (have n := Fintype.card (Fin 2);
  have deg := ⊤.degree ⟨0, ⋯⟩;
  if n = deg then 0 else ↑deg / (↑n - ↑deg)) =
  1
  have hdeg : (⊤ : SimpleGraph (Fin 2)).degree ⟨0, byα:Type uinst✝¹:Fintype αinst✝:DecidableEq α⊢ 0 < 2α:Type uinst✝¹:Fintype αinst✝:DecidableEq αhdeg:⊤.degree ⟨0, ⋯⟩ = 1⊢ (have n := Fintype.card (Fin 2);
  have deg := ⊤.degree ⟨0, ⋯⟩;
  if n = deg then 0 else ↑deg / (↑n - ↑deg)) =
  1 omegaAll goals completed! 🐙α:Type uinst✝¹:Fintype αinst✝:DecidableEq αhdeg:⊤.degree ⟨0, ⋯⟩ = 1⊢ (have n := Fintype.card (Fin 2);
  have deg := ⊤.degree ⟨0, ⋯⟩;
  if n = deg then 0 else ↑deg / (↑n - ↑deg)) =
  1⟩ = 1 := rflα:Type uinst✝¹:Fintype αinst✝:DecidableEq αhdeg:⊤.degree ⟨0, ⋯⟩ = 1⊢ (have n := Fintype.card (Fin 2);
  have deg := ⊤.degree ⟨0, ⋯⟩;
  if n = deg then 0 else ↑deg / (↑n - ↑deg)) =
  1
  rw [show Fintype.card (Fin 2) = 2 from rfl,α:Type uinst✝¹:Fintype αinst✝:DecidableEq αhdeg:⊤.degree ⟨0, ⋯⟩ = 1⊢ (have n := 2;
  have deg := ⊤.degree ⟨0, ⋯⟩;
  if n = deg then 0 else ↑deg / (↑n - ↑deg)) =
  1α:Type uinst✝¹:Fintype αinst✝:DecidableEq αhdeg:⊤.degree ⟨0, ⋯⟩ = 1⊢ (have n := 2;
  have deg := 1;
  if n = deg then 0 else ↑deg / (↑n - ↑deg)) =
  1 hdegα:Type uinst✝¹:Fintype αinst✝:DecidableEq αhdeg:⊤.degree ⟨0, ⋯⟩ = 1⊢ (have n := 2;
  have deg := 1;
  if n = deg then 0 else ↑deg / (↑n - ↑deg)) =
  1α:Type uinst✝¹:Fintype αinst✝:DecidableEq αhdeg:⊤.degree ⟨0, ⋯⟩ = 1⊢ (have n := 2;
  have deg := 1;
  if n = deg then 0 else ↑deg / (↑n - ↑deg)) =
  1]α:Type uinst✝¹:Fintype αinst✝:DecidableEq αhdeg:⊤.degree ⟨0, ⋯⟩ = 1⊢ (have n := 2;
  have deg := 1;
  if n = deg then 0 else ↑deg / (↑n - ↑deg)) =
  1
  norm_numAll goals completed! 🐙

end WrittenOnTheWallII.GraphConjecture3