Overlapping pairs refute the twirling phase index formula

Abstract

Three characters of C3 with multiplicity two contradict the proposed twirling phase index formula.

Theorem 1.1 (Unit modulus of the three characters).

$$\forall i\in \mathrm{Fin}\left(3\right),\forall g\in \mathrm{Multiplicative}\left(\mathrm{ZMod}\left(3\right)\right),\mathrm{star}\left(\mathrm{ZMod}.\mathrm{stdAddChar}(\mathrm{ZMod}.\mathrm{finEquiv}(3,i)\cdot \mathrm{Multiplicative}.\mathrm{toAdd}(g))\right)\cdot \mathrm{ZMod}.\mathrm{stdAddChar}(\mathrm{ZMod}.\mathrm{finEquiv}(3,i)\cdot \mathrm{Multiplicative}.\mathrm{toAdd}(g))=1$$

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

Source. Repository-derived.

Commentary.

For every character index and group element, the character’s conjugate product is one.

Theorem 1.2 (The squared two-coordinate scale).

$$\mathrm{Complex}.\mathrm{normSq}({\sqrt{2}}^{-1})=\frac{1}{2}$$

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

Source. Repository-derived.

Commentary.

The reciprocal of the positive real square root of two is regarded as a complex scalar. Its squared complex modulus is one half.

All vector and matrix coordinates are complex. Fin indices start at zero. Matrix.vecMulVec(x, star(x)) is the rank-one state of x. Anonymous brackets display Lean typeclass assumptions; val displays a unitary matrix’s coercion. Natural suprema and infima encode the extremal dimensions and frame lengths. The finite-group conjecture is implied by the source’s compact-group conjecture.

Definition 1.3 (The finite twirling channel).

$$\forall G\in \mathrm{Type}\left(\right),[\mathrm{Group}\left(G\right)][\mathrm{Fintype}\left(G\right)]\forall I\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall pi\in G{\to }^{\ast }\mathrm{Matrix}.\mathrm{unitaryGroup}(I,\mathbb{C}),\forall X\in \mathrm{Matrix}\left(I,I,\mathbb{C}\right),\mathrm{twirl}\left(pi,X\right)=(\mathrm{Fintype}.\mathrm{card}(G{)}^{-1}:\mathbb{C})\cdot \sum _{g:G}(\mathrm{val}\left(pi(g)\right)\cdot X\cdot \mathrm{star}\left(\mathrm{val}\left(pi(g)\right)\right))$$

Formalization. D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.twirl (✓ std3).

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 3: “We define a linear map Φ_{π, σ}: B(K, H) → B(K, H) by Φ_{π, σ}(T) = ∫_Gπ(g)Tσ(g⁻¹) dμ(g) and denote Φ_{π, σ} by Φ_π when π = σ.” For finite G normalized Haar integration is the uniform average. pi is a group homomorphism into Matrix.unitaryGroup. Unitarity makes the inverse equal to star. I indexes the coordinate space.

Definition 1.4 (Phase retrievable subspaces).

$$\forall I\in \mathrm{Type}\left(\right),\forall Phi\in \mathrm{Matrix}\left(I,I,\mathbb{C}\right)\to \mathrm{Matrix}\left(I,I,\mathbb{C}\right),\forall M\in \mathrm{Submodule}\left(\mathbb{C},I\to \mathbb{C}\right),\mathrm{PhaseRetrievable}\left(Phi,M\right)\iff \left(\forall x\in I\to \mathbb{C},x\in M\Rightarrow \left(\forall y\in I\to \mathbb{C},y\in M\Rightarrow \left(Phi(\mathrm{Matrix}.\mathrm{vecMulVec}(x,\mathrm{star}\left(x\right)))=Phi(\mathrm{Matrix}.\mathrm{vecMulVec}(y,\mathrm{star}\left(y\right)))\Rightarrow \mathrm{Matrix}.\mathrm{vecMulVec}(x,\mathrm{star}\left(x\right))=\mathrm{Matrix}.\mathrm{vecMulVec}(y,\mathrm{star}\left(y\right))\right)\right)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.PhaseRetrievable (✓ std3).

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 5: “A subspace M of H is called phase retrievable under Φ if Φ is pure state injective on M, i.e., Φ(x⊗x) = Φ(y⊗y) implies that x⊗x = y⊗y for x, y∈M, or equivalently if there exists a POVM {F_j}_j∈𝕁 in B(K) such that {P_MΦ^*(F_j)P_M}_j∈𝕁 is a phase retrievable operator valued frame for M, where P_M is the orthogonal projection onto M.” The encoding uses the pure-state-injectivity clause. Phi maps square matrices, M is a complex submodule, and x and y range over every member of M, with no normalization restriction.

Definition 1.5 (The phase retrievability index).

$$\forall I\in \mathrm{Type}\left(\right),\forall Phi\in \mathrm{Matrix}\left(I,I,\mathbb{C}\right)\to \mathrm{Matrix}\left(I,I,\mathbb{C}\right),\mathrm{pr}\left(Phi\right)=\mathrm{sSup}\left(\{k:\mathbb{N}\mid \exists M\in \mathrm{Submodule}\left(\mathbb{C},I\to \mathbb{C}\right),\mathrm{Module}.\mathrm{finrank}(\mathbb{C},M)=k\wedge \mathrm{PhaseRetrievable}\left(Phi,M\right)\}\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.pr (✓ std3).

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 5: “The phase retrievability index pr(Φ_π) is defined to be the largest integer k such that there exits a k-dimensional subspace M⊂H such that M is phase retrievable under Φ.” The spelling exits is retained. k is a natural dimension, finrank is over Complex, and the supremum is over dimensions of all phase retrievable subspaces.

Definition 1.6 (Correctable codes).

$$\forall G\in \mathrm{Type}\left(\right),[\mathrm{Group}\left(G\right)]\forall I\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall pi\in G{\to }^{\ast }\mathrm{Matrix}.\mathrm{unitaryGroup}(I,\mathbb{C}),\forall M\in \mathrm{Submodule}\left(\mathbb{C},I\to \mathbb{C}\right),\mathrm{IsCode}\left(pi,M\right)\iff \left(\exists P\in \mathrm{Matrix}\left(I,I,\mathbb{C}\right),\mathrm{star}\left(P\right)=P\wedge \left(P\cdot P=P\wedge \left(\mathrm{LinearMap}.\mathrm{range}(\mathrm{Matrix}.\mathrm{mulVecLin}(P))=M\wedge \left(\exists c\in G\to \left(G\to \mathbb{C}\right),\forall g\in G,\forall h\in G,P\cdot \mathrm{star}\left(\mathrm{val}\left(pi(g)\right)\right)\cdot \mathrm{val}\left(pi(h)\right)\cdot P=c(g,h)\cdot P\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.IsCode (✓ std3).

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 5, Lemma 3.1: “Let 𝒞 be a subspace of H, and let P be the orthogonal projections onto 𝒞. Suppose Φ is a quantum channel with Kraus operators {E_i}_i=1^r. Then the following are equivalent:” Its first two items read: “(i) 𝒞 is a quantum code for Φ. (ii) there exists a Hermitian matrix A = [a_ij] such that PE_i^*E_jP = a_ijP holds for all i, j.” The encoding takes the Knill–Laflamme clause for the Kraus family pi(g)/sqrt(card G). The common normalization is absorbed into c. A self-adjoint idempotent with range M is its orthogonal projection. The compression scalars are automatically Hermitian for a nonzero code; for the zero code they may be chosen zero.

Definition 1.7 (The code dimension index).

$$\forall G\in \mathrm{Type}\left(\right),[\mathrm{Group}\left(G\right)]\forall I\in \mathrm{Type}\left(\right),[\mathrm{Fintype}\left(I\right)][\mathrm{DecidableEq}\left(I\right)]\forall pi\in G{\to }^{\ast }\mathrm{Matrix}.\mathrm{unitaryGroup}(I,\mathbb{C}),\mathrm{beta}\left(pi\right)=\mathrm{sSup}\left(\{k:\mathbb{N}\mid \exists M\in \mathrm{Submodule}\left(\mathbb{C},I\to \mathbb{C}\right),\mathrm{Module}.\mathrm{finrank}(\mathbb{C},M)=k\wedge \mathrm{IsCode}\left(pi,M\right)\}\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.beta (✓ std3).

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 2: “β(Φ_π) = max{m₁, … , m_d} is the largest number m such that there exists a quantum code of dimension m.” Theorem 3.4, page 7, proves the equality. Here beta(pi) denotes beta of the induced twirling channel, as the supremum of the finranks of the IsCode subspaces.

Definition 1.8 (Minimal complex frame length).

$$\forall k\in \mathbb{N},\mathrm{frameLength}\left(k\right)=\mathrm{sInf}\left(\{n:\mathbb{N}\mid \exists f\in \mathrm{Fin}\left(n\right)\to \left(\mathrm{Fin}\left(k\right)\to \mathbb{C}\right),\forall x\in \mathrm{Fin}\left(k\right)\to \mathbb{C},\forall y\in \mathrm{Fin}\left(k\right)\to \mathbb{C},\left(\forall j\in \mathrm{Fin}\left(n\right),\mathrm{norm}\left(\mathrm{dotProduct}\left(x,\mathrm{star}\left(f(j)\right)\right)\right)=\mathrm{norm}\left(\mathrm{dotProduct}\left(y,\mathrm{star}\left(f(j)\right)\right)\right)\right)\Rightarrow \mathrm{Matrix}.\mathrm{vecMulVec}(x,\mathrm{star}\left(x\right))=\mathrm{Matrix}.\mathrm{vecMulVec}(y,\mathrm{star}\left(y\right))\}\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.frameLength (✓ std3).

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 4: “For an n-dimensional Hilbert space H, we will use ℐ_n to denote the smallest integer N such that there is a phase retrievable frame {x_j}_j=1^N for H.” k is the source’s n, and n is the family’s length N. f has n vectors in Fin k to Complex. The norms of the complex dotProducts are their magnitudes. A retrieving family spans: a nonzero vector orthogonal to the family would collide with zero. No additional frame condition changes the family of admissible lengths.

Definition 1.9 (Nonzero irreducible representations).

$$\forall G\in \mathrm{Type}\left(\right),[\mathrm{Group}\left(G\right)]\forall n\in \mathbb{N},\forall rho\in G{\to }^{\ast }\mathrm{Matrix}.\mathrm{unitaryGroup}(\mathrm{Fin}\left(n\right),\mathbb{C}),\mathrm{Irreducible}\left(rho\right)\iff \left(0<n\wedge \left(\forall M\in \mathrm{Submodule}\left(\mathbb{C},\mathrm{Fin}\left(n\right)\to \mathbb{C}\right),\left(\forall g\in G,\forall x\in \mathrm{Fin}\left(n\right)\to \mathbb{C},x\in M\Rightarrow \mathrm{Matrix}.\mathrm{mulVec}(\mathrm{val}\left(rho(g)\right),x)\in M\right)\Rightarrow \left(M=\mathrm{Bot}.\mathrm{bot}\vee M=\mathrm{Top}.\mathrm{top}\right)\right)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.Irreducible (✓ std3).

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 2: “A representation π is called irreducible if 0 and H are the only invariant subspaces.” rho acts on Fin n to Complex. The dimension is positive, as required for an irreducible representation. Every invariant submodule equals bottom or top.

Definition 1.10 (No invertible intertwiner).

$$\forall G\in \mathrm{Type}\left(\right),[\mathrm{Group}\left(G\right)]\forall n\in \mathbb{N},\forall k\in \mathbb{N},\forall rho\in G{\to }^{\ast }\mathrm{Matrix}.\mathrm{unitaryGroup}(\mathrm{Fin}\left(n\right),\mathbb{C}),\forall sigma\in G{\to }^{\ast }\mathrm{Matrix}.\mathrm{unitaryGroup}(\mathrm{Fin}\left(k\right),\mathbb{C}),\mathrm{Inequivalent}\left(rho,sigma\right)\iff \left(\neg \left(\exists T\in \mathrm{Fin}\left(n\right)\to \mathbb{C}\equiv {}_{l[\mathbb{C}]}\mathrm{Fin}\left(k\right)\to \mathbb{C},\forall g\in G,\forall x\in \mathrm{Fin}\left(n\right)\to \mathbb{C},T(\mathrm{Matrix}.\mathrm{mulVec}(\mathrm{val}\left(rho(g)\right),x))=\mathrm{Matrix}.\mathrm{mulVec}(\mathrm{val}\left(sigma(g)\right),T(x))\right)\right)$$

Formalization. D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.Inequivalent (✓ std3).

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 2: “where m_i∈ℕ and π₁, … , π_d are inequivalent irreducible unitary representations of G acting on Hilbert spaces H₁, … , H_d, respectively.” rho and sigma are inequivalent when there is no complex-linear equivalence intertwining every group element. This is the finite-dimensional unitary equivalence convention.

Definition 1.11 (The multiplicity decomposition).

$$\forall G\in \mathrm{Type}\left(\right),[\mathrm{Group}\left(G\right)]\forall d\in \mathbb{N},\forall n\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall rho\in \left(\forall i\in \mathrm{Fin}\left(d\right),G{\to }^{\ast }\mathrm{Matrix}.\mathrm{unitaryGroup}(\mathrm{Fin}\left(n(i)\right),\mathbb{C})\right),\forall m\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall g\in G,(\mathrm{val}\left(\mathrm{blockRep}\left(rho,m\right)(g)\right):\mathrm{Matrix}\left(\Sigma {}_{i:\mathrm{Fin}\left(d\right)}(\mathrm{Fin}\left(m(i)\right)\times \mathrm{Fin}\left(n(i)\right)),\Sigma {}_{i:\mathrm{Fin}\left(d\right)}(\mathrm{Fin}\left(m(i)\right)\times \mathrm{Fin}\left(n(i)\right)),\mathbb{C}\right))=\mathrm{Matrix}.{\mathrm{blockDiagonal}}^{\prime }(fun(i:\mathrm{Fin}\left(d\right))\mapsto \mathrm{Matrix}.\mathrm{kronecker}((1:\mathrm{Matrix}\left(\mathrm{Fin}\left(m(i)\right),\mathrm{Fin}\left(m(i)\right),\mathbb{C}\right)),\mathrm{val}\left(rho(i,g)\right)))$$

Formalization. D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.blockRep (✓ std3).

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 2 displays U pi(g) U star = m1 pi1 direct-sum … direct-sum md pid and states: “where m_i∈ℕ and π₁, … , π_d are inequivalent irreducible unitary representations of G acting on Hilbert spaces H₁, … , H_d, respectively.” blockRep(rho,m) is the homomorphism with blocks Matrix.kronecker(1,val(rho(i,g))). The dependent index has a block label, a multiplicity coordinate and an irreducible coordinate. The displayed expression binds the complete family n and m.

Definition 1.12 (The final conjecture of Section 5).

$$claim\iff \left(\forall G\in \mathrm{Type}\left(\right),[\mathrm{Group}\left(G\right)][\mathrm{Fintype}\left(G\right)]\forall d\in \mathbb{N},\forall n\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall m\in \mathrm{Fin}\left(d\right)\to \mathbb{N},\forall rho\in \left(\forall i\in \mathrm{Fin}\left(d\right),G{\to }^{\ast }\mathrm{Matrix}.\mathrm{unitaryGroup}(\mathrm{Fin}\left(n(i)\right),\mathbb{C})\right),\left(\forall i\in \mathrm{Fin}\left(d\right),\mathrm{Irreducible}\left(rho(i)\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(d\right),\forall j\in \mathrm{Fin}\left(d\right),i\ne j\Rightarrow \mathrm{Inequivalent}\left(rho(i),rho(j)\right)\right)\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(d\right),1\le m(i)\right)\Rightarrow \left(\forall k\in \mathbb{N},\mathrm{frameLength}\left(k\right)\le d\Rightarrow \left(d<\mathrm{frameLength}\left(k+1\right)\Rightarrow \mathrm{pr}\left(\mathrm{twirl}\left(\mathrm{blockRep}\left(rho,m\right)\right)\right)=\max \left(\mathrm{beta}\left(\mathrm{blockRep}\left(rho,m\right)\right),k\right)\right)\right)\right)\right)\right)$$

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

Citation. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Page 13: “Conjecture. Let π = m₁π₁⊕ … ⊕ m_dπ_d be a unitary representation of G such that π_i and π_j are inequivalent irreducible representations for all i≠j and ℐ_k ≤ d < ℐ_k+1. Then pr(Φ_π) = max {β(Φ_π), k}.” The encoding quantifies finite groups G, the number d of pairwise inequivalent irreducibles, their dimensions n, positive multiplicities m and the frame-length index k. The source’s one-based summand labels become Fin d. The finite-group specialization is sufficient for a refutation of the compact-group assertion.

Theorem 1.13 (The conjecture is false).

$$\neg claim$$

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

Resolves. Problems/han-liu-2023-twirling-phase-retrievability (refuted) by D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.result.

Source. Repository-derived.

Acknowledgement. Deguang Han and Kai Liu (2023). Zero-Error Correctibility and Phase Retrievability for Twirling Channels. DOI: 10.1016/S0034-4877(24)00012-0. URL: https://arxiv.org/abs/2311.16349v1.

Commentary.

Take G = Multiplicative(ZMod(3)), the three one-dimensional characters, d = 3 and every multiplicity equal to two. Character orthogonality identifies the twirl with three-block pinching. The isometric map (u,v,w) to ((u,v),(u,w),(v,w))/sqrt(2) places every entry of a three by three operator in a surviving two by two compression. Its range is phase retrievable, giving pr at least three. Knill–Laflamme compressions force every code to inject into a block of dimension two, and a whole block attains that dimension. One frame vector retrieves the complex one-dimensional space; three vectors cannot retrieve the two-dimensional space, whereas four can. Thus k = 1 and max(beta,k) = 2. The three-vector obstruction uses real rank-nullity to construct nonzero x and y for which x+y and x-y have equal measurements but different rank-one states. The rectangular matrix uses Matrix.conjTranspose, while square matrices use star. The multiplicity-one character case is compatible with this counterexample, as are the source’s code formula and lower bounds.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.Inequivalent
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.Irreducible
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.IsCode
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.PhaseRetrievable
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.beta
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.blockRep
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.chi_unit
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.claim
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.frameLength
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.pr
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.result
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.scale_normSq
• Truth anchor: D5/S3/Quantum/QuantumChannels/TwirlingPhaseRetrievabilityCounterexample.twirl