Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

SYMMETRICALLY THERMALIZING UNITARIES EXIST IN EVERY DIMENSION

Ansh Mishra, Aryan Senthilkumar

Published Sep 29, 2026• 0 citations
Publisher

Abstract

Proof, machine-checked in Lean 4 with Mathlib, of the conjecture of Bakhshinezhad, Clivaz, Vitagliano, Erker, Rezakhani, Huber and Friis (J. Phys. A 52, 465303 (2019)): for every local dimension d, every Hermitian Hamiltonian H and all inverse temperatures 0 <= beta' <= beta, beta > 0, there is a global unitary on C^d (x) C^d that maps two copies of the thermal state at beta to a state whose two marginals are both thermal at beta'. Correlations between identical thermal systems can therefore always be created at the minimal energy cost. The repository contains the paper (LaTeX source and PDF), the complete Lean 4 formalisation (theorem stu_exists_hermitian), exact certificates, independent checkers and verification logs.

DOI
10.5281/zenodo.23030662

Related papers

Symmetry-driven thermalization via finite de Finetti theorems

Uttam Singh, Nicolas J. Cerf

Thermal behavior in subsystems of closed quantum systems is commonly attributed to dynamical chaos, quantum ergodicity, canonical typicality, or the eigenstate thermalization hypothesis, suggesting a fundamentally statistical origin of thermalization. Here, we propose a potential alternative mechanism in which thermal structures emerge deterministically from symmetry considerations alone, without recourse to statistical arguments. We prove a finite de Finetti-type theorem for quantum states invariant under energy-preserving unitaries, establishing that the reduced marginals of any such invariant $N$-qudit state are close (both in trace distance and relative entropy) to convex mixtures of thermal product states, with explicit error bounds vanishing as $N \to \infty$. We further present an example of energy-conserving Lindblad dynamics whose long-time limit is invariant under energy-preserving unitaries, providing a dynamical realization of the desired symmetry class. These results imply that invariance under energy-preserving unitaries suffices as a sole fundamental, deterministic principle to enforce thermal structures.

quant-pharXiv:2604.09410•Physical Review Letters•Apr 13, 2026•0 citations

SYMMETRICALLY THERMALIZING UNITARIES EXIST IN EVERY DIMENSION

Aryan Senthilkumar

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

•Sep 29, 2026•0 citations

Quantum correlations in the thermodynamic limit: the XY-model

Josep Amengual i Batle, Angel Ricardo Plastino, Angel Ricardo Plastino +1 more

We investigate thermal properties of quantum correlations in the thermodynamic limit with reference to the XY-model

arXiv:1108.2285•Aug 10, 2011•0 citations

An almost-entropic Ingleton score below -0.09738: Conditional hashing of a binary parity structure

Sm Riis

We prove an improved lower bound of 0.097387436922 on the largest normalised Ingleton violation among four-variable almost-entropic vectors. Previously reported constructions reach approximately 0.0925, used as a rounded benchmark; the best published universal upper bound is 19/124. Conditional parity hashing combines local binary parity labels, one common linear hash, simultaneous conditional privacy amplification and joint conditioning. Applied to a 24-atom source of Matúš and Csirmaz, it subtracts a multiple of the uniform-matroid rank function U(3,4) from all fifteen entropy coordinates. The limiting signed score lies in [-0.097387436923, -0.097387436922], and finite-alphabet distributions with score below -0.09738 exist. This record contains the preprint PDF, manuscript sources, Lean proof sources, exact numerical checkers, build instructions and verification evidence. The main theorem, including the closed rate interval, score enclosure and finite-alphabet existence statement, was rebuilt and kernel-checked in Lean 4.35.0-rc2 with pinned Mathlib dependencies. The finite sampler and fixed-path optimality argument are written proofs rather than separate Lean declarations. Søren Riis is the creator and coordinator and directed the research. Astra/Codex and Claude contributed mathematical development, computation and verification; Claude contributed the Lean formalisation and adversarial review. The source construction is due to Matúš and Csirmaz; the paper gives full references to the earlier entropy-region and privacy-amplification work. AI checks do not constitute independent human peer review. Licences by component: the paper PDF, LaTeX sources and original figures are CC BY 4.0; Lean sources, Python checkers and build scripts are Apache-2.0. Third-party dependencies retain their own licences. Repository: https://github.com/SR123/conditional-parity-hashing

•Oct 26, 2026•0 citations

Canonical thermalization

Peter Reimann

For quantum systems that are weakly coupled to a much 'bigger' environment, thermalization of possibly far from equilibrium initial ensembles is demonstrated: for sufficiently large times, the ensemble is for all practical purposes indistinguishable from a canonical density operator under conditions that are satisfied under many, if not all, experimentally realistic conditions.

arXiv:1005.5625•New Journal of Physics•May 28, 2010•103 citations

The exact fourth-vector feasibility wall of the canonical MUB triple in dimension six

Noah Erlwein

For the canonical product MUB triple {Z₂ ⊗ Z₃, X₂ ⊗ Q₀, Y₂ ⊗ Q₁} in dimension six, known to admit no vector unbiased to all three bases, we prove an exact two-sided theorem for the projector-space feasibility functional f, where f(v) = 1 would characterize a candidate fourth unbiased vector. We show that the global maximum of f is W = (88 + 3√6) / 100 ≈ 0.9534846923. The bound is attained by an explicit algebraic unit vector, verified entirely in exact arithmetic over the field Q(ζ₂₄, √5). Its symmetry orbit contains 72 distinct maximizing rays. The matching global upper bound f ≤ W is established via an exact positive-semidefinite certificate at the level-2 Veronese lift. The certificate consists of a symmetric matrix over Q(√2, √3), whose polynomial identity and positivity are machine-verified in exact arithmetic and closed deterministically under the triple's 432-element symmetry group. No randomized computation or floating-point arithmetic appears anywhere in the proof chain. We further prove, via exact separating functionals, that degree-4 and degree-6 sum-of-squares certificates do not exist. In this precise sense, the lift level employed is minimal and necessary. Companion results include: • an exact product-vector ceiling for aligned product triples; • the exact wall value for the second known triple; • a complete Weyl-board census in dimension six, together with a Lean 4 kernel-verified combinatorial layer. These results completely characterize the pinned canonical triple. They do not resolve the MUB(6) problem, which remains open. The deposit contains two files: (1) the manuscript (PDF); (2) a complete verification bundle (ZIP; 91 files) containing all computational modules, tests, evidence receipts, execution logs, a SHA-256 manifest, and a minimal independent verifier (verify_global_certificate.py). The verifier is implemented in standard-library-only Python, shares no code with the certificate-construction pipeline, loads the stored exact certificate matrix, and independently re-establishes both directions of the global bound in approximately 150 seconds. Reproduction is available via: make verify-global Code is released under the Apache License 2.0 (with SPDX headers throughout the bundle). The manuscript text is released under CC BY 4.0. This research made extensive use of AI systems for conjecture generation, computation, proof drafting, and adversarial review. However, no mathematical claim depends on the correctness of any AI system. Every reported result is verified by exact rational arithmetic, exact interval arithmetic, or the Lean 4 kernel, and all verification artifacts are included in the deposit.

•Jun 12, 2026•0 citations
Proof, machine-checked in Lean 4 with Mathlib, of the conjecture of Bakhshinezhad, Clivaz, Vitagliano, Erker, Rezakhani, Huber and Friis (J. Phys. A 52, 465303 (2019)): for every local dimension d, every Hermitian Hamiltonian H and all inverse temperatures 0 <= beta' <= beta, beta > 0, there is a global unitary on C^d (x) C^d that maps two copies of the thermal state at beta to a state whose two marginals are both thermal at beta'. Correlations between identical thermal systems can therefore always be created at the minimal energy cost. The repository contains the paper (LaTeX source and PDF), the complete Lean 4 formalisation (theorem stu_exists_hermitian), exact certificates, independent checkers and verification logs.
Thermal behavior in subsystems of closed quantum systems is commonly attributed to dynamical chaos, quantum ergodicity, canonical typicality, or the eigenstate thermalization hypothesis, suggesting a fundamentally statistical origin of thermalization. Here, we propose a potential alternative mechanism in which thermal structures emerge deterministically from symmetry considerations alone, without recourse to statistical arguments. We prove a finite de Finetti-type theorem for quantum states invariant under energy-preserving unitaries, establishing that the reduced marginals of any such invariant NNN-qudit state are close (both in trace distance and relative entropy) to convex mixtures of thermal product states, with explicit error bounds vanishing as N→∞N \to \inftyN→∞. We further present an example of energy-conserving Lindblad dynamics whose long-time limit is invariant under energy-preserving unitaries, providing a dynamical realization of the desired symmetry class. These results imply that invariance under energy-preserving unitaries suffices as a sole fundamental, deterministic principle to enforce thermal structures.
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
We prove an improved lower bound of 0.097387436922 on the largest normalised Ingleton violation among four-variable almost-entropic vectors. Previously reported constructions reach approximately 0.0925, used as a rounded benchmark; the best published universal upper bound is 19/124. Conditional parity hashing combines local binary parity labels, one common linear hash, simultaneous conditional privacy amplification and joint conditioning. Applied to a 24-atom source of Matúš and Csirmaz, it subtracts a multiple of the uniform-matroid rank function U(3,4) from all fifteen entropy coordinates. The limiting signed score lies in [-0.097387436923, -0.097387436922], and finite-alphabet distributions with score below -0.09738 exist. This record contains the preprint PDF, manuscript sources, Lean proof sources, exact numerical checkers, build instructions and verification evidence. The main theorem, including the closed rate interval, score enclosure and finite-alphabet existence statement, was rebuilt and kernel-checked in Lean 4.35.0-rc2 with pinned Mathlib dependencies. The finite sampler and fixed-path optimality argument are written proofs rather than separate Lean declarations. Søren Riis is the creator and coordinator and directed the research. Astra/Codex and Claude contributed mathematical development, computation and verification; Claude contributed the Lean formalisation and adversarial review. The source construction is due to Matúš and Csirmaz; the paper gives full references to the earlier entropy-region and privacy-amplification work. AI checks do not constitute independent human peer review. Licences by component: the paper PDF, LaTeX sources and original figures are CC BY 4.0; Lean sources, Python checkers and build scripts are Apache-2.0. Third-party dependencies retain their own licences. Repository: https://github.com/SR123/conditional-parity-hashing
For the canonical product MUB triple {Z₂ ⊗ Z₃, X₂ ⊗ Q₀, Y₂ ⊗ Q₁} in dimension six, known to admit no vector unbiased to all three bases, we prove an exact two-sided theorem for the projector-space feasibility functional f, where f(v) = 1 would characterize a candidate fourth unbiased vector. We show that the global maximum of f is W = (88 + 3√6) / 100 ≈ 0.9534846923. The bound is attained by an explicit algebraic unit vector, verified entirely in exact arithmetic over the field Q(ζ₂₄, √5). Its symmetry orbit contains 72 distinct maximizing rays. The matching global upper bound f ≤ W is established via an exact positive-semidefinite certificate at the level-2 Veronese lift. The certificate consists of a symmetric matrix over Q(√2, √3), whose polynomial identity and positivity are machine-verified in exact arithmetic and closed deterministically under the triple's 432-element symmetry group. No randomized computation or floating-point arithmetic appears anywhere in the proof chain. We further prove, via exact separating functionals, that degree-4 and degree-6 sum-of-squares certificates do not exist. In this precise sense, the lift level employed is minimal and necessary. Companion results include: • an exact product-vector ceiling for aligned product triples; • the exact wall value for the second known triple; • a complete Weyl-board census in dimension six, together with a Lean 4 kernel-verified combinatorial layer. These results completely characterize the pinned canonical triple. They do not resolve the MUB(6) problem, which remains open. The deposit contains two files: (1) the manuscript (PDF); (2) a complete verification bundle (ZIP; 91 files) containing all computational modules, tests, evidence receipts, execution logs, a SHA-256 manifest, and a minimal independent verifier (verify_global_certificate.py). The verifier is implemented in standard-library-only Python, shares no code with the certificate-construction pipeline, loads the stored exact certificate matrix, and independently re-establishes both directions of the global bound in approximately 150 seconds. Reproduction is available via: make verify-global Code is released under the Apache License 2.0 (with SPDX headers throughout the bundle). The manuscript text is released under CC BY 4.0. This research made extensive use of AI systems for conjecture generation, computation, proof drafting, and adversarial review. However, no mathematical claim depends on the correctness of any AI system. Every reported result is verified by exact rational arithmetic, exact interval arithmetic, or the Lean 4 kernel, and all verification artifacts are included in the deposit.