# Two notions of free entropy differ even when both are finite

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

- [A finite-entropy separation of microstates and nonmicrostates free entropy](../../preprints/A-finite-entropy-separation-of-microstates-and-nonmicrostates-free-entropy-September-25-2026/paper.pdf)

## Scope

The formalization disproves equality of microstates and nonmicrostates free entropy even when both quantities are finite. It constructs a bounded self-adjoint tuple $X$ in a von Neumann algebra with a faithful normal tracial state such that $-\infty<\chi(X)\le\chi^*(X)-1/2<\infty$. Here $\chi$ is the microstates entropy with an operator-norm cutoff and a limsup over matrix sizes, and $\chi^*$ is the nonmicrostates entropy defined using free semicircular noise. The example has a fixed finite number of variables.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Finite separation of microstates and nonmicrostates free entropy | [FiniteEntropySeparation.lean](../ComparatorChallenges/FiniteEntropySeparation.lean) |