slug: garcia-velo-2026-product-unitary-choi-spectrum bibkey: garciavelo2026schwarz doi: 10.48550/arXiv.2601.02282 url: https://arxiv.org/abs/2601.02282v1 triage: theorem motivation_gids:

D5/S3/Quantum/QuantumChannels/ProductUnitaryChoiSpectrum.result

The Choi spectrum of unital product-unitary-equivariant maps

Problem

A. García-Velo and A. Ibort, Schwarz maps with symmetry, arXiv:2601.02282v1, classify the unital, Hermiticity-preserving maps on $M_{n_{1}} (C) \otimes M_{n_{2}} (C)$ that commute with conjugation by $U \otimes V$ : they are $Φ = D_{1} \otimes D_{2} + λ_{01} D_{1} \otimes Q_{2} + λ_{10} Q_{1} \otimes D_{2} + λ_{11} Q_{1} \otimes Q_{2}$ with real weights, where $D_{i} (X) = tr (X) I / n_{i}$ and $Q_{i} = id - D_{i}$ . Lemma V.8 gives the eigenvalues of the Choi matrix $C_{Φ} = \sum_{p, q} E_{pq} \otimes Φ (E_{pq})$ for $n_{1}, n_{2} \in {2, 3}$ , and Remark V.2 conjectures the same four values, with multiplicities $1$ , $n_{1}^{2} - 1$ , $n_{2}^{2} - 1$ and $(n_{1}^{2} - 1) (n_{2}^{2} - 1)$ , in every dimension. The verbatim statements are in the literature note.

Issue #14200 reads the conjecture as an identity of characteristic polynomials, which records the eigenvalues with their algebraic multiplicities, for $n_{1}, n_{2} \geq 1$ and complex weights.

Motivation

The Choi spectrum decides complete positivity of $Φ$ (Choi’s theorem), and the paper uses it to describe the completely positive region and to check the PPT² property for $(n_{1}, n_{2}) = (2, 2)$ and $(2, 3)$ . D5/S3/Quantum/QuantumChannels/ProductUnitaryChoiSpectrum.result proves the conjectured spectrum for all $n_{1}, n_{2} \geq 1$ .

Gap

Issue #14200 records the literature check before any Lean: arXiv lists only v1; arXiv API searches for the title, for product-unitary and local-unitary covariant Choi eigenvalues and for $U (n_{1})$ with $U (n_{2})$ return this paper and arXiv:2404.10895 (qubit $D U (2)$ maps); arXiv:1811.08193 treats single- $U (n)$ equivariant maps and does not state this spectrum; a search seat reported zero INSPIRE citations and no entry in google-deepmind/formal-conjectures; the repository had no result on these maps. not-found-in-searched-scope.

Route

Sector form. The Choi matrix of $D$ is $I / n$ and that of $Q$ is $K - I / n$ , where $K = ω ω^{T}$ and $ω = \sum_{j} e_{j} \otimes e_{j}$ . Grouping the indices of $C_{Φ}$ by factor gives $a I + b (I \otimes K_{2}) + c (K_{1} \otimes I) + d (K_{1} \otimes K_{2})$ with the source’s $a, b, c, d$ .
Shear. With $u = ω - e_{00}$ , $S = I + u e_{00}^{T}$ has inverse $I - u e_{00}^{T}$ because $e_{00}^{T} u = 0$ , and $S^{- 1} K S = e_{00} (ω + (n - 1) e_{00})^{T}$ has a single nonzero row with diagonal entry $n$ .
Blocks. After conjugation by $S_{1} \otimes S_{2}$ the matrix is block upper triangular for the four blocks “first index $= (0, 0)$ or not, second index $= (0, 0)$ or not”, each block a multiple of the identity: values $a + b n_{2} + c n_{1} + d n_{1} n_{2}$ , $a + c n_{1}$ , $a + b n_{2}$ , $a$ on blocks of sizes $1$ , $n_{2}^{2} - 1$ , $n_{1}^{2} - 1$ , $(n_{1}^{2} - 1) (n_{2}^{2} - 1)$ .

Falsifier

The settlement would change under a reading of the eigenvalues other than as the roots of the characteristic polynomial counted with algebraic multiplicity, or under a Choi convention other than $\sum_{p, q} E_{pq} \otimes Φ (E_{pq})$ ; for real weights $C_{Φ}$ is Hermitian, so algebraic and geometric multiplicities agree.

Evidence

Lean owner: D5/S3/Quantum/QuantumChannels/ProductUnitaryChoiSpectrum.lean, module statement id sha256:c8832dbe0412e1a29f77d85253d4e998ebc7907c8121e7ceaafc7db22e0c3bf2.
claim (statement id sha256:187a9b5607d6a7db1552ea74e2ce603c7ca3efe2991912bc3553e30dfd581f24) states the characteristic-polynomial identity for all $n_{1}, n_{2} \geq 1$ and complex weights; result : claim (statement id sha256:f58ed2d9e28956c96241bb85b52e5d77590f78f5beb6a1ce72e9a9d24d7ab21c) proves it.
Freeze event sha256:910a2b2de39f9a730f0a9cc501d442b4d1730e9f33fb28607f033f28aadd543e, with the frozen prerequisite D5/S3/Quantum/Foundation/FiniteKrausChannel (sha256:260af10ef3dd71e5df80b276fb86150bfeac5abf14a7b2ee3dda7ce20167d26a).
#print axioms result: propext, Classical.choice, Quot.sound.

Triage

Tier 1 conjecture of a January 2026 paper, preregistered in issue #14200 before any Lean. theorem; resolution proved.

declaration	proof_shape	escape_witness	admission_basis
result	bind-only	none	open-problem-resolution

The other public declarations (omega, kmat, dmat, qmat, omega_dot_omega, choi_reindex) and the private theorems are bind-only or definitions used on the proof path of result (CLAUDE.md §3.2 「有消费的辅助声明」); the consumer list is in the module’s judgement comment. Utility is none. There is no digestion atom.

What the settlement shows

Proved by result: for all $n_{1}, n_{2} \geq 1$ and complex $λ_{01}, λ_{10}, λ_{11}$ , the characteristic polynomial of $C_{Φ}$ is $(X - e_{1}) (X - e_{2})^{n_{1}^{2} - 1} (X - e_{3})^{n_{2}^{2} - 1} (X - e_{4})^{(n_{1}^{2} - 1) (n_{2}^{2} - 1)}$ with the four values of Lemma V.8.

Established inside the proof. The reindexed Choi matrix equals $D_{1}^{C} \otimes D_{2}^{C} + λ_{01} D_{1}^{C} \otimes Q_{2}^{C} + λ_{10} Q_{1}^{C} \otimes D_{2}^{C} + λ_{11} Q_{1}^{C} \otimes Q_{2}^{C}$ with $D^{C} = I / n$ and $Q^{C} = K - I / n$ (choi_reindex), and the shear conjugation of $K$ (conj_kmat).

Argued, not formalized.

Mechanism. $C_{Φ}$ is a polynomial in the two commuting operators $K_{1} \otimes I$ and $I \otimes K_{2}$ ; each single-factor $K_{i}$ has eigenvalues $n_{i}$ (multiplicity $1$ ) and $0$ (multiplicity $n_{i}^{2} - 1$ ), and tensoring with the identity multiplies these multiplicities by the dimension of the other factor. Each eigenvalue of $C_{Φ}$ is $\sum_{α, β} λ_{α β} c_{α}^{(1)} c_{β}^{(2)}$ with $c_{0}^{(i)} = 1/ n_{i}$ and $c_{1}^{(i)} \in {n_{i} - 1/ n_{i}, - 1/ n_{i}}$ ; this is why the values Lemma V.8 computed in dimensions $2$ and $3$ keep their form.
Extension. The same argument gives the Choi spectrum of $\sum_{S} λ_{S} ⨂_{i} P_{[i \in S]}^{(i)}$ on any number $m$ of tensor factors: $2^{m}$ values indexed by subsets $T$ of the factors, with multiplicity $\prod_{i \in T} (n_{i}^{2} - 1)$ .
Complete positivity. For real weights and $n_{1}, n_{2} \geq 2$ all four multiplicities are positive, so by Choi’s theorem $Φ$ is completely positive iff $e_{1}, e_{2}, e_{3}, e_{4} \geq 0$ : four linear inequalities in every dimension, the form the paper found for $(2, 2)$ and $(2, 3)$ .

Open. The Schwarz-map region for general $(n_{1}, n_{2})$ is not addressed here. The PPT² property of this family in every dimension is the subject of issue #14289.

Effect on the paper. Remark V.2 holds in every dimension, and the complete-positivity description of Propositions V.6 and V.7 extends to all $n_{1}, n_{2} \geq 2$ through Choi’s theorem.

ASSUMED-UNVERIFIED

The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent proof.

Keyboard shortcuts

trureturing — Discovering truth