Written on the Wall II - Conjecture 16

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

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

WOWII Conjecture 16

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