Metadata
bibkey: malkoun2026mo512579
authors: Malkoun
year: 2026
title: Promoting polynomial equalities for nonnegative variables to elementary symmetric polynomial inequalities
doi: null
url: https://mathoverflow.net/questions/512579
claim: "For all complex Hermitian positive semidefinite X,Y and every 1 ≤ k ≤ n, e_k(lambda(XY+YX)) ≤ e_k(lambda(X²+Y²))."
strata_touched:
- D5/S3/Quantum/Matrix/MalkounJordanElementary
license: CC-BY-SA-4.0
triage: anchor
The source is revision 1, revision GUID DFD20136-D37A-462C-8A59-FD828AEEFF9A, of the MathOverflow question by Malkoun (user 81645). Only the explicit two-matrix question is considered. The later unspecified promotion question is outside the assertion. Eigenvalues count algebraic multiplicity; the matrices are complex Hermitian positive semidefinite, the order n is any positive integer, and k ranges from one to n. No positivity of XY+YX is assumed. The question text is licensed under CC BY-SA 4.0.
The proof uses the existing public cauchyBinet in CompoundMatrices and pinned Mathlib spectral and principal-minor identities. CompoundMatrices already contains the source and Apache-2.0 attribution for its supplier; no supplier code is copied here. No claim of worldwide literature priority is made.
Verified locator
https://mathoverflow.net/questions/512579
Revision 1, GUID DFD20136-D37A-462C-8A59-FD828AEEFF9A, by Malkoun, is the source of the explicit two-matrix assertion. Quotations and mathematical notation adapted from this question retain the CC BY-SA 4.0 attribution; the formal proof and its explanation apply the separately attributed existing Lean and Mathlib results.
Scope of the literature reading
The Stack Exchange API question response observed at 2026-10-31T23:02:47Z reported answer_count = 0, is_answered = false and no accepted answer. The exact revision response identifies the source author and the complete first question. These are finite source-page observations, not a literature-wide priority result. The preregistration in issue #24963 supplies the earlier bounded literature check; its wider search results were not independently reproduced here. The repository application is described in the problem dossier.