Binomial and kappa states do not exhaust truncated entropy minimizers

Abstract

The loss-dephasing channel of Memarzadeh and Mancini has a qutrit input with strictly smaller output entropy than every binomial or kappa candidate at the same input energy. The channel is defined by the Kraus equations, including the infinite phase-Kraus series.

Definition 1.1 (Amplitude damping Kraus operator).

$$\forall K:\mathbb{N},\forall j:\mathrm{Fin}\left(K+1\right),\forall f:\mathbb{R},\forall r:\mathrm{Fin}\left(K+1\right),\forall c:\mathrm{Fin}\left(K+1\right),\mathrm{amplitudeKraus}\left(K,j,f\right)\left(r,c\right)=\mathrm{ite}\left(\mathrm{val}\left(r\right)+\mathrm{val}\left(j\right)=\mathrm{val}\left(c\right),\mathrm{ite}\left(\mathrm{val}\left(j\right)\le \mathrm{val}\left(c\right),\mathrm{ofReal}\left(((\mathrm{sqrt}\left(\mathrm{toReal}\left(\mathrm{choose}\left(\mathrm{val}\left(c\right),\mathrm{val}\left(j\right)\right)\right)\right))\cdot ((\mathrm{sqrt}\left(1-f\right){)}^{\mathrm{NatSub}\left(\mathrm{val}\left(c\right),\mathrm{val}\left(j\right)\right)}))\cdot ((\mathrm{sqrt}\left(f\right){)}^{\mathrm{val}\left(j\right)})\right),0\right),0\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.amplitudeKraus (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

Equation (4), pp. 1–2: indices range over Fin(K+1). val is the natural-number value of a finite index, choose is the natural binomial coefficient, toReal is the natural-to-real cast, ofReal is the real-to-complex cast, and NatSub is truncated natural subtraction. Integer powers of square roots express the half-integer powers in the source for f in [0,1].

Definition 1.2 (Phase damping Kraus operator).

$$\forall K:\mathbb{N},\forall k:\mathbb{N},\forall eta:\mathbb{R},\forall r:\mathrm{Fin}\left(K+1\right),\forall c:\mathrm{Fin}\left(K+1\right),\mathrm{phaseKraus}\left(K,k,eta\right)\left(r,c\right)=\mathrm{ite}\left(r=c,\mathrm{ofReal}\left((\mathrm{sqrt}\left(\frac{(((2)\cdot ((\mathrm{toReal}\left(\mathrm{val}\left(r\right)\right){)}^2))\cdot (eta){)}^k}{\mathrm{toReal}\left(\mathrm{factorial}\left(k\right)\right)}\right))\cdot (\exp \left(-\left(((\mathrm{toReal}\left(\mathrm{val}\left(r\right)\right){)}^2)\cdot (eta)\right)\right))\right),0\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.phaseKraus (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

Equation (5), p. 2: k is an arbitrary natural number; the phase-Kraus family remains infinite after space truncation. factorial is the natural factorial, cast to the reals before division.

Definition 1.3 (The composed loss-dephasing channel).

$$\forall K:\mathbb{N},\forall epsilon:\mathbb{R},\forall t:\mathbb{R},\forall rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(K+1\right),\mathrm{Fin}\left(K+1\right),\mathbb{C}\right),\mathrm{lossDephasingChannel}\left(K,epsilon,t,rho\right)=\sum _{j:\mathrm{Fin}\left(K+1\right)}(\sum _{k:\mathbb{N}}^{\prime }((((\mathrm{amplitudeKraus}\left(K,j,1-\exp \left(((-2)\cdot (1-epsilon))\cdot (t)\right)\right))\cdot (\mathrm{phaseKraus}\left(K,k,(epsilon)\cdot (t)\right)))\cdot (rho))\cdot (\mathrm{adjoint}\left((\mathrm{amplitudeKraus}\left(K,j,1-\exp \left(((-2)\cdot (1-epsilon))\cdot (t)\right)\right))\cdot (\mathrm{phaseKraus}\left(K,k,(epsilon)\cdot (t)\right))\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.lossDephasingChannel (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

Equation (3), p. 1, with E_jk=A_j P_k: the amplitude index j is finite after truncation, and the k sum is the infinite series. adjoint is conjugate transpose. The phase factor is obtained by summing that series, rather than assuming a matrix of output entries.

Definition 1.4 (Truncated number observable).

$$\forall K:\mathbb{N},\mathrm{numberOperator}\left(K\right)=\mathrm{diagonal}\left(\lambda i:\mathrm{Fin}\left(K+1\right),\mathrm{toComplex}\left(\mathrm{val}\left(i\right)\right)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.numberOperator (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

The truncated Fock number observable is diagonal with entries 0,…,K. toComplex is the natural-to-complex cast.

Definition 1.5 (Spectral entropy in nats).

$$\forall K:\mathbb{N},\forall rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(K+1\right),\mathrm{Fin}\left(K+1\right),\mathbb{C}\right),\mathrm{vonNeumannEntropy}\left(K,rho\right)=ifh:\mathrm{IsHermitian}\left(rho\right)then\mathrm{shannonEntropy}\left(\mathrm{eigenvalues}\left(rho,h\right)\right)else0$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.vonNeumannEntropy (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

For a Hermitian matrix, use the existing finite Shannon entropy sum of its real eigenvalues, counted with multiplicity: shannonEntropy(p)=sum_i -p_i log(p_i), with the continuous zero convention. The displayed dependent conditional binds the Hermiticity proof h in its true branch. For a non-Hermitian raw matrix the extension is zero. All outputs used below are Hermitian and positive. Natural logarithms differ from the source’s base-two entropy by a positive constant and give the same ordering.

Definition 1.6 (Fixed-energy density inputs).

$$\forall K:\mathbb{N},\forall N:\mathbb{R},\forall rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(K+1\right),\mathrm{Fin}\left(K+1\right),\mathbb{C}\right),\mathrm{admissible}\left(K,N,rho\right)\iff ((\mathrm{PosSemidef}\left(rho\right))\wedge ((\mathrm{trace}\left(rho\right)=1)\wedge (\mathrm{Re}\left(\mathrm{trace}\left((rho)\cdot (\mathrm{numberOperator}\left(K\right))\right)\right)=N)))$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.admissible (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

Equation (9), p. 2: admissible inputs are positive semidefinite matrices of trace one with number expectation N. PosSemidef is Mathlib’s matrix predicate, trace is the complex matrix trace, and Re takes its real part.

Definition 1.7 (Binomial state amplitudes).

$$\forall K:\mathbb{N},\forall M:\mathbb{N},\forall mu:\mathbb{R},\forall i:\mathrm{Fin}\left(K+1\right),\mathrm{binomialKet}\left(K,M,mu\right)\left(i\right)=\mathrm{ite}\left(\mathrm{val}\left(i\right)\le M,\mathrm{ofReal}\left(\mathrm{sqrt}\left(((\mathrm{toReal}\left(\mathrm{choose}\left(M,\mathrm{val}\left(i\right)\right)\right))\cdot ((mu{)}^{\mathrm{val}\left(i\right)}))\cdot ((1-mu{)}^{\mathrm{NatSub}\left(M,\mathrm{val}\left(i\right)\right)})\right)\right),0\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.binomialKet (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

Equation (14), p. 3: the binomial amplitudes are supported on 0,…,M. Natural subtraction M-val(i) is NatSub; the probability powers have natural exponents.

Definition 1.8 (The kappa state family).

$$\forall K:\mathbb{N},\forall N:\mathbb{R},\forall alpha:\mathbb{R},\forall i:\mathrm{Fin}\left(K+1\right),\mathrm{kappaKet}\left(K,N,alpha\right)\left(i\right)=\mathrm{ite}\left(\mathrm{val}\left(i\right)=0,\mathrm{ofReal}\left(\mathrm{sqrt}\left(1-\frac{N}{\mathrm{toReal}\left(K\right)}\right)\right),\mathrm{ite}\left(\mathrm{val}\left(i\right)=K,(\mathrm{ofReal}\left(\mathrm{sqrt}\left(\frac{N}{\mathrm{toReal}\left(K\right)}\right)\right))\cdot (\mathrm{ComplexExp}\left((\mathrm{ComplexI}\left(\right))\cdot (\mathrm{ofReal}\left((alpha)\cdot (\mathrm{toReal}\left(K\right))\right))\right)),0\right)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.kappaKet (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

Equation (11), p. 2: for K>=1 the state has support at 0 and K and relative phase exp(i alpha K). The conditional order agrees with Lean, including its extension at K=0, which the claim excludes. ComplexI is the imaginary unit; real quotients use the real cast of K.

Definition 1.9 (The two proposed optimizer families).

$$\forall K:\mathbb{N},\forall N:\mathbb{R},\forall phi:\mathrm{Fin}\left(K+1\right)\to \mathbb{C},\mathrm{candidate}\left(K,N,phi\right)\iff ((\exists M:\mathbb{N},(1\le M)\wedge ((M\le K)\wedge (\exists mu:\mathbb{R},(0\le mu)\wedge ((mu\le 1)\wedge (((\mathrm{toReal}\left(M\right))\cdot (mu)=N)\wedge (phi=\mathrm{binomialKet}\left(K,M,mu\right)))))))\vee (\exists alpha:\mathbb{R},phi=\mathrm{kappaKet}\left(K,N,alpha\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.candidate (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

The binomial candidates obey 1<=M<=K, 0<=mu<=1 and M mu=N. The other candidates are kappaKet(K,N,alpha) for any real alpha. Equality here is equality of ket functions; the conjecture tests their outer-product matrices.

Definition 1.10 (Conjecture 1).

$$claim\iff (\forall K:\mathbb{N},\forall N:\mathbb{R},\forall epsilon:\mathbb{R},\forall t:\mathbb{R},(1\le K)\Rightarrow ((0\le N)\Rightarrow ((N\le \mathrm{toReal}\left(K\right))\Rightarrow ((0\le epsilon)\Rightarrow ((epsilon\le 1)\Rightarrow ((0\le t)\Rightarrow (\exists phi:\mathrm{Fin}\left(K+1\right)\to \mathbb{C},(\mathrm{candidate}\left(K,N,phi\right))\wedge (\forall rho:\mathrm{Matrix}\left(\mathrm{Fin}\left(K+1\right),\mathrm{Fin}\left(K+1\right),\mathbb{C}\right),(\mathrm{admissible}\left(K,N,rho\right))\Rightarrow (\mathrm{vonNeumannEntropy}\left(K,\mathrm{lossDephasingChannel}\left(K,epsilon,t,\mathrm{rankOneDensity}\left(phi\right)\right)\right)\le \mathrm{vonNeumannEntropy}\left(K,\mathrm{lossDephasingChannel}\left(K,epsilon,t,rho\right)\right))))))))))$$

Formalization. D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.claim (✓ std3).

Citation. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

Conjecture 1, section IV, arXiv v1 PDF p. 4: “In a truncated Hilbert space of dimension K+1, the minimal output entropy of the quantum channel (3) is achieved either by binomial states of Eq.(14) or by states |κ_α⟩ of Eq. (11), depending on the values of ε and t.” The encoding quantifies over K>=1, N in [0,K], epsilon in [0,1] and t>=0. A candidate attains the minimum if its output entropy is no greater than the output entropy of every fixed-energy density input.

Theorem 1.11 (Two-point spreading decreases entropy).

$$\forall u:\mathbb{R},\forall v:\mathbb{R},\forall p:\mathbb{R},\forall q:\mathbb{R},(0\le u)\Rightarrow ((u<v)\Rightarrow ((u\le p)\Rightarrow ((p\le v)\Rightarrow ((p+q=u+v)\Rightarrow (Real.negMulLog\left(u\right)+Real.negMulLog\left(v\right)\le Real.negMulLog\left(p\right)+Real.negMulLog\left(q\right))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.pair_entropy_le (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

For real u, v, p and q, assume 0 <= u < v, u <= p <= v and p + q = u + v. The two inner points p and q are convex combinations of u and v with exchanged weights. Applying the concavity of Real.negMulLog to both combinations and adding gives the entropy inequality, including u = 0.

Theorem 1.12 (Qutrit refutation).

$$\neg claim$$

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

Resolves. Problems/memarzadeh-mancini-2016-truncated-loss-dephasing-optimizer-refutation (refuted) by D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.result.

Source. Repository-derived.

Acknowledgement. Laleh Memarzadeh; Stefano Mancini (2016). Minimum output entropy of a non-Gaussian quantum channel. DOI: 10.1103/PhysRevA.94.022341. URL: https://arxiv.org/abs/1605.04525v1.

Commentary.

Take K=2, N=3/2, epsilon=6/7, t=(7/2)log(2), and psi=(|1>+|2>)/sqrt(2). The only binomial candidate is M=2, mu=3/4. Every kappa phase is covered by diagonal unitary conjugation. The psi output has an eigenvalue above 1/2 and one below 1/8, whereas all eigenvalues of each candidate output lie strictly between 1/8 and 1/2. Trace-one strict majorization and strict concavity of -x log(x) give smaller entropy for psi. The defining Kraus equations give the kappa output’s off-diagonal coefficient sqrt(3)/32768; the displayed section-III coefficient in the source differs from those equations. The result excludes these candidate families as minimizers; it does not assert global optimality of psi. The proof applies the exponential-series, positive-definiteness and strict-concavity results to the displayed instance.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.admissible
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.amplitudeKraus
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.binomialKet
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.candidate
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.claim
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.kappaKet
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.lossDephasingChannel
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.numberOperator
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.pair_entropy_le
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.phaseKraus
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.result
• Truth anchor: D5/S3/Quantum/QuantumChannels/TruncatedLossDephasingOptimizerRefutation.vonNeumannEntropy
• Dependency: D5/S3/Entropy/MaxEntropy
• Dependency: D5/S3/Quantum/PureState/PureStateHandshake