Written on the Wall II - Conjecture 315

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

Definitions

The notions IsTotalDominatingSet, IsMinimalTotalDominatingSet, IsWellTotallyDominated, and pendantVertices live in FormalConjecturesForMathlib.Combinatorics.SimpleGraph.GraphConjectures.WellTotallyDominated.

theorem WrittenOnTheWallII.GraphConjecture315.conjecture315 {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (hG : G.Connected) (h : G.indepNum = G.pendantVertices.card) : G.IsWellTotallyDominated

WOWII Conjecture 315

Let $G$ be a simple connected graph and let $P$ denote the set of pendant vertices (vertices of degree $1$). If $\alpha(G) = |P|$, then $G$ is well totally dominated.

A formal proof of this conjectures has been obtained by Goran Žužić and Moritz Firsching using an experimental pipeline.