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
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
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 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→∞. 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.
This research release presents an analytic proof of the Caputa-Di Giulio-Loc conjecture on symmetry-resolved Krylov complexity and quantum-state spread complexity in finite dimensions. For every real time t, the total complexity satisfies C(t) ≥ Σ_q p_q C_q(t), where C_q(t) is the normalized complexity within sector q and p_q is its initial probability weight. The theorem holds for finite-dimensional Hermitian generators with orthogonal reducing sectors, including degenerate spectra and terminating Lanczos chains. It requires no assumptions of quantum chaos, spectral randomness, or late-time equilibration. The conjecture appears in “Growth of block-diagonal operators and symmetry-resolved Krylov complexity,” Physical Review Research 7, 043055 (2025), DOI: 10.1103/9v9v-54zv, and “Symmetry-resolved spread complexity,” JHEP 02 (2026), 189, DOI: 10.1007/JHEP02(2026)189. The result establishes a general relationship between full-system quantum dynamics and calculations performed separately within symmetry sectors. Its practical importance is that sector computations provide rigorous lower bounds on total complexity at every time. It also identifies precisely when resolving the symmetry leaves complexity unchanged. These conclusions are relevant to mathematical physics, operator growth, quantum many-body dynamics, and the interpretation of Krylov complexity as a diagnostic of quantum chaos. The release proves a stronger statement than the original mean-complexity inequality: the full Krylov-index distribution dominates the probability-weighted sector distribution in first-order stochastic order. Consequently, the inequality extends to every nondecreasing function of the Krylov index. Additional results include: • Two complementary proofs using nested Krylov-space projections and best polynomial approximation in spectral measures.• Concavity under mixing of normalized spectral measures.• Exact nonnegative gap identities, including a moment-Gram formulation valid for singular matrices.• Fixed-time equality criteria and a finite-dimensional characterization of equality at all times.• An explicit three-node example and reproducible numerical diagnostics.• An extension to bounded self-adjoint generators, with explicit domain and completeness assumptions for unbounded generators. The standalone release includes the PDF manuscript, editable LaTeX, complete searchable Markdown proofs, Python verification code, citation metadata, an expert review guide, and machine-readable theorem, assumption, dependency, and proof records for research discovery and AI-assisted retrieval. Research status: a complete analytic proof is supplied for the stated finite-dimensional theorem. Independent peer review and proof-assistant verification have not been completed. Worldwide novelty and priority are not certified; the unrestricted infinite-dimensional conjecture is not claimed to be resolved.
Hamiltonian recognition asks which candidate Hamiltonian generated an unknown quantum evolution when the evolution angle is not observed. This preprint solves a binary two-query qubit setting in which the two unknown angles range from independently resampled to fully shared. A task-specific symmetrization theorem reduces the full sequential optimization exactly to a three-dimensional correlation elliptope. A nine-dimensional legal subset of the most general tester dual is then shown to reduce, by semidefinite-program duality, to the same elliptope problem, yielding P_GEN(beta,eta) = P_SEQ(beta,eta) throughout the stated parameter domain. The resulting PAR-versus-GEN phase diagram contains an exact interior equality curve and an exact high-angle reentrant regime in which the globally optimal causal-processing advantage vanishes at both zero and full temporal correlation but is positive at every intermediate strength. Arbitrarily weak temporal correlation can activate a strict advantage. In this archival v1.1 release, the weak-correlation statement is conservatively formulated as explicit constructive lower bounds of orders eta^2 below 45 degrees, eta^(4/3) at 45 degrees, and eta above 45 degrees. No matching upper-bound derivation is claimed for exact asymptotic equivalence of those exponents. The record includes the main preprint, Supplemental Material, and a reproducibility archive containing proof notes, symbolic verification scripts, numerical cross-check data, revised manuscript source, figures, and integrity hashes. Status: public preprint; not independently peer-reviewed.
We report mechanized proofs, in the Lean 4 proof assistant and its Mathlib library, of Busch’s (2003) theorem on effect-valued (POVM) probability measures, together with its corollary establishing the Born rule on subspaces, and of the finite-dimensional, complex, projection-valued (PVM) case of Gleason’s theorem (n ≥ 3), together with the classical dispersion-free (nohidden-variables) corollary. All four results are verified with zero project-specific axioms: the Lean kernel reports dependence only on propext, Classical.choice, and Quot.sound, the three axioms accepted as standard throughout Mathlib. The proof of Gleason’s theorem follows the real-analytic route of Cooke, Keane and Moran (1985), with a complex reduction via real sections in the style of Dvurečenskij. The mathematical proof strategies and their Lean implementation were developed through sustained, iterative collaboration with large language models; the author’s role was to select the target theorems, orchestrate and redirect this collaboration, critically validate or reject proposed strategies, and enforce the verification discipline described in Section 4. We report this process transparently rather than as a methodological contribution.The full development is available at https://github.com/Bobart0/gleason-theorem-lean.
I show that if a finite-dimensional density matrix has strictly smaller von Neumann entropy than a second one of the same dimension (and the rank is not bigger), then sufficiently (but finitely) many tensor-copies of the first density matrix majorize a density matrix whose single-body marginals are all exactly equal to the second density matrix. This implies an affirmative solution of the exact catalytic entropy conjecture (CEC) introduced by Boes et al. [PRL 122, 210402 (2019)]. Both the Lemma and the solution to the CEC transfer to the classical setting of finite-dimensional probability vectors (with permutations of entries instead of unitary transformations for the CEC).