The triangle conjecture for the maximal symmetric modulus
For $X \in \mathbb{C}^{n \times n}$ let $|X| = (X^*X)^{1/2}$, and let $$M(X) = \lim_{r \to \infty} \bigl(|X|^r + |X^*|^r\bigr)^{1/r} \qquad (r \in \mathbb{N})$$ be its maximal symmetric modulus, the supremum of $|X|$ and $|X^*|$ in Olson's spectral order. Thompson proved that for all $A, B \in \mathbb{C}^{n \times n}$ there are unitaries $U, V$ with $|A + B| \preceq U|A|U^* + V|B|V^*$, where $\preceq$ is the positive semidefinite order. Bourin and Lee asked more generally whether the inequality below holds with some factor $c(n)$, depending only on $n$, on the right.
Problem. For every $n \ge 1$ and all $A, B \in \mathbb{C}^{n \times n}$, are there unitary $U, V \in \mathbb{C}^{n \times n}$ such that $$M(A + B) \preceq U M(A) U^* + V M(B) V^*$$ in the positive semidefinite order?
Source: Bourin and Lee (2026), Conjecture 3.12 in arXiv:2606.15624v2 (3.15 in v1), the case of constant one in their Question 3.11.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- OpenProblemsInNLA, spectral order, symmetric moduli, triangle inequalities
References
@misc{bourin2026,
author = {Bourin, Jean-Christophe and Lee, Eun-Young},
title = {Averages over matrix unitary orbits and spectral order},
year = {2026},
eprint = {2606.15624},
archivePrefix = {arXiv},
}
@article{thompson1976,
author = {Thompson, Robert C.},
title = {Convex and concave functions of singular values of matrix sums},
journal = {Pacific J. Math.},
volume = {66},
number = {1},
year = {1976},
pages = {285--290},
doi = {10.2140/pjm.1976.66.285},
}
@misc{openproblemsinnla-mi07,
author = {Townsend, Alex},
title = {{MI-07}: The triangle conjecture for the maximal symmetric modulus},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-inequalities-and-norms/MI-07/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00101.
namespace RegistryProblems.OP_00101
noncomputable section
open scoped BigOperators Classical ComplexOrder MatrixOrder Topology
/-- The actual positive modulus from continuous functional calculus. -/
def matrixModulus {n : ℕ} (X : Matrix (Fin n) (Fin n) ℂ) :
Matrix (Fin n) (Fin n) ℂ := CFC.abs X
/-- The canonical sequence uses every positive integer exponent, indexed by `r+1`.
The outer exponent is a real CFC power, and the inner powers are matrix ring powers. -/
def rootSequence {n : ℕ} (X : Matrix (Fin n) (Fin n) ℂ) (r : ℕ) :
Matrix (Fin n) (Fin n) ℂ :=
CFC.rpow (matrixModulus X ^ (r + 1) +
matrixModulus X.conjTranspose ^ (r + 1)) (((r + 1 : ℕ) : ℝ)⁻¹)
/-- Actual finite-dimensional limit of the canonical CFC sequence.
`limUnder` is totalized away from convergence. Every counterexample occurrence
has its convergence proved explicitly; its default value is never used. -/
def maximalModulus {n : ℕ} (X : Matrix (Fin n) (Fin n) ℂ) :
Matrix (Fin n) (Fin n) ℂ := Filter.limUnder Filter.atTop (rootSequence X)
/-- Conjugation by an arbitrary genuine unitary matrix. -/
def unitaryConjugate {n : ℕ} (U : Matrix.unitaryGroup (Fin n) ℂ)
(H : Matrix (Fin n) (Fin n) ℂ) : Matrix (Fin n) (Fin n) ℂ :=
(U : Matrix (Fin n) (Fin n) ℂ) * H *
(U : Matrix (Fin n) (Fin n) ℂ).conjTranspose
/-- OP-00101: The triangle conjecture for the maximal symmetric modulus -/
def _root_.RegistryProblems.Problem_OP_00101 : Prop :=
∀ n : ℕ, 1 ≤ n → ∀ A B : Matrix (Fin n) (Fin n) ℂ,
∃ U V : Matrix.unitaryGroup (Fin n) ℂ,
maximalModulus (A + B) ≤
unitaryConjugate U (maximalModulus A) + unitaryConjugate V (maximalModulus B)
end
end RegistryProblems.OP_00101
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_00101 theorem resolution : RegistryProblems.Problem_OP_00101 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00101" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00101 := 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
Proves genuine complex matrix moduli, positive-integer CFC root-sequence limits at all witness matrices, the true spectral-norm topology bridge, an all-unitary trace obstruction, and the full original constant-one conjecture negation.
For a square complex matrix $Z$, the maximal symmetric modulus $\mathcal M(Z)=\lim_{r\to\infty}(|Z|^r+|Z^*|^r)^{1/r}$, over positive integers $r$, is the spectral-order join of $|Z|$ and $|Z^*|$. The note shows that no finite constant $C\ge0$ makes every pair $A,B\in\mathbb M_2(\mathbb C)$ admit unitaries $U,V$ with $\mathcal M(A+B)\le C\bigl(U\mathcal M(A)U^*+V\mathcal M(B)V^*\bigr)$; in particular the constant-one inequality is false. For $A=e_1e_1^*$ and $B=te_1e_2^*$ one has …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-07/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00101, "The triangle conjecture for the maximal symmetric modulus", clopen.solutions.