Bose gases: condensation, quantum depletion, and momentum profiles

Source and verification

This article explains family 267 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ Condensation and the one-particle density matrix

Family 267 studies three-dimensional dilute Bose gases with a fixed interaction, followed first to infinite volume and then, where needed, to small density. Its five manuscripts address positive condensate fractions, positive temperature, the leading quantum depletion, and the distribution of depleted particles in momentum. The distinction between those conclusions is essential: an accurate energy estimate alone does not determine occupation of a single orbital. (OpenAI, 2026) (OpenAI, 2026b) (OpenAI, 2026c) (OpenAI, 2026a) (OpenAI, 2026c)

The prerequisites are Hilbert spaces, quadratic forms, partial traces, Fourier series, elementary probability, and Brownian motion. We introduce the occupation observables and the elementary comparison inequalities before describing the research arguments.

Let ${\Lambda }_L=(\mathbb{R}/L\mathbb{Z}{)}^3$ be the periodic box of volume $V=L^3$. A bosonic wave function is a symmetric function of $N$ particle positions. A state $\Gamma$ is a positive trace-one operator on that symmetric Hilbert space. Its one-particle density matrix is

$$\begin{array}{c}{\gamma }_{\Gamma }^{(1)}=N{\mathrm{Tr}}_{2,\dots ,N}\Gamma ,\\ \mathrm{Tr}{\gamma }_{\Gamma }^{(1)}=N.\end{array}$$

For normalized plane waves $u_{k,L}(x)=L^{-3/2}{e}^{ik\cdot x}$, with $k\in (2\pi /L){\mathbb{Z}}^3$, set

$$\begin{array}{c}{n}_{\Gamma }(k)=⟨u_{k,L},{\gamma }_{\Gamma }^{(1)}{u}_{k,L}⟩,\\ B_{\Gamma }=\frac{n_{\Gamma }(0)}{N},\sum _k{n}_{\Gamma }(k)=N.\end{array}$$

Here $B_{\Gamma }$ is the constant-orbital condensate fraction, and $1-B_{\Gamma }$ is its depletion. A positive lower limit of $B_{\Gamma }$ establishes macroscopic occupation of this specified mode. The formulation does not require an individual ground vector to be translation invariant.

For a normalized pure vector $\Psi$, with $Y$ denoting the other $N-1$ positions, partial tracing gives the useful identity

$$B_{\Psi }=\frac{1}{V}\int {\left|{\int }_{{\Lambda }_L}\Psi (x,Y)dx\right|}^{2}dY.$$

It measures coherent addition over all possible positions of one particle while retaining exactly the same bath $Y$. Controlling the position density $|\Psi {|}^2$ at one point is therefore insufficient.

🏷️ Hard cores, bounded repulsion, and the order of limits

For hard spheres, fix an exclusion distance $a>0$ and allow only configurations with periodic distances $d_L(x_i,x_j)>a$. The Hamiltonian is defined by the quadratic form

$$q[\Psi ]=\sum _{i=1}^N{\int }_{{\Omega }_{N,L,a}}|{\nabla }_i\Psi {|}^2,$$

on symmetric $H_0^1({\Omega }_{N,L,a})$ functions. The zero boundary condition enforces the impenetrable core. Wave functions are extended by zero to the full torus before taking partial traces. In the units ${\hslash }^2/(2m)=1$, the kinetic operator is $-{\sum }_i{\Delta }_i$. The parameter $a$ is also the scattering length, since the exterior zero-energy two-body scattering solution is $1-a/|x|$. It is the distance excluded between centers, rather than the physical radius of each sphere.

The other interaction class consists of fixed bounded, measurable, nonnegative, radial potentials $v$ of finite range, nonzero on a set of positive measure. Periodizing $v$ gives $v_L$, and

$$\begin{array}{rl}{H}_{N,L}^v=& \sum _i(-{\Delta }_i)\\ & +\sum _{i<j}{v}_L(x_i-x_j).\end{array}$$

Its scattering length $a_v>0$ is defined by the radial solution of $(-\Delta +v/2)f=0$ with $f(x)=1-a_v/|x|$ outside the support. Neither radial monotonicity nor nonnegativity of the Fourier transform is assumed. The potential remains fixed as $N$, $L$, and later the density change. (OpenAI, 2026e) (OpenAI, 2026a)

A thermodynamic sequence has $N,L\to \infty$ with $N/L^3\to \rho >0$. For hard spheres the dimensionless gas parameter is $\eta =\rho a^3$; for bounded potentials it is $\rho a_v^3$. In the depletion results, the thermodynamic limit is taken at each fixed density before dilution $\rho \downarrow 0$. This permits arbitrarily large volumes at each positive density. It is not a statement restricted to boxes whose size is tied to dilution.

Manuscript	State and interaction	Claimed conclusion
Ground-state hard spheres	Every pure or mixed ground-space state	A positive fraction uniform for sufficiently small $\rho a^3$
Positive-temperature hard spheres	Exact canonical Gibbs state	A positive fraction at a fixed $T(a,\rho )>0$
Density-uniform condensate bound	Fixed bounded repulsion, $0\le T\le {\rho }^2$	A positive fraction uniform over the admitted densities and temperatures
Hard-sphere depletion and momentum	Every pure or mixed ground-space state	Leading depletion and full scaled momentum measure
Bounded-potential depletion	Fixed bounded repulsion, ground states	Leading total depletion

For the ground-state hard-core result, the source gives absolute constants ${\epsilon }_0,c_0>0$: every fixed $a,\rho$ with $\rho a^3<{\epsilon }_0$ and every thermodynamic sequence have $\mathrm{liminf}{B}_{\Gamma }\ge c_0$, uniformly over ground-space states. This first result does not assert that the fraction tends to one. (OpenAI, 2026c)

For bounded repulsion, there are ${\rho }_{\ast }(v),c_{\ast }(v)>0$ such that, for each $0<\rho <{\rho }_{\ast }(v)$, all sufficiently large $L$, all $N$ with $\rho /2\le N/L^3\le 2\rho$, and every $0\le T\le {\rho }^2$, one has $B_{\Gamma }\ge c_{\ast }(v)$. The volume threshold may depend on $\rho ,v$; the positive fraction does not depend on $\rho$ within the stated range. At positive temperature $\Gamma =e^{-H/T}/\mathrm{Tr}(e^{-H/T})$, with $k_B=1$. Bounded repulsion has a unique finite-volume ground state by positivity improvement of its heat semigroup. (OpenAI, 2026a)

The hard-core thermal theorem instead states existence of a suitable positive temperature at each sufficiently small fixed density. It does not determine the critical temperature or claim the same temperature interval as the bounded-potential result. (OpenAI, 2026b)

🏷️ The depletion coefficient and momentum profile

For hard spheres, define a finite measure on rescaled momentum space by

$${\sigma }_{\Gamma ,L}=\frac{1}{N\sqrt{\eta }}\sum _{k\ne 0}{n}_{\Gamma }(k){\delta }_{k/\sqrt{8\pi \rho a}}.$$

Here ${\delta }_t$ denotes unit point mass at $t$, and $\rho$ is the fixed limiting density. The target Bogoliubov measure is

$$\begin{array}{c}g(t)=\frac{|t{|}^2+1}{2\sqrt{|t{|}^4+2|t{|}^2}}-\frac{1}{2},\\ {\nu }_{\mathrm{Bog}}(dt)=\frac{(8\pi {)}^{3/2}}{(2\pi {)}^3}g(t)dt.\end{array}$$

Claimed hard-sphere momentum limit

For each bounded continuous real function $f$ and each $ϵ>0$, sufficiently small fixed density ensures that, along every thermodynamic sequence, the upper limiting error $|\int fd{\sigma }_{\Gamma ,L}-\int fd{\nu }_{\mathrm{Bog}}|$ is at most $ϵ$, uniformly over all density matrices supported on the ground space. The density threshold may depend on $a,f,ϵ$. (OpenAI, 2026d)

This controls all thermodynamic accumulation values; it does not require the occupation to have a unique thermodynamic limit at a fixed positive gas parameter. Taking $f=1$ gives, in this iterated sense,

$$1-B_{\Gamma }=\frac{8}{3\sqrt{\pi }}\sqrt{\rho a^3}+o(\sqrt{\rho a^3}).$$

The bounded-potential companion claims this same total depletion formula with $a_v$ replacing $a$, with the potential fixed throughout both limits. Its headline theorem concerns total depletion rather than the full momentum-measure assertion above. (OpenAI, 2026e)

The profile is defined for $t\ne 0$; its value at the origin does not affect the measure. Its coefficient can be checked directly. Positivity follows because $(r^2+1{)}^2-(r^4+2r^2)=1$. Also $g(r)=O(r^{-1})$ near zero and $O(r^{-4})$ at infinity, both integrable against the three-dimensional volume element. An antiderivative of $r(r^2+1)/\sqrt{r^2+2}-r^2$ is

$$\begin{array}{rl}G(r)=& \frac{(r^2+2{)}^{3/2}-r^3}{3}\\ & -\sqrt{r^2+2}.\end{array}$$

Since $G(0)=-\sqrt{2}/3$ and $G(r)\to 0$ at infinity, ${\int }_0^{\infty }{r}^{2}g(r)dr=\sqrt{2}/6$. Radial integration with the displayed normalization yields ${\nu }_{\mathrm{Bog}}({\mathbb{R}}^3)=8/(3\sqrt{\pi })$. Computing this integral checks the coefficient of the proposed limit; it does not prove convergence of the many-particle states.

🏷️ Why energy leaves a long-wavelength problem

The first nonconstant plane wave has kinetic energy $(2\pi /L{)}^2$, which vanishes in the thermodynamic limit. An energy surplus can therefore be consistent with a large occupation in very low nonzero momenta. A scalar ground-energy expansion, even through the Lee–Huang–Yang correction, cannot by itself settle condensation.

Partition the torus into cubes of side $\ell$. Let $P_{\ell }$ project one-particle functions onto the functions constant on each cube, and let $P_0$ project onto the single global constant. Since $P_0\le P_{\ell }$, orthogonality gives

$$\begin{array}{rl}1-B_{\Psi }=& ⟨\Psi ,(1-P_{\ell }{)}_1\Psi ⟩\\ & +\Vert (P_{\ell }-P_0{)}_1\Psi {\Vert }^2.\end{array}$$

The subscript means that the projection acts on the first particle. The first term measures variation inside cubes; the second measures disagreement between cube averages over the whole sample.

The depletion papers retain positive operators measuring local Bogoliubov excitations in their energy lower bounds. Comparing them with the matching energy upper bound controls occupation observables, not just the total energy. For hard spheres, the extracted local covariance estimate applies to arbitrary complex one-particle contractions sandwiched between local excitation projections. This is stronger than a statement about diagonal momentum occupations and is needed later for translations. The local inputs involve Neumann restrictions, scattering-length normalization, and quantitative remainder estimates; they are substantial parts of the manuscripts’ proofs. (OpenAI, 2026d) (OpenAI, 2026e)

The second projection term needs a comparison uniform in the total volume. That is the purpose of the probabilistic constructions.

🏷️ Common baths, path changes, and overlap

First take a normalized nonnegative ground function $\Phi$. Its occupation is an integral of $\Phi (x,Y)\Phi (y,Y)$ with the same bath at both tagged positions. A stationary Brownian-path representation has position marginal ${\Phi }^2$. Short portions of paths can be resampled, with hard cores imposed by avoidance of other trajectories.

Along a route through cells, choose particle labels and construct two midpoint assignments. Each selected particle moves from its departure cell in one assignment to the next cell in the other. At an intermediate cell, the arriving and departing labels share the same midpoint across the two copies. Deleting the initial tag in one copy and the terminal tag in the other therefore leaves exactly the same observed bath. The outer endpoints of each path are retained. (OpenAI, 2026c)

The final overlap estimate has an elementary form. For finite measures $P,Q$ with densities $p,q$ relative to a common dominating measure, define their affinity by $\mathcal{A}(P,Q)=\int \sqrt{pq}$. If a common measure $\nu$ has mass $m>0$ and

$$\begin{array}{c}\int {\left(\frac{d\nu }{dP}\right)}^{2}dP\le C_P,\\ \int {\left(\frac{d\nu }{dQ}\right)}^{2}dQ\le C_Q,\end{array}$$

then $\mathcal{A}(P,Q)\ge m^2/\sqrt{C_P{C}_Q}$. Indeed, with $s$ the density of $\nu$, Hölder with exponents $4,4,2$ applied to

$$s=(s^2/p{)}^{1/4}(s^2/q{)}^{1/4}(pq{)}^{1/4}$$

gives $m\le C_P^{1/4}{C}_Q^{1/4}\mathcal{A}(P,Q{)}^{1/2}$. Absolute continuity permits setting the ratios to zero on zero-density sets.

The hard-core manuscript constructs such a common measure for many distant cell pairs. In scaled units, a cell contains order $D$ particles. Splitting labels into order $D$ disjoint groups offsets a factor $1/D$ in the tagged-particle normalization, leaving a fixed positive overlap contribution.

The difficult estimate concerns the likelihood of the path change. Paying a fixed loss at every step of a long route would destroy the bound. Instead the construction averages the likelihood over random routes before taking its second moment. Two independently sampled routes in the same exposed environment appear in that moment. Exact conditional normalizers cancel away from encounters between the routes, leaving a cost controlled by encounter counts and shared particle choices.

Joint bounds on defective cells are needed here; individual one-cell probability estimates do not suffice. Routes detour around defective clusters, and their selection depends on the environment. The manuscripts retain those selection weights and prove encounter bounds for the resulting comparison. Independence of a route from the gas, or independence of interacting bridges, is not assumed.

For the bounded-potential thermal argument, the comparison is phrased using an opened-path measure $\mu$ of total mass $B_{\Gamma }$. A constructed measure $\nu \ll \mu$ has mass at least $m_{\ast }>0$ and density with bounded second moment. Cauchy–Schwarz yields $m_{\ast }^2\le B_{\Gamma }\int (d\nu /d\mu {)}^{2}d\mu$. Reverse insertion supplies the cancellation needed to make that second moment uniform in route length and volume. (OpenAI, 2026a)

🏷️ From deletion measures to the depletion scale

Positive overlap is enough for a constant fraction. The precise depletion law needs errors smaller than $\sqrt{\eta }$. For a cell $A$ and a nonnegative ground function, introduce a finite measure on baths with density

$$s_A(Y{)}^2=\frac{V}{|A|}{\int }_A\Phi (x,Y{)}^{2}dx.$$

Its mass is the expected number of particles in $A$ divided by $(N/V)|A|$. It need not be one for each cell, although it averages to one over equal-volume cells. This is a smoothed particle-deletion measure: the tagged position is integrated out while the bath remains.

Distant comparisons control differences of the root mean squares $s_A$. The projection $P_{\ell }$, however, involves arithmetic averages of $\Phi$. The local fourth-moment estimate bridges these quantities. For a finite nonnegative array $y_i$, let $a={\mathbb{E}}_i{y}_i^2$ and $m={\mathbb{E}}_i{y}_i$. Then

$$(\sqrt{a}-m{)}^2\le \frac{1}{2}{\mathbb{E}}_{i,i^{\prime }}\frac{(y_i-y_{i^{\prime }}{)}^4}{y_i^2+y_{i^{\prime }}^2},$$

with $0/0=0$. To prove it, write the double average on the right before its factor $1/2$ as $Q$. Weighted Cauchy–Schwarz gives $4(a-m^2{)}^2\le 2aQ$. Dividing by $4(\sqrt{a}+m{)}^2\ge 4a$ proves the bound when $a>0$; the zero case is immediate.

Apply this inside larger cells, then use a fine-scale occupation bound to compare each small-cell root mean square with the actual average of $\Phi$. A separate second-moment comparison between distant cells makes their root mean squares nearly constant across the sample. A discrete Fourier argument converts control over a positive proportion of distant displacement pairs into a bound on the full spatial variance. Together these estimates make $\Vert (P_{\ell }-P_0{)}_1\Phi {\Vert }^2=o(\sqrt{\eta })$. (OpenAI, 2026d)

The quantitative route construction keeps portions near the common endpoint unchanged in the copy used to measure the likelihood error. Encounters of the changed portions can then become rare enough for the depletion scale. Bounded repulsion uses the same division into local and distant estimates, with additional control of particle counts. A Boltzmann pair weight $b(\omega )\in [0,1]$ can be written as ${\int }_0^1{1}_{\{u\le b(\omega )\}}du$. This converts the soft interaction into an auxiliary indicator constraint without changing the path marginal. Conditional on the paths, the retained auxiliary variable is uniform on $[0,b(\omega )]$; it is not an independent uniform variable on $[0,1]$. Its value and the conditional normalizer stay in subsequent comparisons. (OpenAI, 2026e)

🏷️ Complex vectors and positive temperature

The hard-core configuration space is not assumed connected. Although equality in the kinetic modulus inequality forces the phase of a ground vector to be constant on each connected component, it need not give a single global phase. The first ground-state condensation paper handles this by fixing the bath and retaining a large region of the allowed one-particle slice whose points communicate through allowed paths. Covering forbidden balls by small cubes and filling bounded pockets produces that region. Joint close-particle estimates control its discarded volume fraction, averaged over the bath law. If that fraction is ${\delta }_{\mathrm{geom}}$, the phase-transfer estimate is

$$B_{\Psi }\ge B_{|\Psi |}-4\sqrt{{\delta }_{\mathrm{geom}}}.$$

The dilution threshold is chosen after the positive modulus bound so this loss is small enough. (OpenAI, 2026c)

The sharper depletion proof uses a different extension. The positive and negative parts of a real ground vector are themselves ground vectors when nonzero: their norms and Dirichlet energies add, and equality of the total Rayleigh quotient forces equality for each part. Splitting real and imaginary parts therefore expresses a complex ground vector using at most four nonnegative ground vectors. Cauchy–Schwarz loses at most a fixed factor in the vanishing long-wavelength error. Uniform pure-state estimates pass to mixed ground-space states by convexity. (OpenAI, 2026d)

At positive temperature, replace the wave function by the nonnegative kernel $\Phi (X,W^{\prime })$ of ${\Gamma }^{1/2}$. Factoring the Gibbs kernel gives

$$\begin{array}{c}M(Y,W^{\prime })=\int \Phi (x,Y,W^{\prime })dx,\\ B_{\Gamma }=\frac{1}{V}\int M(Y,W^{\prime }{)}^{2}dYd{W}^{\prime }.\end{array}$$

The additional configuration $W^{\prime }$ must remain the same in both factors. A short Brownian slab realizes the squared kernel as a joint midpoint law; exact heat-kernel composition proves its normalization. Thermal entropy and free-energy estimates supply joint spatial and trajectory bounds in place of ground-state estimates. (OpenAI, 2026b)

The temperature is fixed before the volume limit. For example, the hard-core proof chooses a fixed constant ${\alpha }_0>0$ and physical scales

$$\begin{array}{c}{s}_{\infty }=\sqrt{\frac{{\alpha }_0}{a\rho }},D_{\infty }=\frac{{\alpha }_0^{3/2}}{\sqrt{\rho a^3}},\\ T_{\mathrm{phys}}=\frac{1}{4s_{\infty }^2{D}_{\infty }}>0.\end{array}$$

Rescaling length by $s_{\infty }$ explains the temperature factor $s_{\infty }^2$. Along density-convergent finite-volume approximations the scaled product $DT$ tends to $1/4$, within the admitted low-temperature range. Every quantity in the displayed physical choice depends on the fixed $a,\rho$, not the total volume.

🏷️ Recovering the full momentum measure

For translation $(T_{h}f)(x)=f(x+h)$, the plane wave $u_k$ is an eigenvector with eigenvalue $e^{ik\cdot h}$. Thus expectations of translations are Fourier transforms of momentum occupation measures. After the long-wavelength contribution is removed, the local covariance estimate can be applied to translations restricted to larger boxes.

A single fixed partition may cut many translations at its faces. Average instead over shifts of the large-box partition while retaining a finer cell grid. For large-box side $b$, fine-cell side $\ell$, and $|h|\le H$, the proportion of shifts separating a point from its translate is at most $C(H+\ell )/b$. This follows by counting possible separating faces in each coordinate and taking a union bound. It gives the same bound in operator norm for the difference between the full translation and the average of its within-box restrictions.

Sandwiching that difference between local excitation projections makes its expectation proportional to the depleted occupation, rather than the full particle number. This factor is essential at the chosen scales. The local covariance formula and Neumann-mode Riemann sums then identify the limiting Fourier transform. Compactly supported tests follow by Fourier inversion. Positivity and convergence of total mass control the tails, extending convergence to every bounded continuous test function. This final step distinguishes the full momentum theorem from merely a calculation of total depletion. (OpenAI, 2026d)

🏷️ Key steps and proof outlines

Retained excitation energy controls complex observables

The hard-sphere depletion paper makes the energy-to-occupation step quantitative. In a local box, write the inverse Bogoliubov transformation as

$$a_p=U_p{b}_p+V_p{b}_p^{\ast }.$$

Here $a_p$ annihilates an ordinary nonconstant mode, whereas $b_p$ annihilates a transformed quasiparticle. Let

$$\mathcal{Q}=\sum _{p\ne 0}{\tilde{D}}_p\Vert b_p\xi {\Vert }^2$$

be its retained positive excitation energy. For a positive one-particle operator $0\le A\le W_R$, define $T_A={\sum }_{p\ne 0}{A}_{pp}|V_p{|}^2$. The source proves

$$\begin{array}{rl}|⟨\mathrm{d}\Gamma (A){⟩}_{\xi }-T_A\Vert \xi {\Vert }^2|\le & C(1+R^2)\mathcal{Q}\\ & +C\sqrt{(1+R^2)\mathcal{Q}{T}_A\Vert \xi {\Vert }^2}.\end{array}$$

The notation $\mathrm{d}\Gamma (A)$ means the sum of $A$ over particles.

To see the mechanism, split the column $(a_p\xi {)}_p$ into its annihilation and creation parts before applying $A^{1/2}$. The cell Poincaré inequality bounds the annihilation part by the excitation energy. Commuting $b_p$ past $b_q^{\ast }$ in the creation part produces precisely the scalar trace $T_A$, plus another energy-controlled term. Cauchy–Schwarz bounds the mixed term by the square-root error above.

For complex matrices $A$, the commutation calculation produces a transpose, rather than the original matrix. Positivity and domination remain valid because the dominating energy matrix is real diagonal. This detail is why the result can ultimately treat complex contractions such as translations. It is also why one cannot replace the proof by a calculation of diagonal occupations alone (OpenAI, 2026d).

Insertion estimates remain valid after exposing the environment

For bounded repulsion, the auxiliary variables introduced above give an exact conditional law

$$\frac{1}{Z(\mathcal{D})}\prod _{i\in I}{J}_i({\omega }_i)\prod _{\{i,k\}\cap I\ne \varnothing }{1}_{\{u_{ik}\le a_{ik}(\omega )\}}\prod _{i\in I}{B}_i(d{\omega }_i).$$

Here $\mathcal{D}$ is the exposed data, $I$ the flagged eligible labels, $B_i$ a bridge with its endpoints and winding fixed, $J_i$ its individual cutoff, and $a_{ik}$ the pair Boltzmann weight. The normalizer $Z(\mathcal{D})$ is positive on almost every realized conditional fiber.

The insertion lemma works with the other allowed paths held fixed, uniformly in the exposed auxiliary variables and after deleting any subset of pair checks. On good data, its specified trial insertions succeed with probability at least $3/4$. The proof sums pairwise approach bounds: sparse flagged paths are controlled by endpoint counts, while the denser frozen paths require short-time oscillation and local-density bounds. Since a pair check can fail only during a close approach, these estimates do not depend on the numerical value of its auxiliary variable.

This uniformity permits successive removal and reinsertion of selected labels while tracking normalization ratios. Merely proving that a fresh bridge succeeds on average under the original gas law would not justify those later conditional operations (OpenAI, 2026e).

Reverse insertion charges encounters, rather than route length

The density-uniform condensate paper compares two selected tuples $I,I^{\prime }$. Let $h=I\cap I^{\prime }$ be their shared labels, and enlarge this exceptional set by adding the predecessors of $h$ along $I$. Its size is at most $2|h|$. Away from it, endpoint assignments in the four configurations match in pairs, so the corresponding free bridge kernels cancel exactly.

The remaining interacting normalizers are compared using positivity of the repulsion and Jensen’s inequality. A one-path conditional density bound follows from a lower bound on its insertion normalization; it continues to hold with other allowed paths frozen. Shared labels cost $C|h|$, while nearby distinct route portions cost $\epsilon (\rho )J$, where $J$ counts encounters and $\epsilon (\rho )\to 0$. Thus the comparison leaves a factor of the form

$$\exp (C|h|+\epsilon (\rho )J).$$

The source also checks that every replacement preserves the required far-away selection weights and adaptation constraints before summing over routes. The route encounter estimates can then control this factor uniformly in volume. Dropping those constraints earlier would discard the dependence of the selected route on the gas configuration (OpenAI, 2026a).

Thermal joint bounds begin with a one-path kernel estimate

The positive-temperature companion transfers free Brownian estimates into the interacting slab. It partitions a path according to the number $n$ of successive unit-ball exits. This controls both the number of cells visited and the spatial region containing its endpoints. For a marked bad event with free probability at most $\epsilon$, the restricted kernel has three bounds: a Gaussian endpoint bound, an exit-count bound $C{t}^{-3/2}{e}^{-c{n}^2/t}$, and a bad-event bound $C{t}^{-3/2}\epsilon$.

Taking their geometric mean retains all three gains, including ${\epsilon }^{1/3}$. After localization, this becomes a bound by a cutoff heat kernel on a region of volume $O((n+1{)}^3|A|)$, where $A$ is the tested set of cells. The subsequent colored trace-sandwich estimate is the manuscript’s interacting input; it turns these local kernels into joint certificate bounds for arbitrarily many prescribed cells. Independent free-path tails by themselves would not establish those joint interacting bounds (OpenAI, 2026b).

Filling small pockets also controls phase ambiguity

For the ground-state hard-core paper, obstacle filling has a quantitative advantage. A small bad microcube component with physical span at most one has filled volume at most $3h^2$ times its number of cubes, with $h\asymp r$. Indeed, every coordinate column meeting the fill must meet the component; otherwise that column provides an escape to infinity. Each forbidden ball meets only a bounded number of microcubes. Summing gives total small-fill volume $O(r^{2}N)$.

A large component instead supplies order $1/r$ distinct particle witnesses with close partners. Joint close-neighbor estimates, combined with an exponential bound on the number of connected lattice sets of a given size, control its probability. This yields a small bath-averaged removed volume. Detouring around filled components then connects retained points with strict clearance from the hard cores. It is this one-coordinate connectivity, with the bath fixed, that transfers the positive modulus occupation to complex ground vectors without assuming connectivity of the full many-particle configuration space (OpenAI, 2026c).

🏷️ Connections

• Area laws and PEPS also separates an energy-gap hypothesis from stronger information about a many-body state. Here the closing one-particle gap motivates the long-distance comparison.
• Coulomb ionization and asymptotics likewise distinguishes energy information from spatial observables and keeps thermodynamic or large-parameter limit orders explicit.

🏷️ Manuscripts and verification scope

• Bose–Einstein condensation at positive temperature in the dilute hard-sphere gas — pinned manuscript and companion source.
• Quantum Depletion and Momentum Distribution in the Dilute Hard-Sphere Bose Gas — pinned manuscript and companion source.
• Quantum Depletion for Fixed Bounded Repulsive Potentials — pinned manuscript and companion source.
• A density-uniform condensate bound for dilute Bose gases — pinned manuscript and companion source.
• Ground-state condensation in the dilute hard-sphere gas — pinned manuscript and companion source.

The family scope page describes selected formalization coverage. Despite its broader heading, the scope page lists only the ground-state hard-sphere manuscript. It describes an absolute positive condensate fraction uniform over sufficiently small gas parameters, along every thermodynamic sequence, for all pure and mixed ground-space states and the normalized ground-space projection. It does not select positive-temperature condensation, the depletion asymptotic, the momentum distribution, or either bounded-potential result. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026a. A density-uniform condensate bound for dilute Bose gases.

🐻  OpenAI 2026b. Bose–Einstein condensation at positive temperature in the dilute hard-sphere gas.

🐻  OpenAI 2026c. Ground-state condensation in the dilute hard-sphere gas.

🐻  OpenAI 2026d. Quantum Depletion and Momentum Distribution in the Dilute Hard-Sphere Bose Gas.

🐻  OpenAI 2026e. Quantum Depletion for Fixed Bounded Repulsive Potentials.