Extended local permutations do not suffice for block-shift form

Abstract

A three-qubit root vector has an above-diagonal support entry after every extended local permutation, excluding contiguous block-shift form.

Definition 1.1 (The signed local flip).

$$J=Matrix.map\left(physicalJ2,\mathrm{algebraMap}\left(\mathbb{R},\mathbb{C}\right)\right)$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.J (✓ std3).

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

The complex matrix J is the scalar extension of physicalJ2 and has rows (0,1) and (-1,0), exactly the local factor in equation (51), p. 26. Matrix.map applies the real-to-complex algebraMap entrywise.

Definition 1.2 (The signed swap).

$$Pout=\left(\begin{array}{cccc}1& 0& 0& 0\\ 0& 0& 1& 0\\ 0& -1& 0& 0\\ 0& 0& 0& 1\end{array}\right)$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.Pout (✓ std3).

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

The signed swap Pout is displayed on p. 26. Rows and columns are ordered 00, 01, 10, 11. Its support swaps the two tensor positions; the entry at row 10 and column 01 has sign -1.

Definition 1.3 (Signed local permutations).

$$\forall n:\mathbb{N},\mathrm{PiLoc}\left(n\right)=\{M:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right)|\exists P:(\mathrm{Fin}\left(n\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right)),(\forall k:\mathrm{Fin}\left(n\right),P\left(k\right)\in \{1,-1,J,-J\})\wedge (M=\mathrm{tensorOp}\left(P\right))\}$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.PiLoc (✓ std3).

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

Conjecture 3.6, pp. 26–27: “Here, Πloc denotes the subgroup of all (signed) local permutations, i.e. Πloc consists of all matrices of the form P1 ⊗ · · · ⊗ Pn with Pk ∈ {±I2, ±[[0, 1], [−1, 0]]} for k = 1, . . . , n, and Πout stands for the subgroup generated by I2 ⊗ · · · ⊗ I2 ⊗ Pout ⊗ I2 ⊗ · · · ⊗ I2 ∈ U(2^n), n ≥ 2, where the factor Pout appears in all possible positions.” The existing tensorOp has entries ∏ k, P k (x k) (y k). Lex(Fin(n) → Fin(2)) gives the Kronecker order, with position 0 most significant. Signs are retained in the complex matrices.

Definition 1.4 (Adjacent signed-swap embeddings).

$$\forall n:\mathbb{N},\forall k:\mathrm{Fin}\left((n-1)\right),\forall x:\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\forall y:\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{adjacent}\left(k,x,y\right)=\mathrm{Pout}\left(\mathrm{finProdFinEquiv}\left((x\left(Fin.mk\left(\mathrm{val}\left(k\right)\right)\right),x\left(Fin.mk\left(\mathrm{val}\left(k\right)+1\right)\right))\right),\mathrm{finProdFinEquiv}\left((y\left(Fin.mk\left(\mathrm{val}\left(k\right)\right)\right),y\left(Fin.mk\left(\mathrm{val}\left(k\right)+1\right)\right))\right)\right)\cdot \prod _{j\in Finset.filter\left((\mathrm{fun}(j:\mathrm{Fin}\left(n\right))\mapsto (\mathrm{val}\left(j\right)\ne \mathrm{val}\left(k\right))\wedge (\mathrm{val}\left(j\right)\ne \mathrm{val}\left(k\right)+1)),(Finset.univ:\mathrm{Finset}\left(\mathrm{Fin}\left(n\right)\right))\right)}(1:\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{C}\right))\left(x\left(j\right),y\left(j\right)\right)$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.adjacent (✓ std3).

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

Conjecture 3.6, p. 27: “where the factor Pout appears in all possible positions.” The index k ranges over Fin(n - 1), with natural subtraction, and selects positions val(k) and val(k) + 1. finProdFinEquiv(a,b) has value 2 val(a) + val(b); identity factors act at every other position. Fin.mk proof arguments are suppressed in the displayed coordinate indices.

Definition 1.5 (Units of the adjacent embeddings).

$$\forall n:\mathbb{N},\mathrm{outGenerators}\left(n\right)=\{u:(\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right){)}^{\times }|\exists k:\mathrm{Fin}\left((n-1)\right),(u:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right))=\mathrm{adjacent}\left(k\right)\}$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.outGenerators (✓ std3).

Source. Repository-derived.

Acknowledgement. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

The generators are the units whose underlying complex matrix is an adjacent embedding. The unit group retains invertibility rather than admitting singular matrices. A unit’s coercion is shown with its matrix type.

Definition 1.6 (The generated signed-swap subgroup).

$$\forall n:\mathbb{N},\mathrm{PiOut}\left(n\right)=Subgroup.closure\left(\mathrm{outGenerators}\left(n\right)\right)$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.PiOut (✓ std3).

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

Conjecture 3.6, pp. 26–27: “Here, Πloc denotes the subgroup of all (signed) local permutations, i.e. Πloc consists of all matrices of the form P1 ⊗ · · · ⊗ Pn with Pk ∈ {±I2, ±[[0, 1], [−1, 0]]} for k = 1, . . . , n, and Πout stands for the subgroup generated by I2 ⊗ · · · ⊗ I2 ⊗ Pout ⊗ I2 ⊗ · · · ⊗ I2 ∈ U(2^n), n ≥ 2, where the factor Pout appears in all possible positions.” Subgroup.closure is taken in the unit group of the matrix ring; inverses and arbitrary finite products are included.

Definition 1.7 (The product set of extended local permutations).

$$\forall n:\mathbb{N},\mathrm{PiEx}\left(n\right)=\{M:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right)|\exists p:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right),(p\in \mathrm{PiLoc}\left(n\right))\wedge (\exists q:(\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right){)}^{\times },(q\in \mathrm{PiOut}\left(n\right))\wedge (M=p\cdot (q:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right))))\}$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.PiEx (✓ std3).

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

Conjecture 3.6, p. 26, defines Πex_loc := Πloc·Πout. The definition uses that product set literally, with p from PiLoc and q from PiOut. It assumes no elementwise commutation of the two signed matrix groups.

Definition 1.8 (The local diagonal torus).

$$\forall n:\mathbb{N},\mathrm{tloc}\left(n\right)=\{D:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right)|\exists lam:(\mathrm{Fin}\left(n\right)\to \mathbb{R}),D=\sum _{k:\mathrm{Fin}\left(n\right)}\mathrm{tensorOp}\left((\mathrm{fun}(j:\mathrm{Fin}\left(n\right))\mapsto \mathrm{ite}\left(j=k,(Complex.I\cdot (lam\left(k\right):\mathbb{C}))\cdot \mathrm{qubitZ},1\right))\right)\}$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.tloc (✓ std3).

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

The local torus is the sum of i lam(k) times Pauli Z on position k, with real coefficients and identities elsewhere. The existing qubitZ is the matrix with diagonal (1,-1). This convention gives equation (50), p. 24, in dimension four. Complex.I denotes the imaginary unit, and (lam(k) : ℂ) is the real-to-complex coercion.

Definition 1.9 (The union of nonzero root spaces).

$$\forall n:\mathbb{N},E\left(n\right)=\{A:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right)|\exists D:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right),(D\in \mathrm{tloc}\left(n\right))\wedge (\exists phi:\mathbb{R},(phi\ne 0)\wedge (D\cdot A-A\cdot D=(Complex.I\cdot (phi:\mathbb{C}))\cdot A))\}$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.E (✓ std3).

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

The source defines E(t) := ⋃_{∆∈t, ϕ≠0} Eϕ(∆) on p. 15. Equation (48), p. 24, reads [∆, Â] = iϕÂ. Here D ranges over tloc(n), phi is a nonzero real frequency, and the Lie bracket is the matrix commutator. The zero matrix may belong to these root spaces; the counterexample used below is nonzero.

Definition 1.10 (Contiguous block-shift form).

$$\forall n:\mathbb{N},\forall M:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right),\mathrm{IsBlockShift}\left(M\right)\iff (\exists beta:(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right)\to \mathbb{N}),(\mathrm{Monotone}\left(beta\right))\wedge (\forall r:\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\forall c:\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),(M\left(r,c\right)\ne 0)\Rightarrow beta\left(r\right)=beta\left(c\right)+1))$$

Formalization. D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.IsBlockShift (✓ std3).

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

Corollary 2.19, p. 15: “The classical C-numerical range of A is rotationally symmetric for all C ∈ ℂN×N if and only if A is unitarily similar to a block-shift matrix M, i.e. M = (Mkl)1≤k,l≤m is of block form such that all the Mkk are square blocks and Mkl = 0 if l + 1 ≠ k.” A monotone natural-valued block index beta describes a contiguous partition of the finite ordered basis. Every nonzero entry goes from block beta(c) to beta(c) + 1. Empty labels can be omitted; the definition does not allow a basis permutation within the partition.

Definition 1.11 (Conjecture 3.6).

$$claim\iff (\forall n:\mathbb{N},(2\le n)\Rightarrow \forall A:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right),(A\in E\left(n\right))\Rightarrow \exists P:\mathrm{Matrix}\left(\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathrm{Lex}\left((\mathrm{Fin}\left(n\right)\to \mathrm{Fin}\left(2\right))\right),\mathbb{C}\right),(P\in \mathrm{PiEx}\left(n\right))\wedge (\mathrm{IsBlockShift}\left(P\cdot A\cdot P^{-1}\right)))$$

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

Citation. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

Conjecture 3.6 (arXiv:math-ph/0702005v1, p. 26): “Every element of E(tloc) is similar to a block-shift matrix via an element of Πex_loc := Πloc·Πout.” The encoding quantifies over every n ≥ 2, every complex A in E(n), and a conjugating matrix P in PiEx(n). Matrices use the lexicographically ordered tensor basis. Matrix inverse in P A P⁻¹ agrees with the inverse of the signed monomial P.

Theorem 1.12 (Conjecture 3.6 is false).

$$\neg claim$$

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

Resolves. Problems/dirr-helmke-kleinsteuber-schulte-herbrueggen-2008-block-shift (refuted) by D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.result.

Source. Repository-derived.

Acknowledgement. Gunther Dirr; Uwe Helmke; Martin Kleinsteuber; Thomas Schulte-Herbrüggen (2008). Relative C-numerical ranges for applications in quantum control and quantum information. DOI: 10.1080/03081080701535898. URL: https://arxiv.org/abs/math-ph/0702005v1.

Commentary.

For n = 3 let A = Σ j |bar(ej)⟩⟨ej|, with ej = Pi.single(j,1), and let D = i Σ k Zk. Then D A - A D = -2 i A, so A is in E(3). Every extended local permutation has support action x ↦ pi(x) ⊕ a. A contiguous block-shift matrix is strictly lower triangular. Among the three supported columns pi(ej) ⊕ a, the first bit takes both values; therefore some supported row lies above its column. Nonzero entries survive signed monomial conjugation, excluding block-shift form for every P in PiEx(3). Corollaries 2.18 and 2.19 retain their stated scopes, including the allowance of unrestricted unitaries in Corollary 2.19. This theorem settles the universal conjecture by one dimension; it does not state the uniform family extension.

References

• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.E
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.IsBlockShift
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.J
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.PiEx
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.PiLoc
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.PiOut
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.Pout
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.adjacent
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.claim
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.outGenerators
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.result
• Truth anchor: D5/S3/Quantum/Information/LocalPermutationBlockShiftRefutation.tloc
• Dependency: D5/S3/Quantum/Information/StabilizerPairLocalUnitaryInequivalence
• Dependency: D5/S3/Quantum/Thermal/PositiveOneModeWilliamson