Concurrence and tangle are faithful selective LOCC monotones

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.entanglement_monotones

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

prove2quantum

Across all positive finite local dimensions, let $C$ be the convex roof of normalized pure I-concurrence and let $\tau$ be the convex roof of pure tangle. For either $E\in\{C,\tau\}$ and every bipartite density operator $\rho$ , $E(\rho)\ge0$ . For every complete local Kraus instrument on either party, including rectangular instruments that change its dimension, let $p_i$ and $\rho_i$ be the outcome probabilities and normalized posterior states. Then

\sum_i p_i E(\rho_i)\le E(\rho), \qquad E(\rho)=0\ \Longleftrightarrow\ \rho\text{ is separable}.

A zero-probability outcome contributes zero without evaluating a cost on a normalized zero state. Both measures are invariant under local unitary conjugation. The local selective inequalities, together with density convexity, iterate through finite adaptive LOCC, including local pure ancillas and disposal.

These properties make both roofs faithful entanglement monotones in the source's finite-dimensional setting.

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.5, Section 2: nonnegative selective local-instrument monotonicity
on all finite positive local dimensions, and vanishing exactly on separable states.
Together with convexity below these inequalities iterate through adaptive LOCC. -/
theorem entanglement_monotones :
    Frontier30.P30.IsLOCCMonotone (fun _ _ rho => tangle rho) ∧
    Frontier30.P30.IsLOCCMonotone (fun _ _ rho => concurrence rho) ∧
    ∀ a b : ℕ, ∀ ha : 0 < a, ∀ hb : 0 < b,
      ∀ rho : Matrix (Fin a × Fin b) (Fin a × Fin b) ℂ, IsDensityMatrix rho →
        letI : Nonempty (Fin a) := ⟨⟨0, ha⟩⟩
        letI : Nonempty (Fin b) := ⟨⟨0, hb⟩⟩
        (tangle rho = 0 ↔ Entanglement.IsSeparableDensity rho) ∧
        (concurrence rho = 0 ↔ Entanglement.IsSeparableDensity rho) ∧
        ∀ U : Matrix.unitaryGroup (Fin a) ℂ, ∀ V : Matrix.unitaryGroup (Fin b) ℂ,
          let L := Matrix.kronecker (U : Matrix (Fin a) (Fin a) ℂ)
            (V : Matrix (Fin b) (Fin b) ℂ)
          tangle (L * rho * Lᴴ) = tangle rho ∧
          concurrence (L * rho * Lᴴ) = concurrence rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 5, §2: concurrence and tangle are faithful entanglement monotones

Read-back

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

For a bipartite unit vector $\psi$ , define $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 infima of their weighted averages over finite decompositions of $\rho$ into unit-vector projectors, with nonnegative weights summing to $1$ . Both functions are nonnegative on every density matrix in every pair of positive finite dimensions, and both satisfy the following two local-operation inequalities: for arbitrary positive dimensions $a,b,h$ , arbitrary natural $k$ , matrices $K_i:\mathbb C^a\to\mathbb C^h$ with $\sum_{i<k}K_i^\dagger K_i=I_a$ , and a density matrix $\rho$ on $\mathbb C^a\otimes\mathbb C^b$ , let $X_i=(K_i\otimes I_b)\rho(K_i\otimes I_b)^\dagger$ and $p_i=\operatorname{Re}\operatorname{tr}X_i$ ; then

\sum_{i<k} \begin{cases} p_iE_{h,b}(X_i/p_i),&p_i>0,\\ 0,&p_i\le0 \end{cases} \le E_{a,b}(\rho) \quad\text{for each }E\in\{T,C\},

and the corresponding inequality holds for matrices $K_i:\mathbb C^b\to\mathbb C^h$ , branches $X_i=(I_a\otimes K_i)\rho(I_a\otimes K_i)^\dagger$ , and output dimensions $a,h$ . The quantification includes $k=0$ , although its completeness equation cannot hold for positive input dimension. Furthermore, for every positive $a,b$ and every density matrix $\rho$ , $T(\rho)=0$ if and only if $\rho$ is a finite convex combination of products of density matrices, and the same equivalence holds for $C(\rho)=0$ . For every pair of local unitaries $U,V$ , writing $L=U\otimes V$ , one has $T(L\rho L^\dagger)=T(\rho)$ and $C(L\rho L^\dagger)=C(\rho)$ .

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