Partial differential equations · Result 363

Nonuniqueness with local conservation for the hard-sphere Boltzmann equation

2 papersLean

Constructs two distinct global entropy solutions of the three-dimensional periodic hard-sphere Boltzmann equation from the same nonnegative initial density, with bounded velocity support and finite mass, energy and absolute entropy. Both are strongly continuous in L¹ and satisfy exact local conservation of mass, momentum and kinetic energy.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Nonuniqueness with local conservation for the hard-sphere Boltzmann equation

OpenAI · October 5, 2026

We prove nonuniqueness for the three-dimensional periodic hard-sphere Boltzmann equation among global entropy solutions satisfying exact local conservation of mass, momentum, and kinetic energy. We construct one nonnegative initial density with bounded velocity support and finite mass, energy, and absolute entropy that gives rise to two distinct such solutions. Both are strongly continuous in L¹, and their collision gain and loss terms are integrable with every polynomial velocity weight on every bounded time interval.

Read PDF Download Source

Cite

@misc{OAI:Nonuniqueness-with-local-conservation-for-the-hard-sphere-Boltzmann-equation-October-5-2026,
  author = {{OpenAI}},
  title = {{Nonuniqueness with local conservation for the hard-sphere Boltzmann equation}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Nonuniqueness-with-local-conservation-for-the-hard-sphere-Boltzmann-equation-October-5-2026/paper.pdf}{OAI:Nonuniqueness-with-local-conservation-for-the-hard-sphere-Boltzmann-equation-October-5-2026}},
  year = {2026}
}

Nonuniqueness for the periodic hard-sphere Boltzmann equation

OpenAI · September 23, 2026

We prove nonuniqueness for the periodic hard-sphere Boltzmann equation by constructing two distinct global renormalized solutions with the same nonnegative initial density on \(\mathbb T^3\times\mathbb R^3\). This density has bounded velocity support and finite mass, energy, and absolute entropy. Both solutions conserve local mass and total momentum and satisfy the global energy and entropy-dissipation inequalities. On a common initial interval, they are strongly continuous in L¹, and their collision gains and losses are integrable.

Read PDF Download Source

Cite

@misc{OAI:Nonuniqueness-for-the-periodic-hard-sphere-Boltzmann-equation-September-23-2026,
  author = {{OpenAI}},
  title = {{Nonuniqueness for the periodic hard-sphere Boltzmann equation}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Nonuniqueness-for-the-periodic-hard-sphere-Boltzmann-equation-September-23-2026/paper.pdf}{OAI:Nonuniqueness-for-the-periodic-hard-sphere-Boltzmann-equation-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

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

Nonuniqueness for the periodic hard-sphere Boltzmann equation

Scope

The formalization proves nonuniqueness for the periodic hard-sphere Boltzmann equation by constructing two distinct global renormalized solutions on \(\mathbb T^3\times\mathbb R^3\) with the same nonnegative initial density. The data have bounded velocity support and finite mass, energy, and absolute entropy. Both solutions conserve local mass and total momentum and satisfy the global energy and entropy-dissipation inequalities.

On a common initial interval they are strongly continuous in \(L^1\), with integrable collision gains and losses. These are the conditions of the selected periodic result; later local-conservation refinements are outside it.

Comparator links

Result	Comparator statement
Two periodic hard-sphere Boltzmann solutions with the same data	BoltzmannNonuniqueness.lean

Scope note on GitHub →