Two-qutrit formulas, tangent point and optimal component types

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.two_qutrits

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

prove2quantum

For two qutrits and $F\in[0,1]$ , let $\rho_{3,F}=FP_3+(1-F)(I-P_3)/8$ , and let $q_3$ be the raw constrained Schmidt-tangle profile. Then

\tau(\rho_{3,F})=\begin{cases}0&F\le1/3,\\q_3(F)&1/3<F\le8/9,\\3(F-1)+4/3&8/9<F\le1,\end{cases} \quad C(\rho_{3,F})=\begin{cases}0&F\le1/3,\\\sqrt3(F-1/3)&1/3<F\le1.\end{cases}

Moreover $q_3(8/9)=1$ and $q_3'(8/9)=3$ . The equation $q_3'(x)=(4/3-q_3(x))/(1-x)$ has exactly the solution $x=8/9$ on $(1/3,1)$ . An attaining tangle ensemble can have common pure tangle $\tau(\rho_{3,F})$ for $F\le8/9$ , and pure tangles only in $\{1,4/3\}$ above $8/9$ . An attaining concurrence ensemble can use only normalized product or maximally entangled states. These restrictions concern positive-weight members and do not require both types at an endpoint.

This explicit worked dimension illustrates the general tangent construction.

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 pp.10--11, (3.38)--(3.39): explicit qutrit formulas, tangent data,
and attaining ensembles. Sqrt(3) multiplies the full displacement.
Zero-weight components are unrestricted; at F=1 no product component is required. -/
theorem two_qutrits (F : ℝ) (hF : F ∈ Set.Icc (0 : ℝ) 1) :
    tangle (isotropicDensityAtFidelity 3 F) =
      (if F ≤ 1/3 then 0 else if F ≤ 8/9 then explicitQ 3 F else 3*(F-1)+4/3) ∧
    concurrence (isotropicDensityAtFidelity 3 F) = (if F ≤ 1/3 then 0 else Real.sqrt 3 * (F-1/3)) ∧
    explicitQ 3 (8/9) = 1 ∧ deriv (explicitQ 3) (8/9) = 3 ∧
    (∀ x ∈ Set.Ioo (1/3 : ℝ) 1,
      (deriv (explicitQ 3) x = (4/3 - explicitQ 3 x) / (1-x) ↔ x = 8/9)) ∧
    (∃ e : PureEnsemble (Fin 3 × Fin 3), IsOptimalPureEnsemble pureTangle (isotropicDensityAtFidelity 3 F) e ∧
      ∀ k, 0 < e.weight k →
        if F ≤ 8/9 then pureTangle (e.vector k) = tangle (isotropicDensityAtFidelity 3 F)
        else pureTangle (e.vector k) = 1 ∨ pureTangle (e.vector k) = 4/3) ∧
    (∃ e : PureEnsemble (Fin 3 × Fin 3), IsOptimalPureEnsemble pureConcurrence (isotropicDensityAtFidelity 3 F) e ∧
      ∀ k, 0 < e.weight k → IsPureProductState (e.vector k) ∨ IsMaximallyEntangled (e.vector k)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 11, §3.4.2, (3.38)–(3.39): two-qutrit formulas and tangent point

Read-back

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

For every real $F\in[0,1]$ , let $\Omega_3=3^{-1/2}\sum_{i=0}^2|i,i\rangle$ , $\Phi_3=|\Omega_3\rangle\langle\Omega_3|$ , and $\rho_F=F\Phi_3+(1-F)(I-\Phi_3)/8$ . For a unit vector $\psi$ , put $(A_\psi)_{ij}=\sum_b\psi(i,b)\overline{\psi(j,b)}$ , $\tau(\psi)=2(1-\operatorname{Re}\operatorname{tr}(A_\psi^2))$ , and $c(\psi)=\sqrt{\tau(\psi)}$ ; let $T(\sigma)$ and $C(\sigma)$ be the infima of the respective average costs over finite ensembles of unit vectors with nonnegative weights summing to $1$ and average matrix $\sigma$ , using $(|\psi\rangle\langle\psi|)_{uv}=\psi(u)\overline{\psi(v)}$ . Define $a(t)=\sqrt{t/3}+\sqrt{2(1-t)/3}$ , $b(t)=\sqrt{t/3}-\sqrt{(1-t)/6}$ , and $Q(t)=2(1-a(t)^4-2b(t)^4)$ . Then

T(\rho_F)= \begin{cases} 0&F\le\tfrac13,\\ Q(F)&\tfrac13<F\le\tfrac89,\\ 3(F-1)+\tfrac43&F>\tfrac89, \end{cases} \qquad C(\rho_F)= \begin{cases} 0&F\le\tfrac13,\\ \sqrt3(F-\tfrac13)&F>\tfrac13. \end{cases}

Furthermore, $Q(8/9)=1$ , $Q'(8/9)=3$ , and, for every $x\in(1/3,1)$ , $Q'(x)=(4/3-Q(x))/(1-x)$ if and only if $x=8/9$ . There exists a finite ensemble attaining $T(\rho_F)$ such that every positive-weight component has $\tau$ -cost $T(\rho_F)$ when $F\le8/9$ , and has $\tau$ -cost either $1$ or $4/3$ when $F>8/9$ . Separately, there exists a finite ensemble attaining $C(\rho_F)$ such that every positive-weight component is either a tensor product of two unit vectors or a vector $3^{-1/2}\sum_{i=0}^2u_i\otimes v_i$ for orthonormal families $(u_i)$ and $(v_i)$ in $\mathbb C^3$ . Each attaining ensemble has average matrix exactly $\rho_F$ ; zero-weight components are unrestricted by the stated component conditions.

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