Symmetric minimizer for a positive definite Jordan–Kronecker product
Let $n \ge 2$, let $A, B \in \mathbb{R}^{n \times n}$ be symmetric positive definite, and let $T \in \mathbb{R}^{n^2 \times n^2}$ be the commutation matrix, $T \operatorname{vec}(X) = \operatorname{vec}(X^{\mathsf T})$, where $\operatorname{vec}$ stacks columns; its eigenspaces for $1$ and $-1$ consist of the vectorised symmetric and skew-symmetric matrices. Kalantarova and Tunçel proved that for all symmetric $A', B'$ of order $n \le 3$ the smallest and largest eigenvalues of their Jordan–Kronecker product $A' \otimes B' + B' \otimes A'$ have symmetric eigenvectors, and gave a pair of symmetric, not definite, $4 \times 4$ matrices for which the eigenvector of the smallest eigenvalue is skew-symmetric.
Problem. Is it always true that $$\min_{\substack{u \in \mathbb{R}^{n^2} \setminus \{0\} \\ Tu = u}} \frac{u^{\mathsf T}(A \otimes B)u}{u^{\mathsf T}u} \le \min_{\substack{w \in \mathbb{R}^{n^2} \setminus \{0\} \\ Tw = -w}} \frac{w^{\mathsf T}(A \otimes B)w}{w^{\mathsf T}w}?$$ Equivalently, must the smallest eigenvalue of $A \otimes B + B \otimes A$ have an eigenvector $\operatorname{vec}(X)$ with $X = X^{\mathsf T} \ne 0$?
Source: Kalantarova and Tunçel (2021), Conjecture 1.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- OC, SP
- Keywords
- Kronecker products, OpenProblemsInNLA, Rayleigh quotients
References
@article{kalantarova2021,
author = {Kalantarova, Nargiz and Tun{\c{c}}el, Levent},
title = {On the spectral structure of {J}ordan--{K}ronecker products of symmetric and skew-symmetric matrices},
journal = {Linear Algebra Appl.},
volume = {608},
year = {2021},
pages = {343--362},
doi = {10.1016/j.laa.2020.08.022},
eprint = {1805.09737},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-sp05,
author = {Townsend, Alex},
title = {{SP-05}: Symmetric minimizer for a positive definite Jordan–Kronecker product},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/eigenvalues-and-inverse-problems/SP-05/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00120.
namespace RegistryProblems.OP_00120
noncomputable section
open scoped BigOperators Matrix
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℝ
abbrev Vec (n : ℕ) := (Fin n × Fin n) → ℝ
abbrev Operator (n : ℕ) := Matrix (Fin n × Fin n) (Fin n × Fin n) ℝ
/-- The actual commutation permutation matrix, swapping row and column indices. -/
def commutationMatrix (n : ℕ) : Operator n :=
fun i j => if i = j.swap then 1 else 0
/-- Literal real Rayleigh quotient; target vectors are always nonzero. -/
def rayleigh {n : ℕ} (K : Operator n) (v : Vec n) : ℝ :=
dotProduct v (K *ᵥ v) / dotProduct v v
/-- All quotient values in the specified eigenspace of the actual commutation matrix. -/
def sectorValues {n : ℕ} (A B : Mat n) (ε : ℝ) : Set ℝ :=
{r | ∃ v : Vec n, v ≠ 0 ∧ commutationMatrix n *ᵥ v = ε • v ∧
r = rayleigh (Matrix.kronecker A B) v}
/-- OP-00120: Symmetric minimizer for a positive definite Jordan–Kronecker product -/
def _root_.RegistryProblems.Problem_OP_00120 : Prop :=
∀ (n : ℕ), 2 ≤ n → ∀ (A B : Mat n), A.PosDef → B.PosDef →
∃ a b : ℝ, IsLeast (sectorValues A B 1) a ∧
IsLeast (sectorValues A B (-1)) b ∧ a ≤ b
end
end RegistryProblems.OP_00120
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00120 theorem resolution : RegistryProblems.Problem_OP_00120 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00120" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00120 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
The complete original symmetric/skew Rayleigh-minimum inequality for every real symmetric positive-definite pair and every n≥2, with actual attained sector minima. The stronger source result gives a real nonzero PSD eigenmatrix at the global Jordan minimum for every n≥1.
For real symmetric positive definite $n\times n$ matrices $A$ and $B$, the operator $\mathcal L(X)=AXB+BXA$, whose matrix under column vectorization is $A\otimes B+B\otimes A$, has a nonzero real positive-semidefinite eigenmatrix for its smallest eigenvalue. The inverse of $\mathcal L$ is written as $\int_0^\infty M_tYM_t\,dt$ with real symmetric $M_t$, so it preserves positive semidefiniteness. For a symmetric or skew-symmetric eigenmatrix $W$ …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, SP-05/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00120, "Symmetric minimizer for a positive definite Jordan–Kronecker product", clopen.solutions.