Leaf deletion can move the unique mode of a tree domination polynomial by two

Dev D. Goyal

Leaf deletion can move the unique mode of a tree domination polynomial by two

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Burcroff–O'Brien leaf-deletion mode question for tree domination polynomials
Posed in: Attributed to Burcroff and O'Brien, Discrete Math. 346 (2023), 113508, Question 8.1 (arXiv version), and Zhang, arXiv:2111.00641v2, Conjecture 4.1; numbering unverified
Status: Counterexample
Result: A tree on 7284 vertices has a unimodal domination polynomial with unique mode 3978, while deleting one specified leaf gives a 7283-vertex tree whose domination polynomial is unimodal with unique mode 3976.

Abstract

Deleting a leaf can move the unique mode of an explicit tree domination polynomial by two.

Details

Year: 2026
Discipline: Mathematics
Area: Graph polynomials
Subject: Graph theory and graph polynomials
Result type: Standalone theorem and reproducible proof package
Formal proof: Standalone Lean package
Family: leaf-deletion
Keywords: domination polynomial, unimodal sequences, mode of a polynomial, trees, leaf deletion

Statement and scope

Formal scope. The fixed tree, deletion, actual domination counts and unique-mode movement are formalized. External question identity and historical priority remain provisional.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 380 KB
PDF on GitHub: papers/mathematics/leaf-deletion/manuscript/manuscript.pdf
LaTeX source: papers/mathematics/leaf-deletion/manuscript/manuscript.tex
Bibliography: papers/mathematics/leaf-deletion/manuscript/references.bib

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/leaf-deletion/

Lean project

papers/mathematics/leaf-deletion/formalization/ 20 Lean files

Lakefile

papers/mathematics/leaf-deletion/formalization/lakefile.lean

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

The commands below are quoted from papers/mathematics/leaf-deletion/README.md, which gives their context and working directory.

cd formalization
bash build.sh

cd manuscript
bash build.sh

README: papers/mathematics/leaf-deletion/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Questions and answers

Can deleting a leaf move the mode of a tree's domination polynomial by more than one?

Yes. An explicit tree on 7284 vertices has unique mode 3978, and deleting one specified leaf gives a tree with unique mode 3976, both polynomials being unimodal. This answers Burcroff–O'Brien Question 8.1 or Zhang's Conjecture 4.1 only if their definitions match the stated proximity assertion, which is unverified.

Does this settle unimodality of domination polynomials of trees?

No. No all-tree unimodality result, unbounded mode jump or smallest witness is claimed; the result concerns local mode stability under leaf deletion.

Is the proof formally verified?

Yes. Lean 4 formalizes the fixed tree, the induced leaf deletion, the actual dominating-set counts, unimodality and both unique modes. External question identity and historical priority remain provisional.

Cite

Citation file papers/mathematics/leaf-deletion/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@unpublished{goyalLeafDeletion,
 author = {Dev D. Goyal},
 title = {Leaf deletion can move the unique mode of a tree domination polynomial by two},
 year = {2026},
 note = {Unpublished manuscript. Historical novelty remains provisional.}
}