Lin’s operator Wielandt norm conjecture fails
Abstract
A unital 2-positive complex-linear map violates Lin’s operator Wielandt product norm bound.
Minghua Lin, On an operator Kantorovich inequality for positive linear maps, J. Math. Anal. Appl. 402 (2013), 127–132; arXiv:1212.5690v1, §3, p. 6, verbatim: “Theorem 3.1. [3] Let 0 < m ≤ A ≤ M and let X, Y be two partial isometries on H whose final spaces are orthogonal to each other. Then for every 2-positive linear map Φ, Φ(XAY)Φ(YAY)⁻¹Φ(YAX) ≤ ((M−m)/(M+m))² Φ(XAX).” §3, pp. 6–7, immediately before Conjecture 3.4, verbatim: “Despite the invalidity of (3.6), there is some evidence that the following assertion could be true. We have been unable to prove (or disprove) it.” §3, p. 7, verbatim: “Conjecture 3.4. Under the same condition as in Theorem 3.1. Then for every 2-positive linear map Φ, ‖Φ(XAY)Φ(YAY)⁻¹Φ(YAX)Φ(XAX)⁻¹‖ ≤ ((M−m)/(M+m))².” §3, p. 6, verbatim: “Let Φ be a unital positive linear map between C*-algebras. We say that Φ is 2-positive if whenever the 2 × 2 operator matrix [[A, B],[B*, C]] is positive, then so is [[Φ(A), Φ(B)],[Φ(B*), Φ(C)]].” P. Zhang, Remarks on an operator Wielandt inequality, arXiv:1506.00737, describes the conjecture as still open.
Definition 1.1 (Partial isometries).
Formalization. D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.IsPartialIsometry (✓ std3).
Citation. Minghua Lin (2013). On an operator Kantorovich inequality for positive linear maps. DOI: 10.1016/j.jmaa.2013.01.015. URL: https://arxiv.org/abs/1212.5690v1.
Commentary.
For a complex n×n matrix X, the condition is XXX=X. Orthogonality of the final spaces is expressed separately by XY=0: its entries are inner products between columns of X and Y, so the two ranges are orthogonal.
Definition 1.2 (Unital 2-positive linear maps).
Formalization. D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.IsUnitalTwoPositive (✓ std3).
Citation. Minghua Lin (2013). On an operator Kantorovich inequality for positive linear maps. DOI: 10.1016/j.jmaa.2013.01.015. URL: https://arxiv.org/abs/1212.5690v1.
Commentary.
The map is complex-linear, sends I to I, and preserves positive semidefiniteness of every 2×2 block matrix [[A,B],[B*,C]] by entrywise application. This implies positivity by taking B=C=0 and restricting the positive image to its first block. Thus the predicate encodes the unital positive maps in the source definition.
Definition 1.3 (Euclidean operator norm bound).
Formalization. D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.NormLE (✓ std3).
Source. Repository-derived.
Acknowledgement. Minghua Lin (2013). On an operator Kantorovich inequality for positive linear maps. DOI: 10.1016/j.jmaa.2013.01.015. URL: https://arxiv.org/abs/1212.5690v1.
Commentary.
NormLE T c means that every vector v in the complex Euclidean space satisfies ‖Tv‖≤c‖v‖. Matrix.toEuclideanLin supplies precisely this linear action, so this is the induced operator norm inequality.
Definition 1.4 (Conjecture 3.4 in finite dimensions).
Formalization. D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.claim (✓ std3).
Citation. Minghua Lin (2013). On an operator Kantorovich inequality for positive linear maps. DOI: 10.1016/j.jmaa.2013.01.015. URL: https://arxiv.org/abs/1212.5690v1.
Commentary.
The assertion quantifies over all finite dimensions n,k, complex matrices A,X,Y, real bounds m,M, and complex-linear maps Φ. It assumes 0<m≤M, A Hermitian, mI≤A≤MI, partial isometries X,Y with orthogonal ranges, and a unital 2-positive Φ. Both compressed images must have unit determinants, so their inverses are genuine. The general source assertion includes this finite-dimensional case; failure here refutes Conjecture 3.4.
Theorem 1.5 (An exact four-dimensional counterexample).
Proof. Machine-checked in Lean as D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.result (✓ std3). ∎
Resolves. Problems/lin-2013-operator-wielandt-norm-refutation (refuted) by D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.result.
Source. Repository-derived.
Acknowledgement. Minghua Lin (2013). On an operator Kantorovich inequality for positive linear maps. DOI: 10.1016/j.jmaa.2013.01.015. URL: https://arxiv.org/abs/1212.5690v1.
Commentary.
Take n=k=4, m=1/25, M=13, A=[[9,0,2,0],[0,2,1,0],[2,1,1,0],[0,0,0,1]], P=X=diag(1,1,0,0), and Y with entries Y(2,0)=Y(3,1)=1 and all others zero, using zero-based indices. Define Φ(Z)=PZP*+YZY*. Exact LDL* certificates have diagonals (224/25,49/25,33/9800,24/25) for A−mI and (4,11,120/11,12) for MI−A. The lower factor has third row (25/112,25/49,1,0), and the upper factor has third row (−1/2,−1/11,1,0); their other rows equal those of I. Positive diagonal congruences certify the bounds. The proof checks XXX=X, YYY=Y, and XY=0. For a positive block M, conjugation by diag(P,P) and diag(Y,Y) gives positive summands whose sum is its entrywise Φ-image. PP+YY*=I gives unitality. The images Φ(YAY)=I and Φ(XAX)=diag(9,2,9,2) have determinants 1 and 324. Their inverses are I and diag(1/9,1/2,1/9,1/2). The product T consists of two copies of G=[[4/9,1],[2/9,1/2]]. For the unit coordinate vector of index 1, ‖Te₂‖²=5/4>(26244/26569)², whereas the conjectured constant is 26244/26569. The hypotheses therefore hold and the norm conclusion fails. The order inequality survives: D^(−1/2)CE^(−1)CD^(−1/2) is bounded above by qI, but CE^(−1)CD^(−1) is a non-normal similarity of it. This mechanism and the unbounded parameter family in the companion problem are exact mathematical reasoning, not further Lean theorems. Conditional results assuming Conjecture 3.4 retain their conditional form and cannot apply that conjecture universally.
References
- Truth anchor:
D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.IsPartialIsometry - Truth anchor:
D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.IsUnitalTwoPositive - Truth anchor:
D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.NormLE - Truth anchor:
D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.claim - Truth anchor:
D5/S3/Quantum/Matrix/OperatorWielandtNormRefutation.result