Canonical typicality

A small piece of a big quantum system looks thermal not because anything prepared it that way, but because almost every state of the whole makes it so.

proved in corpus · proved here, no imported axiomsLean canonical_typicality_expectation

In plain terms

Here is the problem. Statistical mechanics traditionally starts with an ensemble -- an imagined collection of systems, weighted by probability, from which yours is somehow drawn. But your coffee is not an ensemble. It is one cup, in one state. Why should reasoning about imaginary collections say anything true about one actual cup?

Canonical typicality dissolves the embarrassment. Take one large system in a single definite quantum state -- no ensemble, no drawing. Look at a small piece of it. For the overwhelming majority of possible global states, the piece looks exactly thermal. You do not need to assume equilibrium statistics; you need only fail to be in an astronomically unlikely global state.

Equilibrium, on this view, is not a physical process that happened to you. It is a statement about how much room there is in the space of states, and how little of that room is occupied by exceptions.

In CSD

This is where the programme touches mainstream statistical mechanics, and the traffic goes both ways. Inbound: thermal behaviour is volume, exactly as Born weights are volume, so thermodynamics is native to the construction -- one measure does both jobs. Outbound: the literature's standing complaint about canonical typicality is that its measure is an unmotivated prior. What does most look like, and who chose the ruler? CSD has an answer nobody else has: the ruler is the substrate's own volume, with a uniqueness theorem behind it. That converts the programme's central manoeuvre into a contribution to someone else's open problem.

The corpus is precise about what it has: the expectation, and polynomial-rate concentration for diagonal statistics -- a single sample does see the thermal value, up to Chebyshev. The exponential rate is the one piece still owed. Read the next register before citing this one.

Mathematically

For a global pure state drawn from the Fubini-Study measure, the average reduced state of a tensor subsystem is exactly maximally mixed. That is the first theorem: the EXPECTATION.

The second is concentration at polynomial rate. The Fubini-Study second moments turn out to be pure symmetry algebra -- a two-coordinate Hadamard rotation, a sign flip and a quarter-phase force E[x_i^2] = 2/(N(N+1)) and E[x_i x_j] = 1/(N(N+1)) with no integral ever computed -- so every diagonal statistic has variance O(1/N) and Chebyshev makes a single sample typical (fs_chebyshev_concentration).

The literature's headline rate -- exponentially close to one -- needs Levy's lemma, concentration of measure on high-dimensional spheres, which the proof assistant's library does not carry. That deviation-rate upgrade is the one piece recorded as a named residual rather than papered over. And none of this is dynamical thermalisation, which would need mixing assumptions and is out of scope.

The name

The modern result has two independent birth certificates, both from 2006: Goldstein, Lebowitz, Tumulka and Zanghi -- the Rutgers-Bochum-Genoa axis of the Bohmian school, which had kept typicality arguments alive through decades of unfashion -- and Popescu, Short and Winter, coming from quantum information at Bristol and Cambridge. Same theorem, two vocabularies, two communities that barely cited each other.

The idea itself is older: Schrodinger sketched it in the 1920s and von Neumann proved a version in 1929 that was misunderstood, mistranslated and dismissed for eighty years before being rehabilitated. Few results have been discovered this many times.

Module
CsdLean4/Thermo/CanonicalTypicality.lean
Related
fubini study measure, von neumann entropy, born weight
Referenced
Wikipedia

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy