∑math20

Mathematical physics · Result 280

Unitary vertex operator algebras and conformal nets

1 paperLean

Proves the strongly rational case of the strong-locality conjecture: every simple unitary strongly rational complex vertex operator algebra generates a completely rational conformal net. Its simple modules are unitarizable, and its representation category agrees with the net’s finite-index sectors as a braided unitary tensor category.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Strongly rational unitary vertex operator algebras and conformal nets

Strongly rational unitary vertex operator algebras and conformal nets

OpenAI · September 25, 2026

Every simple unitary strongly rational vertex operator algebra generates a completely rational conformal net. All its simple grading-restricted modules are unitarizable, its canonical fusion forms are positive, and the Carpi–Weiner–Xu functor gives a braided unitary tensor equivalence from its grading-restricted finite-length module category onto the finite-index sectors of the net. Gui's extension theorems then identify normalized irreducible finite-index local extensions of these nets with simple CFT-type conformal extensions of the vertex operator algebras.

Read PDF Download Source

Cite
@misc{OAI:Strongly-rational-unitary-vertex-operator-algebras-and-conformal-nets-September-25-2026,
  author = {{OpenAI}},
  title = {{Strongly rational unitary vertex operator algebras and conformal nets}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Strongly-rational-unitary-vertex-operator-algebras-and-conformal-nets-September-25-2026/paper.pdf}{OAI:Strongly-rational-unitary-vertex-operator-algebras-and-conformal-nets-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

The linked formalization proves the first construction step relating strongly rational unitary vertex operator algebras to conformal nets. For a simple unitary strongly rational vertex operator algebra, it establishes polynomial energy bounds and strong locality and constructs an irreducible conformal net with the stated covariance, vacuum, and positive-energy properties.

The selected statement does not include complete rationality of the net, unitarizability of all simple modules, the braided tensor equivalence, or the classification of local extensions described in the paper.

Comparator links

ResultComparator statement
Energy bounds, strong locality, and an irreducible conformal netVertexAlgebraNet.lean

Scope note on GitHub →