Real trace fidelity and Frobenius distance

Open

QAlgorithms.Papers.Independent.Intakethird100.P39.traceFidelity_frobenius

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

prove2quantum

Let $n\ge0$ , $N=2^n$ , and let $U,V\in U(N)$ be unitary matrices in the computational basis. Define the phase-sensitive real trace fidelity by $F_{\rm tr}(U,V)=\operatorname{Re}\operatorname{tr}(V^\dagger U)/N$ . Then

F_{\rm tr}(U,V)=\frac{\operatorname{Re}\operatorname{tr}(V^\dagger U)}{N}=1-\frac{\|V-U\|_F^2}{2N},\qquad\|V-U\|_F^2=\sum_{a,b}|(V-U)_{ab}|^2.

This identity uses the Frobenius norm and retains global phase. In particular the fidelity can be negative; for $U=-V$ it is $-1$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF p.5, Eq. (14). The distance is explicitly the squared Frobenius
norm; arbitrary real trace fidelity, including -1, is allowed. -/
theorem traceFidelity_frobenius (n : ℕ)
    (U V : Matrix (Qubits n) (Qubits n) ℂ)
    (hU : U ∈ Matrix.unitaryGroup (Qubits n) ℂ)
    (hV : V ∈ Matrix.unitaryGroup (Qubits n) ℂ) :
    traceFidelity U V = (Matrix.trace (star V * U)).re / (2 : ℝ) ^ n ∧
    traceFidelity U V = 1 -
      (∑ a : Qubits n, ∑ b : Qubits n, Complex.normSq ((V - U) a b)) /
        (2 * (2 : ℝ) ^ n) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P39

Source

Quantum CISC Compilation by Optimal Control and Scalable Assembly of Complex Instruction Sets beyond Two-Qubit Gates, arXiv:0712.3227v2, PDF p. 5, Real trace fidelity and Frobenius identity, Eq. (14)

Read-back

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

For every natural number $n$ and complex unitary matrices $U,V$ indexed by $Q_n=\{0,1\}^n$ , both of the following equalities hold, where $V^\ast$ denotes conjugate transpose and $\operatorname{traceFidelity}(U,V)$ is defined as $\operatorname{Re}\operatorname{tr}(V^\ast U)/2^n$ :

\operatorname{traceFidelity}(U,V) =\frac{\operatorname{Re}\operatorname{tr}(V^\ast U)}{2^n}, \qquad \operatorname{traceFidelity}(U,V) =1-\frac{\displaystyle\sum_{a\in Q_n}\sum_{b\in Q_n}|V_{ab}-U_{ab}|^2}{2\cdot2^n}.

The case $n=0$ is included: the index set then has one element, so these are identities for $1\times1$ unitary matrices.

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