Noisy entanglement curvature can exceed quantum Fisher information

Abstract

A two-qubit amplitude-damped probe starting at diag(1,11,3,1)/16 has smooth concurrence curvature 1 and quantum Fisher information 8/15 at t=1, kappa=log 2 and g=pi/4.

Definition 1.1 (First amplitude-damping jump).

$$jump1=\mathrm{kroneckerMap}\left(\mathrm{fun}x:\mathbb{C}\mapsto \mathrm{fun}y:\mathbb{C}\mapsto x\cdot y,sigmaMinus,(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))\right)$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.jump1 (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Equation (41), p. 8, and Appendix B use the jump operators σ₋ on the two qubits, with σ₋ = (σx − iσy)/2. The computational basis is |ij⟩ indexed by (i,j) in Fin 2 × Fin 2. The reused sigmaMinus is the matrix [[0,0],[1,0]], so this is σ₋ ⊗ I.

Definition 1.2 (Second amplitude-damping jump).

$$jump2=\mathrm{kroneckerMap}\left(\mathrm{fun}x:\mathbb{C}\mapsto \mathrm{fun}y:\mathbb{C}\mapsto x\cdot y,(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),sigmaMinus\right)$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.jump2 (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Equation (41), p. 8: the second jump is I ⊗ σ₋. Both identity matrices are complex two-by-two matrices.

Definition 1.3 (Flip-flop Hamiltonian).

$$\forall g:\mathbb{R},\mathrm{hamiltonian}\left(g\right)=\mathrm{fun}a:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\mapsto \mathrm{fun}b:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\mapsto \mathrm{if}((a=(0,1))\wedge (b=(1,0)))\vee ((a=(1,0))\wedge (b=(0,1)))\mathrm{then}(\mathrm{val}\left(g\right):\mathbb{C})\mathrm{else}0$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.hamiltonian (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Equation (21), p. 4, specialized to etaXY=1: Hprobe = g(σ₋⁽¹⁾σ₊⁽²⁾ + σ₊⁽¹⁾σ₋⁽²⁾). Its only nonzero entries are g at (01,10) and (10,01). The complex cast of g is displayed explicitly.

Definition 1.4 (Lindblad dissipator).

$$\forall O:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall rho:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{dissipator}\left(O,rho\right)=O\cdot rho\cdot \mathrm{Matrix}.\mathrm{conjTranspose}\left(O\right)-\mathrm{SMul}.\mathrm{smul}\left((\frac{1}{2}:\mathbb{C}),\mathrm{Matrix}.\mathrm{conjTranspose}\left(O\right)\cdot O\cdot rho+rho\cdot (\mathrm{Matrix}.\mathrm{conjTranspose}\left(O\right)\cdot O)\right)$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.dissipator (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Equation (41), p. 8, defines D[O](rho) = O rho O† − (O† O rho + rho O† O)/2. conjTranspose is the matrix adjoint; the factor 1/2 is a complex scalar acting by smul.

Definition 1.5 (Open evolution generator).

$$\forall g:\mathbb{R},\forall kappa:\mathbb{R},\forall rho:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{generator}\left(g,kappa,rho\right)=\mathrm{SMul}.\mathrm{smul}\left(-I,\mathrm{hamiltonian}\left(g\right)\cdot rho-rho\cdot \mathrm{hamiltonian}\left(g\right)\right)+\mathrm{SMul}.\mathrm{smul}\left((\mathrm{val}\left(kappa\right):\mathbb{C}),\mathrm{dissipator}\left(jump1,rho\right)+\mathrm{dissipator}\left(jump2,rho\right)\right)$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.generator (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Equation (41), p. 8: the commutator term is −i[Hprobe,rho], and the two amplitude-damping dissipators each have rate kappa. The rate is cast to the complex numbers before scalar multiplication.

Definition 1.6 (Solutions of the initial-value problem).

$$\forall rhoZero:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall kappa:\mathbb{R},\forall rho:\mathbb{R}\to \mathbb{R}\to \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{IsTrajectory}\left(rhoZero,kappa,rho\right)\iff ((\forall g:\mathbb{R},rho\left(g,0\right)=rhoZero)\wedge (\forall g:\mathbb{R},\forall t:\mathbb{R},\forall a:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\forall b:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathrm{HasDerivAt}\left(\mathrm{fun}s:\mathbb{R}\mapsto rho\left(g,s,a,b\right),\mathrm{generator}\left(g,kappa,rho\left(g,t\right)\right)\left(a,b\right),t\right)))$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.IsTrajectory (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Equation (41), p. 8, with initial state rhoZero independent of g. Every matrix entry has the stated time derivative, for every real g and t. HasDerivAt is the real-variable derivative with complex values.

Definition 1.7 (Spin-flip matrix).

$$sigmaYY=\mathrm{kroneckerMap}\left(\mathrm{fun}x:\mathbb{C}\mapsto \mathrm{fun}y:\mathbb{C}\mapsto x\cdot y,(!![0,-I;I,0]:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),(!![0,-I;I,0]:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))\right)$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.sigmaYY (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Section II, p. 3, uses σy ⊗ σy in the spin-flip product. Here σy is the complex matrix [[0,−i],[i,0]].

Definition 1.8 (Wootters concurrence).

$$\forall rho:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{concurrence}\left(rho\right)=\mathrm{let}l=((((rho\cdot sigmaYY\cdot (rho).\mathrm{map}\left(star\right)\cdot sigmaYY).\mathrm{charpoly}).\mathrm{roots}).\mathrm{map}\left(\mathrm{fun}z:\mathbb{C}\mapsto \mathrm{Real}.\mathrm{sqrt}\left((z).\mathrm{re}\right)\right)).\mathrm{sort}\left(\mathrm{fun}x:\mathbb{R}\mapsto \mathrm{fun}y:\mathbb{R}\mapsto y\le x\right);\max \left(0,(l).\mathrm{getD}\left(0,0\right)-(l).\mathrm{getD}\left(1,0\right)-(l).\mathrm{getD}\left(2,0\right)-(l).\mathrm{getD}\left(3,0\right)\right)$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.concurrence (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Section II, p. 3: ‘the λi are the square roots of the eigenvalues, in decreasing order, of the matrix R = ρ(σy ⊗ σy)ρ∗(σy ⊗ σy).’ The concurrence formula takes max(0,λ1−λ2−λ3−λ4). The characteristic-polynomial roots retain algebraic multiplicity; map applies sqrt to each real part, then sort orders the resulting real multiset decreasingly. List.getD uses zero-based indices and default zero. The star in Matrix.map conjugates each entry, without transposing.

Definition 1.9 (Derivative with respect to the coupling).

$$\forall rho:\mathbb{R}\to \mathbb{R}\to \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall g:\mathbb{R},\forall t:\mathbb{R},\mathrm{derivG}\left(rho,g,t\right)=\mathrm{Matrix}.\mathrm{of}\left(\mathrm{fun}a:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\mapsto \mathrm{fun}b:(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right))\mapsto \mathrm{deriv}\left(\mathrm{fun}h:\mathbb{R}\mapsto rho\left(h,t,a,b\right),g\right)\right)$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.derivG (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Section II, equation (7), p. 3: ‘we define the curvature of entanglement (CoE) as’ CoE ≡ −∂g² C(rho). The matrix derivative here differentiates each entry in g at fixed t; Matrix.of constructs the matrix with those entries.

Definition 1.10 (Symmetric logarithmic derivative).

$$\forall rho:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall dRho:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall L:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\mathrm{IsSLD}\left(rho,dRho,L\right)\iff ((\mathrm{Matrix}.\mathrm{IsHermitian}\left(L\right))\wedge (dRho=\mathrm{SMul}.\mathrm{smul}\left((\frac{1}{2}:\mathbb{C}),rho\cdot L+L\cdot rho\right)))$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.IsSLD (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Section II, p. 2: the Hermitian SLD L satisfies dRho=(rho L+L rho)/2, and QFI=Tr(rho L²). The displayed predicate includes both Hermiticity and the SLD equation.

Definition 1.11 (The noisy curvature conjecture).

$$claim\iff (\forall rhoZero:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall kappa:\mathbb{R},\forall t:\mathbb{R},\forall rho:\mathbb{R}\to \mathbb{R}\to \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{IsDensity}\left(rhoZero\right))\Rightarrow \left((0<kappa)\Rightarrow \left((0<t)\Rightarrow \left((\mathrm{IsTrajectory}\left(rhoZero,kappa,rho\right))\Rightarrow \forall g:\mathbb{R},(\mathrm{ContDiffAt}\left(\mathbb{R},2,\mathrm{fun}h:\mathbb{R}\mapsto \mathrm{concurrence}\left(rho\left(h,t\right)\right),g\right))\Rightarrow \forall L:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{IsSLD}\left(rho\left(g,t\right),\mathrm{derivG}\left(rho,g,t\right),L\right))\Rightarrow -(\mathrm{deriv}\left(\mathrm{deriv}\left(\mathrm{fun}h:\mathbb{R}\mapsto \mathrm{concurrence}\left(rho\left(h,t\right)\right)\right),g\right))\le ((rho\left(g,t\right)\cdot L\cdot L).\mathrm{trace}).\mathrm{re}\right)\right)\right))$$

Formalization. D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.claim (✓ std3).

Citation. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Section IV.B, p. 9: ‘For the case with decay also there are more general examples we can consider but in all cases we conjecture that CoE ≤ QFI with equality at specific points.’ Encoding: rhoZero is any density matrix, kappa and t are positive real numbers, and rho solves (41) with that initial state. At every g where the concurrence is twice continuously differentiable, the negative second derivative is at most the real part of Tr(rho L²), for every Hermitian SLD L. IsDensity is the reused predicate PosSemidef and trace one. Matrix indices are pairs, with the first coordinate the first qubit. The twice-continuously-differentiable condition restricts the comparison to smooth points.

Theorem 1.12 (Refutation at positive damping).

$$\neg (\forall rhoZero:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),\forall kappa:\mathbb{R},\forall t:\mathbb{R},\forall rho:\mathbb{R}\to \mathbb{R}\to \mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{IsDensity}\left(rhoZero\right))\Rightarrow \left((0<kappa)\Rightarrow \left((0<t)\Rightarrow \left((\mathrm{IsTrajectory}\left(rhoZero,kappa,rho\right))\Rightarrow \forall g:\mathbb{R},(\mathrm{ContDiffAt}\left(\mathbb{R},2,\mathrm{fun}h:\mathbb{R}\mapsto \mathrm{concurrence}\left(rho\left(h,t\right)\right),g\right))\Rightarrow \forall L:\mathrm{Matrix}\left((\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),(\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)),\mathbb{C}\right),(\mathrm{IsSLD}\left(rho\left(g,t\right),\mathrm{derivG}\left(rho,g,t\right),L\right))\Rightarrow -(\mathrm{deriv}\left(\mathrm{deriv}\left(\mathrm{fun}h:\mathbb{R}\mapsto \mathrm{concurrence}\left(rho\left(h,t\right)\right)\right),g\right))\le ((rho\left(g,t\right)\cdot L\cdot L).\mathrm{trace}).\mathrm{re}\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.result (✓ std3). ∎

Resolves. Problems/saleem-et-al-2025-noisy-curvature-of-entanglement (refuted) by D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.result.

Source. Repository-derived.

Acknowledgement. Zain H. Saleem; Anil Shaji; Anjala M. Babu; Da-Wei Luo; Quinn Langfitt; Ting Yu; Stephen K. Gray (2025). Quantum Fisher Information and the Curvature of Entanglement. DOI: 10.48550/arXiv.2504.13729. URL: https://arxiv.org/abs/2504.13729.

Commentary.

Take rhoZero=diag(1,11,3,1)/16, kappa=log 2 and t=1. At g=pi/4 the evolved state is [[1,0,0,0],[0,15,8i,0],[0,−8i,15,0],[0,0,0,33]]/64. Its spin-flip spectrum is {529,49,33,33}/4096. Near that point its concurrence equals sin(2g)/4−sqrt(33)/32, hence its curvature is 1. The Hermitian matrix L=diag(0,−16/15,16/15,0) satisfies the SLD equation and gives QFI=8/15. The conjectured inequality would require 1≤8/15.

References

• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.IsSLD
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.IsTrajectory
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.claim
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.concurrence
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.derivG
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.dissipator
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.generator
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.hamiltonian
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.jump1
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.jump2
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.result
• Truth anchor: D5/S3/Quantum/Information/SaleemNoisyCurvatureRefutation.sigmaYY
• Dependency: D5/S3/Quantum/Dynamics/PronkoFredkinNonCyclicAnnihilation
• Dependency: D5/S3/Quantum/Entanglement/StructuredNegativityCoincidenceRefutation