Convex-Gaussianity of fermionic Gibbs states in perturbation theory
Kaifeng Bu, Yuanjie Ren
quant-ph
Sep 9, 2026 · v1
cond-mat.str-el math-ph
TL;DR
The authors report a Lean 4 formalization of their results, implemented with assistance from OpenAI's Codex.
Abstract
We study the structure of Gibbs states in weakly perturbed interacting fermionic systems. First, for a sparse Hamiltonian $H=H_0+V$ with a quadratic term $H_0$ and a non-quadratic perturbation $V$ of scale $ε$, we show that the Gibbs state $ρ_β$ decomposes into a convex combination of Gaussian states whenever the inverse temperature satisfies $β\le O(\log(1/ε))$. Moreover, we prove that this bound is asymptotically tight by establishing that $β\le Θ(\log(1/ε))$ is necessary for certain sparse Hamiltonians. This general framework applies directly to the weak-coupling (small-$\vert{}U\vert{}$) regime of the Fermi–Hubbard model with hopping $t$ and on-site interaction $U$ on any graph of maximum degree $D$. Complementarily, in the strong-coupling (small-$\vert{}t\vert{}$) regime, we show that the Gibbs state remains convex-Gaussian up to $β\le O\big(\vert{}U\vert{}^{-1}\log(\vert{}U\vert{}/(D\vert{}t\vert{}))\big)$, revealing a mechanism for convex-Gaussianity distinct from the weak-coupling setting.
Problem
The work asks when Gibbs states of weakly perturbed interacting fermionic systems are convex combinations of fermionic Gaussian states (convex-Gaussian). This matters for classical simulability and for non-Gaussian resource theory.
Approach
For sparse Hamiltonians H=H0+V, with H0 quadratic and V a non-quadratic perturbation of scale ε, the interaction-picture expansion is written exactly in the Majorana basis. A support-decoupling construction then expresses e^{-βH} as an expectation over products of terms I+αγ_J, each of which lies in the Gaussian cone. A separate argument treats the strong-coupling regime of the Fermi–Hubbard model around the atomic limit. Part of the derivations and a Lean 4 formalization were carried out with Codex assistance.
Results
Gibbs states are convex-Gaussian for β ≤ O(log(1/ε)), and this bound is asymptotically tight for some sparse Hamiltonians. The result applies to the weak-coupling Hubbard model. In the strong-coupling regime, convex-Gaussianity holds for β ≤ O(|U|^{-1} log(|U|/(D|t|))).
