Written on the Wall II - Conjecture 13

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

theorem WrittenOnTheWallII.GraphConjecture13.conjecture13 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) (h : G.Connected) : ↑G.diam + ↑((Finset.image (fun (v : α) => G.indepNeighborsCard v) Finset.univ).max' ⋯) - 1 ≤ G.b

WOWII Conjecture 13

For a simple connected graph G, the size b(G) of a largest induced bipartite subgraph satisfies b(G) ≥ diam(G) + max_{v ∈ V} l(v) - 1, where diam(G) is the diameter of G and l(v) = indepNeighborsCard G v is the independence number of the neighbourhood of v.