we-solve (beta)

Phys-62 · physics · mathematics · Physics

Condensation in every dilute hard-sphere ground state

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Are there absolute $\epsilon _0,c_0>0$ such that for every $a,\rho >0$ with rho $a^3<\epsilon _0$, every thermodynamic sequence N,L$\to$infinity with $N/L^3\to \rho $, and every normalized bosonic hard-sphere ground eigenvector, the limiting lower condensate fraction is at least $c_0$?

Short English statement

Are there absolute $\epsilon _0,c_0>0$ such that for every $a,\rho >0$ with rho $a^3<\epsilon _0$, every thermodynamic sequence N,L$\to$infinity with $N/L^3\to \rho $, and every normalized bosonic hard-sphere ground eigenvector, the limiting lower condensate fraction is at least $c_0$?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Phys-62-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Phys-62

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 question retains these same parameters and conventions. Within these assumptions, this is a claimed affirmative answer to the stated question.

Condensation in every dilute hard-sphere ground state

OpenAI's claim

OpenAI presents a proof in the selected manuscript. 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.

Mathematical statement of the claimed result

Result 1.
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.

Outline of the argument

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.

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

Go to contribution →