Complete written proof and exact checkers for the pure-state prime-dimensional ECQC question: it holds universally exactly at p=2; every odd prime has a full-Schmidt-rank pure-state counterexample; dimensions 3 and 5 attain the sharp pure-state ratios 3/2 and 5/2. The three-dimensional witness has a separate complete Lean proof, but the full prime-dimensional classification is not claimed Lean-complete. This record explicitly distinguishes prior mixed-state counterexamples and does not claim first priority. The fixed immutable GitHub Release is https://github.com/mxym/math/releases/tag/ecqc-pure-state-classification-v1. AI-assisted research and writing; no external funding. Existing licenses and third-party notices are retained.
Complete written proof and exact checkers for the pure-state prime-dimensional ECQC question: it holds universally exactly at p=2; every odd prime has a full-Schmidt-rank pure-state counterexample; dimensions 3 and 5 attain the sharp pure-state ratios 3/2 and 5/2. The three-dimensional witness has a separate complete Lean proof, but the full prime-dimensional classification is not claimed Lean-complete. This record explicitly distinguishes prior mixed-state counterexamples and does not claim first priority. The fixed immutable GitHub Release is https://github.com/mxym/math/releases/tag/ecqc-pure-state-classification-v1. AI-assisted research and writing; no external funding. Existing licenses and third-party notices are retained.
Complete written proofs and two exact replayable checker implementations classify all full-Schmidt-rank equality states without assuming stabilizer structure, classify every two-qudit pure stabilizer score at odd prime dimension, and determine the sharp pure-state ratio p/2 for every prime p congruent to 1 modulo 4. The general rank-deficient equality classification and the sharp ratio for primes congruent to 3 modulo 4, p at least 7, remain open in this record. This is an independently authored preprint with AI-assisted research and self-audit, not external professional peer review or a priority claim. The fixed immutable GitHub Release is https://github.com/mxym/math/releases/tag/ecqc-extremal-classification-v1. AI-assisted research and writing; no external funding. Existing licenses and third-party notices are retained.
Unrefereed mathematical candidate. Exact counterexamples to a proposed universal mixed-state total concentratable-entanglement upper bound, including full-rank noisy and genuinely tripartite-entangled families; sharp uniform and fixed-size concave-roof impurity repairs. Analytic proofs and producer-side exact arithmetic checks are provided. AI-assisted internal review does not establish external peer review, independent reproduction, formal verification, priority or impact. Original prose and data CC0-1.0; original code MIT. Source literature retains its own terms.
An explicit ternary classical counterexample to Berta-Lami-Tomamichel, arXiv:2408.15226v2 Eq. (106), at arbitrarily small distances: for every 0 < epsilon <= 1/16, the mutual-information difference is 2h(epsilon)-epsilon log 2, exceeding h(epsilon)+epsilon log 8 at exact total variation epsilon. Both marginals change; the equal-one-marginal question remains unresolved. The signed 4-page article, self-contained TeX ZIP, complete classical Lean project and existing independent verification records are included. Those records cover 38 owned declarations and 16,161 dependencies at empty-kernel trust level zero. Quantum diagonal embedding and the necessary coefficient lower bound are written arguments, not claimed formalized. This article preparation is not a fresh Lean execution, external human peer review or a verified historical priority claim. AI assisted research, formalization, review and preparation. No external funding. The original immutable GitHub releases are preserved. Related DOI 10.5281/zenodo.23253152 is an automatic whole-repository software snapshot, with its preexisting CC BY 4.0 metadata retained; this separate article series does not revoke that license. Existing licenses and third-party notices are preserved; otherwise newly unlicensed original material remains all rights reserved.
The generalized Pauli group and its normalizer, the Clifford group, have a rich mathematical structure which is relevant to the problem of constructing symmetric informationally complete POVMs (SIC-POVMs). To date, every known SIC-POVM fiducial vector is an eigenstate of an order 3 unitary in the Clifford group. I show that every order 3 unitary in prime dimensions p > 3 lies in the same conjugacy class of the Clifford group and construct a class representative for all such dimensions. It follows that if even one such SIC-POVM fiducial vector is an eigenvector of such a unitary, then all of them are (for a given such dimension). I also conjecture that in all dimensions d, the number of conjugacy classes is bounded above by 3 and depends only on d mod 9, and I support this claim with numerical evidence.
Symmetrically thermalizing unitaries exist in every dimension Initial public release of our proof of the 2019 conjecture of Bakhshinezhad, Clivaz, Vitagliano, Erker, Rezakhani, Huber, and Friis concerning symmetrically thermalizing unitaries. We prove that for every finite local dimension (d), every Hermitian Hamiltonian (H), every (\beta>0), and every (0\leq\beta'\leq\beta), there exists a global unitary (U) on (\mathbb{C}^d\otimes\mathbb{C}^d) such that both reduced states of [U(\tau_\beta\otimes\tau_\beta)U^\dagger] are exactly (\tau_{\beta'}). Equivalently, correlations between two identical finite-dimensional thermal systems can always be created at the minimum thermodynamically allowed energy cost. Included in this release Full research paper and LaTeX source Complete Lean 4 + Mathlib formalization of the all-dimensional theorem General-Hermitian-Hamiltonian theorem stu_exists_hermitian Explicit constructive proof Exact certificates and independent verification scripts Verification logs and reproducibility material Counterexample showing that the stronger arbitrary-majorization statement fails for (d\geq4) The Lean formalization contains no sorry, no added axioms, and no native_decide; the main theorem depends only on Lean's standard axioms propext, Classical.choice, and Quot.sound. This release is intended to provide a permanent, reproducible snapshot corresponding to the initial preprint. Full Changelog: https://github.com/anshM123/IQOQI-Conjecture/commits/v1.0.0
I construct a positive-operator-valued measure (POVM) which has 2d rank-1 elements and which is informationally complete for generic pure states in d dimensions, thus confirming a conjecture made by Flammia, Silberfarb, and Caves (e-print quant-ph∕0404137). I show that if a rank-1 POVM is required to be informationally complete for all pure states in d dimensions, it must have at least $3d\ensuremath{-}2$ elements. I also show that, in a POVM which is informationally complete for all pure states in d dimensions, for any vector there must be at least $2d\ensuremath{-}1$ POVM elements which do not annihilate that vector.