Magic-basis spectrum determines the interaction phases modulo pi

Open

QAlgorithms.Papers.Independent.Intakethird100.P99.magicSpectrum

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For a two-qubit unitary $U$ , let $\beta$ be an actual interaction-content witness: $U$ is locally equivalent, up to global phase, to $U_\beta=\exp[-i\sum_{k=1}^3\beta_k\sigma_k\otimes\sigma_k]$ , where $\sigma_1,\sigma_2,\sigma_3$ are the Pauli matrices $X,Y,Z$ and $\pi/4\ge\beta_1\ge\beta_2\ge|\beta_3|$ . Fix an actual phase-compatible decomposition $U=(A\otimes B)U_\beta(C\otimes D)$ with $A,B,C,D\in\mathrm{SU}(2)$ . Let $M$ be the matrix of this chosen representative in the ordered magic basis $-i(|01\rangle+|10\rangle)/\sqrt2$ , $(|00\rangle+|11\rangle)/\sqrt2$ , $-i(|00\rangle-|11\rangle)/\sqrt2$ , $(|01\rangle-|10\rangle)/\sqrt2$ . Put $\lambda=(\beta_1+\beta_2-\beta_3,\beta_1-\beta_2+\beta_3,-\beta_1+\beta_2+\beta_3,-\beta_1-\beta_2-\beta_3)$ . Then, for polynomial indeterminate $x$ ,

\operatorname{charpoly}(M^{T}M)(x)=\prod_{j=1}^{4}\bigl(x-e^{-2i\lambda_j}\bigr).

Transpose here has no complex conjugation. Multiplicities are retained; phases determine the $\lambda_j$ modulo $\pi$ , and principal arguments alone need not select the canonical chamber.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P99

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P99

open scoped Matrix Kronecker NNReal ENNReal

open QAlgorithms.Papers.Independent.Information100.P10 (pauli)

open QAlgorithms.Papers.Independent.Information100.P32 (evolution)

noncomputable section

/-- PDF p.13, Appendix A: the characteristic polynomial counts all four eigenphases
with multiplicity, for a phase-compatible decomposition. No principal-argument uniqueness
is asserted. The appendix's printed H=exp(sum ...) is corrected to H=sum ... as in (3). -/
theorem magicSpectrum (U : TwoMatrix) (b : Triple)
    (hU : PhaseCompatibleContent U b) :
    ((magicMatrix U).transpose * magicMatrix U).charpoly =
      ∏ j : Fin 4, (Polynomial.X - Polynomial.C
        (Complex.exp (-2 * Complex.I * (interactionPhases b j : ℂ)))) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P99

Source

Characterization of non-local gates, arXiv:quant-ph/0205100v3, PDF p. 13, Appendix A: spectrum determines interaction phases

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $U$ be a complex matrix on $\mathbb C^2\otimes\mathbb C^2$ , and let $b=(b_0,b_1,b_2)$ be a real triple satisfying $b_1\le b_0$ , $|b_2|\le b_1$ , and $b_0\le\pi/4$ . Let $X=\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$ , $Y=\left(\begin{smallmatrix}0&-i\\i&0\end{smallmatrix}\right)$ , and $Z=\left(\begin{smallmatrix}1&0\\0&-1\end{smallmatrix}\right)$ . Assume there exist one-qubit unitaries $A,B,C,D$ , each with determinant $1$ , such that

U=(A\otimes B)e^{-i(b_0X\otimes X+b_1Y\otimes Y+b_2Z\otimes Z)}(C\otimes D).

Define the matrix $M$ , from coordinates indexed by $0,1,2,3$ to the computational basis indexed by bit pairs, to have the following columns in order:

\frac{-i(|01\rangle+|10\rangle)}{\sqrt2},\qquad \frac{|00\rangle+|11\rangle}{\sqrt2},\qquad \frac{i(|11\rangle-|00\rangle)}{\sqrt2},\qquad \frac{|01\rangle-|10\rangle}{\sqrt2}.

Set $U_{\mathrm m}=M^\dagger UM$ and

(\lambda_0,\lambda_1,\lambda_2,\lambda_3) =(b_0+b_1-b_2,\ b_0-b_1+b_2,\ -b_0+b_1+b_2,\ -b_0-b_1-b_2).

Then the characteristic polynomial satisfies

\det\!\left(xI-U_{\mathrm m}^{\,T}U_{\mathrm m}\right) =\prod_{j=0}^{3}\left(x-e^{-2i\lambda_j}\right),

where $T$ denotes the ordinary transpose and the product includes all four factors, including repetitions when their values coincide.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph