Fixed-fidelity large-dimension limits

Open

QAlgorithms.Papers.Independent.Intakethird100.P21.large_dimension_limits

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

prove2quantum

Fix any $F\in[0,1]$ . For each dimension $d\ge2$ , let $\rho_{d,F}=FP_d+(1-F)(I-P_d)/(d^2-1)$ be the isotropic density, with $P_d$ the maximally entangled projector. Its tangle $\tau$ is the convex roof of pure squared I-concurrence and its concurrence $C$ is the roof of pure I-concurrence. Then

\lim_{d\to\infty}\tau(\rho_{d,F})=2F,\qquad \lim_{d\to\infty}C(\rho_{d,F})=\sqrt2\,F.

These are limits of scalar entanglement values in changing dimensions, with fidelity fixed before the limit. Both endpoint fidelities are included; no uniform convergence rate is asserted.

Formalization Note The sequence is indexed by dimensions $d=n+2$ , removing the two nonphysical initial indices without altering the limit.

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: fixed-F dimension limits, including F=0 and F=1.
Using dimension n+2 removes the two nonphysical initial indices without
asserting a convergence rate or uniform convergence in F. -/
theorem large_dimension_limits (F : ℝ) (hF : F ∈ Set.Icc (0 : ℝ) 1) :
    Tendsto (fun n : ℕ => tangle (isotropicDensityAtFidelity (n+2) F)) atTop (nhds (2*F)) ∧
    Tendsto (fun n : ℕ => concurrence (isotropicDensityAtFidelity (n+2) F)) atTop (nhds (Real.sqrt 2 * 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: fixed-fidelity large-d limits

Read-back

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

For every fixed real $F\in[0,1]$ , including $F=0$ and $F=1$ , and every $d\ge2$ , let $\Omega_d=d^{-1/2}\sum_{i=0}^{d-1}|i,i\rangle$ , $\Phi_d=|\Omega_d\rangle\langle\Omega_d|$ , and $\rho_{d,F}=F\Phi_d+(1-F)(I-\Phi_d)/(d^2-1)$ . For a unit vector $\psi\in\mathbb C^d\otimes\mathbb C^d$ , 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 exactly $\sigma$ , using $(|\psi\rangle\langle\psi|)_{uv}=\psi(u)\overline{\psi(v)}$ ; zero weights are permitted. As the natural number $n$ tends to infinity,

T(\rho_{n+2,F})\longrightarrow 2F, \qquad C(\rho_{n+2,F})\longrightarrow \sqrt2\,F.

The sequence uses dimensions $d=n+2$ , so it starts at $d=2$ ; the convergence is asserted for each fixed $F$ .

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