Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: zhu-2024-clifford-third-moment-kappa-negativity
bibkey: zhu2024thirdmoments
doi: 10.48550/arXiv.2410.13575
url: https://arxiv.org/abs/2410.13575v1
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Magic/CliffordThirdMomentNegativity.result

A negative Clifford third-moment expectation at dimension eleven

Problem

H. Zhu, C. Mao and C. Yi, Third moments of qudit Clifford orbits and 3-designs based on magic orbits, arXiv:2410.13575v1 (Commun. Math. Phys. 407, 242 (2026)), Conjecture 2: for an odd prime and , for every stochastic Lagrangian subspace , together with three aggregate inequalities that the authors derive from it. Here , and . The verbatim statements are in the literature note.

Issue #14367 targets the pointwise clause for every odd prime , every , every normalized and every .

Motivation

The coefficients expand the third moment operator of a Clifford orbit in the commutant frame ; their nonnegativity would give the paper’s conditional bounds on shadow norms and on the aggregate sums.

Gap

The authors prove (Lemma 20), the conjecture for , for stabilizer states and nonnegativity for their cubic-phase families. Issue #14367 records the literature check before any Lean: no later work exhibits a negative ; not-found-in-searched-scope.

Route

, , with , and with over (, ). Since maps to , $\kappa(\Psi,\mathcal T)=40^{-3}\sum_y\prod_k v_{y_k}\overline{v_{(Oy)_k}}=-1196/64000=-299/16000$.

Falsifier

The refutation concerns the pointwise clause as printed (every ); the aggregate inequalities are a different statement and are not refuted here.

Evidence

The canonical source is D5/S3/Quantum/Magic/CliffordThirdMomentNegativity.lean, with public claim and result : ¬ claim. The axiom closure of result is exactly propext, Classical.choice and Quot.sound; there is no sorry, native_decide or new axiom. The 1331-term Gaussian-integer sum is evaluated by kernel decide. The module statement is sha256:8532a0ef00a289544d8e4740ee71c4efe03920036ea636be7b7dca2fd58c007b, the result statement sha256:9600966d695b68a10866e2785508ddc3c245fc3c18eea03ea3890f4af1b6ec75 and the claim statement sha256:f77b58eed855b84858dd3983d641a85311fc5b754f5dca40843b4a8ca26b0e25. The Freeze event is sha256:6f1e7f1909bb5bd57dcbacf1b57dd272d84520dc0cf284c3de6f6235b4209edd; it has no project-level prerequisite (the module imports Mathlib only).

Triage

Tier 1 conjecture of an October 2024 paper (kept in the 2026 CMP version), preregistered in issue #14367 before any Lean. theorem; resolution refuted.

declarationproof_shapeescape_witnessadmission_basis
resultbind-onlynoneopen-problem-resolution

The private declarations (the subspace T, its membership criterion mem_T, stochastic_T, the state psi, norm_v, normalized_psi, gaussian_sum, kappa_T, kappa_psi) are each used on the proof of result; all are bind-only (instantiation, linear-algebra rewriting and kernel-evaluated arithmetic). The settlement is admitted as an external open-problem resolution.

Utility is kind=certified-instance; basis=refutes (the claim and its refutation). There is no digestion atom.

What the refutation shows

Proved by result: the pointwise clause of Conjecture 2 fails at , already for one qudit: .

Computed, not formalized (exact rational arithmetic over and the Gaussian integers).

  • Mechanism. For the operator is the permutation of , so . For it permutes tensor factors and ; for a non-permutation it mixes the three coordinates of the computational basis, and the overlap of with its image can be negative once the amplitudes are unequal.
  • All stochastic Lagrangian subspaces at . The stochastic orthogonal group has 24 elements, equal to , so every is a graph . For the state above the 24 values are (six permutations), (twelve) and (six); all are real.
  • What survives. For this state , and : the three aggregate inequalities of Conjecture 2 hold here, so the pointwise clause is not necessary for them.

Open. Whether the pointwise clause holds for one qudit at and is not determined here. The aggregate lower bounds fail for two qudits at ([dossier](zhu-2024-clifford-third-moment-aggregate-lower-bound.md)), where the pointwise clause fails as well.

Effect on the paper. The derivation of the aggregate inequalities “thanks to Lemma 20” from the pointwise clause no longer applies. The aggregate upper bounds are proved by Lemma 20; the aggregate lower bounds fail for two qudits at .

ASSUMED-UNVERIFIED

The bounded literature check does not establish exhaustive worldwide novelty, priority, or the absence of an independent proof.