we-solve (beta)

Math-2819 · mathematics · Analysis

Single generation of separable-predual finite factors

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Does every type $II_{1}$ factor with separable predual have one bounded operator x with $W*(x)=M$, equivalently two self-adjoint von Neumann generators? This asks for von Neumann generation and makes no norm-closed C*-generation assertion.

Short English statement

Does every type $II_{1}$ factor with separable predual have one bounded operator x with $W*(x)=M$, equivalently two self-adjoint von Neumann generators? This asks for von Neumann generation and makes no norm-closed C*-generation assertion.

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2819-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2819

Manuscript 1 (family 296, 2026-09-23): The problem selects the mathematical statement summarized here, including its stated hypotheses and parameter range. The cited theorem gives a claimed proof of that assertion in full.

Single generation of separable-predual finite factors

OpenAI's claim

All type-II_1 factors with separable predual are claimed to have a single operator generator; the established direct-integral reduction then gives single generation for general separable-predual von Neumann algebras. 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 every type-$\mathrm{II}_1$ factor $M$ with separable predual, OpenAI claims self-adjoint $a,b\in M$ with \[ M=W^*(a,b)=W^*(a+ib). \] Here $W^*$ means generated von Neumann algebra. Its relative generation input says that for every irreducible inclusion $P\subset M$ of such finite factors, the unitaries $u$ with $W^*(P,u)=M$ form a dense $G_\delta$ in the trace $2$-norm topology. The headline conclusion is single non-self-adjoint generation.

Outline of the argument

Manuscript 1 (family 296, 2026-09-23): Free independence lets a small perturbation accumulate along many occurrences in a long word, retaining a definite correlation with a chosen target. A free-group convolution bound controls the nonlinear remainder without growth in word length. Coordinate selection returns the ultrapower construction to the factor; density and a corner-and-matrix argument turn relative generation into one-operator generation.

Formal verification

For family 296, the scope page documents the following selections. Selections give one-operator generation for factors with separable predual and dense relative unitary generators of irreducible inclusions in trace two-norm. No operator-norm separability is required. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: FactorGeneration.lean, RelativeGeneration.lean. Declarations: OAI.Generator.single_generation_of_II1_separable_predual, OAI.RelativeGeneration.main_theorem.

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

Go to contribution →