Thompson-type domination for the arithmetic symmetric modulus
For $X \in \mathbb{C}^{n \times n}$ let $|X| = (X^*X)^{1/2}$ and let $$S(X) = \frac{|X| + |X^*|}{2}$$ be its arithmetic symmetric modulus; $P \preceq Q$ means that $Q - P$ is positive semidefinite. Thompson proved that for all $X, Y$ there are unitaries $U, V$ with $|X + Y| \preceq U|X|U^* + V|Y|V^*$, and Zhang proved the same for the quadratic symmetric modulus $\bigl((|X|^2 + |X^*|^2)/2\bigr)^{1/2}$. For $S$ the inequality below fails with $1$ in place of $\sqrt2$ (Zhang).
Problem. For every $n \ge 1$ and all $X, Y \in \mathbb{C}^{n \times n}$, are there unitary $U, V \in \mathbb{C}^{n \times n}$ such that $$S(X + Y) \preceq \sqrt2\,\bigl(U S(X) U^* + V S(Y) V^*\bigr)?$$
Source: Zhang (2026), Conjecture 1.6, its existence part.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- FA — Functional Analysis
- Secondary
- NA
- Keywords
- OpenProblemsInNLA, symmetric moduli, triangle inequalities, unitary orbits
References
@misc{zhang2026,
author = {Zhang, Teng},
title = {Operator symmetric moduli and sharp triangle inequalities},
year = {2026},
eprint = {2603.01046},
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{zhang2026a,
author = {Zhang, Teng},
title = {An operator triangle inequality for the quadratic symmetric modulus},
year = {2026},
eprint = {2602.01463},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-mi06,
author = {Townsend, Alex},
title = {{MI-06}: Thompson-type domination for the arithmetic 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-06/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00100.
namespace RegistryProblems.OP_00100
noncomputable section
open scoped BigOperators Classical ComplexOrder Matrix MatrixOrder
/-- The genuine positive modulus, defined by continuous functional calculus. -/
def matrixModulus {n : ℕ} (X : Matrix (Fin n) (Fin n) ℂ) :
Matrix (Fin n) (Fin n) ℂ := CFC.abs X
/-- The arithmetic average of the right and left moduli. -/
def symmetricModulus {n : ℕ} (X : Matrix (Fin n) (Fin n) ℂ) :
Matrix (Fin n) (Fin n) ℂ :=
(1 / 2 : ℂ) • (matrixModulus X + matrixModulus X.conjTranspose)
/-- Conjugation by an arbitrary genuine complex 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-00100: Thompson-type domination for the arithmetic symmetric modulus -/
def _root_.RegistryProblems.Problem_OP_00100 : Prop :=
∀ n : ℕ, 1 ≤ n → ∀ A B : Matrix (Fin n) (Fin n) ℂ,
∃ U V : Matrix.unitaryGroup (Fin n) ℂ,
symmetricModulus (A + B) ≤
(Real.sqrt 2 : ℂ) •
(unitaryConjugate U (symmetricModulus A) +
unitaryConjugate V (symmetricModulus B))
end
end RegistryProblems.OP_00100
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_00100 theorem resolution : RegistryProblems.Problem_OP_00100 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00100" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00100 := 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 the genuine CFC square-root modulus identities, an exact rational three-dimensional witness, a nonzero common orthogonal vector for arbitrary complex constraints, all-unitary quadratic bounds, and the full negation of the original universal factor-sqrt(2) PSD domination conjecture.
For a square complex matrix $X$, let $\mathcal S(X)=(|X|+|X^*|)/2$ be its arithmetic symmetric modulus. The note shows that there is no finite constant $C\ge0$ such that every pair $X,Y\in\mathbb M_3(\mathbb C)$ admits unitaries $U,V$ with $\mathcal S(X+Y)\le C\bigl(U\mathcal S(X)U^*+V\mathcal S(Y)V^*\bigr)$ in the Loewner order; in particular the conjectured constant $\sqrt2$ fails. The witnesses are the real rank-one matrices $X=e_1(e_1+te_2)^*$ and …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MI-06/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00100, "Thompson-type domination for the arithmetic symmetric modulus", clopen.solutions.