Diagonal concavity does not imply concavity for sums of elementary symmetric polynomials

Dev D. Goyal

Diagonal concavity does not imply concavity for sums of elementary symmetric polynomials

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

Problem and result

Problem: Lachaume's diagonal concavity conjecture for sums of elementary symmetric polynomials
Posed in: Lachaume, arXiv:1712.10327v1, Conjecture 1
Status: Disproved
Result: For f = 1 + Mσ₁ + σ₂ + Mσ₃ + σ₄ in four variables with M > 0, f^(1/4) is concave on the positive diagonal exactly when M ≥ 1 and on the whole positive orthant exactly when M = 1, so every M > 1 is a counterexample.

Abstract

For positive M, let f=1+Mσ₁+σ₂+Mσ₃+σ₄ in four variables. Its fourth root is concave on the positive diagonal exactly when M≥1. It is concave on the full positive orthant exactly when M=1. Every M>1 therefore disproves Lachaume’s diagonal criterion with strictly positive coefficients.

Details

Year: 2026
Discipline: Mathematics
Area: Inequalities and real analysis
Subject: Inequalities and real analysis
Result type: Counterexample and complete parameter classification
Formal proof: Shared Lean library
Family: diagonal-concavity
Keywords: elementary symmetric polynomials, concavity, Lachaume criterion, hyperbolic polynomials, fourth root concavity

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 293 KB
PDF on GitHub: papers/mathematics/diagonal-concavity/paper.pdf
LaTeX source: papers/mathematics/diagonal-concavity/paper.tex
Bibliography: papers/mathematics/diagonal-concavity/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/DiagonalConcavity/Main.lean
Family sources: lean/MathAndTheory/Mathematics/DiagonalConcavity/
Challenge: lean/Challenges/Mathematics/DiagonalConcavity/Main.lean
Solution interface: lean/Solutions/Mathematics/DiagonalConcavity/Main.lean
Comparator file: lean/comparator/mathematics/diagonal-concavity.json
Statement guide: lean/docs/mathematics/diagonal-concavity.md
Toolchain: leanprover/lean4:v4.35.0

Checked theorems

Namespace MathAndTheory.DiagonalConcavity

ConcavityChallenge.result

Reproduce

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

Reproduce the computation

python3 papers/mathematics/diagonal-concavity/verification/scripts/verify.py

Reproduce the formal checks

cd lean
lake exe cache get
lake build MathAndTheory.Mathematics.DiagonalConcavity.Main Solutions.Mathematics.DiagonalConcavity.Main
lake env lean Solutions/Mathematics/DiagonalConcavity/Main.lean

Reproduce the formal checks

bash scripts/verify-comparator.sh comparator/mathematics/diagonal-concavity.json

README: papers/mathematics/diagonal-concavity/README.md
Verification guide: papers/mathematics/diagonal-concavity/verification/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Original problem. Lachaume, arXiv:1712.10327v1, Conjecture 1.

Questions and answers

Is Lachaume's diagonal concavity conjecture true?

No. Conjecture 1 of Lachaume (arXiv:1712.10327v1) asserts that concavity of (Σ aⱼσⱼ)^(1/p), aⱼ ≥ 0, on the positive orthant is equivalent to concavity on its positive diagonal; for n = p = 4 and coefficients (1, M, 1, M, 1), the fourth root is diagonally concave for every M ≥ 1 but concave on the orthant only at M = 1. For example, (1, 2, 1, 2, 1) is a counterexample with all coefficients positive.

How general is the classification?

It is a complete classification for this one-parameter family in four variables with M > 0; it does not classify arbitrary coefficient vectors or other dimensions. The case M = 1 follows from concavity of the geometric mean.

Is the result formally verified?

Yes. Both equivalences are proved in Lean 4 with Mathlib's ConcaveOn predicate and elementary symmetric functions, checked against an independent Comparator challenge statement, using only the axioms propext, Classical.choice and Quot.sound.

Cite

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

@misc{goyal2026diagonalconcavity,
  author = {Dev D. Goyal},
  title = {Diagonal concavity does not imply concavity for sums of elementary symmetric polynomials},
  year = {2026},
  month = oct,
  howpublished = {Preprint},
  version = {1.0.0},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/diagonal-concavity},
  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.}
}