Papers With

← All papers
First page of The 2-Domination Number and the Upper Median Degree: A Proof of Graffiti.pc Conjecture 387

The 2-Domination Number and the Upper Median Degree: A Proof of Graffiti.pc Conjecture 387

Jun Qing

math.CO Jul 28, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
Graffiti.pc Conjecture 387 on the 2-domination number bound was formalized and machine-checked in Lean 4 using Mathlib.
Abstract
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 gamma_2(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.
Problem

Graffiti.pc Conjecture 387 predicts that for connected graphs the 2-domination number satisfies gamma_2(G) <= n - m(G) + 1, where m(G) is the upper median degree.

Approach

The proof works with the complement graph and encodes selected nonneighborhoods as products of linear polynomials. An elementary lemma on minimally linearly dependent polynomial families is used to construct a 2-dominating set of the required size. The theorem is then formalized in Lean 4 with Mathlib, with no proof placeholders or custom axioms.

Results

The inequality gamma_2(G) <= n - m(G) + 1 is proven for every nonempty finite simple graph, removing the connectedness hypothesis. The formal development yields declarations Graffiti387.graffiti_pc_387 and Graffiti387.twoDominationNumber_le, archived on Zenodo and GitHub.