OpenAI claim summary for Math-2830

Relative bicentralizer and continuous-core commutants

OpenAI's claim

An expected inclusion with separable preduals is claimed to contain an expected amenable subalgebra of its lower algebra preserving the relative commutant inside the upper algebra's continuous core. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.

For a unital inclusion $N\subset M$ of von Neumann algebras whose preduals are separable and a conditional expectation that is faithful and normal $E_N:M\to N$, OpenAI claims an injective (amenable) unital $P\subset N$ and conditional expectation that is faithful and normal $F:N\to P$ satisfying \[ P'\cap c(M)=N'\cap c(M). \] The continuous core is $c(M)=M\rtimes_{\sigma^\psi}\mathbb R$ for a faithful normal state $\psi$, with the canonical embedding of $M$. Equality is inside this whole core, not only inside $M$.

Outline of the argument

Manuscript 1 (family 290, 2026-09-23): Absolute bicentralizer reduction establishes multiplication isometries through modular averaging and a spectral contradiction. In the relative setting, completely positive packaging of long words gives estimates uniform in tensor length and modular shifts. Repeated randomized comparisons would exhaust the available norm if an error remained, identifying the core fixed algebra and invoking the amenable-subalgebra criterion.

Formal verification

For family 290, the scope page documents the following selections. The selected modular recovery statement widens shrinking spectral bands by a factor four while keeping algebra elements uniformly bounded and their tested images nonzero. It assumes the stated scalar-centralizer representation and does not select absolute bicentralizer triviality. Manuscript 1 is not among the papers selected by that page, so the family link does not formalize its main conclusion. It does not establish formal coverage of the complete problem clause.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

• OpenAI, Expected amenable subalgebras preserving core commutants, 2026-09-23; citation key OAI:Expected-amenable-subalgebras-preserving-core-commutants-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 290: Lean scope.
• OpenAI catalogue entry.