we-solve (beta)

Phys-7-A2 · revision r1 · on Phys-7

OpenAI claim summary for Phys-7

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status at unsolvedmath.com: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

For the stated interacting continuum models, the selected sources bound the fraction occupying the constant orbital away from zero along every thermodynamic sequence. This establishes Bose condensation by the macroscopic-mode criterion, including positive temperatures in the specified dilute regime. The target additionally asks for a pointwise infinite-distance limit of the thermodynamic one-particle density kernel; that limit is not asserted by these occupation-fraction theorems. The match therefore remains partial.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Bose-Einstein Condensation in Continuum Models
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Result 2.
  6. Result 3.
  7. Result 4.
  8. Result 5.
  9. Outline of the argument
  10. Formal verification
  11. Status caveat
  12. Sources

Bose-Einstein Condensation in Continuum Models

OpenAI's claim

The linked manuscripts present the following claims by OpenAI: For fixed bounded repulsive finite-range potentials, the constant-mode condensate fraction is claimed uniformly positive at sufficiently small density and temperatures up to the density squared; For sufficiently small fixed hard-sphere density, a positive volume-independent temperature is claimed to give a positive thermodynamic constant-mode condensate fraction; Every ground state of a sufficiently dilute fixed-density three-dimensional hard-sphere gas is claimed to place a uniform positive particle fraction in the constant orbital; The hard-sphere ground state is claimed to have the full scaled Bogoliubov momentum law, with depletion $\frac{8}{3\sqrt\pi}\sqrt{\rho a^3}+o(\sqrt{\rho a^3})$; The same leading depletion coefficient is claimed for every fixed bounded nonnegative radial finite-range potential of positive scattering length, uniformly over ground-state density matrices. Together they provide the following support within the scopes described below.

Mathematical statement of the claimed result

Result 1.
Take a bounded measurable radial potential $v:\mathbb R^3\to[0,\infty)$, supported in a ball of finite radius and nonzero on a set of positive measure. On $(\mathbb R/L\mathbb Z)^3$, use the symmetric $N$-particle Hamiltonian \[ H_{N,L}=-\sum_i\Delta_i+\sum_{i<j}v_L(x_i-x_j),\qquad v_L(x)=\sum_{k\in\mathbb Z^3}v(x+Lk). \] Let $\gamma^{(1)}_{N,L,T}$ be the canonical state's one-particle matrix, of trace $N$, and $u_0=L^{-3/2}$. The claim provides $\rho_*(v),c_*(v)>0$ such that every $0<\rho<\rho_*$ has a finite $L_0(\rho,v)$, with \[ L\ge L_0,\quad\rho/2\le N/L^3\le2\rho,\quad0\le T\le\rho^2 \quad\Longrightarrow\quad \frac{\langle u_0,\gamma^{(1)}_{N,L,T}u_0\rangle}{N}\ge c_*. \] The positive fraction is uniform throughout the indicated dilute density range.
Result 2.
Fix exclusion distance $a>0$. On the three-dimensional torus of side $L$, the hard-sphere Hamiltonian is the symmetric Dirichlet kinetic operator on configurations with every interparticle torus distance greater than $a$. Let $\gamma^{(1)}_{N,L,T}$ be the canonical Gibbs one-particle matrix, of trace $N$, and $u_{0,L}=L^{-3/2}$. The source asserts that some $\rho_*(a)>0$ has the property \[ 0<\rho<\rho_*(a)\quad\Longrightarrow\quad \exists T(a,\rho)>0:\quad \liminf_{L\to\infty,\ N/L^3\to\rho} \frac{\langle u_{0,L},\gamma^{(1)}_{N,L,T}u_{0,L}\rangle}{N}>0. \] Here $a,\rho,T$ remain fixed during the thermodynamic limit.
Result 3.
For the three-dimensional torus hard-sphere Bose Hamiltonian, impose Dirichlet exclusion at pair distance $a$, with kinetic energy $-\sum_i\Delta_i$. For a normalized symmetric ground vector $\Psi$, put \[ B(\Psi)=N^{-1}\langle L^{-3/2},\gamma^{(1)}_\Psi L^{-3/2}\rangle, \qquad\operatorname{Tr}\gamma^{(1)}_\Psi=N. \] The claimed universal constants $\varepsilon_0,c_0>0$ give \[ \rho a^3<\varepsilon_0,\quad N_k,L_k\to\infty,\quad N_k/L_k^3\to\rho \quad\Longrightarrow\quad\liminf_k B(\Psi_k)\ge c_0 \] for every choice of ground vectors, allowing complex vectors and degeneracy.
Result 4.
For the three-dimensional periodic hard-sphere Bose gas of exclusion distance $a>0$, let $\mathcal G_{N,L,a}$ be all trace-one states supported on the lowest eigenspace, and $n_{\Gamma,L}(k)$ the occupation of $L^{-3/2}e^{ik\cdot x}$. Define \[ g(t)=\frac{|t|^2+1}{2\sqrt{|t|^4+2|t|^2}}-\frac12,\qquad d\nu_{\mathrm{Bog}}(t)=\frac{(8\pi)^{3/2}}{(2\pi)^3}g(t)\,dt. \] For each bounded continuous real $f$ and $\varepsilon>0$, the source gives $\rho_0(a,f,\varepsilon)>0$. If $0<\rho<\rho_0$, $\eta=\rho a^3$, and $N_j,L_j\to\infty$, $N_j/L_j^3\to\rho$, then \[ \limsup_j\sup_{\Gamma\in\mathcal G_{N_j,L_j,a}} \left|\frac{\sum_{k\in(2\pi/L_j)\mathbb Z^3,\ k\ne0} f(k/\sqrt{8\pi\rho a})n_{\Gamma,L_j}(k)}{N_j\sqrt\eta} -\int f\,d\nu_{\mathrm{Bog}}\right|\le\varepsilon. \] The measure has total mass $8/(3\sqrt\pi)$.
Result 5.
Let $v\ge0$ be bounded, measurable, radial, compactly supported, and nonzero on a positive-measure set. Its scattering length $a_v>0$ is determined by $(-\Delta+v/2)f=0$, with $f(x)=1-a_v/|x|$ outside the support. For the periodic symmetric Hamiltonian $-\sum_i\Delta_i+\sum_{i<j}v_L(x_i-x_j)$, let $\mathcal G^v_{N,L}$ contain all ground-space trace-one states and $B_\Gamma=N^{-1}\langle L^{-3/2},\gamma^{(1)}_\Gamma L^{-3/2}\rangle$. For every $\varepsilon>0$, some $\rho_0(v,\varepsilon)>0$ satisfies \[ 0<\rho<\rho_0,\ N_k,L_k\to\infty,\ N_k/L_k^3\to\rho \ \Longrightarrow\ \limsup_k\sup_{\Gamma\in\mathcal G^v_{N_k,L_k}} \left|\frac{1-B_\Gamma}{\sqrt{\rho a_v^3}}-\frac8{3\sqrt\pi}\right|\le\varepsilon. \] Volume and particle number tend to infinity while density remains fixed.

Outline of the argument

Energy and free-energy estimates control cell occupancy and isolation. A short imaginary-time slab supplies joint trajectory bounds; defective-cell handling and insertion comparisons connect distant cells and preserve a density-uniform coherence lower bound. Scaled kinetic and particle-count bounds localize the canonical state. Thermal-slab trajectory estimates permit moving paths between adjacent cells; environment exposure retains movable groups and turns their long-range coherence into the condensate lower bound.

Energy and spatial bounds produce stationary hard-core path samples. Neighbor-cell moves, retained movable groups, and routes through sparse obstacles compare phase coherence across the volume, giving a constant-mode lower bound also for complex ground states. Local energy estimates keep excitations instead of discarding them. One-body covariance and short-trajectory certificates are compared through smoothed deletion measures, while random encounter routes connect local momentum data to the thermodynamic occupation measure before the dilute limit.

Local density tails and ground-state path bounds control occupations at the relevant scattering scale. Spatial comparison transports these local estimates to the constant orbital, identifying every thermodynamic accumulation value before density tends to zero.

Formal verification

For family 267, the selected statement is a density-uniform hard-sphere ground-state condensate lower bound for pure and mixed ground states. Positive-temperature condensation and quantum-depletion asymptotics are beyond it. The listed Comparator files are HardSphere.lean. The inventory does not supply a named declaration for these Comparator entries. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources