A stabilizer measurement exceeds every maximally entangled one

G. Lo Monaco, S. Lorenzo, A. Ferraro, M. Paternostro, G. M. Palma and L. Innocenti, The non-stabilizerness cost of quantum state estimation, arXiv:2510.00157v2, Section IV, Conjecture 1 (PDF page 8), state:

For any pure |ψ⟩, the maximal value of s_μ can be obtained with maximally entangled S.

For n data qubits and m ancillas, a stabilizer measurement is an orthonormal common-eigenvector basis of a maximal Abelian Pauli subgroup excluding −I. Its effective effects are μ_b = (I⊗⟨ψ|)|Φ_b⟩⟨Φ_b|(I⊗|ψ⟩), and s_μ is the complex dimension of their linear span. The source defines 2p = n+m−dim(S_n)−dim(S_m), where S_n and S_m are the data-supported and ancilla-supported subgroups. Maximal entanglement means p=min(n,m). The formal claim retains all n,m and all pure normalized ancillas and compares every stabilizer basis for the same ancilla.

The frozen declaration D5/S3/Quantum/Measurement/StabilizerPovmMaximalEntanglementRefutation.result refutes this universal claim. At n=m=3, one pure ancilla has only 31 nonzero Pauli expectations. Every maximally entangled stabilizer measurement has s_μ≤31, whereas a basis with two Bell pairs and a local Z measurement on the third pair has s_μ≥32.

Issue #11467 preregisters the Tier 1 source statement, full quantifiers, literature check and proposed counterexample before the Lean probe. The source's Conjecture 1 remains a conjecture in the directly read v2 text. The issue's citing-work check reports arXiv:2608.14798, 2607.19070, 2604.12441 and 2510.13950 as background citations without a settlement. That citing-work scan is orchestrator-reported; the source reading and formalization do not establish an exhaustive literature absence or priority.

Take ψ=(1−i,1+i,−2,−2,2,2,2+2i,2−2i)/6 in computational order 000,…,111. Exact Gaussian-integer arithmetic certifies its squared norm as one and its Pauli support cardinality as 31. Pauli trace orthogonality and subgroup maximality place every stabilizer-basis projector in its group span. For a maximally entangled basis, projection onto ancilla Pauli labels is injective; the frozen IsometricCompression.compress(ancillaEmbedding(ψ), A) therefore bounds the effective span by the ancilla support. The ancilla frame uses Mathlib Matrix.kronecker and Matrix.replicateCol with the concatenated indices.

Conjugating the computational basis by two Bell transforms gives a genuine stabilizer basis for the group generated by X_0X_3, Z_0Z_3, X_1X_4, Z_1Z_4, Z_2 and Z_5. For every two-qubit Pauli word P, at least one expectation of P⊗I or P⊗Z survives. Hence all 32 independent data words P⊗I and P⊗Z belong to its effective span. The inequality 32>31 contradicts the claimed optimum.

The refutation requires a bound for every maximally entangled basis, not only sampled Bell bases. It also requires a normalized pure ancilla, actual Pauli subgroups with the source's maximality and exclusion conditions, an orthonormal complete common eigenbasis, and linear independence of the 32 effective data operators. These obligations are proved on the live path of result; no conjectural subgroup-size or injectivity assumption is supplied as a hypothesis. The conclusion is ¬ claim with no added assumptions.

The canonical Lean module and its Scribe mirror carry 19 authored public definitions, including claim, and the single settling theorem result. The kernel checks the finite Gaussian-integer expectation table and the structural support and span arguments. Reproduction:

make lean LEAN_TARGETS=D5.S3.Quantum.Measurement.StabilizerPovmMaximalEntanglementRefutation

The proof uses only propext, Classical.choice and Quot.sound; it adds no axiom and uses no sorry or native_decide. The Scribe resolution is Refuted, attached to the frozen settling declaration.

Tier 1 externally published named conjecture, preregistration #11467; resolution refuted. The public theorem has proof_shape: content and admission_basis: open-problem-resolution. Utility is kind=certified-instance; basis=refutes, with typed claim and result.

What the settlement shows

Proved in this module: for equal data and ancilla sizes, maximal entanglement forces an injective ancilla Pauli-label map and thus a support-count upper bound. The explicit basis admits 32 independent data operators although the ancilla has support 31. Reduced entanglement permits different data operators to share surviving ancilla labels; counting those labels alone cannot bound every stabilizer measurement. The equal-size support bound for maximally entangled bases survives and is used to prove the refutation.

Computed: the binary group generated by these six operators has 64 elements, with two data-only and two ancilla-only elements. Thus its source parameter is p=(6−1−1)/2=2. This parameter computation is independent evidence, not a separately exposed kernel-certified theorem. The following command returns 64 2 2:

python3 -c 'from itertools import product; from functools import reduce; from operator import xor; g=[9,576,18,1152,256,2048]; G={reduce(xor,(v for b,v in zip(s,g) if b),0) for s in product(range(2),repeat=6)}; print(len(G),sum(v&3640==0 for v in G),sum(v&455==0 for v in G))'

Bits 0,…,5 encode X labels and bits 6,…,11 encode Z labels; qubits 0,…,2 are data and 3,…,5 are ancillas. Masks 3640 and 455 select the ancilla and data coordinates respectively.

Literature-attested: Appendix D, Example 8 reports the maximally entangled case for n=m=2. That example is not invalidated by a counterexample at n=m=3; its separate source calculation is not proved here. The source's derived results that do not assume Conjecture 1 retain their stated hypotheses. Any use of Conjecture 1 to restrict a global search to maximally entangled measurements loses that justification.

Open: the global optimum for this ancilla, minimal counterexample size, robustness under perturbations, a structural criterion for when maximal entanglement is optimal, and Conjecture 2. These require separate literature and admission checks and are not added as declarations to this module.

The Lean kernel does not authenticate the external publication or establish exhaustive novelty. The citing-work literature scan is orchestrator-reported. Information-escape registration is paused under CLAUDE.md §3.9.