2026/07/28 by Jun Qing
Mathematics · #math.CO #msc:05C69
5 pages. The bound is sharp. A complete Lean 4/mathlib formalization is available at https://github.com/qscqesze/graffiti-pc-conjecture-387 and archived at https://doi.org/10.5281/zenodo.21621226
arxiv created 2026/07/28 · arxiv updated 2026/07/31
Let G be a nonempty finite simple graph of order n, and let m(G) be the upper median of its degree sequence. We prove that the 2-domination number satisfies gamma2(G) <= n - m(G) + 1. This proves Graffiti.pc Conjecture 387. In fact, the argument establishes the inequality for every nonempty finite simple graph, so the connectedness hypothesis in the original formulation is unnecessary. The proof uses the complement graph and a minimally linearly dependent family of polynomials encoding selected nonneighborhoods.