Pure tangle: Schmidt formula, local invariance and range

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.pure_state_properties

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

prove2quantum

Let $d_A,d_B>0$ , $r=\min(d_A,d_B)$ , and let $\psi$ be a normalized bipartite pure state. Schmidt probabilities $\mu_j\ge0$ satisfy $\sum_j\mu_j=1$ and enter its Schmidt expansion as amplitudes $\sqrt{\mu_j}$ in orthonormal local families. With $C$ the I-concurrence roof, $\tau$ the pure-tangle roof, and $T(\psi)=2(1-\operatorname{tr}\rho_A^2)$ for $\rho_A=\operatorname{Tr}_B|\psi\rangle\langle\psi|$ ,

\tau(|\psi\rangle\langle\psi|)=C(\psi)^2=T(\psi)=2\Bigl(1-\sum_j\mu_j^2\Bigr)=4\sum_{j<k}\mu_j\mu_k, \qquad 0\le T(\psi)\le\frac{2(r-1)}r.

The concurrence roof also agrees with pure concurrence on the pure projector. The pure tangle is smooth on normalized vectors and invariant under arbitrary local unitaries. It is zero exactly on normalized product states, and reaches its upper endpoint exactly on states with all $r$ Schmidt probabilities equal to $1/r$ . For $r=1$ the two endpoints coincide at zero.

This identifies the pure cost underlying the two distinct convex roofs.

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.4, (2.2): Schmidt formula, smoothness, local-unitary invariance,
pure-roof agreement, range, and its product/maximally-entangled endpoints.
The min(dA,dB)=1 case is retained. -/
theorem pure_state_properties (a b : ℕ) (ha : 0 < a) (hb : 0 < b) :
    ContDiffOn ℝ ⊤ (pureTangle (I := Fin a) (J := Fin b)) {psi | IsState psi} ∧
    (∀ s : SchmidtData a b,
      IsState (schmidtVector s) ∧
      pureTangle (schmidtVector s) = schmidtCost s.probability ∧
      schmidtCost s.probability =
        4 * ∑ i, ∑ j, (if i < j then s.probability i * s.probability j else 0)) ∧
    (∀ psi : EuclideanSpace ℂ (Fin a × Fin b), IsState psi →
      tangle (pureDensity psi) = pureTangle psi ∧
      concurrence (pureDensity psi) = pureConcurrence psi ∧
      pureConcurrence psi ^ 2 = pureTangle psi ∧
      0 ≤ pureTangle psi ∧ pureTangle psi ≤ 2 * ((min a b : ℝ) - 1) / min a b ∧
      (pureTangle psi = 0 ↔ IsPureProductState psi) ∧
      (pureTangle psi = 2 * ((min a b : ℝ) - 1) / min a b ↔ IsMaximallyEntangled psi) ∧
      ∀ U : Matrix.unitaryGroup (Fin a) ℂ, ∀ V : Matrix.unitaryGroup (Fin b) ℂ,
        pureTangle (act (Matrix.kronecker (U : Matrix (Fin a) (Fin a) ℂ)
          (V : Matrix (Fin b) (Fin b) ℂ)) psi) = pureTangle psi) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P21

end

Source

I-concurrence and tangle for isotropic states, arXiv:quant-ph/0208002v1, PDF p. 4, §2, (2.2): Schmidt expression, local-unitary invariance and range of pure tangle

Read-back

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

For every pair of positive natural numbers $a,b$ , write $r=\min(a,b)$ , $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)}$ ; let $T$ and $C$ be the infima of the respective weighted pure-vector costs over finite unit-vector decompositions with nonnegative weights summing to $1$ . The function $T_0$ is infinitely differentiable over $\mathbb R$ on the set of unit vectors, in the sense of differentiability within that set. For every collection of probabilities $\mu_i\ge0$ , $i<r$ , summing to $1$ , and orthonormal families $u_i\in\mathbb C^a$ , $v_i\in\mathbb C^b$ , the vector $\psi=\sum_{i<r}\sqrt{\mu_i}\,u_i\otimes v_i$ has norm $1$ and satisfies

T_0(\psi)=2\left(1-\sum_{i<r}\mu_i^2\right) =4\sum_{i<j<r}\mu_i\mu_j.

For every unit vector $\psi\in\mathbb C^a\otimes\mathbb C^b$ ,

T(|\psi\rangle\langle\psi|)=T_0(\psi),\qquad C(|\psi\rangle\langle\psi|)=C_0(\psi),\qquad C_0(\psi)^2=T_0(\psi),\qquad 0\le T_0(\psi)\le\frac{2(r-1)}r.

Moreover, $T_0(\psi)=0$ if and only if $\psi=u\otimes v$ for unit vectors $u,v$ ; equality with the upper bound holds if and only if $\psi$ has a decomposition of the displayed orthonormal form with every $\mu_i=1/r$ . Finally, $T_0((U\otimes V)\psi)=T_0(\psi)$ for every unitary $U$ on $\mathbb C^a$ and every unitary $V$ on $\mathbb C^b$ . Dimensions equal to $1$ are included; when $r=1$ , the upper bound is zero and the sum over $i<j$ is empty.

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