Math and TheorySharp log-concavity for alternating Motzkin sums
Problem and result
- Problem
- Bounded-forcing log-concavity for Motzkin-type recurrences and alternating Motzkin sums
- Posed in
- Motivated by Zhao, INTEGERS 26 (2026), A55, Conjecture 1 (p. 8); the extensions answer no posed question
- Status
- New theorem
- Result
- Real aₙ with (m+2)aₘ = m(2aₘ₋₁+3aₘ₋₂)+εₘ, |εₘ| ≤ 2 for m ≥ 14, a₁₂ > 1800 and L₁₂ < a₁₃/a₁₂ < U₁₂ satisfy aₙ > 8(n+3)² and a ratio log-concavity margin 800aₙ⁴/(n+3)³ for all n ≥ 12.
Abstract
A robust bounded-forcing recurrence theorem and corrected scaled corollary, with applications to alternating Motzkin-type sums.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Integer sequences
- Subject
- Integer sequences and combinatorics
- Result type
- Standalone theorem and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
motzkin-bounded-forcing- Keywords
- Motzkin numbers, log-concavity, linear recurrences, bounded forcing, alternating Motzkin sums
Statement and scope
Formal scope. The arbitrary-real recurrence theorem and scaled corollary, including zero forcing, are formalized. Concrete sequences, uniform-family applications, root transfer and threshold classification retain conventional proofs.
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.pdf345 KB- PDF on GitHub
papers/mathematics/ motzkin/ bounded-forcing/ manuscript.pdf - LaTeX source
papers/mathematics/ motzkin/ bounded-forcing/ 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/ motzkin/ bounded-forcing/ - Lean project
papers/10 Lean filesmathematics/ motzkin/ bounded-forcing/ formalization/ - Lakefile
papers/mathematics/ motzkin/ bounded-forcing/ formalization/ lakefile.toml - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
Reproduce the formal proof
python3 -B check_package.py
lake exe cache get
python3 -B verify.pyCheck the arithmetic support
python3 -B -O -S verification/verify_original.py
python3 -B -O -S verification/verify_extensions.py --no-regressions
python3 -B -O -S verification/mutation_tests.py- README
papers/mathematics/ motzkin/ bounded-forcing/ README.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Questions and answers
What does this paper prove?
Real sequences satisfying the Motzkin-type recurrence up to errors |εₘ| ≤ 2 (scaled version: ≤ B), with the stated seed at n = 12, grow, keep a strict ratio interval and are ratio log-concave with margin 800aₙ⁴/(n+3)³ for n ≥ 12. Applications give optimal quotient-tail start 10 and root-tail start 5 for alternating Motzkin sums and classify sharp thresholds for Aₙ(s) = Rₙ₊₁ + s(−1)ⁿ, 0 ≤ s ≤ 1.
Is it formally verified?
Lean 4 proves the bounded-forcing theorem and the scaled corollary, including B = 0, for arbitrary real sequences. The concrete-sequence applications, uniform family, root transfer and threshold classifications have conventional proofs only.
Is there prior work on the original conjecture?
Yes. A public manuscript dated 17 October 2026 already claims Zhao's root-log-concavity conjecture, and ratio-to-root transfer is prior methodology (Chen, Guo and Wang). No priority is claimed, and the novelty of the extensions is unresolved.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@unpublished{Goyal2026MotzkinForcing,
author = {Goyal, Dev D.},
title = {Sharp log-concavity for alternating Motzkin sums},
year = {2026},
note = {Preprint; not peer reviewed}
}