Exact constrained Schmidt minimum and an attaining probability vector

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.fixed_fidelity_minimum

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

prove2quantum

Let $d\ge2$ and $F\in[1/d,1]$ . Consider all $d$ nonnegative Schmidt probabilities $\mu_k$ summing to one with $\sum_k\sqrt{\mu_k}=\sqrt{dF}$ . Define

\gamma=\sqrt{F/d}+\sqrt{(d-1)(1-F)/d},\qquad \delta=\sqrt{F/d}-\sqrt{(1-F)/(d(d-1))}.

The constrained pure-tangle minimum is

q_d(F)=\min_{\mu}\,2\Bigl(1-\sum_k\mu_k^2\Bigr) =2\bigl(1-\gamma^4-(d-1)\delta^4\bigr).

It is attained by the feasible vector $(\gamma^2,\delta^2,\ldots,\delta^2)$ . Zero probabilities at $F=1/d$ and uniform probabilities at $F=1$ are included.

This gives the exact raw profile whose convex envelope yields isotropic tangle.

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.8--9, (3.30)--(3.32): exact attained constrained Schmidt minimum,
including zero Schmidt probabilities at F=1/d and the equal endpoint F=1. -/
theorem fixed_fidelity_minimum (d : ℕ) (hd : 2 ≤ d) (F : ℝ)
    (hF : F ∈ Set.Icc (1 / (d : ℝ)) 1) :
    constrainedSchmidtTangle d F = explicitQ d F ∧
    IsLeast (profileValues d F) (explicitQ d F) ∧
    (∃ mu : SchmidtProbabilities d,
      mu.probability = minimizingProbabilities d F ∧
      (∑ k, Real.sqrt (mu.probability k)) = Real.sqrt ((d : ℝ) * F) ∧
      schmidtCost mu.probability = explicitQ 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. 9, §3.3, (3.30)–(3.32): exact constrained Schmidt minimum

Read-back

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

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

a_d(F)=\sqrt{\frac Fd}+\sqrt{\frac{(d-1)(1-F)}d}, \qquad b_d(F)=\sqrt{\frac Fd}-\sqrt{\frac{1-F}{d(d-1)}}, \qquad Q_d(F)=2\bigl(1-a_d(F)^4-(d-1)b_d(F)^4\bigr).

Let $V_d(F)$ be the set of numbers $2(1-\sum_{i=0}^{d-1}\mu_i^2)$ obtained from real vectors satisfying $\mu_i\ge0$ , $\sum_i\mu_i=1$ , and $\sum_i\sqrt{\mu_i}=\sqrt{dF}$ , and let $P_d(F)=\inf V_d(F)$ . Then $P_d(F)=Q_d(F)$ , and $Q_d(F)$ belongs to $V_d(F)$ and is no larger than every other member of that set. In particular, there exists such a probability vector with $\mu_0=a_d(F)^2$ and $\mu_i=b_d(F)^2$ for every $i\ne0$ ; it satisfies the square-root-sum constraint and has cost $2(1-\sum_i\mu_i^2)=Q_d(F)$ . Zero coordinates are allowed, and the assertions include both endpoints $F=1/d$ and $F=1$ ; no uniqueness of a minimizing probability vector is asserted.

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