AbsoluteTwoIncoherencePurityRefutation

Abstract

Absolute two-incoherence beyond the purity bound.

Definition 1.1 (IsAbsolutelyKIncoherent).

$$\forall (n:\mathbb{N}),\forall (k:\mathbb{N}),\forall (\mathrm{rho}:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),\mathrm{IsAbsolutelyKIncoherent}k\mathrm{rho}=((D5.S3.\mathrm{Quantum}.\mathrm{Information}.\mathrm{SLDSpectralEnergy}.\mathrm{IsDensity}\mathrm{rho})\wedge (\forall (U:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(U\in \mathrm{Matrix}.\mathrm{unitaryGroup}(\mathrm{Fin}n)\mathbb{C})\to D5.S3.\mathrm{Quantum}.\mathrm{Measurement}.\mathrm{FactorWidthTwoCone}.\mathrm{IsKIncoherentSum}k(U\cdot \mathrm{rho}\cdot \mathrm{star}(U))))$$

Formalization. D5/S3/Quantum/Measurement/AbsoluteTwoIncoherencePurityRefutation.IsAbsolutelyKIncoherent (✓ std3).

Citation. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

Definition 3, page 10: “A mixed quantum state ρ ∈ Mₙ⁺ is absolutely k-incoherent if UρU* ∈ I_{k,n} for all unitary matrices U ∈ Mₙ.” The matrix has positive semidefinite trace-one density, and every unitary conjugate is a finite sum of outer products of k-sparse vectors.

Definition 1.2 (claim).

$$\mathrm{claim}=(\forall (n:\mathbb{N}),(4\le n)\to \forall (\mathrm{rho}:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(\mathrm{IsAbsolutelyKIncoherent}2\mathrm{rho})\to (((\mathrm{rho}\cdot \mathrm{rho})).\mathrm{trace}).\mathrm{re}\le \frac{1}{((n:\mathbb{R})-1)})$$

Formalization. D5/S3/Quantum/Measurement/AbsoluteTwoIncoherencePurityRefutation.claim (✓ std3).

Citation. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

Section 5, page 17: “Theorem 7 gives a sufficient condition for absolute 2-incoherence that is also necessary in dimension n = 3. It is unclear whether or not it is necessary in dimension n = 4 or higher.” The natural number n ranges over dimensions at least four; purity is the real trace of the square.

Theorem 1.3 (result).

$$\neg (\forall (n:\mathbb{N}),(4\le n)\to \forall (\mathrm{rho}:\mathrm{Matrix}(\mathrm{Fin}n)(\mathrm{Fin}n)\mathbb{C}),(\mathrm{IsAbsolutelyKIncoherent}2\mathrm{rho})\to (((\mathrm{rho}\cdot \mathrm{rho})).\mathrm{trace}).\mathrm{re}\le \frac{1}{((n:\mathbb{R})-1)})$$

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

Resolves. Problems/jmpp-2022-absolute-two-incoherence-purity (refuted) by D5/S3/Quantum/Measurement/AbsoluteTwoIncoherencePurityRefutation.result.

Source. Repository-derived.

Acknowledgement. Nathaniel Johnston; Shirin Moein; Rajesh Pereira; Sarah Plosker (2022). Absolutely k-incoherent quantum states and spectral inequalities for factor width of a matrix. DOI: 10.1103/PhysRevA.106.052417. URL: https://arxiv.org/abs/2205.05110v2.

Commentary.

A density matrix in dimension five is absolutely two-incoherent and has purity strictly greater than one quarter. The rank of a squared-modulus Gram matrix is at most four, which separates the relevant unitary orbit from the trace-one locally positive matrices.

References

• Truth anchor: D5/S3/Quantum/Measurement/AbsoluteTwoIncoherencePurityRefutation.IsAbsolutelyKIncoherent
• Truth anchor: D5/S3/Quantum/Measurement/AbsoluteTwoIncoherencePurityRefutation.claim
• Truth anchor: D5/S3/Quantum/Measurement/AbsoluteTwoIncoherencePurityRefutation.result
• Dependency: D5/S3/Quantum/Decoherence/ProjectedUnistochasticDynamics
• Dependency: D5/S3/Quantum/Entanglement/GHZMeasureBiseparableBound
• Dependency: D5/S3/Quantum/Information/SLDSpectralEnergy
• Dependency: D5/S3/Quantum/Matrix/CartesianVariance
• Dependency: D5/S3/Quantum/Matrix/CommutatorGap
• Dependency: D5/S3/Quantum/Measurement/AntidistinguishabilityOverlapNonTight
• Dependency: D5/S3/Quantum/Measurement/FactorWidthTwoCone
• Dependency: D5/S3/Quantum/Measurement/OverlapLowRankDistance
• Dependency: D5/S3/Quantum/TensorNetworks/BridgeGraph/QuantumMaxFlowBound