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.
| declaration | proof_shape | escape_witness | admission_basis |
|---|---|---|---|
| result | bind-only | none | open-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.