Sharp root log-concavity of alternating Motzkin sums

Dev D. Goyal

Sharp root log-concavity of alternating Motzkin sums

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

Problem and result

Problem: Zhao's root log-concavity conjecture for alternating sums of Motzkin numbers
Posed in: Feng-Zhen Zhao, INTEGERS 26 (2026), A55, Conjecture 1
Status: Proved
Result: With Tₙ the alternating sum of the Motzkin numbers M₀,…,Mₙ, the sequence Tₙ^(1/n) is strictly log-concave from n = 5 and the inequality reverses at center 5, so 5 is optimal; this contains Zhao's tail from n = 9.

Abstract

Let Tₙ be the alternating sum of Motzkin numbers through index n. The sequence Tₙ^(1/n) is strictly log-concave on its tail starting at five. The inequality reverses at center five, so no earlier tail is log-concave. This strengthens Zhao’s proposed tail starting at nine. The source recurrence and finite sum are linked in Lean.

Details

Year: 2026
Discipline: Mathematics
Area: Integer sequences and combinatorics
Subject: Integer sequences and combinatorics
Result type: Conjecture resolution with an optimal threshold
Formal proof: Shared Lean library
Family: alternating-motzkin
Keywords: Motzkin numbers, alternating sums, log-concavity, root log-concavity, Zhao conjecture

Statement and scope

Result summary. The catalogue summary repeats the abstract above, including its stated limits. The formally checked statements are listed under Formal proof.

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 314 KB
PDF on GitHub: papers/mathematics/motzkin/paper.pdf
LaTeX source: papers/mathematics/motzkin/paper.tex
Bibliography: papers/mathematics/motzkin/references.bib

Formal proof

The selected theorems of this result are proved in the shared Lean 4 library of the repository. Its Comparator configuration checks each one against the matching statement in the Challenge module and permits only the axioms propext, Classical.choice and Quot.sound.

Proof module: lean/MathAndTheory/Mathematics/Motzkin/Source.lean
Family sources: lean/MathAndTheory/Mathematics/Motzkin/
Challenge: lean/Challenges/Mathematics/Motzkin/Main.lean
Solution interface: lean/Solutions/Mathematics/Motzkin/Main.lean
Comparator file: lean/comparator/mathematics/motzkin.json
Statement guide: lean/docs/mathematics/motzkin.md
Toolchain: leanprover/lean4:v4.35.0

Checked theorems

Namespace MathAndTheory.Motzkin

MathAndTheory.Motzkin.Palomar.source_defined_result

Reproduce

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

python3 papers/mathematics/motzkin/verification/scripts/verify.py

cd lean
lake build MathAndTheory.Mathematics.Motzkin.Source
lake env lean Challenges/Mathematics/Motzkin/Main.lean
lake env lean Solutions/Mathematics/Motzkin/Main.lean

lake env lean --stdin <<'LEAN'
import MathAndTheory.Mathematics.Motzkin.Source
#print axioms MathAndTheory.Motzkin.Source.solution
#print axioms MathAndTheory.Motzkin.Source.finite_sum_roots_strict_log_concave
#print axioms MathAndTheory.Motzkin.Source.finite_sum_roots_sharp_failure
LEAN

./scripts/verify-comparator.sh comparator/mathematics/motzkin.json

The same file gives further commands.

README: papers/mathematics/motzkin/README.md
Verification guide: papers/mathematics/motzkin/verification/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Original problem. Zhao, INTEGERS 26 (2026), A55, Conjecture 1; OEIS A187306.

Questions and answers

Is Zhao's Conjecture 1 on alternating Motzkin sums true?

Yes. The preprint proves that (Tₙ^(1/n)) is strictly log-concave on the tail starting at n = 5, which contains Zhao's tail from 9, and shows the inequality fails at center 5, so no earlier tail works. The separate claim that the roots increase to three is outside the formal theorem.

Has anyone else claimed this result?

Yes. A public manuscript added on 17 October 2026 to the xzwwwwww/math repository claims strict root log-concavity at centers n ≥ 10, i.e. Zhao's tail. No priority is claimed here, and the method builds on Došlić–Veljan, Zhao, Chen–Guo–Wang and Hou–Li.

Is the proof formally verified?

Yes. Lean 4 proves strict log-concavity from 5 and the sharp failure at center 5, and links the source recurrence and finite sum to the sequence used in the proof; no lattice-path correspondence is formalized.

Cite

Citation file papers/mathematics/motzkin/citation.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026alternatingmotzkin,
  author = {Dev D. Goyal},
  title = {Sharp root log-concavity of alternating {Motzkin} sums},
  year = {2026},
  month = oct,
  howpublished = {Math and Theory research collection},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/motzkin},
  note = {Preprint, 26 October 2026. Not peer reviewed. Includes a Lean 4.35.0 formalization. See the collection's authorship disclosure for the autonomous research process.}
}