Isolated quantum systems never really relax. Their exact evolution keeps perfect memory, and yet the everyday quantities we measure in them do settle to steady thermal values. The leading explanation locates this puzzle inside the system's individual energy states, but it is still largely a well-supported hypothesis whose rigorous status depends heavily on what exactly one asks. Instead of chasing a new phenomenon, this paper takes one thoroughly studied benchmark chain and gathers what is genuinely known about it into a single transparent account, with every step labelled as proved, computed, or taken from the literature. The spin chain it works with is a standard one, chosen because it behaves like a generic chaotic system, and the case is built in layers. First the paper confirms by computer that the chain really is generic: its energy levels follow the universal statistics of chaotic systems, and it hides no extra conserved quantities or other structure that would spoil thermalization. On that basis it proves a weak thermalization theorem for the chain's average magnetization, showing that all but a vanishing fraction of energy states already carry the thermal value. This is done by taking established general theorems and instantiating them for the concrete model with every constant written out. The paper then looks at the tiny residual fluctuations between states and finds they carry a distinctive statistical fingerprint predicted by a modern branch of mathematics called free probability. It calibrates the whole picture against a specially solvable version of the model in which certain quantities can be computed exactly. Its genuinely new technical core is a precise algebraic identity that governs those fluctuations. The value here is discipline rather than spectacle. By taking a single well-worn model and saying which parts of its thermal behaviour are proved, which are seen only in simulation, and which are imported wholesale, the paper converts a diffuse body of belief into one honestly bookkept account. It is open about the limits. It establishes the weak form of thermalization but does not claim the stronger, exception-free version, and it does not claim a sharp bound on the fluctuation structure. Leaving those openly unfinished is part of what makes the claims it does make trustworthy.
Isolated quantum systems never really relax. Their exact evolution keeps perfect memory, and yet the everyday quantities we measure in them do settle to steady thermal values. The leading explanation locates this puzzle inside the system's individual energy states, but it is still largely a well-supported hypothesis whose rigorous status depends heavily on what exactly one asks. Instead of chasing a new phenomenon, this paper takes one thoroughly studied benchmark chain and gathers what is genuinely known about it into a single transparent account, with every step labelled as proved, computed, or taken from the literature. The spin chain it works with is a standard one, chosen because it behaves like a generic chaotic system, and the case is built in layers. First the paper confirms by computer that the chain really is generic: its energy levels follow the universal statistics of chaotic systems, and it hides no extra conserved quantities or other structure that would spoil thermalization. On that basis it proves a weak thermalization theorem for the chain's average magnetization, showing that all but a vanishing fraction of energy states already carry the thermal value. This is done by taking established general theorems and instantiating them for the concrete model with every constant written out. The paper then looks at the tiny residual fluctuations between states and finds they carry a distinctive statistical fingerprint predicted by a modern branch of mathematics called free probability. It calibrates the whole picture against a specially solvable version of the model in which certain quantities can be computed exactly. Its genuinely new technical core is a precise algebraic identity that governs those fluctuations. The value here is discipline rather than spectacle. By taking a single well-worn model and saying which parts of its thermal behaviour are proved, which are seen only in simulation, and which are imported wholesale, the paper converts a diffuse body of belief into one honestly bookkept account. It is open about the limits. It establishes the weak form of thermalization but does not claim the stronger, exception-free version, and it does not claim a sharp bound on the fluctuation structure. Leaving those openly unfinished is part of what makes the claims it does make trustworthy.
One pillar of modern physics is the idea that a sufficiently chaotic isolated quantum system looks thermal even when you examine it one energy state at a time. A sharper version asks about entanglement: does the entanglement between two halves of the system settle to a single predictable value as the system grows, instead of jumping around from state to state? For a genuinely large piece of the system this has resisted proof, because the obvious approach dissolves into an astronomically large sum of contributions. This paper shows that the whole difficulty funnels down to one clean, standard quantity, which turns an unmanageable calculation into a single sharp question. An earlier companion paper had already reduced the problem to controlling a handful of statistical quantities. Here the paper takes the decisive further step and proves that all of those quantities are governed by the size of a single object: a covariance matrix that records how the readings of local measurements vary from one energy state to the next, and in particular by that matrix's largest mode. If the largest mode shrinks as the system grows, the entanglement provably settles down. If it does not, the settling fails. The same object does double duty, since it also delivers the standard thermalization behaviour for all local measurements and fixes the size of the tiny residual fluctuations. The negative side gets equal care, through a companion obstruction result: whenever the system carries a conserved quantity that is not tied to its energy, that one mode refuses to vanish and the entanglement cannot settle. That is what separates the special non-thermalizing systems from ordinary chaotic ones. A problem that looked hopelessly tangled comes down to a single number. Rather than track an exponential explosion of interacting pieces, one only has to ask whether one mode of one matrix fades away as the system grows, and the answer settles whether a chaotic quantum system smooths itself into thermal predictability or holds on to a memory it can never erase. The paper is careful about the boundary of the claim. The reduction and its mechanism are proved and confirmed, but the last step, for a full half of the system, still rests on this one clean and clearly isolated conjecture, which the paper does not claim to have settled.
The thermalization claim comes in two strengths. The weak version says almost every energy state looks thermal, apart from a vanishing fraction. The strong version forbids exceptions entirely. What sits between them is the rare, misbehaving states, and controlling them is a central open problem. This paper takes one honest step across that gap, sharpening a statement about the vanishing fraction of exceptions into a statement about their vanishing number. The upgrade turns on a single contest between two rates. One is how fast the fluctuations that mark a state as athermal die away as the system grows. The other is how fast the number of states in the energy window multiplies. If the first outpaces the second, the actual count of exceptions cannot keep growing, and the stronger statement follows. Working inside one clean symmetry sector of the benchmark chain, and simulating systems up to eighteen particles, the paper measures the decay rate directly and finds the contest is won with room to spare. That margin holds up even at the pessimistic edge of the statistical error bars, and even after the growth rate is pushed to its largest possible value. A short chain of finite algebraic lemmas reduces the controlling inequality to one standard statistical assumption about the size of fourth-order fluctuations. Each lemma is discharged as a machine-checked certificate showing there is no way for it to fail. The hard goal of controlling every state moves one concrete rung closer once you learn to count the exceptions rather than only weigh them. The paper is careful about what remains. The result holds at a fixed tolerance rather than the sharp thermodynamic one, and it still leans on a plausible but unproven assumption about the tails of the fluctuations, whose proof from first principles is left open. This is a waypoint, not a finish line.
When a chaotic quantum system reaches equilibrium, any small piece of it should end up looking thermal, statistically indistinguishable from a patch cut out of a heat bath. Here, one benchmark chain is used to measure, in four independent ways, how close a small region actually comes to that thermal ideal and how quickly it gets there. Every finite mathematical step behind the four measures is checked by machine. The four measures complement each other. The first is a direct distance between a region's true quantum state and its ideal thermal counterpart. The second is an entropy shortfall whose sign is fixed once and for all by a provable identity, which guarantees the true state always sits on the expected side. The third is a two-part envelope that bounds how far an observable can still be wandering at any later time, so it captures equilibration over time rather than in a single state. The fourth is a one-shot probabilistic bound on how unlikely a single energy state is to stray far from the thermal value. Only one piece has fully rigorous, exact content: a clean inequality that rewrites a region's distance from thermal as a sum of simple ingredients, which simulations find to be about 88% tight, close to the best possible. Subsystem thermalization becomes four audited numbers rather than a slogan. The paper is clear about where rigor stops. The headline scalings that fall off exponentially with entropy are reported as patterns seen in simulation, not as theorems, and every claim is tagged as proved, imported, or numerical. A reader can therefore tell at a glance how much of "a small piece looks thermal" has really been pinned down, and how much still rests on the evidence of the computer.
We analyze thermalization and eigenstate thermalization in the random free fermion model, a quadratic Hamiltonian with a Gaussian Orthogonal Ensemble hopping matrix, by an exact random-matrix calculation. For a single-particle observable A we compute the ensemble average and fluctuations of Tr(Aρ(t)): we derive the relaxation envelope g2(t/τλ) with τλ=ℏ/(2ηN) and its oscillatory ∣t∣−3 tail, both properties of the semicircular limiting density, and we show that the variance of the fluctuations is O(1/N), so that the relaxation profile self-averages at fixed scaled time. Incorporating particle-number conservation, we prove a factorization theorem for the energy-shell statistics of the many-body eigenstates: the energy-independent ETH structure follows from the statistical independence of the eigenvector matrix and the spectrum, and at fixed realization the energy constraint enters only through a covariance subtraction of relative order 1/N. A controlled eigenvector--eigenvalue correlation deformation H(ε)=H0+εH1 then generates, at first order in ε, the energy dependence of the diagonal energy-resolved slope and of the off-diagonal spectral function, a single-particle diagnostic of the ETH structure in the allowed particle-hole sector. Correlation-function fluctuations and the single-particle spectral form factor finally identify the subleading O(1/N) late-time fingerprints of two-level spectral correlations. The model thus separates eigenbasis chaos from spectral chaos and identifies the statistical origin of energy-independent versus energy-dependent ETH.
Physicists have a well-tested story for why an isolated quantum system, left alone, appears to settle into equilibrium: the answer is already written into its individual energy states. That story is really a family of related claims of differing strength, and its conclusions usually get assembled by stitching together hand-written arguments, borrowed theorems, and computer simulations. In such a patchwork it is easy to lose track of what has actually been proved, what was imported, and what was only checked by example. This paper builds the first machine-verified library for the logical skeleton of the whole subject, so that its core reasoning is certified once, by a computer, and can be reused with confidence. The work first separates the parts of the thermalization story that are genuinely universal, meaning plain mathematical facts about averages, fluctuations, and counting, from the parts that depend on a particular physical model. It then formalizes the universal parts inside a proof assistant, a program that checks every logical step against its foundations and refuses to accept a gap. The resulting library collects five building blocks that until now lived scattered across separate projects. The first is a basic toolkit for reasoning about weighted averages and how quantities fluctuate. Next comes the key reduction that identifies when the fine detail of a system's entanglement smooths out, and the condition under which it does not. A third layer draws the line between the weaker claim that almost every energy state looks thermal and the stronger claim that every one does, and shows how to count the rare exceptions that flag unusual systems. A fourth gives a general recipe for how a small region of a large system relaxes toward equilibrium. The last is the backbone of the fluctuation relations that fix the direction of the second law. Each is written out in full and proved from scratch. Everything is certified two independent ways. Each core result passes through the proof assistant with no unproven steps and only minimal logical assumptions, and each numerical piece is confirmed separately by an automated theorem-checker. The paper also shows the library replacing duplicate definitions that had been reinvented across seven earlier projects, and it points to where these tools fill a real gap in the standard mathematical libraries and could be contributed back. The effect is to give a decades-old body of physics a spine that a machine can trust. Pulling out the reasoning shared by many results and proving it once, in reusable form, replaces a patchwork of arguments with a single dependable foundation. It also makes plain, for the first time, which claims stand on proof, which rest on borrowed results, and which are still open. As far as the author knows, this is the first time the mathematics of thermalization and many-body statistical physics has been brought inside a proof assistant at all.
A very fundamental problem in quantum statistical mechanics involves whether—and how—an isolated quantum system will reach thermal equilibrium after waiting a long time. In quantum systems that do thermalize, the long-time expectation value of any “reasonable” operator will match its predicted value in the canonical ensemble. The Eigenstate Thermalization Hypothesis (ETH) posits that this thermalization occurs at the level of each individual energy eigenstate; in fact, any single eigenstate in a microcanonical energy window will predict the expectation values of such operators exactly. In the first part of this dissertation, we identify, for a generic model system, precisely which operators satisfy ETH, as well as limits to the information contained in a single eigenstate. Remarkably, our results strongly suggest that a single eigenstate can contain information about energy densities—and therefore temperatures—far away from the energy density of the eigenstate.Additionally, we study the possible breakdown of quantum thermalization in a model of itinerant electrons on a one-dimensional chain, with both spin and charge degrees of freedom. This model exhibits peculiar properties in the entanglement entropy, the apparent scaling of which is modified from a “volume law” to an “area law” after performing a partial, site-wise measurement on the system. These properties and others suggest that this model realizes a new, non-thermal phase of matter, known as a Quantum Disentangled Liquid (QDL). The putative existence of this phase has striking implications for the foundations of quantum statistical mechanics.