oai-math-revised beta

Browse › Operator algebras › 298 Two notions of free entropy differ even when both are finite

A finite-entropy separation of microstates and nonmicrostates free entropy

OpenAI · September 25, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

We answer the finite-entropy equality question for microstates and nonmicrostates free entropy negatively. We construct a bounded self-adjoint tuple X in a von Neumann algebra with faithful normal tracial state such that $-\infty\lt \chi(X)\leq\chi^*(X)-\tfrac12\lt \infty$. Here χ is the original microstates entropy with an operator-norm cutoff and a limsup over matrix sizes. The counterexample uses a large but fixed number of variables.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

  • David Jekel, On counterexamples to the unification of free entropy (arXiv:2610.27243, 19 Oct 2026). Cites this preprint as the first example with $-\infty<\chi<\chi^*$, and presents a similar example with a diffuse (semicircular) last variable in place of the discrete one, proving the gap through a Wasserstein-distance lower bound instead of the data-processing argument.

Formalization

  • mathcommunity/oai-math-revised, lean/docs/298.md (Lean scope notes of the release). States that the formalization constructs a bounded self-adjoint tuple with $-\infty<\chi(X)\le\chi^*(X)-1/2<\infty$, using operator-norm cutoff and a limsup over matrix sizes, and links the comparator statement FiniteEntropySeparation.lean.
  • OpenAI, lean/OAI/Analysis/FreeEntropy/Main.lean (openai/math, commit adc7f12). The release's Lean proof of the theorem FiniteEntropySeparation.main, whose statement is given in the separate comparator file FiniteEntropySeparation.lean, where chi and chiStar are defined from first principles.

Digests and expositions

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:A-finite-entropy-separation-of-microstates-and-nonmicrostates-free-entropy-September-25-2026,
  author = {{OpenAI}},
  title = {{A finite-entropy separation of microstates and nonmicrostates free entropy}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-finite-entropy-separation-of-microstates-and-nonmicrostates-free-entropy-September-25-2026/paper.pdf}{OAI:A-finite-entropy-separation-of-microstates-and-nonmicrostates-free-entropy-September-25-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/298.md. The Lean statements have not been checked by people against the paper's claims.

Family 298: Two notions of free entropy differ even when both are finite

Constructs a bounded self-adjoint tuple in a tracial von Neumann algebra whose microstates and nonmicrostates free entropies satisfy $-\infty\lt \chi\lt \chi^*\lt \infty$. This answers Voiculescu’s finite-entropy equality question negatively: the matrix-approximation and free-Fisher-information definitions differ even when both are finite.

This is the only paper in this family.