Wigner distance minimum attainment

Abstract

The free Wigner polytopes are compact and nonempty, so the source minimum defining C is attained and minimal in the L1 norm.

Definition 1.1 (The phase-point carrier).

$$PhasePoint=\mathrm{Fin}\left(2\right)\times \mathrm{Fin}\left(2\right)$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.PhasePoint (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

A phase point is a pair (q,p) of binary indices, with Fin 2 representing the elements 0 and 1 of the paper’s F₂.

Definition 1.2 (The Wootters phase-point operator).

$$\forall a\in PhasePoint,\mathrm{phasePoint}\left(a\right)=\mathrm{smul}\left(\frac{1}{2},(1+\mathrm{smul}\left((0-1{)}^{\mathrm{val}\left(\mathrm{snd}\left(a\right)\right)},\mathrm{pauliMatrix}\left(X\right)\right)+\mathrm{smul}\left((0-1{)}^{\mathrm{val}\left(\mathrm{fst}\left(a\right)\right)+\mathrm{val}\left(\mathrm{snd}\left(a\right)\right)},\mathrm{pauliMatrix}\left(Y\right)\right)+\mathrm{smul}\left((0-1{)}^{\mathrm{val}\left(\mathrm{fst}\left(a\right)\right)},\mathrm{pauliMatrix}\left(Z\right)\right))\right)$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.phasePoint (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

Page 3: “The single-qubit phase-point operators are indexed by αₖ = (qₖ, pₖ) ∈ F₂²:” followed by A_(qₖ,pₖ) = ½(I + (−1)^pₖ X + (−1)^(qₖ+pₖ) Y + (−1)^qₖ Z). Here q = fst(a), p = snd(a), and val reads their natural-number representatives. The coefficient ½ and the sign powers are complex scalars; 1 inside the matrix sum is the identity matrix.

Definition 1.3 (The product frame).

$$\forall a\in PhasePoint\times PhasePoint,\mathrm{phasePointTwo}\left(a\right)=\mathrm{kronecker}\left(\mathrm{phasePoint}\left(\mathrm{fst}\left(a\right)\right),\mathrm{phasePoint}\left(\mathrm{snd}\left(a\right)\right)\right)$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.phasePointTwo (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

Page 3: “For n qubits, A_α = A_α₁ ⊗ ··· ⊗ A_αₙ, and the discrete Wigner function is” W_ρ(α) = (1/2ⁿ) tr(ρ A_α). phasePointTwo uses n = 2. kronecker denotes the matrix tensor product in the product computational basis.

Definition 1.4 (The Wigner transform).

$$\forall iota\in Type,\forall alpha\in Type,[\mathrm{Fintype}\left(iota\right)],\forall A\in alpha\to \mathrm{Matrix}\left(iota,iota,\mathbb{C}\right),\forall rho\in \mathrm{Matrix}\left(iota,iota,\mathbb{C}\right),\forall a\in alpha,\mathrm{Wigner}\left(A,rho\right)\left(a\right)=\frac{\mathrm{re}\left(\mathrm{trace}\left(rho\cdot A\left(a\right)\right)\right)}{\mathrm{realCast}\left(\mathrm{card}\left(iota\right)\right)}$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.Wigner (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

Page 3: “For n qubits, A_α = A_α₁ ⊗ ··· ⊗ A_αₙ, and the discrete Wigner function is” W_ρ(α) = (1/2ⁿ) tr(ρ A_α). The generic transform divides the real part of the trace by the Hilbert-space dimension, card(ι); for one and two qubits this is 2 and 4. The trace is real on Hermitian states. The division is real division after casting card(ι) to R.

Definition 1.5 (One-qubit Wigner coordinates).

$$\forall rho\in QubitMatrix,\mathrm{WignerOne}\left(rho\right)=\mathrm{Wigner}\left(phasePoint,rho\right)$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.WignerOne (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

WignerOne is the transform in the four-point single-qubit frame.

Definition 1.6 (Two-qubit Wigner coordinates).

$$\forall rho\in TwoQubitMatrix,\mathrm{WignerTwo}\left(rho\right)=\mathrm{Wigner}\left(phasePointTwo,rho\right)$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.WignerTwo (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

WignerTwo is the transform in the sixteen-point product frame.

Definition 1.7 (The phased Pauli group on two qubits).

$$\forall P\in TwoQubitMatrix,(P\in pauliTwo)\iff (\exists c\in \mathbb{C},(c\in \{1,0-1,i,0-i\})\wedge (\exists p\in Pauli,\exists q\in Pauli,P=\mathrm{smul}\left(c,\mathrm{kronecker}\left(\mathrm{pauliMatrix}\left(p\right),\mathrm{pauliMatrix}\left(q\right)\right)\right)))$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.pauliTwo (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

Page 3: “The n-qubit Pauli group Pₙ consists of n-fold tensor products of {I, X, Y, Z} with phases {±1, ±i}.” These are the actual phased tensor-product matrices, including all four phases.

Definition 1.8 (Stabilizer states from their subgroups).

$$\forall iota\in Type,[\mathrm{Fintype}\left(iota\right)],[\mathrm{DecidableEq}\left(iota\right)],\forall P\in \mathrm{Set}\left((\mathrm{Matrix}\left(iota,iota,\mathbb{C}\right))\right),\forall rho\in \mathrm{Matrix}\left(iota,iota,\mathbb{C}\right),(rho\in \mathrm{Stab}\left(P\right))\iff (\exists S\in \mathrm{Subgroup}\left(\mathrm{unitaryGroup}\left(iota,\mathbb{C}\right)\right),\exists psi\in iota\to \mathbb{C},(((((\forall g\in S,\mathrm{val}\left(\mathrm{val}\left(g\right)\right)\in P)\wedge (\mathrm{NatCard}\left(S\right)=\mathrm{card}\left(iota\right)))\wedge (\forall g\in S,\forall h\in S,g\cdot h=h\cdot g))\wedge (\sum _{j:iota}(\mathrm{norm}\left(psi\left(j\right)\right){)}^2=1))\wedge (\forall v\in iota\to \mathbb{C},(\forall g\in S,\mathrm{mulVec}\left(\mathrm{val}\left(\mathrm{val}\left(g\right)\right),v\right)=v)\iff (\exists c\in \mathbb{C},v=\mathrm{smul}\left(c,psi\right))))\wedge (rho=\mathrm{vecMulVec}\left(psi,\mathrm{star}\left(psi\right)\right)))$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.Stab (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

Page 3: “A stabilizer state is the unique +1 eigenstate of an abelian subgroup S ≤ Pₙ of size 2ⁿ.” Stab(P) requires an actual subgroup of the matrix unitary group whose matrices belong to P, with cardinality equal to the Hilbert-space dimension. The subgroup is abelian, ψ is normalized, and its common +1 eigenspace is exactly the complex line spanned by ψ. The density is the outer product ψψ*. NatCard denotes Nat.card; card denotes Fintype.card. The two val calls unwrap the subgroup and unitary subtypes. mulVec is matrix action, smul is scalar multiplication, and vecMulVec is the outer product.

Definition 1.9 (The free Wigner polytope).

$$\forall iota\in Type,\forall alpha\in Type,[\mathrm{Fintype}\left(iota\right)],[\mathrm{DecidableEq}\left(iota\right)],\forall A\in alpha\to \mathrm{Matrix}\left(iota,iota,\mathbb{C}\right),\forall P\in \mathrm{Set}\left((\mathrm{Matrix}\left(iota,iota,\mathbb{C}\right))\right),\mathrm{Wfree}\left(A,P\right)=\mathrm{convexHull}\left(\mathbb{R},\mathrm{image}\left(\mathrm{Wigner}\left(A\right),\mathrm{Stab}\left(P\right)\right)\right)$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.Wfree (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

Page 3: “The stabilizer Wigner polytope is Wfree := conv{W_σ : σ ∈ Stabₙ} ⊂ R^(4ⁿ).” The imported pauliSet is the phased one-qubit Pauli group. Wfree(A,P) takes the real convex hull of the image of the subgroup-defined stabilizer set under Wigner(A). image is set image, so the representation includes every free mixture.

Definition 1.10 (The single-qubit Wigner distance).

$$\forall rho\in QubitMatrix,\mathrm{COne}\left(rho\right)=\mathrm{infDist}\left(\mathrm{toLp}\left(1,\mathrm{WignerOne}\left(rho\right)\right),\mathrm{image}\left(\mathrm{toLp}\left(1\right),\mathrm{Wfree}\left(phasePoint,pauliSet\right)\right)\right)$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.COne (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

Page 3, Definition 3.1 (Wigner distance): “C(ρ) := min_{W_f ∈ Wfree} ‖W_ρ − W_f‖₁.” COne uses the paper’s four-point frame and actual local stabilizer polytope. COne_min proves attainment and minimality for every qubit matrix.

Definition 1.11 (The two-qubit Wigner distance).

$$\forall rho\in TwoQubitMatrix,\mathrm{CTwo}\left(rho\right)=\mathrm{infDist}\left(\mathrm{toLp}\left(1,\mathrm{WignerTwo}\left(rho\right)\right),\mathrm{image}\left(\mathrm{toLp}\left(1\right),\mathrm{Wfree}\left(phasePointTwo,pauliTwo\right)\right)\right)$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.CTwo (✓ std3).

Citation. Soumyojyoti Dutta; Tushar (2026). A Phase-Space Geometric Measure of Magic in Qubit Systems. DOI: 10.48550/arXiv.2603.20792. URL: https://arxiv.org/abs/2603.20792v3.

Commentary.

Page 3, Definition 3.1 (Wigner distance): “C(ρ) := min_{W_f ∈ Wfree} ‖W_ρ − W_f‖₁.” CTwo uses the sixteen-point frame and actual two-qubit stabilizer polytope, including entangled stabilizers. CTwo_min proves attainment and minimality for every two-qubit matrix.

Definition 1.12 (Pauli spectral projectors).

$$\forall p\in Pauli,\forall epsilon\in \mathrm{Fin}\left(2\right),\mathrm{spectral}\left(p,epsilon\right)=\mathrm{smul}\left(\frac{1}{2},(1+\mathrm{smul}\left((0-1{)}^{\mathrm{val}\left(epsilon\right)},\mathrm{pauliMatrix}\left(p\right)\right))\right)$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.spectral (✓ std3).

Source. Repository-derived.

Commentary.

For a nonidentity Pauli p, spectral(p,epsilon) is the rank-one projector onto its eigenvalue (-1)^epsilon. The identity case is included in the definition.

Definition 1.13 (Explicit Pauli eigenvectors).

$$\forall epsilon\in \mathrm{Fin}\left(2\right),(((\mathrm{eigenVector}\left(I,epsilon\right)=[1,0])\wedge (\mathrm{eigenVector}\left(X,epsilon\right)=[\mathrm{complexCast}\left(\mathrm{inv}\left(\mathrm{sqrt}\left(2\right)\right)\right),(0-1{)}^{\mathrm{val}\left(epsilon\right)}\cdot \mathrm{complexCast}\left(\mathrm{inv}\left(\mathrm{sqrt}\left(2\right)\right)\right)]))\wedge (\mathrm{eigenVector}\left(Y,epsilon\right)=[\mathrm{complexCast}\left(\mathrm{inv}\left(\mathrm{sqrt}\left(2\right)\right)\right),i\cdot (0-1{)}^{\mathrm{val}\left(epsilon\right)}\cdot \mathrm{complexCast}\left(\mathrm{inv}\left(\mathrm{sqrt}\left(2\right)\right)\right)]))\wedge (\mathrm{eigenVector}\left(Z,epsilon\right)=\mathrm{ite}\left(epsilon=0,[1,0],[0,1]\right))$$

Formalization. D5/S3/Quantum/Magic/WignerDistanceMinimum.eigenVector (✓ std3).

Source. Repository-derived.

Commentary.

The bracket notation denotes a two-component complex vector. The scalar r is the complex cast of the inverse square root of 2, and t = (-1)^epsilon. The four cases are I: [1,0], X: [r,tr], Y: [r,itr], and Z: [1,0] for epsilon = 0 and [0,1] otherwise.

Theorem 1.14 (Actual local stabilizer subgroups).

$$\forall p\in Pauli,\forall epsilon\in \mathrm{Fin}\left(2\right),(p\ne I)\Rightarrow ((\mathrm{spectral}\left(p,epsilon\right)\in \mathrm{Stab}\left(pauliSet\right))\wedge (\exists U\in \mathrm{MonoidHom}\left(\mathrm{Multiplicative}\left(\mathrm{ZMod}\left(2\right)\right),\mathrm{unitaryGroup}\left(\mathrm{Fin}\left(2\right),\mathbb{C}\right)\right),(((((\mathrm{Injective}\left(U\right))\wedge (\forall x\in \mathrm{Multiplicative}\left(\mathrm{ZMod}\left(2\right)\right),\mathrm{val}\left(U\left(x\right)\right)\in pauliSet))\wedge (\forall x\in \mathrm{Multiplicative}\left(\mathrm{ZMod}\left(2\right)\right),\mathrm{trace}\left(\mathrm{val}\left(U\left(x\right)\right)\right)=\mathrm{ite}\left(x=1,2,0\right)))\wedge (\sum _{j:\mathrm{Fin}\left(2\right)}(\mathrm{norm}\left(\mathrm{eigenVector}\left(p,epsilon\right)\left(j\right)\right){)}^2=1))\wedge (\mathrm{smul}\left(\mathrm{inv}\left(\mathrm{complexCast}\left(\mathrm{card}\left(\mathrm{Multiplicative}\left(\mathrm{ZMod}\left(2\right)\right)\right)\right)\right),\sum _{x:\mathrm{Multiplicative}\left(\mathrm{ZMod}\left(2\right)\right)}\mathrm{val}\left(U\left(x\right)\right)\right)=\mathrm{vecMulVec}\left(\mathrm{eigenVector}\left(p,epsilon\right),\mathrm{star}\left(\mathrm{eigenVector}\left(p,epsilon\right)\right)\right)))\wedge (\mathrm{spectral}\left(p,epsilon\right)=\mathrm{vecMulVec}\left(\mathrm{eigenVector}\left(p,epsilon\right),\mathrm{star}\left(\mathrm{eigenVector}\left(p,epsilon\right)\right)\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Magic/WignerDistanceMinimum.spectral_stabilizer (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each nonidentity Pauli spectral projector is an actual stabilizer state. An injective homomorphism from the multiplicative cyclic group of order two supplies its subgroup. Its nonidentity matrix has trace zero, its eigenvector is normalized, and its group average is exactly the eigenvector’s outer product.

Theorem 1.15 (Actual product stabilizer subgroups).

$$\forall p\in Pauli,\forall q\in Pauli,\forall epsilon\in \mathrm{Fin}\left(2\right),\forall delta\in \mathrm{Fin}\left(2\right),(p\ne I)\Rightarrow ((q\ne I)\Rightarrow (\mathrm{kronecker}\left(\mathrm{spectral}\left(p,epsilon\right),\mathrm{spectral}\left(q,delta\right)\right)\in \mathrm{Stab}\left(pauliTwo\right)))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Magic/WignerDistanceMinimum.spectral_product_stabilizer (✓ std3). ∎

Source. Repository-derived.

Commentary.

Tensoring two Pauli spectral projectors gives a stabilizer state in the full phased two-qubit Pauli group. The construction uses the product of the two local cyclic subgroups and the tensor eigenvector.

Theorem 1.16 (The single-qubit Wigner distance attains the source minimum).

$$\forall rho\in QubitMatrix,\exists f\in PhasePoint\to \mathbb{R},(f\in \mathrm{Wfree}\left(phasePoint,pauliSet\right))\wedge ((\mathrm{COne}\left(rho\right)=\mathrm{norm}\left(\mathrm{toLp}\left(1,\mathrm{WignerOne}\left(rho\right)-f\right)\right))\wedge (\forall g\in PhasePoint\to \mathbb{R},(g\in \mathrm{Wfree}\left(phasePoint,pauliSet\right))\Rightarrow (\mathrm{COne}\left(rho\right)\le \mathrm{norm}\left(\mathrm{toLp}\left(1,\mathrm{WignerOne}\left(rho\right)-g\right)\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Magic/WignerDistanceMinimum.COne_min (✓ std3). ∎

Source. Repository-derived.

Commentary.

$$\mathrm{COne}\left(rho\right)=\underset{f\in \mathrm{Wfree}\left(phasePoint,pauliSet\right)}{\min }\mathrm{norm}\left(\mathrm{toLp}\left(1,\mathrm{WignerOne}\left(rho\right)-f\right)\right)$$

For every qubit matrix rho, the source formula C(rho) := min_{W_f ∈ Wfree} ‖W_rho − W_f‖₁ is attained by some f in the compact nonempty free polytope, and COne rho is no larger than every free candidate.

Theorem 1.17 (The two-qubit Wigner distance attains the source minimum).

$$\forall rho\in TwoQubitMatrix,\exists f\in PhasePoint\times PhasePoint\to \mathbb{R},(f\in \mathrm{Wfree}\left(phasePointTwo,pauliTwo\right))\wedge ((\mathrm{CTwo}\left(rho\right)=\mathrm{norm}\left(\mathrm{toLp}\left(1,\mathrm{WignerTwo}\left(rho\right)-f\right)\right))\wedge (\forall g\in PhasePoint\times PhasePoint\to \mathbb{R},(g\in \mathrm{Wfree}\left(phasePointTwo,pauliTwo\right))\Rightarrow (\mathrm{CTwo}\left(rho\right)\le \mathrm{norm}\left(\mathrm{toLp}\left(1,\mathrm{WignerTwo}\left(rho\right)-g\right)\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Magic/WignerDistanceMinimum.CTwo_min (✓ std3). ∎

Source. Repository-derived.

Commentary.

$$\mathrm{CTwo}\left(rho\right)=\underset{f\in \mathrm{Wfree}\left(phasePointTwo,pauliTwo\right)}{\min }\mathrm{norm}\left(\mathrm{toLp}\left(1,\mathrm{WignerTwo}\left(rho\right)-f\right)\right)$$

For every two-qubit matrix rho, the same source minimum C(rho) := min_{W_f ∈ Wfree} ‖W_rho − W_f‖₁ is attained by some f in the compact nonempty two-qubit free polytope, and CTwo rho is no larger than every free candidate.

References

• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.COne
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.COne_min
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.CTwo
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.CTwo_min
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.PhasePoint
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.Stab
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.Wfree
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.Wigner
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.WignerOne
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.WignerTwo
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.eigenVector
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.pauliTwo
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.phasePoint
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.phasePointTwo
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.spectral
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.spectral_product_stabilizer
• Truth anchor: D5/S3/Quantum/Magic/WignerDistanceMinimum.spectral_stabilizer
• Dependency: D5/S3/Quantum/Information/BinaryStabilizerLocalInequivalence
• Dependency: D5/S3/Quantum/Information/StabilizerPairLocalUnitaryInequivalence
• Dependency: D5/S3/QuantumBounds/CHSHWitness