Exact tangle and I-concurrence of two-qudit isotropic states

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.isotropic_exact

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

prove2quantum

Let $d\ge3$ be an integer and $0\le F\le1$ . Put $\Phi_d=d^{-1/2}\sum_{j=1}^d|j,j\rangle$ , $P_d=|\Phi_d\rangle\langle\Phi_d|$ , and $\rho_{d,F}=FP_d+(1-F)(I-P_d)/(d^2-1)$ . Let $C$ be the convex roof of pure I-concurrence $\sqrt{2(1-\operatorname{tr}\rho_A^2)}$ , and let $\tau$ be the separate convex roof of its square. Define $a_d=4(d-1)/d^2$ , $\gamma=\sqrt{F/d}+\sqrt{(d-1)(1-F)/d}$ , $\delta=\sqrt{F/d}-\sqrt{(1-F)/(d(d-1))}$ , and $q_d(F)=2(1-\gamma^4-(d-1)\delta^4)$ . Then $\rho_{d,F}$ is a density operator and

\tau(\rho_{d,F})=\begin{cases}0&F\le1/d,\\q_d(F)&1/d<F\le a_d,\\\dfrac{2d(F-1)}{d-1}+\dfrac{2(d-1)}d&a_d<F\le1,\end{cases} \qquad C(\rho_{d,F})=\begin{cases}0&F\le1/d,\\\sqrt{\dfrac{2d}{d-1}}(F-1/d)&1/d<F\le1.\end{cases}

These are exact mixed-state entanglement formulas; in general the tangle is not the square of mixed-state concurrence.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P21

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P21

open scoped Matrix ComplexConjugate

open Filter

open QAlgorithms

open QAlgorithms.Papers.Independent.Information100.P03
  (PureEnsemble convexRoof pureConcurrence concurrence SchmidtData schmidtVector)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.13, (3.41)--(3.42), inheriting d>=3 from p.12:
exact mixed-state tangle and I-concurrence, over the full physical F interval. -/
theorem isotropic_exact (d : ℕ) (hd : 3 ≤ d) (F : ℝ) (hF : F ∈ Set.Icc (0 : ℝ) 1) :
    IsDensityMatrix (isotropicDensityAtFidelity d F) ∧
    tangle (isotropicDensityAtFidelity d F) = tangleFormula d F ∧
    concurrence (isotropicDensityAtFidelity d F) = concurrenceFormula d F := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 13, §3.4.3, (3.41)–(3.42): exact tangle and I-concurrence of two-qudit isotropic states

Read-back

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

For every natural number $d\ge3$ and every real $F\in[0,1]$ , let

\Phi_d=\frac1{\sqrt d}\sum_{i<d}|i,i\rangle,\qquad \rho_F=F|\Phi_d\rangle\langle\Phi_d| +\frac{1-F}{d^2-1}\bigl(I-|\Phi_d\rangle\langle\Phi_d|\bigr).

For a vector $\psi$ , put $A_\psi=\operatorname{Tr}_2(|\psi\rangle\langle\psi|)$ , $T_0(\psi)=2(1-\operatorname{Re}\operatorname{tr}(A_\psi^2))$ , and $C_0(\psi)=\sqrt{T_0(\psi)}$ ; define $T(\rho)$ and $C(\rho)$ as the respective infima of $\sum_kw_kT_0(\psi_k)$ and $\sum_kw_kC_0(\psi_k)$ over all finite decompositions $\rho=\sum_kw_k|\psi_k\rangle\langle\psi_k|$ into unit vectors with nonnegative weights summing to $1$ . Then $\rho_F$ is positive semidefinite with trace $1$ , and, writing

F_*=\frac{4(d-1)}{d^2},\qquad u=\sqrt{\frac Fd}+\sqrt{\frac{(d-1)(1-F)}d},\qquad v=\sqrt{\frac Fd}-\sqrt{\frac{1-F}{d(d-1)}},

its two infima satisfy

T(\rho_F)= \begin{cases} 0,&F\le1/d,\\ 2(1-u^4-(d-1)v^4),&1/d<F\le F_*,\\ \dfrac{2d(F-1)}{d-1}+\dfrac{2(d-1)}d,&F>1/d,\ F>F_*, \end{cases} \qquad C(\rho_F)= \begin{cases} 0,&F\le1/d,\\ \sqrt{\dfrac{2d}{d-1}}(F-1/d),&F>1/d. \end{cases}

The endpoints $F=0,1,1/d$ , and $F_*$ are included according to the displayed non-strict inequalities.

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