A stabilizer measurement beyond every maximally entangled one

Abstract

A pure three-qubit ancilla separates the information dimensions of two stabilizer measurements: two Bell pairs and local Z measurements give at least 32, whereas every maximally entangled stabilizer measurement gives at most 31. This refutes Conjecture 1 of Lo Monaco et al., arXiv:2510.00157v2.

Definition 1.1 (State vectors).

$$\forall n:\mathbb{N},\mathrm{State}\left(n\right)=((\mathrm{Fin}\left(n\right))\to \mathrm{Fin}\left(2\right))\to \mathbb{C}$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.State (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

State vectors are complex functions on the computational indices.

Definition 1.2 (Operators).

$$\forall n:\mathbb{N},\mathrm{Operator}\left(n\right)=\mathrm{Matrix}\left((\mathrm{Fin}\left(n\right))\to \mathrm{Fin}\left(2\right),(\mathrm{Fin}\left(n\right))\to \mathrm{Fin}\left(2\right),\mathbb{C}\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.Operator (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Operators are complex matrices with computational row and column indices.

Definition 1.3 (Pauli phases).

$$\forall c:\mathbb{C},\mathrm{Phase}\left(c\right)\iff ((c=1)\vee ((c=-1)\vee ((c=i)\vee (c=-i))))$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.Phase (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

The allowed scalar phases are 1, -1, i and -i; i is the imaginary unit.

Definition 1.4 (Pauli product labels).

$$\forall p:\mathrm{Pauli},\forall q:\mathrm{Pauli},\mathrm{letterProduct}\left(p,q\right)=Pauli.rec\left(q,Pauli.rec\left(Pauli.X,Pauli.I,Pauli.Z,Pauli.Y,q\right),Pauli.rec\left(Pauli.Y,Pauli.Z,Pauli.I,Pauli.X,q\right),Pauli.rec\left(Pauli.Z,Pauli.Y,Pauli.X,Pauli.I,q\right),p\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.letterProduct (✓ std3).

Source. Repository-derived.

Commentary.

The product label discards the scalar phase: equal nonidentity letters multiply to I, while two distinct nonidentity letters give the remaining letter. I is the identity label.

Definition 1.5 (Pauli product phases).

$$\forall p:\mathrm{Pauli},\forall q:\mathrm{Pauli},\mathrm{letterPhase}\left(p,q\right)=Pauli.rec\left(1,Pauli.rec\left(1,1,Complex.I,-Complex.I,q\right),Pauli.rec\left(1,-Complex.I,1,Complex.I,q\right),Pauli.rec\left(1,Complex.I,-Complex.I,1,q\right),p\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.letterPhase (✓ std3).

Source. Repository-derived.

Commentary.

The cyclic products XY, YZ and ZX have phase i; their reversals have phase -i. Identity products and squares have phase one.

Definition 1.6 (Binary coordinates of a Pauli label).

$$((\mathrm{bellInput}\left(Pauli.I\right)=(0,0))\wedge (\mathrm{bellInput}\left(Pauli.X\right)=(0,1)))\wedge ((\mathrm{bellInput}\left(Pauli.Y\right)=(1,1))\wedge (\mathrm{bellInput}\left(Pauli.Z\right)=(1,0)))$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.bellInput (✓ std3).

Source. Repository-derived.

Commentary.

The first bit records the Z component and the second bit records the X component: I gives (0,0), X gives (0,1), Y gives (1,1), and Z gives (1,0).

Theorem 1.7 (The Pauli multiplication table).

$$\forall p:\mathrm{Pauli},\forall q:\mathrm{Pauli},\mathrm{pauliMatrix}\left(p\right)\cdot \mathrm{pauliMatrix}\left(q\right)=SMul.smul\left(\mathrm{letterPhase}\left(p,q\right),\mathrm{pauliMatrix}\left(\mathrm{letterProduct}\left(p,q\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.letter_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

Multiplying two Pauli matrices gives the matrix of letterProduct, multiplied by letterPhase. This separates the label and scalar parts of each product.

Lemma 1.8 (Multiplication of Pauli words).

$$\forall n:\mathbb{N},\forall v:\mathrm{Fin}\left(n\right)\to \mathrm{Pauli},\forall w:\mathrm{Fin}\left(n\right)\to \mathrm{Pauli},\mathrm{wordOp}\left(v\right)\cdot \mathrm{wordOp}\left(w\right)=SMul.smul\left(\prod _{i:\mathrm{Fin}\left(n\right)}\mathrm{letterPhase}\left(v\left(i\right),w\left(i\right)\right),\mathrm{wordOp}\left(\lambda i:\mathrm{Fin}\left(n\right),\mathrm{letterProduct}\left(v\left(i\right),w\left(i\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.word_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any number n of qubits, multiplication is letterwise multiplication with the product of the one-letter phases as a scalar.

Lemma 1.9 (Signed commutation of Pauli letters).

$$\forall p:\mathrm{Pauli},\forall q:\mathrm{Pauli},\mathrm{pauliMatrix}\left(p\right)\cdot \mathrm{pauliMatrix}\left(q\right)=SMul.smul\left((Int.cast\left(\mathrm{sgn}\left(p,q\right)\right):\mathbb{C}),\mathrm{pauliMatrix}\left(q\right)\cdot \mathrm{pauliMatrix}\left(p\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.letter_comm (✓ std3). ∎

Source. Repository-derived.

Commentary.

The integer sign sgn(p,q) is minus one exactly when p and q anticommute; its complex cast multiplies the reversed matrix product.

Lemma 1.10 (Signed commutation of Pauli words).

$$\forall n:\mathbb{N},\forall v:\mathrm{Fin}\left(n\right)\to \mathrm{Pauli},\forall w:\mathrm{Fin}\left(n\right)\to \mathrm{Pauli},\mathrm{wordOp}\left(v\right)\cdot \mathrm{wordOp}\left(w\right)=SMul.smul\left(\prod _{i:\mathrm{Fin}\left(n\right)}(Int.cast\left(\mathrm{sgn}\left(v\left(i\right),w\left(i\right)\right)\right):\mathbb{C}),\mathrm{wordOp}\left(w\right)\cdot \mathrm{wordOp}\left(v\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.word_comm_sign (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any number n of qubits, the commutation sign is the product of the complex casts of the one-letter integer signs.

Lemma 1.11 (Trace orthogonality of Pauli words).

$$\forall n:\mathbb{N},\forall v:\mathrm{Fin}\left(n\right)\to \mathrm{Pauli},\forall w:\mathrm{Fin}\left(n\right)\to \mathrm{Pauli},Matrix.trace\left(\mathrm{wordOp}\left(v\right)\cdot \mathrm{wordOp}\left(w\right)\right)=\mathrm{ite}\left(v=w,(2:\mathbb{C}{)}^n,0\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.word_trace_pair (✓ std3). ∎

Source. Repository-derived.

Commentary.

The trace of the product of two n-qubit Pauli words is 2 to the power n when the words agree, and zero otherwise. This includes n = 0.

Definition 1.12 (The Pauli group).

$$\forall n:\mathbb{N},\forall u:(\mathrm{Operator}\left(n\right){)}^{\times },u\in \mathrm{pauliGroup}\left(n\right)\iff (\exists c:\mathbb{C},(\mathrm{Phase}\left(c\right))\wedge (\exists w:(\mathrm{Fin}\left(n\right))\to Pauli,(\mathrm{val}\left(u\right):\mathrm{Operator}\left(n\right))=c\cdot \mathrm{wordOp}\left(w\right)))$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.pauliGroup (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Appendix A, PDF page 15: “The n-qubit Pauli group Pₙ is the group generated by the n-fold tensor products of the single-qubit Pauli matrices, {I, X, Y, Z}, along with multiplicative factors of ±1, ±i.” The displayed membership gives the literal subgroup of matrix units, including its scalar phases.

Definition 1.13 (Stabilizer groups).

$$\forall n:\mathbb{N},\mathrm{StabilizerGroup}\left(n\right)=\{S:\mathrm{Subgroup}\left((\mathrm{Operator}\left(n\right){)}^{\times }\right)\mid (S\le \mathrm{pauliGroup}\left(n\right))\wedge ((\forall x:(\mathrm{Operator}\left(n\right){)}^{\times },(x\in S)\Rightarrow \forall y:(\mathrm{Operator}\left(n\right){)}^{\times },(y\in S)\Rightarrow x\cdot y=y\cdot x)\wedge ((\neg (-\mathrm{one}\left((\mathrm{Operator}\left(n\right){)}^{\times }\right)\in S))\wedge (\forall T:\mathrm{Subgroup}\left((\mathrm{Operator}\left(n\right){)}^{\times }\right),(T\le \mathrm{pauliGroup}\left(n\right))\Rightarrow \left((\forall x:(\mathrm{Operator}\left(n\right){)}^{\times },(x\in T)\Rightarrow \forall y:(\mathrm{Operator}\left(n\right){)}^{\times },(y\in T)\Rightarrow x\cdot y=y\cdot x)\Rightarrow \left((\neg (-\mathrm{one}\left((\mathrm{Operator}\left(n\right){)}^{\times }\right)\in T))\Rightarrow \left((S\le T)\Rightarrow T=S\right)\right)\right))))\}$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.StabilizerGroup (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Section II, PDF page 4: “Equivalently, a stabilizer group can be defined as a maximal Abelian subgroup of Pₙ that does not contain −I.” StabilizerGroup n is the record of a subgroup S and proofs of precisely the displayed conditions. Maximality is among Abelian Pauli subgroups excluding the negative identity, not among all Abelian subgroups.

Definition 1.14 (Common eigenvectors).

$$\forall n:\mathbb{N},\forall S:\mathrm{StabilizerGroup}\left(n\right),\forall v:\mathrm{State}\left(n\right),\mathrm{CommonEigenvector}\left(S,v\right)\iff (\forall u:(\mathrm{Operator}\left(n\right){)}^{\times },(u\in \mathrm{subgroup}\left(S\right))\Rightarrow \exists e:\mathbb{C},\mathrm{mulVec}\left((\mathrm{val}\left(u\right):\mathrm{Operator}\left(n\right)),v\right)=e\cdot v)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.CommonEigenvector (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

A vector is a common eigenvector if every matrix unit of S has an eigenvalue on that vector. The definition itself allows zero vectors; the stabilizer basis record imposes orthonormality.

Definition 1.15 (Pure normalized ancillas).

$$\forall m:\mathbb{N},\mathrm{UnitState}\left(m\right)=\{\psi :\mathrm{EuclideanSpace}\left(\mathbb{C},(\mathrm{Fin}\left(m\right))\to \mathrm{Fin}\left(2\right)\right)\mid \Vert \psi \Vert =1\}$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.UnitState (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

A pure ancilla is represented by a vector of Hilbert norm one. EuclideanSpace uses the sum-of-squared-moduli norm, rather than the maximum coordinate norm.

Definition 1.16 (The ancilla isometry).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall \psi :\mathrm{UnitState}\left(m\right),\mathrm{ancillaEmbedding}\left(\psi \right)=Matrix.of\left(\lambda z:(\mathrm{Fin}\left(n+m\right))\to \mathrm{Fin}\left(2\right),\lambda x:(\mathrm{Fin}\left(n\right))\to \mathrm{Fin}\left(2\right),\mathrm{ite}\left(Prod.fst\left(Equiv.symm\left(Fin.appendEquiv\left(n,m\right)\right)\left(z\right)\right)=x,\mathrm{val}\left(\psi \right)\left(Prod.snd\left(Equiv.symm\left(Fin.appendEquiv\left(n,m\right)\right)\left(z\right)\right)\right),0\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.ancillaEmbedding (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

The frame I tensor ket psi inserts the normalized ancilla and preserves the data inner product. It uses Matrix.kronecker with the identity and Matrix.replicateCol, reindexed by Fin.appendEquiv. Compression uses IsometricCompression.compress(U,A)=U* A U, where U* is the conjugate transpose. Val denotes the underlying UnitState vector.

Definition 1.17 (Compression to the data system).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall \psi :\mathrm{UnitState}\left(m\right),\forall A:\mathrm{Operator}\left(n+m\right),\mathrm{compress}\left(\mathrm{ancillaEmbedding}\left(\psi \right),A\right)=\mathrm{conjTranspose}\left(\mathrm{ancillaEmbedding}\left(\psi \right)\right)\cdot A\cdot \mathrm{ancillaEmbedding}\left(\psi \right)$$

Formalization. D5/S3/Quantum/Reduction/IsometricCompression.compress (✓ std3).

Source. Repository-derived.

Acknowledgement. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

IsometricCompression.compress is U* A U, with U* the conjugate transpose. Here U is ancillaEmbedding(psi)=I tensor ket psi, so this is the source’s matrix compression.

Definition 1.18 (Stabilizer bases).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\mathrm{StabilizerBasis}\left(n,m\right)=\{(G:\mathrm{StabilizerGroup}\left(n+m\right),v:((\mathrm{Fin}\left(n+m\right))\to \mathrm{Fin}\left(2\right))\to \mathrm{State}\left(n+m\right))\mid (\forall i:(\mathrm{Fin}\left(n+m\right))\to \mathrm{Fin}\left(2\right),\forall j:(\mathrm{Fin}\left(n+m\right))\to \mathrm{Fin}\left(2\right),\sum _{x:(\mathrm{Fin}\left(n+m\right))\to \mathrm{Fin}\left(2\right)}(\mathrm{star}\left(v\left(i,x\right)\right)\cdot v\left(j,x\right))=\mathrm{ite}\left(i=j,1,0\right))\wedge ((\forall i:(\mathrm{Fin}\left(n+m\right))\to \mathrm{Fin}\left(2\right),\mathrm{CommonEigenvector}\left(G,v\left(i\right)\right))\wedge (\mathrm{span}\left(\mathbb{C},\mathrm{range}\left(v\right)\right)=\mathrm{top}\left(\mathrm{Submodule}\left(\mathbb{C},\mathrm{State}\left(n+m\right)\right)\right)))\}$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.StabilizerBasis (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Section II, PDF page 4: “We will instead talk of a stabilizer basis to refer to an orthonormal basis of pure (stabilizer) states that are the common eigenvectors of some stabilizer group.” The record consists of G, the vector family v, and the three displayed proof fields. Its 2^(n+m) vectors are indexed by binary functions on Fin(n+m).

Definition 1.19 (Effective POVM elements).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall \psi :\mathrm{UnitState}\left(m\right),\forall v:\mathrm{State}\left(n+m\right),\mu \left(\psi ,v\right)=\mathrm{compress}\left(\mathrm{ancillaEmbedding}\left(\psi \right),\mathrm{rankOneDensity}\left(v\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.mu (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Section II, equation (1), PDF page 3: “μ_b = Tr_R[U† P_{Φ′b} U (𝕀 ⊗ ρ_R)] = (I ⊗ ⟨ψ|) P{Φ_b} (I ⊗ |ψ⟩)”, with “P_{Φ_b} ≡ |Φ_b⟩⟨Φ_b|”. Here v is Φ_b, the Heisenberg-evolved joint vector; rankOneDensity is the existing outer product v v*; the unitary is absorbed in v, and μ(psi,v) is precisely the second expression.

Definition 1.20 (The information dimension).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall \psi :\mathrm{UnitState}\left(m\right),\forall B:\mathrm{StabilizerBasis}\left(n,m\right),\mathrm{smu}\left(\psi ,B\right)=\mathrm{finrank}\left(\mathbb{C},\mathrm{span}\left(\mathbb{C},\mathrm{range}\left(\lambda b:(\mathrm{Fin}\left(n+m\right))\to \mathrm{Fin}\left(2\right),\mu \left(\psi ,\mathrm{vectors}\left(B\right)\left(b\right)\right)\right)\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.smu (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Section II, PDF page 3: “s_μ ≡ dim span({μ_b}_{b=1}^{n_out})”. The displayed smu denotes s_μ. The dimension is the complex finrank of the linear span of the 2^(n+m) effective matrices, allowing repeated or zero effects.

Definition 1.21 (Support in a set of qubits).

$$\forall n:\mathbb{N},\forall J:\mathrm{Set}\left(\mathrm{Fin}\left(n\right)\right),\forall u:(\mathrm{Operator}\left(n\right){)}^{\times },u\in \mathrm{supportedPauliGroup}\left(n,J\right)\iff (\exists c:\mathbb{C},(\mathrm{Phase}\left(c\right))\wedge (\exists w:(\mathrm{Fin}\left(n\right))\to Pauli,((\mathrm{val}\left(u\right):\mathrm{Operator}\left(n\right))=c\cdot \mathrm{wordOp}\left(w\right))\wedge (\forall i:\mathrm{Fin}\left(n\right),(\neg i\in J)\Rightarrow w\left(i\right)=Pauli.I)))$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.supportedPauliGroup (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

A phased Pauli word is supported in J exactly when every letter outside J is I. Support ignores the scalar phase and is defined by this literal subgroup of matrix units.

Definition 1.22 (Support only on the data qubits).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall S:\mathrm{StabilizerGroup}\left(n+m\right),\mathrm{dataSubgroup}\left(n,m,S\right)=\inf \left(\mathrm{subgroup}\left(S\right),\mathrm{supportedPauliGroup}\left(n+m,\{i:\mathrm{Fin}\left(n+m\right)\mid \mathrm{val}\left(i\right)<n\}\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.dataSubgroup (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Section IV, PDF page 7: “Sₙ, Sₘ ≤ S the subgroups of operators with support only on Hₙ and Hₘ, respectively”. Sₙ is the intersection of S with the Pauli subgroup supported in positions whose natural index is less than n.

Definition 1.23 (Support only on the ancilla qubits).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall S:\mathrm{StabilizerGroup}\left(n+m\right),\mathrm{ancillaSubgroup}\left(n,m,S\right)=\inf \left(\mathrm{subgroup}\left(S\right),\mathrm{supportedPauliGroup}\left(n+m,\{i:\mathrm{Fin}\left(n+m\right)\mid n\le \mathrm{val}\left(i\right)\}\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.ancillaSubgroup (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Section IV, PDF page 7: “Sₙ, Sₘ ≤ S the subgroups of operators with support only on Hₙ and Hₘ, respectively”. Sₘ is the intersection with the Pauli subgroup supported in positions whose natural index is at least n.

Definition 1.24 (Binary dimension of the data subgroup).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall S:\mathrm{StabilizerGroup}\left(n+m\right),\mathrm{dimData}\left(n,m,S\right)=Nat.log\left(2,Nat.card\left(\mathrm{dataSubgroup}\left(n,m,S\right)\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.dimData (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

The F₂-dimension of the finite elementary Abelian support subgroup is the base-two natural logarithm of its cardinality. Nat.log is the floor logarithm; on these power-of-two subgroup orders it is the exact binary dimension.

Definition 1.25 (Binary dimension of the ancilla subgroup).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall S:\mathrm{StabilizerGroup}\left(n+m\right),\mathrm{dimAncilla}\left(n,m,S\right)=Nat.log\left(2,Nat.card\left(\mathrm{ancillaSubgroup}\left(n,m,S\right)\right)\right)$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.dimAncilla (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

The ancilla support subgroup uses the same base-two natural logarithm convention.

Definition 1.26 (Entanglement parameter).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall S:\mathrm{StabilizerGroup}\left(n+m\right),\mathrm{entanglementP}\left(n,m,S\right)=\frac{(Nat.cast\left(n\right):\mathbb{Q})+(Nat.cast\left(m\right):\mathbb{Q})-(Nat.cast\left(\mathrm{dimData}\left(n,m,S\right)\right):\mathbb{Q})-(Nat.cast\left(\mathrm{dimAncilla}\left(n,m,S\right)\right):\mathbb{Q})}{2}$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.entanglementP (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Section IV, PDF page 7: “The parameter p quantifies the entanglement of the states and satisfies 2p = n + m − dim(Sₙ) − dim(Sₘ) and 0 ≤ p ≤ min(n, m).” The definition uses rational arithmetic for the half-difference; each natural dimension is explicitly cast to Q.

Definition 1.27 (Maximal entanglement).

$$\forall n:\mathbb{N},\forall m:\mathbb{N},\forall B:\mathrm{StabilizerBasis}\left(n,m\right),\mathrm{MaximallyEntangled}\left(B\right)\iff (\mathrm{entanglementP}\left(n,m,\mathrm{group}\left(B\right)\right)=(Nat.cast\left(\min \left(n,m\right)\right):\mathbb{Q}))$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.MaximallyEntangled (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Section IV, PDF page 7: “States are separable for p = 0 and maximally entangled for p = min(n, m).” The basis is maximally entangled exactly when its group’s rational parameter equals the natural minimum, cast to Q.

Definition 1.28 (Conjecture 1).

$$claim\iff (\forall n:\mathbb{N},\forall m:\mathbb{N},\forall \psi :\mathrm{UnitState}\left(m\right),\exists B:\mathrm{StabilizerBasis}\left(n,m\right),(\mathrm{MaximallyEntangled}\left(B\right))\wedge (\forall B^{\prime }:\mathrm{StabilizerBasis}\left(n,m\right),\mathrm{smu}\left(\psi ,B^{\prime }\right)\le \mathrm{smu}\left(\psi ,B\right)))$$

Formalization. D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.claim (✓ std3).

Citation. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

Conjecture 1, Section IV, PDF page 8: “For any pure |ψ⟩, the maximal value of s_μ can be obtained with maximally entangled S.” The encoding fixes n data qubits, m ancillas and a unit vector psi, and asks for a maximally entangled stabilizer basis B whose information dimension dominates that of every stabilizer basis B′ for the same psi.

Theorem 1.29 (A pure-state refutation).

$$\neg claim$$

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

Resolves. Problems/lo-monaco-2025-stabilizer-povm-maximal-entanglement-refutation (refuted) by D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.result.

Source. Repository-derived.

Acknowledgement. Gabriele Lo Monaco; Salvatore Lorenzo; Alessandro Ferraro; Mauro Paternostro; G. Massimo Palma; Luca Innocenti (2025). The non-stabilizerness cost of quantum state estimation. DOI: 10.48550/arXiv.2510.00157. URL: https://arxiv.org/abs/2510.00157v2.

Commentary.

For n = m = 3 take psi = (1-i, 1+i, -2, -2, 2, 2, 2+2i, 2-2i)/6 in computational order 000 through 111. Its squared norm is one. Among the 64 three-qubit Pauli words, exactly 31 have nonzero expectations. Pauli trace orthogonality and stabilizer maximality put every basis projector in the stabilizer-group span. Maximal entanglement makes the ancilla-word projection injective, so every such basis has s_mu at most 31. For the group generated by X_0 X_3, Z_0 Z_3, X_1 X_4, Z_1 Z_4, Z_2, Z_5, take two Bell transforms and the identity on the third pair. Their columns form an orthonormal common eigenbasis of a maximal stabilizer group. For each two-qubit Pauli word P, at least one expectation of P tensor I or P tensor Z is nonzero. The 32 independent data words P tensor I and P tensor Z therefore lie in its effective span, giving s_mu at least 32. Since 32 > 31, no maximally entangled basis attains the optimum for this pure ancilla.

References

• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.CommonEigenvector
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.MaximallyEntangled
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.Operator
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.Phase
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.StabilizerBasis
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.StabilizerGroup
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.State
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.UnitState
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.ancillaEmbedding
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.ancillaSubgroup
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.bellInput
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.claim
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.dataSubgroup
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.dimAncilla
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.dimData
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.entanglementP
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.letterPhase
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.letterProduct
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.letter_comm
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.letter_mul
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.mu
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.pauliGroup
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.result
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.smu
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.supportedPauliGroup
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.word_comm_sign
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.word_mul
• Truth anchor: D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.word_trace_pair
• Truth anchor: D5/S3/Quantum/Reduction/IsometricCompression.compress
• Dependency: D5/S3/Quantum/Information/SignedPauliSumNormRefutation
• Dependency: D5/S3/Quantum/PureState/PureStateHandshake
• Dependency: D5/S3/Quantum/Reduction/IsometricCompression