Relative bicentralizers and modular spectral recovery

2 papersLean

Proves Connes' bicentralizer conjecture for every type III₁ factor with separable predual and every faithful normal state. More generally, for every inclusion \(N\subset M\) of von Neumann algebras with separable preduals admitting a faithful normal conditional expectation, constructs an amenable expected subalgebra \(P\subset N\) with \(P'\cap c(M)=N'\cap c(M)\), resolving the relative bicentralizer conjecture.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Expected amenable subalgebras preserving core commutants

OpenAI · September 23, 2026

We prove that every inclusion \(N\subset M\) of von Neumann algebras with separable preduals and a faithful normal conditional expectation contains an expected amenable subalgebra \(P\subset N\) such that \(P'\cap c(M)=N'\cap c(M)\), where \(c(M)\) denotes the continuous core of M. This resolves the relative bicentralizer conjecture in this setting.

Read PDF Download Source

Cite

@misc{OAI:Expected-amenable-subalgebras-preserving-core-commutants-September-23-2026,
  author = {{OpenAI}},
  title = {{Expected amenable subalgebras preserving core commutants}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Expected-amenable-subalgebras-preserving-core-commutants-September-23-2026/Expected-amenable-subalgebras-preserving-core-commutants-September-23-2026.pdf}{OAI:Expected-amenable-subalgebras-preserving-core-commutants-September-23-2026}},
  year = {2026}
}

Bounded recovery for modular spectral averages

OpenAI · September 23, 2026

We prove a bounded spectral recovery theorem for a von Neumann algebra with a faithful normal state whose centralizer consists only of scalars. A positive averaged squared norm for an arbitrary bounded Hilbert-space operator on shrinking modular spectral bands can be recovered on uniformly bounded algebra elements with shrinking spectral support. We apply this theorem to spectral intertwining rigidity and obtain an alternative proof of bicentralizer triviality for type III₁ factors with separable predual.

Read PDF Download Source

Cite

@misc{OAI:Bounded-recovery-for-modular-spectral-averages-September-23-2026,
  author = {{OpenAI}},
  title = {{Bounded recovery for modular spectral averages}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Bounded-recovery-for-modular-spectral-averages-September-23-2026/Bounded-recovery-for-modular-spectral-averages-September-23-2026.pdf}{OAI:Bounded-recovery-for-modular-spectral-averages-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):

Bounded recovery for modular spectral averages

Scope

For a faithful normal state with scalar centralizer in the stated standard-space representation, the formalized result converts positive modular spectral averages into uniformly bounded algebra elements. Given unit vectors in shrinking spectral bands around a real number \(s\) and a positive limiting symmetric average for a bounded operator \(T\), it finds a subsequence of bounded algebra elements whose images under \(T\) stay uniformly nonzero and whose spectral bands have four times the original widths. The absolute bicentralizer conjecture is not included.

Comparator links

Result	Comparator statement
Bounded recovery from modular spectral averages	BoundedRecovery.lean

Scope note on GitHub →