Written on the Wall II - Conjecture 18

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

theorem WrittenOnTheWallII.GraphConjecture18.conjecture18 {α : Type u_1} [Fintype α] [DecidableEq α] [Nontrivial α] (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected) : have M := {v : α | G.degree v = G.maxDegree}; ↑G.indepNum + ↑⌈√↑(G.eccSet M)⌉ ≤ G.b

WOWII Conjecture 18

For a simple connected graph $G$, the size $b(G)$ of a largest induced bipartite subgraph satisfies $b(G) \ge \alpha(G) + \lceil \sqrt{\mathrm{eccSet}(G, M)} \rceil$, where $\alpha(G)$ is the independence number, $M$ is the set of maximum-degree vertices, and $\mathrm{eccSet}(G, M)$ is the set eccentricity of $M$ — the maximum over all vertices of the minimum distance from that vertex to $M$. We use the SimpleGraph.eccSet invariant.