Commuting Qubit Midpoint Contraction

Abstract

Commuting qubit density inputs contract generalized Bures distance at the scalar midpoint reference.

All matrices are complex. A density matrix is positive semidefinite with trace one. The root-fidelity definition and weighted-root norm identity allow any finite decidable index type; the remaining results concern two-by-two matrices. Every square root is the positive functional-calculus root; F is the ordered generalized fidelity, B(R,P,Q)=Re tr(P+Q)-2 Re F(R,P,Q), and the distance is sqrt(B). Only P and Q commute in the channel theorem. Their outputs can have arbitrary complex coherence. The transported reference must be positive definite.

Ma, Rajaei and Zhang, Generalized Fidelity, the Data Processing Inequality, and Convexity, arXiv:2609.09753v3, give the ordered-root quotient, Pauli and Bloch identities, the weighted-root norm formula and scalar sufficient criteria. Their unrestricted-DPI counterexample supersedes the unresolved unrestricted question in v1. Afham and Ferrie, arXiv:2410.04937v2, supply the generalized-fidelity and squared-Bures conventions and transported-reference question. Vuong, arXiv:2605.28885v1, recomputes pair-dependent polar references; these need not equal the transported midpoint. The results below concern this positive commuting-input family and the failure of scalar-balance necessity. They give no full classification of Good triples.

Definition 1.1 (A full Bloch chord).

$$\forall (d:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))(e:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))(z:\mathbb{R}),r\left(d,e,z\right)=d+\sqrt{1-\Vert d{\Vert }^2}(2z-1)e$$

Formalization. D5/S3/Quantum/CommutingMidpoint.chordVector (✓ std3).

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

For d,e in Euclidean three-space and real z, r(z)=d+sqrt(1-||d|| squared)(2z-1)e. The full physical chord has d perpendicular to e, ||e||=1, ||d|| squared<1 and z in [0,1].

Definition 1.2 (Actual states on a chord).

$$\forall (d:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))(e:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))(z:\mathbb{R}),X\left(d,e,z\right)=\mathrm{rho}\left(r\left(d,e,z\right)\right)$$

Formalization. D5/S3/Quantum/CommutingMidpoint.chordState (✓ std3).

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

X(z) is blochMatrix(1,r(z)), the canonical complex qubit matrix. On the full physical chord it is PSD with trace one; interior parameters give PD states.

Theorem 1.3 (The Bloch commutator Gram identity).

$$\forall (a,b:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right)),\Re (\mathrm{tr}\left(\mathrm{conjTranspose}\left((\mathrm{blochMatrix}\left(1,a\right)\mathrm{blochMatrix}\left(1,b\right)-\mathrm{blochMatrix}\left(1,b\right)\mathrm{blochMatrix}\left(1,a\right))\right)(\mathrm{blochMatrix}\left(1,a\right)\mathrm{blochMatrix}\left(1,b\right)-\mathrm{blochMatrix}\left(1,b\right)\mathrm{blochMatrix}\left(1,a\right))\right))=\frac{1}{2}(\mathrm{norm}{\left(a\right)}^2\mathrm{norm}{\left(b\right)}^2-\mathrm{inner}{\left(a,b\right)}^2)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint.bloch_commutator_gram (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

For arbitrary real Euclidean three-vectors a,b, the real trace of C conjugate-transpose times C, where C=blochMatrix(1,a)blochMatrix(1,b)-blochMatrix(1,b)blochMatrix(1,a), equals (||a|| squared ||b|| squared-inner(a,b) squared)/2.

Theorem 1.4 (The sign-sensitive chord factorization).

$$\forall (d:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))(e:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))(r:\mathbb{R})(s:\mathbb{R})(t:\mathbb{R}),\mathrm{inner}\left(d,e\right)=0\wedge \mathrm{norm}\left(e\right)=1\wedge \mathrm{norm}{\left(d\right)}^2<1\wedge 0<r<1\wedge 0\le s\le 1\wedge 0\le t\le 1\Rightarrow \forall (a,b,f,w:\mathbb{R}),(a=U\left(X\left(d,e,r\right),X\left(d,e,s\right)\right)\wedge b=U\left(X\left(d,e,r\right),X\left(d,e,t\right)\right)\wedge f=\Re (F\left(X\left(d,e,r\right),X\left(d,e,s\right),X\left(d,e,t\right)\right))\wedge w=H\left(s,t\right))\Rightarrow (0<a\wedge 0<b\wedge 0\le f\wedge 0\le w\wedge (f^2-w^2)a^2{b}^2=\mathrm{norm}{\left(d\right)}^2(1-w^2)(a^2+b^2-1)\wedge (1\le a^2+b^2\Rightarrow w\le f))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint.qubit_chord_factorization (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

ChordDomain means d perpendicular to e, ||e||=1, tau=||d|| squared<1, 0<r<1 and s,t in [0,1]. Put a=U(X(r),X(s)), b=U(X(r),X(t)), f=Re F(X(r),X(s),X(t)), w=H(s,t). All signs in the display hold. The binary Gram identity and U(X(x),X(y)) squared=tau+(1-tau)H(x,y) squared give the factorization. Since a,b>0 and f,w>=0, a squared+b squared>=1 implies f>=w.

Theorem 1.5 (Strict comparison and degenerate boundaries).

$$\forall (d:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))(e:\mathrm{EuclideanSpace}\left(\mathbb{R},\mathrm{Fin}\left(3\right)\right))(r:\mathbb{R})(s:\mathbb{R})(t:\mathbb{R}),\mathrm{inner}\left(d,e\right)=0\wedge \mathrm{norm}\left(e\right)=1\wedge \mathrm{norm}{\left(d\right)}^2<1\wedge 0<r<1\wedge 0\le s\le 1\wedge 0\le t\le 1\Rightarrow \forall (a,b,f,w:\mathbb{R}),(a=U\left(X\left(d,e,r\right),X\left(d,e,s\right)\right)\wedge b=U\left(X\left(d,e,r\right),X\left(d,e,t\right)\right)\wedge f=\Re (F\left(X\left(d,e,r\right),X\left(d,e,s\right),X\left(d,e,t\right)\right))\wedge w=H\left(s,t\right))\Rightarrow ((0<\mathrm{norm}{\left(d\right)}^2\wedge s\ne t\Rightarrow (w\le f\iff 1\le a^2+b^2)\wedge (f=w\iff a^2+b^2=1))\wedge (\mathrm{norm}{\left(d\right)}^2=0\Rightarrow f=w)\wedge (s=t\Rightarrow f=w=1))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint.qubit_chord_strict_sign_and_boundary (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

Use the same chord domain and a,b,f,w,tau as above. If tau>0 and s differs from t, 1-w squared is strictly positive, giving both exact equivalences. On a diameter, tau=0 gives f=w. Equal states s=t give f=w=1. These are fixed-chord statements, without a classification of arbitrary channel triples.

Definition 1.6 (Mixtures of actual matrices).

$$\forall (p:\mathbb{R})(A:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(B:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),\mathrm{mix}\left(p,A,B\right)=pA+(1-p)B$$

Formalization. D5/S3/Quantum/CommutingMidpoint.mixture (✓ std3).

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

mixture(p,A,B)=p A+(1-p)B, with real scalar multiplication on complex matrices.

Theorem 1.7 (Arbitrary prepared outputs).

$$\forall (A:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(B:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(p:\mathbb{R})(q:\mathbb{R}),\mathrm{PSD}\left(A\right)\wedge \mathrm{tr}\left(A\right)=1\wedge \mathrm{PSD}\left(B\right)\wedge \mathrm{tr}\left(B\right)=1\wedge 0\le p\le 1\wedge 0\le q\le 1\wedge \mathrm{PD}\left(\mathrm{mix}\left(\frac{1}{2},A,B\right)\right)\Rightarrow H\left(p,q\right)\le \Re (F\left(\mathrm{mix}\left(\frac{1}{2},A,B\right),\mathrm{mix}\left(p,A,B\right),\mathrm{mix}\left(q,A,B\right)\right))\wedge 0\le B\left(\mathrm{mix}\left(\frac{1}{2},A,B\right),\mathrm{mix}\left(p,A,B\right),\mathrm{mix}\left(q,A,B\right)\right)\wedge B\left(\mathrm{mix}\left(\frac{1}{2},A,B\right),\mathrm{mix}\left(p,A,B\right),\mathrm{mix}\left(q,A,B\right)\right)\le 2-2H\left(p,q\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint.prepared_qubit_midpoint_fidelity (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

For arbitrary complex qubit densities A,B set T=(A+B)/2, S=pA+(1-p)B and V=qA+(1-q)B, with p,q in [0,1]. If T is PD then the full displayed conclusion holds. The Bloch line through distinct A,B extends to a full chord. The midpoint dominates each prepared state by one half, so the chord comparison applies; classical preparation then gives H(p,q). Equal A,B are treated directly. No output commutation is required.

Definition 1.8 (The scalar midpoint reference).

$$R_0=\frac{1}{2}I$$

Formalization. D5/S3/Quantum/CommutingMidpoint.midpointReference (✓ std3).

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

R0=I/2 as a complex two-by-two matrix; it is PD and has trace one.

Theorem 1.9 (Every positive trace-preserving linear map).

$$\forall (P:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(Q:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(Phi:\mathrm{ComplexLinearMap}\left(\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right),\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)\right)),\mathrm{PSD}\left(P\right)\wedge \mathrm{tr}\left(P\right)=1\wedge \mathrm{PSD}\left(Q\right)\wedge \mathrm{tr}\left(Q\right)=1\wedge PQ=QP\wedge (\forall (M:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),(\mathrm{PSD}\left(M\right))\Rightarrow (\mathrm{PSD}\left(\mathrm{Phi}\left(M\right)\right)))\wedge (\forall (M:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),\mathrm{tr}\left(\mathrm{Phi}\left(M\right)\right)=\mathrm{tr}\left(M\right))\wedge \mathrm{PD}\left(\mathrm{Phi}\left(R_0\right)\right)\Rightarrow U\left(P,Q\right)=\Re (F\left(R_0,P,Q\right))\wedge U\left(P,Q\right)\le \Re (F\left(\mathrm{Phi}\left(R_0\right),\mathrm{Phi}\left(P\right),\mathrm{Phi}\left(Q\right)\right))\wedge B\left(\mathrm{Phi}\left(R_0\right),\mathrm{Phi}\left(P\right),\mathrm{Phi}\left(Q\right)\right)\le B\left(R_0,P,Q\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint.commuting_midpoint_all_positive_trace_preserving (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

Phi ranges over every complex-linear map on all complex qubit matrices that maps each PSD matrix to a PSD matrix and preserves trace on every matrix. R0=I/2. For commuting density P,Q and PD Phi(R0), root fidelity equals the input ordered fidelity and is bounded by the output ordered fidelity; B contracts. For distinct inputs, the exact squared commutator trace forces their full Bloch chord to be a diameter. Its endpoints E1,E0 satisfy R0=(E1+E0)/2. Complex linearity sends the same three inputs to mixtures of Phi(E1),Phi(E0), so the prepared-output theorem applies. Equal inputs follow from the norm identity.

Theorem 1.10 (Canonical physical channels).

$$\forall (P,Q:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(Phi:\mathrm{QuantumChannel}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right)\right)),\mathrm{PSD}\left(P\right)\wedge \mathrm{tr}\left(P\right)=1\wedge \mathrm{PSD}\left(Q\right)\wedge \mathrm{tr}\left(Q\right)=1\wedge PQ=QP\wedge \mathrm{PD}\left(\mathrm{Phi}\left(R_0\right)\right)\Rightarrow 0\le B\left(\mathrm{Phi}\left(R_0\right),\mathrm{Phi}\left(P\right),\mathrm{Phi}\left(Q\right)\right)\wedge 0\le B\left(R_0,P,Q\right)\wedge B\left(\mathrm{Phi}\left(R_0\right),\mathrm{Phi}\left(P\right),\mathrm{Phi}\left(Q\right)\right)\le B\left(R_0,P,Q\right)\wedge \sqrt{B\left(\mathrm{Phi}\left(R_0\right),\mathrm{Phi}\left(P\right),\mathrm{Phi}\left(Q\right)\right)}\le \sqrt{B\left(R_0,P,Q\right)}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint.commuting_midpoint_canonical_CPTP (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

Phi is every existing QuantumChannel(Fin 2,Fin 2); its action is GeneralizedFidelity.rawMatrix. Here Bin=B(R0,P,Q) and Bout=B(Phi(R0),Phi(P),Phi(Q)). The input hypotheses are PSD trace-one P,Q with PQ=QP, and the only output-reference restriction is PD Phi(R0). The channel’s all-amplification complete positivity implies ordinary positivity. Its canonical trace-preserving and complex-linear action gives the previous theorem. The norm identity establishes both nonnegativities before taking square roots.

Definition 1.11 (Universal transported-reference contraction).

$$\forall (P:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(Q:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(R:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),\mathrm{Good}\left(P,Q,R\right)\iff (\forall (Phi:\mathrm{QuantumChannel}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right)\right)),(\mathrm{PD}\left(\mathrm{Phi}\left(R\right)\right))\Rightarrow (B\left(\mathrm{Phi}\left(R\right),\mathrm{Phi}\left(P\right),\mathrm{Phi}\left(Q\right)\right)\le B\left(R,P,Q\right)))$$

Formalization. D5/S3/Quantum/CommutingMidpoint.Good (✓ std3).

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

Good(P,Q,R) quantifies all canonical qubit CPTP channels with PD transported reference. Its physical uses require P,Q density matrices and R PD of trace one. The same channel acts on all three matrices.

Theorem 1.12 (A faithful outside-balance triple).

$$\forall (P,Q:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),P=\mathrm{diag}\left(\frac{9}{10},\frac{1}{10}\right)\wedge Q=\mathrm{diag}\left(\frac{4}{5},\frac{1}{5}\right)\Rightarrow \mathrm{PD}\left(P\right)\wedge \mathrm{PD}\left(Q\right)\wedge \mathrm{PD}\left(R_0\right)\wedge \mathrm{tr}\left(P\right)=1\wedge \mathrm{tr}\left(Q\right)=1\wedge \mathrm{tr}\left(R_0\right)=1\wedge \mathrm{Good}\left(P,Q,R_0\right)\wedge U{\left(R_0,P\right)}^2=\frac{4}{5}\wedge U{\left(R_0,Q\right)}^2=\frac{9}{10}\wedge U{\left(P,Q\right)}^2=\frac{49}{50}\wedge |U{\left(R_0,P\right)}^2-U{\left(R_0,Q\right)}^2|=\frac{1}{10}\wedge 1-U{\left(P,Q\right)}^2=\frac{1}{50}\wedge 1-U{\left(P,Q\right)}^2<|U{\left(R_0,P\right)}^2-U{\left(R_0,Q\right)}^2|\wedge B\left(R_0,P,Q\right)=2-\frac{7\sqrt{2}}{5}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint.faithful_Good_outside_balance (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

Take P=diag(9/10,1/10), Q=diag(4/5,1/5), R0=I/2. All three matrices are PD densities. The theorem proves Good, the three exact squared root fidelities, absolute squared imbalance 1/10, residual 1/50 and their strict inequality. It also gives B(R0,P,Q)=2-7 sqrt(2)/5. Good follows from the universal channel theorem; the scalar values use the actual matrix trace-determinant root formula.

Theorem 1.13 (A singular outside-balance triple).

$$\forall (P,Q:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),P=\mathrm{diag}\left(1,0\right)\wedge Q=\mathrm{diag}\left(\frac{3}{4},\frac{1}{4}\right)\Rightarrow \mathrm{PSD}\left(P\right)\wedge \mathrm{PSD}\left(Q\right)\wedge \mathrm{PD}\left(R_0\right)\wedge \mathrm{tr}\left(P\right)=1\wedge \mathrm{tr}\left(Q\right)=1\wedge \mathrm{tr}\left(R_0\right)=1\wedge \mathrm{rank}\left(P\right)=1\wedge \mathrm{Good}\left(P,Q,R_0\right)\wedge U{\left(R_0,P\right)}^2=\frac{1}{2}\wedge U{\left(R_0,Q\right)}^2=\frac{1}{2}+\frac{\sqrt{3}}{4}\wedge U{\left(P,Q\right)}^2=\frac{3}{4}\wedge |U{\left(R_0,P\right)}^2-U{\left(R_0,Q\right)}^2|=\frac{\sqrt{3}}{4}\wedge 1-U{\left(P,Q\right)}^2=\frac{1}{4}\wedge 1-U{\left(P,Q\right)}^2<|U{\left(R_0,P\right)}^2-U{\left(R_0,Q\right)}^2|\wedge B\left(R_0,P,Q\right)=2-\sqrt{3}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/CommutingMidpoint.singular_Good_outside_balance (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

Take P=diag(1,0), Q=diag(3/4,1/4), R0=I/2. P,Q are PSD trace-one states, R0 is PD of trace one, and rank(P)=1. The theorem proves Good, the three exact squared root fidelities, imbalance sqrt(3)/4, residual 1/4 and the strict inequality. It also gives B(R0,P,Q)=2-sqrt(3). The rank and root values are exact, and the universal channel statement includes singular inputs.

Definition 1.14 (The proposed scalar necessity).

$$\mathrm{claim}\left(\right)\iff (\forall (P:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(Q:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))(R:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),(\mathrm{PSD}\left(P\right)\wedge \mathrm{tr}\left(P\right)=1\wedge \mathrm{PSD}\left(Q\right)\wedge \mathrm{tr}\left(Q\right)=1\wedge \mathrm{PD}\left(R\right)\wedge \mathrm{tr}\left(R\right)=1\wedge \mathrm{Good}\left(P,Q,R\right))\Rightarrow (|U{\left(R,P\right)}^2-U{\left(R,Q\right)}^2|\le 1-U{\left(P,Q\right)}^2))$$

Formalization. D5/S3/Quantum/CommutingMidpoint.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

The proposed necessity ranges over every PSD density pair P,Q and every PD trace-one reference R. It says that Good implies scalar balance. No commutation assumption occurs in this proposed global assertion.

Theorem 1.15 (Scalar balance is not necessary).

$$\neg \mathrm{claim}\left(\right)$$

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

Source. Repository-derived.

Acknowledgement. Haobo Ma, Reza Rajaei, Wenlin Zhang (2026). Generalized Fidelity, the Data Processing Inequality, and Convexity. URL: https://arxiv.org/html/2609.09753v3.

Commentary.

The faithful triple above refutes claim. Thus there exist three PD density matrices with Good and strict failure of balance. The singular triple gives an additional boundary example. This disproves the proposed necessity and the corresponding full iff; it does not supply a replacement necessary-and-sufficient classification.

References

• Truth anchor: D5/S3/Quantum/CommutingMidpoint.Good
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.bloch_commutator_gram
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.chordState
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.chordVector
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.claim
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.commuting_midpoint_all_positive_trace_preserving
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.commuting_midpoint_canonical_CPTP
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.faithful_Good_outside_balance
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.midpointReference
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.mixture
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.prepared_qubit_midpoint_fidelity
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.qubit_chord_factorization
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.qubit_chord_strict_sign_and_boundary
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.result
• Truth anchor: D5/S3/Quantum/CommutingMidpoint.singular_Good_outside_balance
• Dependency: D5/S3/Quantum/CommutingMidpoint/Fidelity