A sharp form of quantum thermalization asks whether the entanglement carried by an individual energy state settles to a single predictable value as the system grows, instead of scattering from state to state. It shows up in every simulation but has no general proof. This paper gives a fully self-contained analysis, proving each finite step explicitly, and it also finds a hard ceiling on how far the most natural line of attack can reach. The analysis goes in stages. It first uses an exact algebraic identity to rewrite the question as one about the fluctuations of a few simple summaries of a region's quantum state. From a single standard assumption it then proves that the entanglement of a modest, sub-linear block does settle down. The key negative result is that this size limit is not a weakness of the particular argument. It is built into any approach based on measuring distances between states, because the largest reachable block is fixed by the quality of the input assumption, and covering a full half of the system would need an input of exponentially high quality. Along the way the paper proves a sharp obstruction: a mathematically convenient stand-in for the entanglement turns out to be the worst possible target to analyze. It then develops an alternative entropy-direct route that concentrates the remaining difficulty into one clearly named leftover assumption, which simulations show already accounts for 99.7% of the effect. The paper advances the problem and, at the same time, maps its own frontier. It settles the small-block case, gives a clean formula for why the natural method stalls before it reaches the whole system, and isolates the one precisely stated leftover that any full proof still has to handle. The result reads more like a good map than a conquest. It proves what can be proved, names what cannot yet be, and marks the exact spot where the remaining work sits.
A sharp form of quantum thermalization asks whether the entanglement carried by an individual energy state settles to a single predictable value as the system grows, instead of scattering from state to state. It shows up in every simulation but has no general proof. This paper gives a fully self-contained analysis, proving each finite step explicitly, and it also finds a hard ceiling on how far the most natural line of attack can reach. The analysis goes in stages. It first uses an exact algebraic identity to rewrite the question as one about the fluctuations of a few simple summaries of a region's quantum state. From a single standard assumption it then proves that the entanglement of a modest, sub-linear block does settle down. The key negative result is that this size limit is not a weakness of the particular argument. It is built into any approach based on measuring distances between states, because the largest reachable block is fixed by the quality of the input assumption, and covering a full half of the system would need an input of exponentially high quality. Along the way the paper proves a sharp obstruction: a mathematically convenient stand-in for the entanglement turns out to be the worst possible target to analyze. It then develops an alternative entropy-direct route that concentrates the remaining difficulty into one clearly named leftover assumption, which simulations show already accounts for 99.7% of the effect. The paper advances the problem and, at the same time, maps its own frontier. It settles the small-block case, gives a clean formula for why the natural method stalls before it reaches the whole system, and isolates the one precisely stated leftover that any full proof still has to handle. The result reads more like a good map than a conquest. It proves what can be proved, names what cannot yet be, and marks the exact spot where the remaining work sits.
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.
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.
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.
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.
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.
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.