Ultra-log-concavity of domination sequences of powers of paths and cycles

Dev D. Goyal

Ultra-log-concavity of domination sequences of powers of paths and cycles

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

Problem and result

Problem: Galvin–Zhang conjecture on ultra-log-concave domination sequences of path and cycle powers
Posed in: Galvin and Zhang, arXiv:2408.12731, Conjecture 1.8; also Zhang's 2025 dissertation, Conjecture 4.1.8
Status: Proved
Result: For every n ≥ 0 and power ℓ ≥ 1, the number d_k of size-k dominating sets of P_n^ℓ and of C_n^ℓ satisfies (k+1)(n−k+1)d_{k−1}d_{k+1} ≤ k(n−k)d_k², so d_k/binom(n,k) is log-concave.

Abstract

The domination counts of every natural power of a path or cycle form an ultra-log-concave sequence. The proof includes all natural graph orders and powers, the binomial normalization, and the boundary graph cases.

Details

Year: 2026
Discipline: Mathematics
Area: Graph theory
Subject: Graph theory and graph polynomials
Result type: Ultra-log-concavity of domination sequences
Formal proof: Standalone Lean package
Family: galvin-zhang
Keywords: domination polynomial, ultra-log-concavity, powers of paths, powers of cycles, Galvin–Zhang, dominating sets

Statement and scope

Formal scope. Actual finite graph domination counts for powers of paths and cycles. No theorem for arbitrary graphs or real-rootedness is asserted.

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 301 KB
PDF on GitHub: papers/mathematics/galvin-zhang/manuscript.pdf
LaTeX source: papers/mathematics/galvin-zhang/manuscript.tex

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/galvin-zhang/ 18 Lean files

Lakefile

papers/mathematics/galvin-zhang/lakefile.toml

Toolchain

leanprover/lean4:v4.19.0

Library roots

Reproduce

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

Reproduce the proof

lake exe cache get
lake build
lake env lean -j1 -DwarningAsError=true Audit.lean

README: papers/mathematics/galvin-zhang/README.md
Verification record: papers/mathematics/galvin-zhang/VERIFICATION.md
Related work: papers/mathematics/galvin-zhang/RELATED_WORK.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. Galvin and Zhang, Conjecture 1.8.

Questions and answers

Is the Galvin–Zhang conjecture on domination sequences true?

Yes, for the statement of Conjecture 1.8: this preprint proves that for every n ≥ 0 and ℓ ≥ 1 the domination sequences of P_n^ℓ and C_n^ℓ are ultra-log-concave, meaning d_k/binom(n,k) is log-concave. Galvin and Zhang had proved unimodality for both families.

Does the result apply to other graphs or give real-rootedness?

No. The theorem concerns only powers of paths and cycles; it makes no real-rootedness claim and gives no conclusion for arbitrary graphs or all trees.

Is the proof formally verified?

Yes. The Lean 4 theorem DominationULC.galvin_zhang_conjecture is stated for cardinalities of actual dominating vertex subsets, for all orders and powers (including ℓ = 0), with no finite cutoff; the audit permits only propext, Classical.choice and Quot.sound.

Cite

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

@misc{goyal2026domination,
  author = {Goyal, Dev D.},
  title = {Ultra-log-concavity of domination sequences of powers of paths and cycles},
  year = {2026},
  note = {Preprint},
  url = {https://github.com/dvgyl/math-and-theory}
}