slug: rubboli-takagi-tomamichel-2024-magic-additivity-refutation
bibkey: rubboli2024magicadditivity
doi: 10.22331/q-2024-10-04-1492
url: https://arxiv.org/abs/2307.08258v4
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Magic/RenyiBoundaryMagicAdditivityRefutation.result

The boundary α-z Rényi relative entropies of magic are not additive on three qubits

Problem

R. Rubboli, R. Takagi and M. Tomamichel, Mixed-state additivity properties of magic monotones based on quantum relative entropies for single-qubit states and beyond, Quantum 8, 1492 (2024), arXiv:2307.08258v4, define the α-z Rényi relative entropies of magic D_{α,z}(ρ) = inf over σ ∈ S̄_n of D_{α,z}(ρ‖σ) (Eq. (10)), where:

• S̄_n is the convex hull of the pure stabilizer states, the Clifford images of |0^n⟩ under the group generated by H, S and CNOT;
• D_{α,z} is the α-z Rényi divergence with the support conventions of Eq. (2).

They prove additivity for all single-qubit states on the boundary |(1 − α)/z| = 1 of the data-processing region. §5 states: “It is still an open problem whether the α-z Rényi relative entropies of magic in the range |(1−α)/z| = 1 are additive for all two and three-qubit states”. Table 1 and §10 conjecture that they are. The verbatim statements are in the literature note.

Issue #15943 fixes the reading: for every (α, z) in the region D with |(1 − α)/z| = 1, every pair of states on two or three qubits each satisfies D_{α,z}(ρ₁ ⊗ ρ₂) = D_{α,z}(ρ₁) + D_{α,z}(ρ₂).

Motivation

Additivity would reduce the magic of a product of few-qubit states to single-system computations, which the source uses for bounds on magic state distillation (§6). Its failure means that entangled stabilizer states can serve as joint references more efficiently than products of the best references for each factor.

Gap

Issue #15943 records the literature check before any Lean:

• arXiv v4 and the published version state the question;
• of the citing works, Beigi–Rubboli–Tomamichel (arXiv:2507.05696) give a sufficient condition and no three-qubit statement, and the relative-entropy nonadditivity paper (arXiv:2605.22392) treats α = z = 1, off this boundary;
• Zenodo and web searches return no settlement;
• the repository had no α-z magic result.

not-found-in-searched-scope.

Route

Let S be the sum of the seven pairwise anticommuting three-qubit Paulis XII, YII, ZXI, ZYI, ZZX, ZZY, ZZZ, so that S² = 7I.

1. The stabilizer polar is not tensor-closed (ThreeQubitStabilizerPolarEscape).
   • A Clifford conjugate of a Pauli is a Pauli up to sign, and a pure stabilizer state has Pauli expectations in {0, ±1}.
   • Two anticommuting Paulis cannot both have nonzero expectation, so Tr(ηS) ≤ 1 on S̄₃.
   • Hence W_s = (I + sS)/(1 + s) satisfies Tr(ηW_s) ≤ 1 on S̄₃ for 1/3 < s and 7s² < 1, while the three-Bell-pair stabilizer state P ∈ S̄₆ has Tr(P (W_s ⊗ W̄_s)) = (1 + 7s²)/(1 + s)² > 1.
2. The marginals (RenyiBoundaryMagicAdditivityRefutation), at (α, z) = (2, 1), where D(ρ‖η) = log₂ Tr(ρ²η⁻¹) for full-rank η.
   • Take ρ = (11I + 4S)/88 and C = ρσ⁻¹ with σ = (7I + S)/56.
   • The completed square Tr[(ρ − ηC)† η⁻¹ (ρ − ηC)] ≥ 0 and the polar bound at s = 119/316 give Tr(ρ²η⁻¹) ≥ Q = 1015/726 for every full-rank η ∈ S̄₃. Singular η gives +∞.
   • The same holds for ρ̄.
3. The product. τ = (4095/4096) σ ⊗ σ̄ + (1/4096) P ∈ S̄₆, and the rank-one inverse gives Tr((ρ ⊗ ρ̄)² τ⁻¹) = 270853390336/138572892315 < Q². So D(ρ ⊗ ρ̄) < D(ρ) + D(ρ̄).

Falsifier

The refutation would fail if the source’s stabilizer set were smaller than the convex hull of Clifford orbits of |0^n⟩ (it is not; §2), if the divergence at (2, 1) did not reduce to log₂ Tr(ρ²σ⁻¹) on full-rank σ, or if (2, 1) were outside the source’s region. The source lists 1 < α ≤ 2, α/2 ≤ z ≤ α, which contains (2, 1).

Evidence

The canonical sources are two modules.

• D5/S3/Quantum/Magic/ThreeQubitStabilizerPolarEscape.lean (797 lines):
  • definitions of qubit registers, tensor products, the generated Clifford group, pure stabilizer states, STAB, S, sigma, bell, W and gammaWords;
  • the public theorem stabilizer_polar_tensor_escape, and the public local-gate laws local_adjoint, local_identity and local_product, consumed on the proof paths of both modules.
• D5/S3/Quantum/Magic/RenyiBoundaryMagicAdditivityRefutation.lean (960 lines): the definitions SupportLE, log2, DPI, Qaz, Daz and magic; claim and result.
• They reuse the frozen StabilizerPairLocalUnitaryInequivalence Pauli words and local operators, the frozen Operator of StabilizerPovmMaximalEntanglementRefutation, IsDensity of GHZMeasureBiseparableBound, RHLinalg.rtrace, tensor_adj of BinaryStabilizerGraphNormalForm (made public here), the frozen Hadamard of NandiMutualPredictabilityLOCCRefutation, and Mathlib’s Hermitian functional calculus, CFC.inverse_eq_rpow_neg_one, convex hulls and Kronecker products.
• Both use only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.
• The escape registrations in Reg/D5/S3/Quantum/Magic/ThreeQubitStabilizerPolarEscape.lean (four, one per public theorem of the first module) and in Reg/D5/S3/Quantum/Information/BinaryStabilizerGraphNormalForm.lean (for the newly public tensor_adj, tensor_unitary, tensor_smul and gate_unitary) are declared_validated.

Frozen states:

• Golden/Frozen/state/D5/S3/Quantum/Magic/ThreeQubitStabilizerPolarEscape.lean.json, statement sha256:aea03a163d528e58c6f4490119d0c57898b1409a45f75bf7b7ef418ae1d72946;
• Golden/Frozen/state/D5/S3/Quantum/Magic/RenyiBoundaryMagicAdditivityRefutation.lean.json, statement sha256:e4f5cd2beb922aceff5c87bb3727c54e357649241b4412a39e1d53fce514b577.

Declaration statements:

• result: sha256:85b461556b71c65f84900a8d5d3fd3031093ad22faabc6e07085d93b35d48327;
• claim: sha256:182025dea3036be449a81b97d6bd69879f6393e4a7495785e22cc52ae775e5fd;
• stabilizer_polar_tensor_escape: sha256:e317cec588dace5e27d36f347e4cb1221b4aa8c31f7052fd36fee57f57899fff.

Triage

Tier 1 question of a 2024 paper, preregistered in issue #15943 before any Lean. theorem; resolution refuted.

Every other declaration is a definition used by a public statement or a bind-only private helper on the proof path of a public theorem (CLAUDE.md §3.2 「有消费的辅助声明」). The second module’s utility is certified-instance with basis refutes of claim; the first module’s is none. There is no digestion atom.

What the settlement shows

Proved by result: the statement is false. At (α, z) = (2, 1) there is a three-qubit state ρ with D_{2,1}(ρ ⊗ ρ̄) < D_{2,1}(ρ) + D_{2,1}(ρ̄).

Established inside the proofs.

• The positive polar of S̄₃ is not closed under tensor products: W_s and W̄_s lie in it, while W_s ⊗ W̄_s has expectation (1 + 7s²)/(1 + s)² > 1 on the three-Bell-pair stabilizer state (first module).
• Each marginal satisfies D_{2,1} ≥ log₂(1015/726).
• The free six-qubit state τ gives D_{2,1}(ρ ⊗ ρ̄) ≤ log₂(270853390336/138572892315) < 2 log₂(1015/726).

Argued, not formalized.

• Where additivity breaks. At (2, 1) the lower bound for each marginal comes from the polar element C² = Q·W_{119/316}: Tr(ηC²) ≤ Q on S̄₃. For three-qubit stabilizer states, |Tr(η₁S)| ≤ 1 and |Tr(η₂S̄)| ≤ 1: the module proves Tr(ηS) ≤ 1, and the same argument applied to the seven pairwise anticommuting words −P_j gives Tr(ηS) ≥ −1, likewise for S̄. Hence for a product state Tr((η₁ ⊗ η₂)(S ⊗ S̄)) = Tr(η₁S) Tr(η₂S̄) ≤ |Tr(η₁S)| |Tr(η₂S̄)| ≤ 1. On the three-Bell-pair state, however, Tr(P (S ⊗ S̄)) = Tr(S²)/8 = 7. Mixing a small weight of P into σ ⊗ σ̄ therefore lowers the joint divergence below the sum of the marginal ones.
• A family. With ρ_t = (I + tS)/8 the same argument works for every t in ((19 − 3√2)/49, 1/√7), with a t-dependent Bell weight ε (#15943 design comment). The fixed weight 1/4096 does not serve the whole interval; for example it fails at t = 151/500.
• The construction uses seven pairwise anticommuting Paulis, which exist only from three qubits on (n qubits carry at most 2n + 1). Whether the five-term analogue on two qubits also violates additivity was not checked.

Open.

• Additivity on two qubits.
• Additivity at the other boundary points, the branch z = 1 − α with α < 1, including the stabilizer fidelity (α = z = 1/2).

Effect on the paper. Table 1’s “conjecture all” for two- and three-qubit states on |(1 − α)/z| = 1 is false for three qubits at (2, 1). The §10 route through stabilizer-aligned states cannot cover all three-qubit states at this point.

ASSUMED-UNVERIFIED

The bounded literature check does not establish exhaustive worldwide novelty or priority. The statements in “Argued, not formalized” are not formalized.