# Positive-temperature Bose–Einstein condensation and exact quantum depletion

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Ground-state condensation in the dilute hard-sphere gas](../../preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf)

## Scope

The formalization proves ground-state Bose–Einstein condensation in the dilute hard-sphere gas. There are absolute constants $\varepsilon_0,c_0>0$ such that, whenever the density $\rho$ and hard-sphere radius $a$ satisfy $\rho a^3<\varepsilon_0$, the condensate occupation fraction has limit inferior at least $c_0$ along every thermodynamic sequence with $N/L^3\to\rho$.

The bound covers every pure ground state, every mixed state supported on the ground space, and the normalized ground-space projection. It is uniform in the gas parameter within this range and concerns ground states, without a positive-temperature assertion.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Uniform ground-state condensation in the dilute hard-sphere gas | [HardSphere.lean](../ComparatorChallenges/HardSphere.lean) |